Abstract
In this paper we show a novel method for modelling behaviours of security protocols using networks of communicating automata in order to verify them with SAT-based bounded model checking. These automata correspond to executions of the participants as well as to their knowledge about letters. Given a bounded number of sessions, we can verify both correctness or incorrectness of a security protocol proving either reachability or unreachability of an undesired state. We exemplify all our notions on the Needham Schroeder Public Key Authentication Protocol (NSPK) and show experimental results for checking authentication using the verification tool VerICS.
The authors acknowledge partial support from the Ministry of Science and Information Society Technologies under the grant number 3 T11C 01128.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Armando, A., Basin, D., Boichut, Y., Chevalier, Y., Compagna, L., Cuellar, J., Drielsma, P.H., Heám, P.C., Kouchnarenko, O., Mantovani, J., Mödersheim, S., von Oheimb, D., Rusinowitch, M., Santiago, J., Turuani, M., Viganó, L., Vigneron, L.: The AVISPA tool for the automated validation of internet security protocols and applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 281–285. Springer, Heidelberg (2005)
Bella, G., Paulson, L.C.: Using Isabelle to prove properties of the Kerberos authentication system. In: Orman, H., Meadows, C., (eds). Proceedings of the DIMACS Workshop on Design and Formal Verification of Security Protocols (CD-ROM) (DIMACS 1997) (1997)
Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W., Weise, C.: New generation of Uppaal. In: Proc. of the Int. Workshop on Software Tools for Technology Transfer (STTT 1998), BRICS Notes Series, pp. 43–52 (1998)
Bolignano, D.: An approach to the formal verification of cryptographic protocols. In: Proceedings of the 3rd ACM Conference on Computer and Communication Security, pp. 106–118 (1996)
Bozga, L., Ene, C., Lakhnech, Y.: A Symbolic Decision Procedure for Cryptographic Protocols with Time Stamps. Journal of Logic and Algebraic Programming 65(1), 1–35 (2005)
Burrows, M., Abadi, M., Needham, R.: A Logic of Authentication. In: Proceedings of the Royal Society of London A, vol. 426, pp. 233–271 (1989)
Clark, J.A., Jacob, J.L.: A survey of authentication protocol literature. Technical Report 1.0, http://www.cs.york.ac.ukjac/papers/drareview.ps.gz (1997)
Clarke, E.M., Jha, S., Marrero, W.: Verifying security protocols with Brutus. ACM Transactions on Software Engineering and Methodology 9(4), 443–487 (2000)
Cohen, E.: Taps: A first-order verifier for cryptographic protocols. In: CSFW ’00: Proceedings of the 13th IEEE Computer Security Foundations Workshop (CSFW 2000), pp. 144–158. IEEE Computer Society, Los Alamitos (2000)
Corin, R., Etalle, S., Hartel, P.H., Mader, A.: Timed model checking of security protocols. In: Atluri, V., Backes, M., Basin, D., Waidner, M. (eds.) 2nd ACM Workshop on Formal Methods in Security Engineering: From Specifications to Code (FMSE), pp. 23–32. ACM Press, New York (2004)
Dembiński, P., Janowska, A., Janowski, P., Penczek, W., Półrola, A., Szreter, M., Woźna, B., Zbrzezny, A.: VerICS: A tool for verifying timed automata and Estelle specifications. In: Garavel, H., Hatcliff, J. (eds.) ETAPS 2003 and TACAS 2003. LNCS, vol. 2619, pp. 278–283. Springer, Heidelberg (2003)
Dolev, D., Yao, A.: On the security of public key protocols. IEEE Transactions on Information Theory 29(2), 198–208 (1983)
Evans, N., Schneider, S.: Analysing time dependent security properties in csp using pvs. In: Cuppens, F., Deswarte, Y., Gollmann, D., Waidner, M. (eds.) ESORICS 2000. LNCS, vol. 1895, pp. 222–237. Springer, Heidelberg (2000)
Holzmann, G.J.: The model checker SPIN. IEEE Trans. on Software Eng. 23(5), 279–295 (1997)
Jakubowska, G., Penczek, W.: Is Your Security Protocol on Time? In: Proc. of International Symposium on Fundamentals of Software Engineering (FSEN 2007) (to appear, 2007)
Jakubowska, G., Penczek, W., Srebrny, M.: Verifying security protocols with timestamps via translation to timed automata. In: Czaja, L., (ed) Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P 2005), Warsaw University Press, pp. 100–115 (2005)
Jha, S., Clarke, E.M., Marrero, W.: Using state space exploration and a natural deduction style message derivation engine to verify security protocols. In: Gries, D., De Roever, W.P. (eds.) Proceedings of the IFIP Working Conference on Programming Concepts and Methods (PROCOMET 1998), pp. 87–106. Chapmann and Hall, Sydney (1998)
Kurkowski, M.: Deductive methods for verification of correctness of the authentication protocols (in polish). PhD thesis, Institute of Computer Science, Polish Academy of Sciences (2003)
Kurkowski, M., Penczek, W.: Verifying Cryptographic Protocols modeled by networks of automata. In: Proc. of CS&P 2006, Humboldt University Press, pp. 292–303 (2006)
Kurkowski, M., Penczek, W.: SAT-based Verification of Security Protocols via Translation to Networks of Automata. Report 998 of ICS PAS, Warsaw, http://www.imi.ajd.czest.pl/pub/report_kp_07.zip (2007)
Lowe, G.: Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 147–166. Springer, Heidelberg (1996)
Lowe, G., Roscoe, B.: Using CSP to Detect Errors in The TMN Protocol. IEEE Transaction on Software Engineering 23(10), 659–669 (1997)
Lowe, G.: Casper: A compiler for the analysis of security protocols. Journal of Computer Security 6(1-2), 53–84 (1998)
McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)
Meadows, C.: The NRL protocol analyzer: An overview. Journal of Logic Programming 26(2), 13–131 (1996)
Mitchell, M., Mitchell, J.C., Stern, U.: Automated analysis of cryptographic protocols using murφ. In: Proc. of the 1997 IEEE Symposium on Security and Privacy, pp. 141–151. IEEE Computer Society Press, Los Alamitos (1997)
Needham, R., Schroeder, M.: Using Encryption for Authentication in large networks of computers. Communications of the ACM 21(12), 993–999 (1978)
Panti, M., Spalazzi, L., Tacconi, S.: Using the NUSMV model checker to verify the Kerberos Protocol. In: Proc. of the Third Collaborative Technologies Symposium (CTS-2002), pp. 27–31 (2002)
Yovine, S.: KRONOS: A verification tool for real-time systems. International Journal of Software Tools for Technology Transfer 1(1/2), 123–133 (1997)
Zbrzezny, A.: SAT-based reachability checking for timed automata with diagonal constraints. Fundamenta Informaticae 67(1-3), 303–322 (2005)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kurkowski, M., Penczek, W., Zbrzezny, A. (2007). SAT-Based Verification of Security Protocols Via Translation to Networks of Automata. In: Edelkamp, S., Lomuscio, A. (eds) Model Checking and Artificial Intelligence. MoChArt 2006. Lecture Notes in Computer Science(), vol 4428. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74128-2_10
Download citation
DOI: https://doi.org/10.1007/978-3-540-74128-2_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-74127-5
Online ISBN: 978-3-540-74128-2
eBook Packages: Computer ScienceComputer Science (R0)