Analysis and simulations of timed security protocols

Sabina Szymoniak

Abstract


This paper contains a description of the problem of timed security protocols verification, taking into account delays in the network. Using a specially constructed formal model, which became the basis for the implementation of the special tool, it is possible to calculate the correct time of execution protocol. The tool enables testing timed security protocols, including simulations.

Keywords


timed analysis; security protocols; simulations

Full Text:

PDF (Polski)

References


Needham R., Schroeder M.: Using encryption for authentication in large networks of computers. Commun. ACM, Vol. 21, No. 12, 1978, s. 993÷999.

Dolev D., Yao A.: On the security of public key protocols. IEEE Transactions on Information Theory, Vol. 29, No. 2, 1983, s. 198÷208.

Burrows M., Abadi M., Needham R.: A logic of authentication. Proceedings of the Royal Society of London A, Vol. 426, DEC Systems Research Center, 1989, s. 233÷271.

Szymoniak S., Kurkowski M., Piątkowski J.: Timed models of security protocols including delays in the network. Journal of Applied Mathematics and Computational Mechanics, Vol. 14, No. 3, 2015, s. 127÷139.

Szymoniak S., Siedlecka-Lamch O., Kurkowski M.: Timed Analysis of Security Protocols. Proceedings of the 37th International Conference ISAT 2016, Advances in Intelligent Systems and Computing, Vol. 522, Springer, Karpacz, Poland 2016, s. 53÷63.

Paulson L.: Inductive Analysis of the Internet Protocol TLS, TR440. Computer Laboratory, University of Cambridge 1998.

Kurkowski M., Penczek W.: Applying timed automata to model checking of security protocols. [w:] Wang J. (ed.): Handbook of Finite State Based Models and Applications, Chapman and Hall/CRC Press, 2013, s. 223÷254.

Armando A. i in.: The Avispa Tool for the automated validation of internet security protocols and applications. Proceedings of CAV 2005, Computer Aided Verification, LNCS 3576, Springer Verlag, 2005.

Cremers C.J.F.: The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols. [w:] Gupta A., Malik S. (ed.): Computer Aided Verification 2008, Lecture Notes in Computer Science, Vol. 5123, Springer, Berlin-Heidelberg 2008.

Kurkowski M.: Formalne metody weryfikacji własności protokołów zabezpieczających w sieciach komputerowych. Wyd. Exit, Warszawa 2013.

Jakubowska G., Penczek W.: Modeling and Checking Timed Authentication Security Protocols. Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P’06), Informatik-Berichte, Vol. 206, No. 2, Humboldt University 2006, s. 280÷291.

Jakubowska G., Penczek W.: Is Your Security Protocol on Time? Proc. of the IPM Int. Symp. on Fundamentals of Software Engineering (FSEN’07), LNCS, Vol. 4767, Springer-Verlag, 2007, s. 65÷80.

Repozytorium protokołów zabezpieczających SPORE: http://www.lsv.ens-cachan.fr/Software/spore/table.html, dostęp listopad 2016.

Penczek W., Półrola A.: Advances in Verification of Time Petri Nets and Timed Automata: A Temporal Logic Approach. Springer-Verlag, 2006.

Kurkowski M., Grosser A., Piątkowski J., Szymoniak S.: ProToc – an universal language for security protocols specification. Advances in Intelligent Systems and Computing, Vol. 342, Springer Verlag, 2015, s. 237÷248.




DOI: http://dx.doi.org/10.21936/si2017_v38.n2.801