Modelling and Checking Timed Authentication of Security Protocols

• Autorzy: Jakubowska G. , Penczek W.
• Języki publikacji: EN

Abstrakty

EN

In this paper we offer a novel methodology for verifying correctness of (timed) security protocols. The idea consists in computing the time of a correct execution of a session and finding out whether the Intruder can change it to shorter or longer by an active attack. Moreover, we generalize the correspondence property so that attacks can be also discovered when some time constraints are not satisfied. An implementation of our method is described. As case studies we verify generalized (timed) authentication of KERBEROS, TMN, Neumann Stubblebine Protocol, Andrew Secure Protocol, Wide Mouthed Frog, and NSPK.

Słowa kluczowe

EN

security protocols; modelling protocols; timing

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2007
• Tom: Vol. 79, nr 3-4
• Strony: 363--378
• Opis fizyczny: bibliogr. 25 poz., wykr.

Twórcy

autor

Jakubowska G.

autor

Penczek W.

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

Bibliografia

• [1] Security protocols open repository. http://www.lsv.ens-cachan.fr//spore, 2003.
• [2] 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 Oheimb, 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), volume 3576 of LNCS, pages 281-285. Springer-Verlag, 2005.
• [3] A. Armando and L. Compagna. SATMC: A SAT-based model checker for security protocols. In Proc. Of the 9th European Conference on Logics in Artificial Intelligence (JELIA'04), volume 3229 of LNCS, pages 730-733. Springer, 2004.
• [4] A. Armando and L. Compagna. An optimized intruder model for SAT-based model-checking of security protocols. ENTCS, 125(1):91-108, 2005.
• [5] D. A. Basin, S. Mödersheim, and Luca Vigan`o. OFMC: A symbolic model checker for security protocols. International Journal of Information Security, 4(3):181-208, 2005.
• [6] J. Bengtsson, K. G. Larsen, F. Larsson, P. Pettersson, W. Yi, and C. Weise. New generation of UPPAAL. In Proc. of the Int. Workshop on Software Tools for Technology Transfer, 1998.
• [7] M. Boreale andM. G. Buscemi. Experimenting with STA, a tool for automatic analysis of security protocols. In Proc. of the 2002 ACM Symposium on Applied Computing (SAC'02), pages 281-285. ACM, 2002.
• [8] M. Burrows, M. Abadi, and R. Needham. A logic of authentication. ACM Trans. Comput. Syst., 8(1):18-36, 1990.
• [9] J. A. Clark and J. L. Jacob. A survey of authentication protocol literature. Technical Report 1.0, 1997.
• [10] 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), pages 23-32. ACM, 2004.
• [11] C. Daws, A. Olivero, S. Tripakis, and S. Yovine. The tool KRONOS. In Hybrid Systems III, volume 1066 of LNCS, pages 208-219. Springer-Verlag, 1995.
• [12] 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), volume 2988 of LNCS, pages 342-356. Springer, 2004.
• [13] 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. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'03), volume 2619 of LNCS, pages 278-283. Springer-Verlag, 2003.
• [14] A. Doroś, A. Janowska, and P. Janowski. From specification languages to timed automata. In Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P'02), volume 161(1) of Informatik-Berichte, pages 117-128. Humboldt University, 2002.
• [15] 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), volume 1895 of LNCS, pages 222-237. Springer, 2000.
• [16] 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), volume 2618 of LNCS, pages 114-128. Springer, 2003.
• [17] G. Jakubowska and W. Penczek. Verifying timed properties of security protocols. Technical Report 991, ICS PAS, Ordona 21, 01-237Warsaw, March 2006.
• [18] G. Jakubowska and W. Penczek. Is your security protocol on time? In Proc. of the Int. Symp. on Fundamentals of Software Engineering (FSEN'07), pages 77-94. IPM Teheran, 2007.
• [19] 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), pages 100-115.Warsaw University, 2005.
• [20] M. Kurkowski, W. Penczek, and A. Zbrzezny. Sat-based verification of security protocols via translation to networks of automata. In MoChart IV, volume 4428 of LNAI, pages 146-165. Springer-Verlag, 2007.
• [21] G. Lowe. An attack on the needham-schroeder public-key authentication protocol. Information Processing Letters, 56(3):131-133, 1995.
• [22] G. Lowe. Casper: A compiler for the analysis of security protocols. Journal of Computer Security, 6(1-2):53-84, 1998.
• [23] A. J. Menezes, P. C. van Oorschot, and S. A. Vanstone. Handbook of Applied Cryptography. CRC Press, 2001.
• [24] M. Panti, L. Spalazzi, and S. Tacconi. Using the NuSMV model checker to verify the kerberos protocol. In Simulation Series, volume 34, pages 230-236. Society for Computer Simulation, 2002.
• [25] T. Y. C. Woo and S. S. Lam. A semantic model for authentication protocols. In Proc. of the 1993 IEEE Symposium on Security and Privacy (SP'93), pages 178-194. IEEE Computer Society, 1993.