Timed automata based model checking of timed security protocols

• Autorzy: Kurkowski M. , Penczek W.

Warianty tytułu

PL

Automaty czasowe w weryfikacji czasowych protokołów kryptograficznych

• Języki publikacji: EN

Abstrakty

EN

A new approach to verification of timed security protocols is given. The idea consists in modelling a finite number of users (including an intruder) of the computer network and their knowledge about secrets by timed automata. The runs of the product automaton of the above automata correspond to all the behaviours of the protocol for a fixed number of sessions. Verification is performed using the module BMC of the tool VerICS.

PL

W pracy przedstawiono nową metodę weryfikacji czasowych protokołów kryptograficznych. Sko\'nczona liczba użytkowników sieci oraz ich wiedza podczas wykonywania protokołu są modelowane przy pomocy automatów czasowych. Sieć automatów w pełni odzwierciedla zachowania podczas wykonywania protokołu niezbędne do weryfikowania założonych własności. Weryfikacja przeprowadzana jest za pomocą modułu BMC narzędzia VerICS.

Słowa kluczowe

EN

security protocols; model checking; authentication

PL

protokoły kryptograficzne; weryfikacja modelowa

• Wydawca: Instytut Podstaw Informatyki PAN
• Czasopismo: Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
• Rocznik: 2008
• Tom: nr 1010
• Strony: 1--36
• Opis fizyczny: Bibliogr. 14 poz.

Twórcy

autor

Kurkowski M.

autor

Penczek W.

• Institute of Mathematics and Computer Science Jan Długosz University Al. Armii Krajowej 13/15,

Bibliografia

• [1] A. Armando, et all, The AVISPA tool for the automated validation of internet security protocols and applications. In Proc. of 17th International Conference on Computer Aided Verification (CAV05), vol. 3576 of LNCS, pp. 281-285. Springer-Verlag, 2005.
• [2] A. Armando and L. Compagna. Sat-based model-checking for security protocols analysis. Int. J. Inf. Secur., 7(l):3-32, 2008.
• [3] J. Bengtsson, K. G. Larsen, F. Larsson and P. Pettersson, W. Yi, and C. Weise. New generation of uppaal. In Proc. of the Int. Workshop on Software Tools for Technology Transfer, 1998.
• [4] M. Benerecetti, N. Cuomo and A. Peron. TPMC: A Model Checker for Time-Sensitive Security Protocols. In: Proceedings of the 2007 high performance computing and simulation conference (HPCS 2007), pp. 742-749, Prague, 2007.
• [5] R. Corin, S. Etalle, P. H. Kartel, and A. Mader. Timed model checking of security protocols. In Proc. of the 2004 ACM Workshop on Formal Methods in Security Engineering (FMSE'O4), pp. 23-32. ACM, 2004.
• [6] G. Delzanno and P. Ganty. Automatic verification of time sensitive cryptographic protocols. In Proc. of the 10th International Conference on Tools and Algorithms for the Construction and Analysis o f Systems (TACAS'04), vol. 2988 of LNCS, pp. 342-356. Springer, 2004.
• [7] A. Doroś, A. Janowska, and P. Janowski. From Specification languages to timed automata. In Proc. of the Int. Workshop on Goncurrency, Specification and Programming, vol. 161(1) of Informatik-Berichte, pp. 117-128. Humboldt Univ., 2002.
• [8] N. Evans and S. Schneider. Analysing time dependent security properties in CSP using PVS. In Proc. of the 6th European Symposium on Research in Computer Security (ESORICS'00), vol. 1895 of LNCS, pp. 222-237. Springer, 2000.
• [9] R. Gorrieri, E. Locatelli, and F. Martinelli. A simple language for real-time cryptographic protocol analysis. In Proc. of the 12th European Symposium on Programming (ESOP'03), vol. 2618 of LNCS, pp. 114-128. Springer, 2003.
• [10] G. Jakubowska and W. Penczek. Is your security protocol on time? In Proc. of the Int. Symp. on Fundamentals of Software Engineering (FSEN'07), pp. 77-94. IPM Teheran, 2007.
• [11] G. Jakubowska, W. Penczek, and M. Srebrny. Verifying security protocols with timestamps via translation to timed automata. In Proc. o f the International Workshop on Concurrency, Specification and Programming (CS&P'05), pp. 100-115. Warsaw University, 2005.
• [12] M. Kurkowski. Deductive methods for verification of correctnes of the authentication protocols (in polish). PhD thesis, Institute of Computer Science, Polish Academy of Sciences, 2003.
• [13] M. Kurkowski, W. Penczek, and A. Zbrzezny. Sat-based verification of security protocols via translation to networks of automata. In MoChart IV, vol. 4428 of LNAI, pp. 146-165. Springer-Verlag, 2007.
• [14] G. Lowe. Casper: A compiler for the analysis of security protocols. Journal of Computer Security, 6(l-2):53-84, 1998.