Timed Automata Based Model Checking of Timed Security Protocols

• Autorzy: Kurkowski M. , Penczek W.
• 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.

Słowa kluczowe

EN

timed security protocols; model checking; authentication

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2009
• Tom: Vol. 93, nr 1-3
• Strony: 245--259
• Opis fizyczny: Bibliogr. 16 poz., tab.

Twórcy

autor

Kurkowski M.

autor

Penczek W.

• Institute of Computer Science, Polish Academy of Sciences Ordona 21, 01-237 Warsaw, Poland,

Bibliografia

• [1] A. Armando, D. Basin, Y. Boichut, Y. Chevalier, L. Compagna, J. Cuellar, P. Hankes Drielsma, P.C. Heám, O. Kouchnarenko, J. Mantovani, S. Mödersheim, D. von Oheimband M. Rusinowitch, J. Santiago, M. Turuani, L. Viganó, and L. Vigneron. The AVISPA tool for the automated validation of internet security protocols and applications. In Proc. of 17th International Conference on Computer Aided Verification (CAV'05), 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(1):3-32, 2008.
• [3] J. Bengtsson, K. G. Larsen, F. Larsson andP. 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: AModel 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. Hartel, and A. Mader. Timed model checking of security protocols. In Proc. of the 2004 ACM Workshop on Formal Methods in Security Engineering (FMSE'04), 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 of 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 Concurrency, 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 andW. Penczek. Is your security protocol on time? In Proc. of the Int. Symp. on Fundamentals of Software Engineering (FSEN'07), vol. 4767 of LNCS, pp. 65-80. Springer-Verlag, 2007.
• [11] G. Jakubowska, W. Penczek, and M. Srebrny. Verifying security protocols with timestamps via translation to timed automata. In Proc. of the International Workshop on Concurrency, Specification and Programming (CS&P'05), pp. 100-115.Warsaw University, 2005.
• [12] P. Dembiński, A. Janowska, P. Janowski, W. Penczek, A. Półrola, M. Szreter, B. Woźna and A. Zbrzezny, VerICS: A Tool for Verifying Timed Automata and Estelle Specifications. In Proc. of the 9th Int. Conf. TACAS'03, vol. 2619 of LNCS, pp. 278-283 Springer-Verlag, 2003.
• [13] 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.
• [14] M. Kurkowski and W. Penczek. Verifying Security Protocols Modelled by Networks of Automata. Fundamenta Informaticae, vol. 79, pp. 453-471. 2007.
• [15] G. Lowe. Casper: A compiler for the analysis of security protocols. Journal of Computer Security, 6(1-2):53-84, 1998.
• [16] Security Protocols Open Repository (SPORE): http://www.lsv.ens-cachan.fr/Software/spore/