nach oben

Erschienen in:

2019 | OriginalPaper | Buchkapitel

Analysing Security Protocols Using Scenario Based Simulation

verfasst von : Farah Al-Shareefi, Alexei Lisitsa, Clare Dixon

Erschienen in: Verification and Evaluation of Computer and Communication Systems

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

In this paper, we present a methodology for analysing security protocols using scenario based simulation. A scenario of a potential attack specifies the flow but not the content of messages. Using scenarios can reduce the number of protocol runs to be explored during attack searching via simulation. The number of runs can be further reduced by minimizing the number of intruder’s generated messages. The intruder’s ability to generate messages is limited by considering: the expected message content and type matching. Our approach uses two tools that support the Abstract State Machines method: the AsmetaL for modelling purposes and the AsmetaS for performing the simulation. We propose a simple model for the specification of commutative encryption. Several protocols are examined to show the effectiveness of our method.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Static Detection of Event-Driven Races in HTML5-Based Mobile Apps

Nächstes Kapitel Running on Fumes

http://www.coreasm.org/.

http://asmeta.sourceforge.net/.

Bella, G., Riccobene, E.: Formal analysis of the Kerberos authentication system. J. Univers. Comput. Sci. 3(12), 1337–1381 (1997)MATH

Bella, G., Riccobene, E.: A realistic environment for crypto-protocol analyses by ASMs. In: Workshop on Abstract State Machines, pp. 127–138 (1998)

Ben Henda, N.: Generic and efficient attacker models in SPIN. In: SPIN Symposium on Model Checking of Software, pp. 77–86. ACM (2014)

Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: 14th IEEE Computer Security Foundations Workshop, pp. 82–96. IEEE (2001)

Börger, E., Raschke, A.: Modeling Companion for Software Practitioners. Springer, Heidelberg (2018). https://doi.org/10.1007/978-3-662-56641-1CrossRef

Börger, E., Stärk, R.: Abstract State Machines: A Method Forhigh-level System Design and Analysis. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-642-18216-7CrossRefMATH

Budkowski, S., Dembinski, P.: An introduction to Estelle: a specification language for distributed systems. Comput. Netw. ISDN Syst. 14(1), 3–23 (1987)CrossRef

Carlsen, U.: Cryptographic protocol flaws: know your enemy. In: Proceedings the Computer Security Foundations Workshop VII, pp. 192–200. IEEE (1994)

Clark, J.A., Jacob, J.L.: A survey of authentication protocol literature. Technical report 1.0 (1997)

10.

Dolev, D., Yao, A.: On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198–208 (1983)MathSciNetCrossRef

11.

Farah, A.S., Lisitsa, A., Clare, D.: The AsmetaL specifications for five security protocols and five attack scenarios. https://doi.org/10.5281/zenodo.2628743

12.

Farahbod, R., Gervasi, V., Glässer, U.: CoreASM: an extensible ASM execution engine. Fund. Inform. 77(1–2), 71–103 (2007)MathSciNetMATH

13.

Gargantini, A., Riccobene, E., Scandurra, P.: A metamodel-based language and a simulation engine for abstract state machines. J. UCS 14(12), 1949–1983 (2008)

14.

Gargantini, A., Riccobene, E., Scandurra, P.: Model-driven language engineering: The ASMETA case study. In: The Third International Conference on Software Engineering Advances. ICSEA, pp. 373–378. IEEE (2008)

15.

Jacquemard, F.: Security protocols open repository (2003). http://www.lsv.ens-cachan.fr//spore/

16.

Jakubowska, G., Dembiński, P., Penczek, W., Szreter, M.: Simulation of security protocols based on scenarios of attacks. Fund. Inform. 93(1–3), 185–203 (2009)MathSciNetMATH

17.

Jakubowska, G., Penczek, W., Srebrny, M.: Verifying security protocols with timestamps via translation to timed automata. In: Proceedings of the International Workshop on Concurrency, Specification and Programming (CS&P 2005), pp. 100–115 (2005)

18.

Lafourcade, P., Puys, M.: Performance evaluations of cryptographic protocols verification tools dealing with algebraic properties. In: Garcia-Alfaro, J., Kranakis, E., Bonfante, G. (eds.) FPS 2015. LNCS, vol. 9482, pp. 137–155. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-30303-1_9CrossRef

19.

Lomuscio, A., Pecheur, C., Raimondi, F.: Automatic verification of knowledge and time with NuSMV. In: Proceedings of the Twentieth International Joint Conference on Artificial Intelligence, pp. 1384–1389. IJCAI/AAAI Press (2007)

20.

Lowe, G.: An attack on the needham-schroeder public-key authentication protocol. Inf. Process. Lett. 56(3), 131–132 (1995)CrossRef

21.

Massey, J.L.: An introduction to contemporary cryptology. Proc. IEEE 76(5), 533–549 (1988)CrossRef

22.

Meier, S., Schmidt, B., Cremers, C., Basin, D.: The TAMARIN prover for the symbolic analysis of security protocols. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 696–701. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8_48CrossRef

23.

Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Commun. ACM 21(12), 993–999 (1978)CrossRef

24.

Shamir, A., Rivest, R.L., Adleman, L.M.: Mental poker. Technical report TM-125, MIT Laboratry for Computer Science (1978)

25.

Syverson, P.: A taxonomy of replay attacks. In: Computer Security Foundations Workshop VII (CSFW 1994), pp. 187–191. IEEE (1994)

26.

Woo, T.Y., Lam, S.S.: A semantic model for authentication protocols. In: Proceedings of the 1993 IEEE Computer Society Symposium on Research in Security and Privacy, 1993, pp. 178–194. IEEE (1993)

Titel: Analysing Security Protocols Using Scenario Based Simulation
verfasst von: Farah Al-Shareefi
Alexei Lisitsa
Clare Dixon
Verlag: Springer International Publishing
Buch: Verification and Evaluation of Computer and Communication Systems
Print ISBN: 978-3-030-35091-8

Electronic ISBN: 978-3-030-35092-5

Copyright-Jahr: 2019
DOI: https://doi.org/10.1007/978-3-030-35092-5_4

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner