Weryfikacja protokołów zabezpieczających z uwzględnieniem opóźnień w sieci

• Autorzy: Szymoniak S.

Warianty tytułu

EN

Verification of security protocols including delays in the network

• Języki publikacji: PL

Abstrakty

PL

W pracy zawarto opis problemu modelowania i weryfikacji czasowych protokołów zabezpieczających z uwzględnieniem opóźnień w sieci. Specyfikacje protokołów są zapisane w formacie ProToc, który umożliwia pełną specyfikację czasowego protokołu. Integralną częścią tej pracy jest zaprojektowane i zaimplementowane narzędzie, służące weryfikacji czasowych protokołów zabezpieczających. Narzędzie warunkuje określenie podatności danego protokołu zabezpieczającego na ataki, przy uwzględnieniu opóźnień w sieci.

EN

This paper contains a description of the problem for modeling and verification of timed security protocols including delays in the network. Protocol specifications are written in the format ProToc, which allows full specification of the timed protocol. An integral part of this work is to designed and implemented tool for verifying time network security protocols. This tool allows specifying a particular protocol security vulnerability to attacks, taking into account the delays in the network.

Słowa kluczowe

PL

weryfikacja; protokoły zabezpieczające; bezpieczeństwo

EN

verification; security protocols; security

• Wydawca: Wydawnictwo Politechniki Śląskiej
• Czasopismo: Studia Informatica
• Rocznik: 2016
• Tom: Vol. 37, nr 1
• Strony: 71--82
• Opis fizyczny: Bibliogr. 14 poz.

Twórcy

autor

Szymoniak S.

• Politechnika Częstochowska, Instytut Informatyki Teoretycznej i Stosowanej, ul. Dąbrowskiego 69, 42-200 Częstochowa, Polska

Bibliografia

• 1. Needham R., Schroeder M.: Using encryption for authentication in large networks of computers. Commun. ACM, Vol. 21(12), 1978, s. 993÷999.
• 2. Dolev D., Yao A.: On the security of public key protocols. IEEE Transactions on In-formation Theory, Vol. 29(2), 1983, s. 198÷208.
• 3. 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.
• 4. Lowe G.: An Attack on The Needham-Schroeder Public-Key Authentication Protocol. Information Processing Letters, Vol. 56, No 3, 1995, s. 131÷133.
• 5. Lowe G.: Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR. Proceedings of TACAS, Springer-Verlag, 1996, s. 147÷166.
• 6. Kurkowski M., Penczek W.: Applying timed automata to model checking of security protocols. [in:] Wang J. (ed.): Handbook of Finite State Based Models and Applications, Chapman and Hall/CRC Press, 2013, s. 223÷254.
• 7. Bella G., Paulson L.C.: Using Isabelle to prove properties of the Kerberos authentica-tion system. [in:] Orman H., Meadows C. (eds.): Proceedings of the DIMACS Work-shop on Design and Formal Verification of Security Protocols (CD-ROM) (DI-MACS’97), 1997.
• 8. Benerecetti M., Cuomo N., Peron A.: TPMC: A Model Checker For Time-Sensitive Security Protocols. Journal of Computers, North America, 2009.
• 9. Kurkowski M.: Formalne metody weryfikacji własności protokołów zabezpieczających w sieciach komputerowych. Wyd. Exit, Warszawa 2013.
• 10. Jakubowska G., Penczek W.: Modeling and Checking Timed Authentication Security Protocols. Proceedings of the International Workshop on Concurrency, Specification and Programming (CS&P’06), Informatik-Berichte, Vol. 206(2), Humboldt University 2006, s. 280÷291.
• 11. Jakubowska G., Penczek W.: Is Your Security Protocol on Time? Proceedings of the IPM International Symposium on Fundamentals of Software Engineering (FSEN’07), LNCS, Vol. 4767, Springer-Verlag, 2007, s. 65÷80.
• 12. Repozytorium protokołów zabezpieczających SPORE: http://www.lsv.ens-cachan.fr/Software/spore/table.html, dostęp listopad 2015.
• 13. Penczek W., Półrola A.: Advances in Verification of Time Petri Nets and Timed Auto-mata: A Temporal Logic Approach. Springer-Verlag, 2006.
• 14. Kurkowski M., Grosser A., Piątkowski J., Szymoniak S.: ProToc – an universal lan-guage for security protocols specification. Advances in Intelligent Systems and Computing, Vol. 342, Springer-Verlag, 2015, s. 237÷248.

Uwagi

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