Use of probabilistic timed automata for security protocols modeling

Olga Siedlecka-Lamch

Abstract


Probabilistic timed automata can be used for modeling and verification of systems whose characteristic is real-time and probabilistic. Analyzing stochastic behavior of network communication, many common points of security protocols and automata can be easily found. Modeling with automata allows to use relations and algorithms, such as bisimulation or minimization. This can lead to verification/simplification protocols.

Keywords


probabilistic timed automata; security protocols; security protocols modeling

Full Text:

PDF (Polski)

References


Alur R., Dill D.: A Theory of Timed Automata. Theoretical Computer Science 126, 1994, s. 183÷235.

Anderson R.J. and Needham R.M.: Programming Satan’s Computer. Computer Science Today-Commemorative Issue. Lecture Notes in Computer Science, vol. 1000, Springer-Verlag, Berlin Germany 1995, s. 426÷441.

Armando A., et. al.: The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications. Proceedings of 17th Int. Conf. on Computer Aided Veriffcation CAV’05, LNCS, vol. 3576, Springer, 2005, s. 281÷285.

Bengtsson J., Yi W.: Timed Automata: Semantics, Algorithms and Tools. In Lectures on Concurrency and Petri Nets, Lecture Notes in Computer Science, vol. 3098, Springer, 2013, s. 87÷124.

Blanchet B.: Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif. Foundations and Trends in Privacy and Security, 1(1-2), 2016, s. 1÷135.

Cremers C.: The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols. Proceedings CAV’08, vol. 5123, 2008, s. 414÷418.

Dembinski P., Janowska A., Janowski P., Penczek W., Polrola A., Szreter M., Wozna B., Zbrzezny A.: VerICS: A Tool for Verifying Timed Automata and Estelle Specifications. Proceedings of 9th Int. Conf. TACAS’03, LNCS, vol. 2619, Springer-Verlag, 2003, s. 278÷283.

Kurkowski, M., Penczek, W.: Verifying Security Protocols Modelled by Networks of Automata. Fundamenta Informaticae, vol. 79 (3-4), 2007, s. 453÷471.

Kurkowski M., Siedlecka-Lamch O., Dudek P.: Using Backward Induction Techniques in (Timed) Security Protocols Verification. Proceedings of 12th Int. Conf. CISIM 2013, Lecture Notes in Computer Science, vol. 8104, Krakow Poland 2013, s. 265÷276.

Kwiatkowska M., Norman G., Parker D., Sproston J.: Performance Analysis of Probabilistic Timed Automata Using Digital Clocks. Formal Methods in System Design, vol. 29 (1), 2006, s. 33÷78.

Kwiatkowska M., Norman G., Segala R., Sproston J.: Automatic Verification of Real-time Systems with Discrete Probability Distributions. Theoretical Computer Science, vol. 282, 2002, s. 101÷150.

Kwiatkowska M., Norman G., Sproston J., Wang F.: Symbolic Model Checking for Probabilistic Timed Automata. Information and Computation, vol. 205(7), 2007, s. 1027÷1077.

Lowe G.: Breaking and Fixing the Needham-Schroeder Public-key Protocol Using fdr. In TACAS, LNCS, Springer, 1996, s. 147÷166.

Lowe G.: Some New Attacks Upon Security Protocols, IEEE Computer Society Press. Proceedings of the Computer Security Foundations Workshop VIII, 1996.

Norman G., Parker D., Sproston J.: Model Checking for Probabilistic Timed Automata. Formal Methods in System Design 43(2), 2013, s. 164÷190.

Siedlecka-Lamch O., Kurkowski M., Piatkowski J.: Using Probabilistic Automata for Security Protocols Verification. Journal of Applied Mathematics and Computational Mechanics, vol. 15, issue 2, 2016, s. 125÷131.

Siedlecka-Lamch O., Kurkowski M., Piatkowski J.: Probabilistic Model Checking of Security Protocols without Perfect Cryptography Assumption. Proceedings of 23rd International Conference on Computer Networks, Brunow, Poland, Communications in Computer and Information Science, vol. 608, Springer-Verlag, 2016, s. 107÷117.

Sokolova A., de Vink E.: Probabilistic Automata: System Types, Parallel Composition and Comparison. Validation of Stochastic Systems: A Guide to Current Research, LNCS vol. 2925, 2004, s. 1÷43.

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




DOI: http://dx.doi.org/10.21936/si2017_v38.n3.821