On some specification languages of cryptographic protocols

• Autorzy: Dudek P. , Kurkowski M.
• Języki publikacji: EN

Abstrakty

EN

A key element of the security systems in computer networks are cryptographic protocols (CP). These protocols are concurrent algorithms used to provide relevant system security goals. Their main purpose is, for example, amutual authentication (identification) of communicating parties (users, servers), distribution of new keys and session encryption. Literature indicates numerous errors in protocol constructions. Thus, there is a need to create methods for CP specification and verification. In this paper, we investigate a problem of CP specification. The paper discusses the so-called Common Language - the simplest language of CP specification and HLPSL - a specification language used in the European verification project Avispa. Finally, we introduce PTL - the new language developed for CP specification which allows fully automatic verification.

Słowa kluczowe

EN

cryptographic protocol; HLPSL language; VerICS system

PL

protokół kryptograficzny; język HLPSL; system VerICS

• 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: 2010
• Tom: Vol. 15
• Strony: 121--130
• Opis fizyczny: Bibliogr. 12 poz.

Twórcy

autor

Dudek P.

• Institute of Computer and Information Sciences Częstochowa University of Technology ul. Dąbrowskiego 73, 42-200 Częstochowa, Poland

autor

Kurkowski M.

• Institute of Computer and Information Sciences Częstochowa University of Technology ul. Dąbrowskiego 73, 42-200 Częstochowa, Poland

Bibliografia

• [1] Security Protocols Open Repository (SPORE): http://www.lsv.ens-cachan.fr/Software/spore/
• [2] R. Needham, M. Schroeder. Using encryption for authentication in large networks of computers. Comm. ACM, 21 (12), 993-999, 1978.
• [3] D. Dolev, A. Yao. On the security of public key protocols. IEEE Trans. Information Theory, 29 (2), 198-208, 1983.
• [4] G. Lowe. Breaking and xing the Needham-Schroeder public-key protocol using FDR. In: Proc. TACAS, pp. 147-166, Springer, 1996.
• [5] P. Dembiński, A. Janowska, P. Janowski, W. Penczek, A. Półrola, M. Szreter, B. Wo¹na, A. Zbrzezny. VerICS: A tool for verifying timed automata and estelle specifications. In: Proc. 9th Int. Conf. TACAS'03, vol. 2619 of LNCS, pp. 278-283, Springer, 2003.
• [6] A. Menezes, P. van Oorschot, S. Vanstone. Kryptografia stosowana, WNT, 2005.
• [7] A. Armando, D. Basin, Y. Boichut, Y. Chevalier, L. Compagna, J. Cuellar, P. Hankes Drielsma, P.C. Heam, O. Kouchnarenko, J. Mantovani, S. Modersheim, D. von Oheimband M. Rusinowitch, J. Santiago, M. Turuani, L. Vigano, L. Vigneron. The AVISPA tool for the automated validation of internet security protocols and applications. In: Proc. 17th Int. Conf. Computer Aided Verification (CAV'05),vol. 3576 of LNCS, pp. 281-285, Springer, 2005.
• [8] M. Benerecetti, N. Cuomo, A. Peron. TPMC: A model checker for time-sensitive security protocols. In: Proc. 2007 High Performance Computing and Simulation Conf. (HPCS 2007), pp. 742-749, Prague, 2007.
• [9] M. Kurkowski, W. Penczek. Verifying security protocols modelled by networks of automata. Fund. Informaticae, 79 (3-4), 453-471, 2007.
• [10] A. Armando, L. Compagna. Sat-based model-checking for security protocols analysis. Int. J. Information Security, 7 (1), 3-32, 2008.
• [11] M. Kacprzak, W. Nabiałek, A. Niewiadomski, W. Penczek, A. Półrola, M. Szreter, A. Zbrzezny. Verics 2008 - a model checker for high-level languages. Artificial Intelligence Studies 5 (28), 131-140, 2008.
• [12] M. Kurkowski, W. Penczek. Verifying timed security protocols via translation to timed automata. Fund. Informaticae, 93 (1-3), 245-259, 2009.