Using probabilistic automata for security protocols verification

• Autorzy: Siedlecka-Lamch O. , Kurkowski M. , Piątkowski J.

Identyfikatory

DOI

10.17512/jamcm.2016.2.13

• Języki publikacji: EN

Abstrakty

EN

The article discusses the issues of modeling and the analysis of executions, which is a substantial part of modern communication protocols - authentication protocols, which are generally referred to herein as security protocols. The article presents a way of security protocols executions analysis with the use of probabilistic automata, without well known and widely used perfect cryptography assumption (we assume allowing the possibility of breaking a key with a specified probability). This type of analysis leads to interesting observations about the operation of the protocol and its weaknesses.

Słowa kluczowe

EN

verification of security protocols; probabilistic methods

PL

weryfikacja protokołów bezpieczeństwa; metody probabilistyczne; protokoły uwierzytelniania

• Wydawca: Wydawnictwo Politechniki Częstochowskiej
• Czasopismo: Journal of Applied Mathematics and Computational Mechanics
• Rocznik: 2016
• Tom: Vol. 15, nr 2
• Strony: 119--125
• Opis fizyczny: Bibliogr. 9 poz., rys.

Twórcy

autor

Siedlecka-Lamch O.

• Czestochowa University of Technology, Institute of Computer and Information Sciences Częstochowa, Poland

autor

Kurkowski M.

• Cardinal Stefan Wyszynski University in Warsaw, Institute of Computer Sciences Warszawa, Poland

autor

Piątkowski J.

• Czestochowa University of Technology, Institute of Computer and Information Sciences Częstochowa, Poland

Bibliografia

• [1] Armando A. et al., The AVISPA tool for the automated validation of internet security protocolsand applications, Proc. of 17th Int. Conf. on Computer Aided Verification (CAV’05), vol. 3576 of LNCS, Springer 2005, 281-285.
• [2] Kurkowski M., Grosser A., Piątkowski J., Szymoniak S., ProToc - an universal language for security protocols specification, [in:] Advances in Intelligent Systems and Computing, eds. A. Wiliński, I.E. Fray, J. Pejas, Springer Verlag 2015, Vol. 342, 237-248.
• [3] Millen J., Denker G., MuCAPSL, Proc. of DISCEX III, DARPA Information Survivability Conference and Exposition, IEEE Computer Society 2003, 238-249.
• [4] Kurkowski M., Penczek W., Verifying security protocols modeled by networks of automata, Fund. Inform. 2007, 79 (3-4), 453-471.
• [5] Siedlecka-Lamch O., Kurkowski M., Szymoniak S., Piech H., Parallel bounded model checking of security protocols, Proc. of PPAM’13, vol. 8384 of LNCS, Springer Verlag 2014, 224-234.
• [6] Siedlecka-Lamch O., Kurkowski M., Piech H., A new effective approach for modelling and verification of security protocols, Proceedings of 21th International Workshop on Concurrency, Specification and Programming (CS&P 2012), Humboldt University Press, Berlin 2012, 191-202.
• [7] Dolev D., Yao A., On the security of public key protocols, IEEE Transactions on Information Theory 1983, 29(2), 198-207.
• [8] Burrows M., Abadi M., Needham R., A logic of authentication, ACM Transactions on Computer Systems 1990, 8, 18-36.
• [9] Anderson R., Needham R., Programming satan's computer, Computer Science Today, LNCS 1995, 1000, 426-440.

Uwagi

Opracowanie ze środków MNiSW w ramach umowy 812/P-DUN/2016 na działalność upowszechniającą naukę.