Verifying Timed Properties of Security Protocols

• Autorzy: Jakubowska, G. , Penczek, W.

Warianty tytułu

PL

Weryfikacja własności zależnych od czasu dla protokołów uwierzytelniania stron

• Języki publikacji: EN

Abstrakty

EN

In this paper we offer a methodology for verifying correctness of (timed) security protocols whose actions are parametrised with time. To this aim the model of a protocol involves delays and timeouts on transitions, and sets time constraints on actions to be executed. Our approach consists in specifying a security protocol, possibly with timestamps, in a higher-level language and translating automatically the specification to a timed automaton (or their networks). Moreover, we generalise the correspondence property so that attacks can be also discovered when some time constraints are not satisfied. Then, one can use each of the verification tools for timed automata (e.g., Kronos, UppAal, or Yerics) for model checking generalised time authentication of security protocols. As a case study we verify generalised (timed) authentication of KERBEROS, TMN, Neuman Stubblebine, and Andrew Secure Protocol.

PL

Weryfikacja własności zależnych od czasu dla protokołów uwierzytelniania stron. Proponujemy metodologię weryfikacji poprawności (czasowych) protokołów kryptograficznych, których akcje parametryzowane są czasem. W tym celu do modelu protokołu wprowadzone zostały opóźnienia, oczekiwania na tranzycjach oraz ustalone zostały ograniczenia czasowe dla akcji. Nasze podejście polega na specyfikacji protokołu (mogącego zawierać znaczniki czasu) w języku wysokiego poziomu i automatycznej translacji tej specyfikacji do automatu czasowego (lub do sieci automatów czasowych). Ponadto uogólniamy własność "correspondence" w taki sposób, by umożliwić wykrycie ataków, gdy pewne czasowe ograniczenia nie będą spełnione. Dzięki temu, korzystając z dowolnego narzędzia do weryfikacji automatów' czasowych (np. Kronos, UppAal, Yerics) możliwe jest sprawdzenie czy w modelu spełniona jest uogólniona czasowa własność uwierzytelnienia dla protokołów kryptograficznych. Jako przykłady przedstawiamy weryfikację protokołów KERBEROS, TMN, Neuman Stubblebine i Andrew Secure Protocol

Słowa kluczowe

PL

weryfikacja modelowa

EN

cryptographic protocols; model checking

• Czasopismo: Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk
• Rocznik: 2006
• Tom: Nr 991
• Strony: 1-38
• Opis fizyczny: Bibliogr. 32 poz., rys.

Twórcy

autor

Jakubowska, G.

autor

Penczek, W.

• Faculty of Computer Science and Information Systems Szczecin University of Technology Żołnierska 49 70-212 Szczecin, Poland,

Bibliografia

• [ABB+05] A. Armando, D. Basin, Y. Boichut, Y. Chevalier, L. Compagna, J. Cuellar, P. Hankes Drielsma, P. C. Heam, 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 (CAV05), volume 3576 of LNCS, pages 281-285. Springer-Verlag, 2005.
• [AC04] 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.
• [AC05] A. Armando and L. Compagna. An optimized intruder model for SAT-based model-checking of security protocols. ENTCS, 125(1):91-108, 2005.
• [AD90] R. Alur and D. Dill. Automata for modelling real-time systems. In Proc. of the 17th Int. Colloquium on Automata, Languages and Programming (ICALP'90), volume 443 of LNCS, pages 322-335. Springer-Verlag, 1990.
• [AD94] R. Alur and D. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183-235, 1994.
• [BAN90] M. Burrows, M. Abadi, and R. Needham. A logic of authentication. ACM Trans. Comput. Syst., 8(l):18-36, 1990.
• [BB02] M. Boreale and M. 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.
• [Bla01] B. Blanchet. An efficient cryptographic protocol verifier based on Prolog rules. In Proc. of the 14th IEEE Computer Security Foun-dations Workshop (CSFW-14'01), pages 82-96. IEEE Computer Society, 2001.
• [BLP03] L. Bozga, Y. Lakhnech, and M. Périn, Pattern-based abstraction for verifying secrecy in protocols. In Proc. of the 9th International Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS'03), volume 2619 of LNCS, pages 299-314. Springer, 2003.
• [BMV05] D. A. Basin, S. Mödersheim, and Luca Viganó. OFMC: A symbolic model checker for security protocols. International Journal of Information Security, 4(3):181-208, 2005.
• [BP98] G. Bella and L. C. Paulson. Kerberos version 4: Inductive analysis of the secrecy goals. In Proc. of the 5th European Symposium on Research in Computer Security (ESORICS'98), volume 1485 of LNCS, pages 361-375. Springer, 1998.
• [CEHM04] 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.
• [CJ97J J. A. Clark and J. L. Jacob. A survey of authentication protocol literature. Technical Report 1.0, 1997.
• [CohOO] E. Cohen. TAPS: A first-order verifier for cryptographic protocols. In Proc. of the 12th International Conference on Computer Aided Verification (CAVOO), volume 1855 of LNCS, pages 568-571. Springer, 2000.
• [DG04] G. Delzanno and P. Ganty. Automatic verification of time sensitive cryptographic protocols. In Proc. o f the lOth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'04), volume 2988 of LNCS, pages 342-356. Springer, 2004.
• [DJJ02] 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.
• [DJJ+03] 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.
• [ESOO] 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.
• [GLM03] R. Gorrieri, E. Locatelli, and F. Martinelli. A simple language for real-time cryptographlc protocol analysis. In Proc. of the 12th European Symposium on Programming (ESOP'03), volume 2618 of LNCS, pages 114-128. Springer, 2003.
• [HLL+95] T. Hwang, N.-Y. Lee, C.-M. Li, M.-Y. Ko, and Y.-H. Chen. Two attacks on neuman-stubblebine authentication protocols. Information Processing Letters, 53(2):103-107, 1995.
• [JPS05] 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.
• [Low98] G. Lowe. Casper: A compiler for the analysis of security protocols. Journal of Computer Security, 6(l-2):53-84, 1998.
• [LR97] Gavin Lowe and A. W. Roscoe. Using CSP to detect errors in the TMN protocol. IEEE Transactions on Software Engineering, 23(10):659-669, 1997.
• [MvOV01] A. J. Menezes, P. C. van Oorschot, and S. A. Yanstone. Handbook of Applied Cryptography. CRC Press, 2001.
• [NS93] B. C. Neuman and S. G. Stubblebine. A note on the use of times-tamps as nonces. Operating Systems Review, 27(2):10—14, 1993.
• [PLOO] P. Pettersson and K. G. Larsen. UPFAAL2k. Bulletin of the European Association for Theoretical Computer Science, 70:40-44, February 2000.
• [PST02] M. Panti, L. Spalazzi, and S. Tacconi. Using the NuSMV model checker to verify the kerberos protocol. In In Proc. of the Third Collaborative Technologies Symposium (CTS-02), 2002.
• [Son99] D. X. Song. Athena: A new efficient automatic checker for security protocol analysis.   In Proc. of the 12th IEEE Computer Security Foundations Workshop (CSFW'99), pages 192-202. IEEE Computer Society, 1999.
• [SPO03] Security protocols open repository. http://www.lsv.ens-cachan.fr//spore, 2003.
• [TMJ89] M. Tatebayashi, N. Matsuzaki, and D. B. Newman Jr. Key distribution protocol for digital mobile communication systems. In Advances in Cryptology: Proc. of the 9th Annual International Cryptology Conference (CRYPTO '89), volume 435 of LNCS, pages 324-334. Springer, 1989.
• [WL93] 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.
• [Yov97] S. Yovine. KRONOS: A verification tool for real-time systems. International Journal of Software Tools for Technology Transfer, 1(1/2):123-133, 1997.