SAT-Based Verification of Security Protocols Via Translation to Networks of Automata | SpringerLink
Skip to main content
Springer Nature Link
Log in

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

  • Conference paper
Model Checking and Artificial Intelligence (MoChArt 2006)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 4428))

Included in the following conference series:

  • 409 Accesses

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

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  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. 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. 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. 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. 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)

    Article  MATH  MathSciNet  Google Scholar 

  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. 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. Clarke, E.M., Jha, S., Marrero, W.: Verifying security protocols with Brutus. ACM Transactions on Software Engineering and Methodology 9(4), 443–487 (2000)

    Article  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. Dolev, D., Yao, A.: On the security of public key protocols. IEEE Transactions on Information Theory 29(2), 198–208 (1983)

    Article  MATH  MathSciNet  Google Scholar 

  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)

    Chapter  Google Scholar 

  14. Holzmann, G.J.: The model checker SPIN. IEEE Trans. on Software Eng. 23(5), 279–295 (1997)

    Article  MathSciNet  Google Scholar 

  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. 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. 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. 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. 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. 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. 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. Lowe, G., Roscoe, B.: Using CSP to Detect Errors in The TMN Protocol. IEEE Transaction on Software Engineering 23(10), 659–669 (1997)

    Article  Google Scholar 

  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. McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)

    MATH  Google Scholar 

  25. Meadows, C.: The NRL protocol analyzer: An overview. Journal of Logic Programming 26(2), 13–131 (1996)

    Article  Google Scholar 

  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. Needham, R., Schroeder, M.: Using Encryption for Authentication in large networks of computers. Communications of the ACM 21(12), 993–999 (1978)

    Article  MATH  Google Scholar 

  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. Yovine, S.: KRONOS: A verification tool for real-time systems. International Journal of Software Tools for Technology Transfer 1(1/2), 123–133 (1997)

    Article  MATH  Google Scholar 

  30. Zbrzezny, A.: SAT-based reachability checking for timed automata with diagonal constraints. Fundamenta Informaticae 67(1-3), 303–322 (2005)

    MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Mathematics and Computer Science, Jan Długosz University, Armii Krajowej 13/15, 42-200 Czȩstochowa,  

    Mirosław Kurkowski & Andrzej Zbrzezny

  2. Institute of Computer Science, PAS, Ordona 21, 01-237 Warsaw, Poland

    Wojciech Penczek

  3. Institute of Informatics, Podlasie Academy, Sienkiewicza 51, 08-110 Siedlce, Poland

    Wojciech Penczek

Authors
  1. Mirosław Kurkowski
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Wojciech Penczek
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Andrzej Zbrzezny
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Stefan Edelkamp Alessio Lomuscio

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics