Attacking Each Other

  • Wihem Arsac
  • Giampaolo Bella
  • Xavier Chantry
  • Luca Compagna
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7028)


The theme of this year’s workshop emphasises the widespread use of security protocols in the current epoch. The Web 2.0 for example demands secure transactions for “brief encounters”, that is between principals that share a shortlived goal such as an e-bay purchase.

In this setting, the untouchable Dolev-Yao threat model is inappropriate. It seems more suitable to assume that principals do not share private knowledge and that each of them pursue personal interests without colluding with anyone else. They may attack each other.

This position paper attempts at exceeding Dolev-Yao. It analyses the best-known protocol scenario (which pertains to the Needham-Schroeder-Lowe protocol) under the new threat model, and discusses some novel findings. It shows that current validation methods based on machine-assisted finite-state enumeration scale up to our extended analysis.


Model Check Security Protocol Linear Temporal Logic Threat Model Linear Temporal Logic Formula 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Bellare, M., Rogaway, P.: Provably secure session key distribution– the three party case. In: Proceedings 27th Annual Symposium on the Theory of Computing, pp. 57–66. ACM (1995)Google Scholar
  2. 2.
    Abadi, M., Rogaway, P.: Reconciling Two Views of Cryptography. In: Watanabe, O., Hagiya, M., Ito, T., van Leeuwen, J., Mosses, P.D. (eds.) TCS 2000. LNCS, vol. 1872, pp. 3–22. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  3. 3.
    Gollmann, D.: On the verification of cryptographic protocols — a tale of two committees. In: Proc. of the Workshop on Secure Architectures and Information Flow. ENTCS 32, Elsevier Science (2000)Google Scholar
  4. 4.
    Backes, M., Pfitzmann, B.: Relating symbolic and cryptographic secrecy. In: IEEE Symposium on Security and Privacy (2005)Google Scholar
  5. 5.
    Bella, G., Bistarelli, S., Massacci, F.: Retaliation: Can we live with flaws? In: Essaidi, M., Thomas, J. (eds.) Proc. of the Nato Advanced Research Workshop on Information Security Assurance and Security. Nato through Science, vol. 6, pp. 3–14. IOS Press (2006),
  6. 6.
    Lowe, G.: Breaking and Fixing the Needham-Shroeder Public-Key Protocol Using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 147–166. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  7. 7.
    Ryan, P.Y.A., Schneider, S., Goldsmith, M., Lowe, G., Roscoe, A.W.: Modelling and Analysis of Security Protocols. AW (2001)Google Scholar
  8. 8.
    Bella, G.: Formal Correctness of Security Protocols. Information Security and Cryptography. Springer (2007)Google Scholar
  9. 9.
    Armando, A., Basin, D., Boichut, Y., Chevalier, Y., Compagna, L., Cuellar, J., Drielsma, P.H., Heám, P.C., Kouchnarenko, O., Mantovani, J., Mödersheim, S., von Oheimb, D., Rusinowitch, M., Santiago, J., Turuani, M., Viganò, L., Vigneron, L.: The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 281–285. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  10. 10.
    Armando, A., Carbone, R., Compagna, L.: LTL Model Checking for Security Protocols. In: Proceedings of the 20th IEEE Computer Security Foundations Symposium, CSF20, Venice, Italy, July 6-8. IEEE Computer Society (2007)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Wihem Arsac
    • 1
  • Giampaolo Bella
    • 2
  • Xavier Chantry
    • 1
  • Luca Compagna
    • 1
  1. 1.SAP Research LabsMouginsFrance
  2. 2.Dipartimento di Matematica e InformaticaUniversità di CataniaCataniaItaly

Personalised recommendations