Verifying Untimed Version of the WMF Protocol Using networks of Autamata

• Autorzy: Grondys K. , Kurkowski M. , Sowik A. , Szczypior I.
• Języki publikacji: EN

Abstrakty

EN

In this paper we present some results of symbolic verification of untimed version of The Wide-Mouth Frog Protocol. This protocol is designed for achieving authentication between communicating sides in the computer network and exchange a new session cryptographic key. For our investigation we model executions of this protocol by a network of synchronized untimed automata. We investigate suitable protocols properties by testing reachablity of some distinguished states in the defined network. We use VerICS [5] - the symbolic model checker - for searching in our network.

Słowa kluczowe

EN

cryptograpic authentication protocols; verification; Model Checking technique

PL

protokoły uwierzytelniania kryptograficznego; weryfikacja; technika Model Checking

• 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: 2006
• Tom: Vol. 11
• Strony: 51--58
• Opis fizyczny: Bibliogr. 11 poz.

Twórcy

autor

Grondys K.

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

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

autor

Sowik A.

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

autor

Szczypior I.

• 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] A. Armando et al. The AVISPA tool for the automated validation of internet security protocols and applications. In: CAV 2005, 17th Int. Conf. on Computer Aided Verification, Edinburgh, Scotland, UK, pp. 281-285, 2005.
• [2] G. Bella, L.C. Paulson. Using Isabelle to prove properties of the kerberos authentication system. In: H. Orman, C. Meadows editors), Proceedings of the DIMACS Workshop on Design and Formal Verification of Security Protocols, 1997. http://dimacs.rutgers.edu/Workshops/Security/
• [3] J.A. Clark, J.L. Jacob. A survey of authentication protocol literature. Technical Report 1.0, 1997. http://www.cs.york.ac.ukjac/papers/drareview.ps.gz
• [4] E.M. Clarke, S. Jha, VV. Marrero. Verifying security protocols with Brutus. ACM Transactions on Software Engineering and Methodology,9 (4),443-487,2000.
• [5] P. Dembiński et al. VerICS: A tool for verifying timed automata and Estelle specifications. In: Proc. 9th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'03), vol. 2619 of LNCS, Springer-Verlag, pp. 278-283, 2003.
• [6] M. Kurkowski, W. Penczek. Verifying cryptographic protocols modeled by networks of automata. In: Proceedings of XV CS&P Concurrency, Specification and Programming), Humboldt University Press, Berlin, pp. 292-303, 2006.
• [7] G. Lowe. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: Proceedings of TACAS, Springer Verlag, pp. 147-166, 1996.
• [8] G. Lowe, B. Roscoe. Using CSP to detect errors in the TMN protocol. IEEE Transaction on Software Engineering, 23, No. 10, pp. 659-669, 1997.
• [9] G. Lowe. A Family of Attacks upon Authentication Protocols. Technical report 1997/5, Department of Mathematics and Computer Science, University of Leicester, 1997.
• [10] C. Meadows. The NRL protocol analyzer: An overview. Journal of Logic Programming, 26, (2), 13-131, 1996.
• [11] R. Needham, M. Schroeder. Using encryption for authentication in large networks of computers. Communications of the ACM, 21, (12), 993-999, 1978.