Advertisement

SAT-Based Verification of Security Protocols Via Translation to Networks of Automata

  • Mirosław Kurkowski
  • Wojciech Penczek
  • Andrzej Zbrzezny
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4428)

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.

Keywords

security protocols model checking authentication 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    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)Google Scholar
  2. 2.
    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)Google Scholar
  3. 3.
    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)Google Scholar
  4. 4.
    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)Google Scholar
  5. 5.
    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)zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    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)Google Scholar
  7. 7.
    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)
  8. 8.
    Clarke, E.M., Jha, S., Marrero, W.: Verifying security protocols with Brutus. ACM Transactions on Software Engineering and Methodology 9(4), 443–487 (2000)CrossRefGoogle Scholar
  9. 9.
    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)CrossRefGoogle Scholar
  10. 10.
    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)CrossRefGoogle Scholar
  11. 11.
    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)Google Scholar
  12. 12.
    Dolev, D., Yao, A.: On the security of public key protocols. IEEE Transactions on Information Theory 29(2), 198–208 (1983)zbMATHCrossRefMathSciNetGoogle Scholar
  13. 13.
    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)CrossRefGoogle Scholar
  14. 14.
    Holzmann, G.J.: The model checker SPIN. IEEE Trans. on Software Eng. 23(5), 279–295 (1997)CrossRefMathSciNetGoogle Scholar
  15. 15.
    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)Google Scholar
  16. 16.
    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)Google Scholar
  17. 17.
    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)Google Scholar
  18. 18.
    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)Google Scholar
  19. 19.
    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)Google Scholar
  20. 20.
    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)
  21. 21.
    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)Google Scholar
  22. 22.
    Lowe, G., Roscoe, B.: Using CSP to Detect Errors in The TMN Protocol. IEEE Transaction on Software Engineering 23(10), 659–669 (1997)CrossRefGoogle Scholar
  23. 23.
    Lowe, G.: Casper: A compiler for the analysis of security protocols. Journal of Computer Security 6(1-2), 53–84 (1998)Google Scholar
  24. 24.
    McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)zbMATHGoogle Scholar
  25. 25.
    Meadows, C.: The NRL protocol analyzer: An overview. Journal of Logic Programming 26(2), 13–131 (1996)CrossRefGoogle Scholar
  26. 26.
    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)Google Scholar
  27. 27.
    Needham, R., Schroeder, M.: Using Encryption for Authentication in large networks of computers. Communications of the ACM 21(12), 993–999 (1978)zbMATHCrossRefGoogle Scholar
  28. 28.
    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)Google Scholar
  29. 29.
    Yovine, S.: KRONOS: A verification tool for real-time systems. International Journal of Software Tools for Technology Transfer 1(1/2), 123–133 (1997)zbMATHCrossRefGoogle Scholar
  30. 30.
    Zbrzezny, A.: SAT-based reachability checking for timed automata with diagonal constraints. Fundamenta Informaticae 67(1-3), 303–322 (2005)zbMATHMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • Mirosław Kurkowski
    • 1
  • Wojciech Penczek
    • 2
    • 3
  • Andrzej Zbrzezny
    • 1
  1. 1.Institute of Mathematics and Computer Science, Jan Długosz University, Armii Krajowej 13/15, 42-200 Czȩstochowa 
  2. 2.Institute of Computer Science, PAS, Ordona 21, 01-237 WarsawPoland
  3. 3.Institute of Informatics, Podlasie Academy, Sienkiewicza 51, 08-110 SiedlcePoland

Personalised recommendations