Effective reduction of cryptographic protocols specification for model-checking with Spin

• Autorzy: Krawczyk U. , Sapiecha P.
• Języki publikacji: EN

Abstrakty

EN

In this article a practical application of the Spin model checker for verifying cryptographic protocols was shown. An efficient framework for specifying a minimized protocol model while retaining its functionality was described. Requirements for such a model were discussed, such as powerful adversary, multiple protocol runs and a way of specifying validated properties as formulas in temporal logic.

Słowa kluczowe

EN

cryptographic protocols; Spin model checker

• Wydawca: Wydawnictwo UMCS
• Czasopismo: Annales Universitatis Mariae Curie-Skłodowska. Sectio AI, Informatica
• Rocznik: 2011
• Tom: Vol. 11, no. 3
• Strony: 27--40
• Opis fizyczny: Bibliogr. 23 poz., rys., tab.

Twórcy

autor

Krawczyk U.

• Krypton-Polska, Al. Jerozolimskie 131, Warsaw, Poland

autor

Sapiecha P.

• Krypton-Polska, Al. Jerozolimskie 131, Warsaw, Poland
• Department of Electronics and Information Technology, Warsaw University of Technology, Warsaw, Poland

Bibliografia

• [1] Uk chip and pin credit / debit cards are insecure (2009) http://www.youtube.com/watch?v=JPAX321gkrw
• [2] Schneider S., Ryan P., Modelling and analisis of security protocols, Addison–Wesley (2001).
• [3] Holzmann G. J., Hu C., Logic Model Checking - lectures, (2008) http://spinroot.com/spin/Doc/course/
• [4] Merz S., Model Checking: A Tutorial Overview, Technical report M¨unchen University (2000)
• [5] Mukund M., Linear-time temporal logic and Büchi automata, SPIC Mathematical Institute, Madras, India (1997)
• [6] Tauriainen H., Automated testing of B¨uchi automata translators for linear temporal logic, Helsinki University of Technology (2000)
• [7] Spin model checker: http://www.spinroot.com
• [8] Spin Workshop: http://spinroot.com/spin/Workshops/index.html
• [9] BEEM: BEnchmarks for Explicit Model checkers: Needham-Schroeder protocol model http://anna.fi.muni.cz/models/cgi/model info.cgi?name=needham
• [10] Khan A. S., Mukund M., Suresh S. P., Generic verification of security protocols, Springer Berlin / Heidelberg (2005)
• [11] Sapiecha P., Krawczyk U., Validation of cryptographic protocols using model checker spin, CECC (2010).
• [12] Lafuente A. L., Promela database: X.509 protocol model http://www.albertolluch.com/research/promelamodels
• [13] Maggi P., Sisto R., Using SPIN to to verify security properties of cryptographic protocols, In LNCS Springer-Verlag (2002): 187.
• [14] Merz S., Needham–schroeder protocol model http://www.loria.fr/ merz/papers/NeedhamSchroeder.spin
• [15] Yongjian L., Rui X.,Design of a CIL Connector to Spin (2008)
• [16] Compagna L., Armando A., Carbone R., LTL model checking for security protocols 23 (2009).
• [17] Gordon A. D., Progress on provable implementations of security protocols, Technical Report, Microsoft Research (2009).
• [18] Stamer H., Verification of cryptographic protocols, Technical Report, University of Kassel (2005).
• [19] Schnoebelen Ph., The complexity of temporal logic model checking, Advances in Modal Logic (2003).
• [20] Rozier K. Y., Vardi M. Y., LTL satisfiability checking (2008).
• [21] Casper: A compiler for the analysis of security protocols http://web.comlab.ox.ac.uk/people/Gavin.Lowe/Security/Casper/
• [22] ProVerif: Cryptographic protocol verifier in the formal model http://www.proverif.ens.fr/
• [23] Denker G., Millen J., CAPSL and CIL Language design, Technical Report, Computer Sciene Laboratory (1999).