Simulation of Security Protocols based on Scenarios of Attacks

• Autorzy: Jakubowska G. , Dembiński P. , Penczek W. , Szreter M.
• Języki publikacji: EN

Abstrakty

EN

In this paper we offer a methodology allowing for simulation of security protocols, implemented in the higher-level language Estelle, using scenarios designed for external attacks. To this aim we apply a translation of specifications of security protocols from Common Syntax to Estelle and an encoding of schemes of attacks into Estelle scenarios. We show that such an intelligent simulation may efficiently serve for validating security protocols.

Słowa kluczowe

EN

security protocols; simulation

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2009
• Tom: Vol. 93, nr 1-3
• Strony: 185--203
• Opis fizyczny: Bibliogr. 19 poz., tab., wykr.

Twórcy

autor

Jakubowska G.

autor

Dembiński P.

autor

Penczek W.

autor

Szreter M.

• Institute of Computer Science, PAS, J.K. Ordona 21, 01-237 Warszawa, Poland,

Bibliografia

• [1] Security protocols open repository. http://www.lsv.ens-cachan.fr//spore, 2003.
• [2] A. Armando and L. Compagna. Sat-based model-checking for security protocols analysis. Int. J. Inf. Secur., 7(1):3-32, 2008.
• [3] S. Budkowski. Estelle development toolset (edt). Comput. Netw. ISDN Syst., 25(1):63-82, 1992.
• [4] S. Budkowski, A. B. Alkhechi, M.-L. Benalycherif, P. Dembinski, M. Gardie, E. Lallet, J. P. Mouchel La Fosse, and Y. Souissi. Formal specification, validation and performance evaluation of the xpress transfer protocol. In Proceedings of the IFIP TC6/WG6.1 International Symposium on Protocol Specification, Testing and Verification XIII, pages 191-206, Amsterdam, The Netherlands, 1993. North-Holland Publishing Co.
• [5] S. Budkowski and P. Dembinski. An introduction to estelle: A specification language for distributed systems. Computer Networks, 14:3-23, 1987.
• [6] 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.
• [7] J. A. Clark and J. L. Jacob. A survey of authentication protocol literature. Technical Report 1.0, 1997.
• [8] V. Cortier, S. Delaune, and P. Lafourcade. A survey of algebraic properties used in cryptographic protocols. Journal of Computer Security, 14(1):1-43, 2006.
• [9] P. Dembinski and G. Jakubowska. Modelling and validating of security protocols. In Proc. of the Int. Workshop on Concurrency, Specification and Programming (CS&P'07), pages 100-115.Warsaw University, 2007.
• [10] L. Hohwiller and S. Wendling. Fieldbus network simulation using a time extended estelle formalism. In MASCOTS '00: Proc. of the 8th Intern. Symp. on Modeling, Analysis and Simulation of Computer and Telecommunication Systems, page 92,Washington, DC, USA, 2000. IEEE Computer Society.
• [11] K. G. Indiradevi and V. S. S. Nair. Simulation based validation of authentication protocols. J. Integr. Des. Process Sci., 8(4):79-98, 2004.
• [12] 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.
• [13] 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.
• [14] C. Jard and T. Jron. Verification and distributed observation of the alternating bit protocol. In FORTE/PSTV'98, ECASP: Special Session on Educational Case Studies in Protocols, Paris, France, 1998.
• [15] G. Lowe. A family of attacks upon authentication protocols. Technical Report 1997/5, Department of Mathematics and Computer Science, University of Leicester, 1997.
• [16] 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.
• [17] 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.
• [18] N. Su, R.N. Zobel, and F.O. Iwu. Simulation in cryptographic protocol design and analysis. In Proc. of the 15th European Simulation Symposium (ESS'03), lll, page 123. v, 2003.
• [19] 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.