Towards Scenarios of External Attacks upon Security Protocols

• Autorzy: Dembiński P. , Jakubowska G. , Penczek W.

Warianty tytułu

PL

Scenariusze dla zewnętrznych ataków na protokoły kryptograficzne

• Języki publikacji: EN

Abstrakty

EN

In this paper we consider a taxonomy of external attacks on security protocols in terms of a message origin and destination in addition to a session and step number. We use this taxonomy for designing algorithms, which for a given type of attack and parameters of the protocol return a scenario of an attack of this type. This way we can dramatically reduce the number of protocol runs to be generated in order to look for an attack upon a protocol in the process of verification or simulation. We show that our algorithms generate scenarios of attacks upon all the protocols, classified within our taxonomy, which are known to susceptible to these attacks. We exemplify the results of our algorithms for several protocols from \cite{SPORE} and \cite{CJ}.

PL

Rozważamy taksonomię zewnętrznych ataków na protokoły kryptograficzne w terminach nazwy wysyłającego i odbierającego wiadmość oraz numeru kroku i sesji. Używamy tej taksonomii do zaprojektowania algorytmów, które dla zadanego typu ataku i parametrów protokołu, zwracają scenariusze ataku tego typu. W ten sposób bardzo istotnie redukujemy liczbę przebiegów protokołu, które mają byc wygenerowane w celu poszukiwania ataku na protokół w procesie weryfikacji lub symulacji W Raporcie jest pokazane, że nasze alorytmy generują scenariusze ataków na protokoły, sklasyfikowane w naszej taksonomii, na które istnieją ataki tego typu. Wyniki zastosowania algorytmów prezentujemy na przykładzie kilku protokołów z \cite{SPORE} i \cite{CJ}.

Słowa kluczowe

EN

model checking; cryptographic protocols; simulation

PL

weryfikacja modelowa; protokoły kryptograficzne; symulacja

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

Twórcy

autor

Dembiński P.

autor

Jakubowska G.

autor

Penczek W.

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

Bibliografia

• [ABB+05] 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. Tumani, 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.
• [AC08] A. Armando and L. Compagna. Sat-based model-checking for security protocols analysis. Int. J. Inf. Secur., 7(l):3-32, 2008.
• [BP97] G. Bella and L.C. Paulson. Using isabelle to prove properties of the kerberos authentication system. In Proc. of the DIMACS Workshop on Design and Formal Verification of Security Protocols (DIMACS'97), 1997.
• [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.
• [CJ97] J. A. Clark and J. L. Jacob. A survey of authentication protocol literature. Technical Report l .0, 1997.
• [CLC03] H. Comon-Lundh and V. Cortier. Security properties: Two agents are sufficient. In Pierpaolo Degano, editor, ESOP, volume 2618 of Lecture Notes in Computer Science, pages 99-113. Springer, 2003.
• [CMS+04] W. Chocianowicz, W. Maćków, A. Skrobek, P. Sukiennik, and J.Pejas. Design and implementation of an universal module for reliable presentation of a document to be signed or verific, project no. 6111 2003 c/0 6280 technical report7. Szczecin University of Technology, 2004.
• [CPR05] W. Chocianowicz, J. Pejaś, and A. Ruciński. The proposal of protocol for electronic signature creation in public environment. Enhanced methods in computer security, biometric and artificial intelligence systems, pages 113-124,2005.
• [JP07] G. Jakubowska and W. Penczek. Is your security protocol on time ? In Farhad Arbab and Marjan Sirjani, editors, Proc. of Int. Symposium on Fundamentals of Software Engineering, International Symposium, FSEN 2007, Tehran, Iran, April 17-19, 2007, volume 4767 of LNCS, pages 65-80. Springer, 2007.
• [KPZ07] 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.
• [Li05] T.  Li, Attack  pattern  analysis  with  simulation  matrix. ID:993868577, 2005.
• [Low97] G. Lowe. A family of attacks upon authentication protocols. Technical Report 1997/5, Department of Mathematics and Computer Science, University of Leicester, 1997.
• [OC08] M. Olszewski and L. Cyra. An integrated framework for security protocol analysis. In ASIACCS '08: Proceedings of the 2008 ACM symposium on Information, computer and Communications security, pages 77-86, New York, NY, USA, 2008. ACM.
• [PST02] 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.
• [SPO03] Security protocols open repository. http://www.lsv.ens-cachan.fr// spore, 2003.
• [Syv94] Paul F. Syverson. A taxonomy of replay attacks. In Proc. of the 7th IEEE Computer Security Foundations Workshop (CSFW'94), pages 187-191. IEEE Computer Society, 1994.
• [SZI03] N. Su, R.N. Zobel, and F.O. Iwu. Simulation in cryptographic protocol design and analysis. In Proc. of the I5th European Simulation Symposium (ESS'03), 111, page 123. v, 2003.
• [YasOO] Alec Yasinsac. Dynamic analysis of security protocols. In NSPW '00: Proceedings of the 2000 workshop on New security paradigms, pages 77-87, New York, NY, USA, 2000. ACM.