A State Transition Model for Honest Executions of Authentication Protocols

• Autorzy: Kurkowski M.
• Konferencja: Proceedings of the IX Conference "Applications of algebra" (9 ; 07-13.03.2005 ; Zakopane, Poland)
• Języki publikacji: EN

Abstrakty

EN

Cryptographic protocols are very good tools to achieve authentication in large distributed computer network. These protocols are precisely defined sequences of actions (communication and computation steps) which use some cryptographic mechanism such as encryption and decryption. It is well known that the design of authentication cryptographic protocols is error prone. Several protocols have been shown flawed in computer security literature. Due to this it is necessary to have some methods of analysis and properties verification of these protocols. It is obvious that in investigations of these properties a suitable formal model is needed. This model should express all important properties and ideas of protocols. Usually size of modeIs introduced by many people is very huge and searching of these modeIs is impossible. In this paper we propose a new formal model of honest executions of cryptographic authentication protocol. To decrease number of states in our model we propose some partial order reduction. We hope that this model is a good startpoint for further investigations and will be usefull in verification of real executions of cryptographic protocols.

Słowa kluczowe

EN

cryptographic authentication protocols; verification; model checking

PL

protokoły uwierzytelniania kryptograficznego; weryfikacja; sprawdzanie modelu

• Wydawca: Wydawnictwo Uniwersytetu Humanistyczno-Przyrodniczego im. Jana Długosza w Częstochowie
• Czasopismo: Scientific Issues of Jan Długosz University in Częstochowa. Mathematics
• Rocznik: 2005
• Tom: Vol. 10
• Strony: 83--94
• Opis fizyczny: Bibliogr. 17 poz., rys.

Twórcy

autor

Kurkowski M.

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

Bibliografia

• [1] M. Abadi. Explicit communication revisited: two new attacks on authentication protocols. IEEE Transactions on Software Engineering, 23, 3, pp. 185-186, 1997.
• [2] U. Carlsen. Generating formal cryptographic protocol specifications. Proceedings of the 1994 IEEE Computer Society Symposium on Research in Security and Privacy, IEEE Computer Society Press, pp. 137-146, 1994.
• [3] E. Clarke, S. Jha, W. Marrero. Partial order reductions for security, protocols verification. Proceedings of TACAS/ETAPS, Springer - Verlag, pp. 503-518, 2000.
• [4] E. Clarke, W. Marrero, S. Jha. A machine checkable logic of knowledge for specifying security properties of electronic commerce protocols, Proc. IFIP Working Conference on Programming Concepts and Methods (PROCOMET), June 1998.
• [5] S. Gritzalis, D. Spinellis, P. Georgiadis. Security protocols over open networks and distributed systems: formal methods for their analysis, design and verification, ACM Computer Communications, 22, 8, pp. 695-707, 1999
• [6] M. Kurkowski. Dedukcyjne metody weryfikacji poprawności protokolow uwierzytelniania, Deduction methods of verification of authentication protocols. PhD dissertation, Institute of Computer Science of The Polish Academy of Sciences, Warsaw, Poland 2003.
• [7] G. Lowe. An attack on the Needham-Schroeder public-key authentication protocol. Information Processing Letters, 56, No 3, pp. 131-133, 1995.
• [8] G. Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. Proceedings of TACAS, Springer-Verlag, pp. 147-166, 1996.
• [9] G. Lowe. A Family of Attacks upon Authentication Protocols. Technical report 1997/5, Department of Mathematics and Computer Science, University of Leicester.
• [10] G. Lowe. Some new attacks upon security protocols. Proceedings of the IEEE Computer Security Foundations Workshop IX, IEEE Computer Society Press, 1996.
• [11] W. Marrero, E. Clarke, S. Jha. Model Checking for Security Protocols. CMU Report No. CMU-CS-97-139, 1997.
• [12] C. Meadows. Applying formal methods to the analysis of a key management protocol. Joumal of Computer Security, 1, pp. 5-35, 1992.
• [13] C. Meadows. Formal verification of cryptographic protocols: a survey. Advances in Cryptology, Proceedings of ASIACRYPT ‘94, Springer-Verlag, pp. 133-150, 1995.
• [14] C. Meadows. Language generation and verification in the NRL protocol analyzer. Proceedings of the 1996 IEEE Computer Security Foundation Workshop IX, IEEE Computer Society Press, pp. 48-61, 1996.
• [15] C. Meadows. The NRL protocol analyzer: an overview. Journal of Logic Programming, 26, No. 2, pp. 113-131, 1996.
• [16] C. Meadows. Using the NRL protocol analyzer to examine protocol suites. Proceedings of the 1998 LICS Workshop on Formal Methods and Security Protocols, 1998. http://www.cs.bell-labs.com/who/nch/fmsp/program.html
• [17] V. Varadharajan, Verification of network security protocols. Computers and Security. Elsevier Advanced Technology, 8, pp. 693-708, 1989.