Analysing Security Protocols Using Scenario Based Simulation

  • Farah Al-ShareefiEmail author
  • Alexei Lisitsa
  • Clare Dixon
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11847)


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.


Security protocols Abstract State Machines Protocol simulation Attack scenarios 



A. Lisitsa and C. Dixon were partially supported by the EPSRC funded RAI Hub FAIR-SPACE (EP/R026092/1). F. Al-Shareefi was supported by the Higher Committee for Education Development in Iraq (HCED).


  1. 1.
    Bella, G., Riccobene, E.: Formal analysis of the Kerberos authentication system. J. Univers. Comput. Sci. 3(12), 1337–1381 (1997)zbMATHGoogle Scholar
  2. 2.
    Bella, G., Riccobene, E.: A realistic environment for crypto-protocol analyses by ASMs. In: Workshop on Abstract State Machines, pp. 127–138 (1998)Google Scholar
  3. 3.
    Ben Henda, N.: Generic and efficient attacker models in SPIN. In: SPIN Symposium on Model Checking of Software, pp. 77–86. ACM (2014)Google Scholar
  4. 4.
    Blanchet, B.: An efficient cryptographic protocol verifier based on Prolog rules. In: 14th IEEE Computer Security Foundations Workshop, pp. 82–96. IEEE (2001)Google Scholar
  5. 5.
    Börger, E., Raschke, A.: Modeling Companion for Software Practitioners. Springer, Heidelberg (2018). Scholar
  6. 6.
    Börger, E., Stärk, R.: Abstract State Machines: A Method Forhigh-level System Design and Analysis. Springer, Heidelberg (2003). Scholar
  7. 7.
    Budkowski, S., Dembinski, P.: An introduction to Estelle: a specification language for distributed systems. Comput. Netw. ISDN Syst. 14(1), 3–23 (1987)CrossRefGoogle Scholar
  8. 8.
    Carlsen, U.: Cryptographic protocol flaws: know your enemy. In: Proceedings the Computer Security Foundations Workshop VII, pp. 192–200. IEEE (1994)Google Scholar
  9. 9.
    Clark, J.A., Jacob, J.L.: A survey of authentication protocol literature. Technical report 1.0 (1997)Google Scholar
  10. 10.
    Dolev, D., Yao, A.: On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198–208 (1983)MathSciNetCrossRefGoogle Scholar
  11. 11.
    Farah, A.S., Lisitsa, A., Clare, D.: The AsmetaL specifications for five security protocols and five attack scenarios.
  12. 12.
    Farahbod, R., Gervasi, V., Glässer, U.: CoreASM: an extensible ASM execution engine. Fund. Inform. 77(1–2), 71–103 (2007)MathSciNetzbMATHGoogle Scholar
  13. 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)Google Scholar
  14. 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)Google Scholar
  15. 15.
    Jacquemard, F.: Security protocols open repository (2003).
  16. 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)MathSciNetzbMATHGoogle Scholar
  17. 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)Google Scholar
  18. 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). Scholar
  19. 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)Google Scholar
  20. 20.
    Lowe, G.: An attack on the needham-schroeder public-key authentication protocol. Inf. Process. Lett. 56(3), 131–132 (1995)CrossRefGoogle Scholar
  21. 21.
    Massey, J.L.: An introduction to contemporary cryptology. Proc. IEEE 76(5), 533–549 (1988)CrossRefGoogle Scholar
  22. 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). Scholar
  23. 23.
    Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Commun. ACM 21(12), 993–999 (1978)CrossRefGoogle Scholar
  24. 24.
    Shamir, A., Rivest, R.L., Adleman, L.M.: Mental poker. Technical report TM-125, MIT Laboratry for Computer Science (1978)Google Scholar
  25. 25.
    Syverson, P.: A taxonomy of replay attacks. In: Computer Security Foundations Workshop VII (CSFW 1994), pp. 187–191. IEEE (1994)Google Scholar
  26. 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)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Farah Al-Shareefi
    • 1
    Email author
  • Alexei Lisitsa
    • 1
  • Clare Dixon
    • 1
  1. 1.Department of Computer ScienceUniversity of LiverpoolLiverpoolUK

Personalised recommendations