Verifying Security Protocols Modelled by Networks of Automata

• Autorzy: Kurkowski M. , Penczek W.
• Języki publikacji: EN

Abstrakty

EN

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.

Słowa kluczowe

EN

security protocols; model checking

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2007
• Tom: Vol. 79, nr 3-4
• Strony: 453--471
• Opis fizyczny: bibliogr. 29 poz., tab.

Twórcy

autor

Kurkowski M.

autor

Penczek W.

• Institute of Mathematics and Computer Science, Jan Długosz University, Armii Krajowej 13/15, 42-200 Częstochowa, Poland,

Bibliografia

• [1] A. Armando, D. Basin, Y. Boichut, Y. Chevalier, L. Compagna, J. Cuellar, P. Hankes Drielsma, P.C. Heám, O. Kouchnarenko, J. Mantovani, S. Mödersheim, D. von Oheimb, M. Rusinowitch, J. Santiago, M. Turuani, L. Viganó, and L. Vigneron. The AVISPA tool for the automated validation of internet security protocols and applications. In Proc. of CAV'05, volume 3576 of LNCS, pages 281-285. Springer-Verlag, 2005.
• [2] G. Bella and L.C. Paulson. Using Isabelle to prove properties of the Kerberos authentication system. In H. Orman and C. Meadows, editors, Proceedings of the DIMACS Workshop on Design and Formal Verification of Security Protocols (CD-ROM) (DIMACS'97), 1997.
• [3] J. Bengtsson, K. G. Larsen, F. Larsson, P. Pettersson, W. Yi, and C. Weise. New generation of UPPAAL. In Proc. of the Int. Workshop on Software Tools for Technology Transfer (STTT'98), BRICS Notes Series, pages 43-52, 1998.
• [4] D. Bolignano. An approach to the formal verification of cryptographic protocols. In Proceedings of the 3rd ACM Conference on Computer and Communication Security, pages 106-118, 1996.
• [5] L. Bozga, C. Ene, Y. Lakhnech. A Symbolic Decision Procedure for Cryptographic Protocols with Time Stamps (Extended Abstract), In Proc. CONCUR'04, pages 177-192, 2004.
• [6] M. Burrows, M. Abadi, R. Needham. A Logic of Authentication. In Proceedings of the Royal Society of London A, 426, pages 233-271, 1989. A preliminary version appeared as Research Report 39, DEC Systems Research Center, Palo Alto, February 1989.
• [7] J. A. Clark and J. L. Jacob. A survey of authentication protocol literature. Technical Report 1.0, http://www.cs.york.ac.uk jac/papers/drareview.ps.gz, 1997.
• [8] E. M. Clarke, S. Jha, and W. Marrero. Verifying security protocols with Brutus. In ACM Transactions on Software Engineering and Methodology, 9(4), pages 443-487, 2000.
• [9] E. Cohen. Taps: A first-order verifier for cryptographic protocols. In CSFW '00: Proceedings of the 13th IEEE Computer Security Foundations Workshop (CSFW'00), page 144-158, Washington, DC, USA, 2000. IEEE Computer Society.
• [10] R. Corin, S. Etalle, P. H. Hartel, and A. Mader. Timed model checking of security protocols. In V. Atluri, M. Backes, D. Basin, and M. Waidner, editors, 2nd ACM Workshop on Formal Methods in Security Engineering: From Specifications to Code (FMSE), pages 23-32, Fairfax, Virginia, Oct 2004. ACM Press, New York.
• [11] P. Dembiński, A. Janowska, P. Janowski, W. Penczek, A. Półrola, M. Szreter, B. Woźna, and A. Zbrzezny. VerICS: A tool for verifying timed automata and Estelle specifications. In Proc. of the 9th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'03), volume 2619 of LNCS, pages 278-283. Springer-Verlag, 2003.
• [12] D. Dolev and A. Yao. On the security of public key protocols. In IEEE Transactions on Information Theory, 29(2), pages 198-208, 1983.
• [13] N. Evans and S. Schneider. Analysing time dependent security properties in csp using pvs. In ESORICS '00: Proceedings of the 6th European Symposium on Research in Computer Security, pages 222-237, London, UK, 2000. Springer-Verlag.
• [14] G. J. Holzmann. The model checker SPIN. In IEEE Trans. on Software Eng., 23(5), pages 279-295, 1997.
• [15] G. Jakubowska,W. Penczek, and M. Srebrny. Verifying security protocols with timestamps via translation to timed automata. In L. Czaja, editor, Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P'05), pages 100-115.Warsaw University, 2005.
• [16] S. Jha E. M. Clarke and W. Marrero. Using state space exploration and a natural deduction style message derivation engine to verify security protocols. In D. Gries and W. P. De Roever, editors, Proceedings of the IFIP Working Conference on Programming Concepts and Methods (PROCOMET'98). Chapmann and Hall, pp. 87-106, 1998.
• [17] M. Kurkowski. Deductive methods for verification of correctness of the authentication protocols (in polish). PhD thesis, Institute of Computer Science, Polish Academy of Sciences, 2003.
• [18] M. Kurkowski, W. Penczek. Verifying Security Protocols Modeled by Networks of Automata. Report 998 of ICS PAS, Warsaw, January 2007.
• [19] M. Kurkowski, W. Penczek, and A. Zbrzezny. SAT-based Verification of Security Protocols via Translation to Networks of Automata. In Proc. of MoChart IV, volume 4428 of LNAI, pages 146-165. Springer-Verlag, 2007.
• [20] G. Lowe. Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR, In Proceedings of TACAS, (1996) 147-166, Springer Verlag.
• [21] G. Lowe, B. Roscoe. Using CSP to Detect Errors in The TMN Protocol. In IEEE Transaction on Software Engineering, vol. 23, No 10. pages 659-669, 1997.
• [22] G. Lowe. Casper: A compiler for the analysis of security protocols. In Journal of Computer Security, 6(1-2), pages 53-84, 1998.
• [23] K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.
• [24] C. Meadows. The NRL protocol analyzer: An overview. In Journal of Logic Programming, 26(2), pages 13-131, 1996.
• [25] M. Mitchell J.C. Mitchell and U. Stern. Automated analysis of cryptographic protocols using mur_. In Proc. of the 1997 IEEE Symposium on Security and Privacy. IEEE Computer Society Press, pages 141-151, 1997.
• [26] R. Needham, M. Schroeder. Using Encryption for Authentication in large networks of computers. In Communications of the ACM, 21(12), pages 993-999, 1978.
• [27] M. Panti, L. Spalazzi, and S. Tacconi. Using the NUSMV model checker to verify the Kerberos Protocol. In Proc. of the Third Collaborative Technologies Symposium (CTS-02), pages 27-31, 2002.
• [28] S. Yovine. KRONOS: A verification tool for real-time systems. In International Journal of Software Tools for Technology Transfer, 1(1/2), pages 123-133, 1997.
• [29] A. Zbrzezny. SAT-based reachability checking for timed automata with diagonal constraints. Fundamenta Informaticae, 67(1-3), pages 303-322, 2005.