Timed models of security protocols including delays in the network

• Autorzy: Szymoniak S. , Kurkowski M. , Piątkowski J.

Identyfikatory

DOI

10.17512/jamcm.2015.3.14

• Języki publikacji: EN

Abstrakty

EN

A very important part of the network and computer systems is to ensure an appropriate level of information transmission security. Security is based primarily on properly selected communication in security protocol. Unfortunately, the time-dependent protocols are vulnerable to attacks; therefore there is a need to verify these protocols. For verification purposes, protocols can be modeled using timed automata. During the modeling and verification of the protocols, one should also keep in mind delays in the network. So far, delays in the network were not modeled.

Słowa kluczowe

EN

computer science; mathematical models

PL

informatyka; modele matematyczne

• Wydawca: Wydawnictwo Politechniki Częstochowskiej
• Czasopismo: Journal of Applied Mathematics and Computational Mechanics
• Rocznik: 2015
• Tom: Vol. 14, nr 3
• Strony: 127--139
• Opis fizyczny: Bibliogr. 12 poz.

Twórcy

autor

Szymoniak S.

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

autor

Kurkowski M.

• Institute of Computer Science, Cardinal Stefan Wyszynski University Warszawa, Polska

autor

Piątkowski J.

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

Bibliografia

• [1] Kurkowski M., Penczek W., Applying timed automata to model checking of security protocols, [in:] Handbook of Finite State Based Models and Applications, J. Wang ed., Chapman and Hall/CRC Press 2013, 223-254.
• [2] Kurkowski M., Grosser A., Piątkowski J., Szymoniak S., ProToc - an universal language for security protocols specification, Advances in Intelligent Systems and Computing 2015, 342, 237-248.
• [3] Paulson L., Proving Properties of Security Protocols by Induction, Proceedings of the IEEE Computer Security Foundations Workshop X, IEEE Computer Society Press, 1997, 70-83.
• [4] Burrows M., Abadi M., Needham R., A Logic of Authentication, Proceedings of the Royal Society of London A, 1989, vol. 426, 233-271. A preliminary version appeared as Research Report 39, DEC Systems Research Center, Palo Alto, February 1989.
• [5] Dolev D., Yao A., On the security of public key protocols, IEEE Transactions on Information Theory 1983, 29(2), 198-208.
• [6] Kurkowski M., Formalne metody weryfikacji własności protokołów zabezpieczających w sieciach komputerowych, Wyd. Exit, Warszawa 2013.
• [7] Benerecetti M., Cuomo N., Peron A., TPMC: A Model Checker For Time-Sensitive Security Protocols, Journal of Computers, North America, 2009.
• [8] Armando A., Basin D., Boichut Y., Chevalier Y., Compagna L., Cuellar J., Hankes Drielsma P., Heám P.C., Kouchnarenko O., Mantovani J., Mödersheim S., von Oheimband D., Rusinowitch M., Santiago J., Turuani M., Viganó L., Vigneron L., The AVISPA tool for the automated validation of internet security protocols and applications, Proc. of 17th International Conference on Computer Aided Verification (CAV’05), vol. 3576 of LNCS, Springer-Verlag, 2005, 281-285.
• [9] Cremers C., Feltz M., Operational Semantics and Verification of Security Protocols, Information Security and Cryptography series, Springer, 2012.
• [10] 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 Humboldt University, 2006, 206(2), 280-291.
• [11] 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, 65-80.
• [12] Penczek W., Półrola A., Advances in Verification of Time Petri Nets and Timed Automata: A Temporal Logic Approach,. Studies in Computational Intelligence 20, Springer-Verlag 2006.