Automated Analysis of Equivalence Properties for Security Protocols Using Else Branches

  • Ivan GazeauEmail author
  • Steve KremerEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10493)


In this paper we present an extension of the AKISS protocol verification tool which allows to verify equivalence properties for protocols with else branches, i.e., disequality tests. While many protocols are represented as linear sequences or inputs, outputs and equality tests, the reality is often more complex. When verifying equivalence properties one needs to model precisely the error messages sent out when equality tests fail. While ignoring these branches may often be safe when studying trace properties this is not the case for equivalence properties, as for instance witnessed by an attack on the European electronic passport. One appealing feature of our approach is that our extension re-uses the saturation procedure which is at the heart of the verification procedure of AKISS as a black box, without need to modify it. As a result we obtain the first tool that is able verify equivalence properties for protocols that may use xor and else branches. We demonstrate the tool’s effectiveness on several case studies, including the AKA protocol deployed in mobile telephony.


  1. 1.
    Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: 28th Symposium on Principles of Programming Languages (POPL 2001), pp. 104–115. ACM (2001)Google Scholar
  2. 2.
    Abadi, M., Fournet, C.: Private authentication. Theoret. Comput. Sci. 322(3), 427–476 (2004)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: the spi calculus. Inf. Comput. 148(1), 1–70 (1999)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    3GPP: Technical specification group services and system aspects; 3G security; security architecture (release 9). Technical report, Technical Report TS 33.102 V9.3.0, 3rd Generation Partnership Project (2010)Google Scholar
  5. 5.
    Arapinis, M., Chothia, T., Ritter, E., Ryan, M.D.: Analysing unlinkability and anonymity using the applied pi calculus. In: 23rd Computer Security Foundations Symposium (CSF 2010), pp. 107–121. IEEE Computer Society (2010)Google Scholar
  6. 6.
    Arapinis, M., Mancini, L.I., Ritter, E., Ryan, M., Golde, N., Redon, K., Borgaonkar, R.: New privacy issues in mobile telephony: fix and verification. In: 19th Conference on Computer and Communications Security (CCS 2012), pp. 205–216. ACM (2012)Google Scholar
  7. 7.
    Armando, A., et al.: 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). doi: 10.1007/11513988_27CrossRefGoogle Scholar
  8. 8.
    Baelde, D., Delaune, S., Gazeau, I., Kremer, S.: Symbolic verification of privacy-type properties for security protocols with XOR. In: 30th Computer Security Foundations Symposium (CSF 2017). IEEE Computer Society (2017, to appear)Google Scholar
  9. 9.
    Baelde, D., Delaune, S., Hirschi, L.: Partial order reduction for security protocols. In: 26th International Conference on Concurrency Theory (CONCUR 2015). LIPICS, vol. 42, pp. 497–510. Leibniz-Zentrum für Informatik (2015)Google Scholar
  10. 10.
    Basin, D.A., Dreier, J., Sasse, R.: Automated symbolic proofs of observational equivalence. In: 22nd Conference on Computer and Communications Security (CCS 2015), pp. 1144–1155. ACM (2015)Google Scholar
  11. 11.
    Baudet, M.: Deciding security of protocols against off-line guessing attacks. In: 12th Conference on Computer and Communications Security (CCS 2005), pp. 16–25. ACM (2005)Google Scholar
  12. 12.
    Blanchet, B.: Automatic proof of strong secrecy for security protocols. In: Symposium on Security and Privacy (S&P 2004), pp. 86–100. IEEE Computer Society (2004)Google Scholar
  13. 13.
    Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. J. Log. Algebr. Program. 75(1), 3–51 (2008)MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Blanchet, B., Smyth, B., Cheval, V.: Automatic Cryptographic Protocol Verifier, User Manual and Tutorial (2016)Google Scholar
  15. 15.
    Chadha, R., Cheval, V., Ciobâcă, Ş., Kremer, S.: Automated verification of equivalence properties of cryptographic protocol. ACM Trans. Comput. Logic 17(4), 23:1–23:32 (2016). Article no. 23MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    Cheval, V., Comon-Lundh, H., Delaune, S.: Automating security analysis: symbolic equivalence of constraint systems. In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 412–426. Springer, Heidelberg (2010). doi: 10.1007/978-3-642-14203-1_35CrossRefGoogle Scholar
  17. 17.
    Cheval, V., Comon-Lundh, H., Delaune, S.: Trace equivalence decision: negative tests and non-determinism. In: 18th Conference on Computer and Communications Security (CCS 2011), pp. 321–330. ACM (2011)Google Scholar
  18. 18.
    Cheval, V., Cortier, V., Delaune, S.: Deciding equivalence-based properties using constraint solving. Theoret. Comput. Sci. 492, 1–39 (2013)MathSciNetCrossRefzbMATHGoogle Scholar
  19. 19.
    Chevalier, Y., Rusinowitch, M.: Decidability of equivalence of symbolic derivations. J. Autom. Reason. (2010, to appear)Google Scholar
  20. 20.
    Chothia, T., Smirnov, V.: A traceability attack against e-passports. In: Sion, R. (ed.) FC 2010. LNCS, vol. 6052, pp. 20–34. Springer, Heidelberg (2010). doi: 10.1007/978-3-642-14577-3_5CrossRefGoogle Scholar
  21. 21.
    Cremers, C.J.F.: The scyther tool: verification, falsification, and analysis of security protocols. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 414–418. Springer, Heidelberg (2008). doi: 10.1007/978-3-540-70545-1_38CrossRefGoogle Scholar
  22. 22.
    Delaune, S., Kremer, S., Ryan, M.D.: Verifying privacy-type properties of electronic voting protocols. J. Comput. Secur. 17(4), 435–487 (2009)CrossRefzbMATHGoogle Scholar
  23. 23.
    Dierks, T., Rescorla, E.: The transport layer security (TLS) protocol version 1.1. RFC 4346, Internet Engineering Task Force (2008)Google Scholar
  24. 24.
    Escobar, S., Meadows, C., Meseguer, J.: Maude-NPA: cryptographic protocol analysis modulo equational properties. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007-2009. LNCS, vol. 5705, pp. 1–50. Springer, Heidelberg (2009). doi: 10.1007/978-3-642-03829-7_1CrossRefGoogle Scholar
  25. 25.
    Gazeau, I., Kremer, S.: Automated analysis of equivalence properties for security protocols using else branches (extended version). Research report, Inria Nancy - Grand Est (2017).
  26. 26.
    Machine readable travel documents. Doc 9303, International Civil Aviation Organization (ICAO) (2008)Google Scholar
  27. 27.
    Kaufman, C., Hoffman, P., Nir, Y., Eronen, P.: Internet key exchange protocol version 2 (ikev2). RFC 7296, Internet Engineering Task Force (2014)Google Scholar
  28. 28.
    Neuman, C., Hartman, S., Raeburn, K.: The kerberos network authentication service (v5). RFC 4120, Internet Engineering Task Force (2005)Google Scholar
  29. 29.
    Ryan, P.Y.A., Schneider, S.A.: An attack on a recursive authentication protocol. A cautionary tale. Inf. Process. Lett. 65(1), 7–10 (1998)CrossRefzbMATHGoogle Scholar
  30. 30.
    Santiago, S., Escobar, S., Meadows, C., Meseguer, J.: A formal definition of protocol indistinguishability and its verification using maude-NPA. In: Mauw, S., Jensen, C.D. (eds.) STM 2014. LNCS, vol. 8743, pp. 162–177. Springer, Cham (2014). doi: 10.1007/978-3-319-11851-2_11Google Scholar
  31. 31.
    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). doi: 10.1007/978-3-642-39799-8_48CrossRefGoogle Scholar
  32. 32.
    Tiu, A., Dawson, J.: Automating open bisimulation checking for the spi-calculus. In: 23rd Computer Security Foundations Symposium (CSF 2010), pp. 307–321. IEEE Computer Society (2010)Google Scholar
  33. 33.
    van Deursen, T., Radomirovic, S.: Attacks on RFID protocols. IACR Cryptology ePrint Archive, 2008:310 (2008)Google Scholar
  34. 34.
    Yang, F., Escobar, S., Meadows, C.A., Meseguer, J., Santiago, S.: Strand spaces with choice via a process algebra semantics. In: 18th International Symposium on Principles and Practice of Declarative Programming (PPDP 2016), pp. 76–89. ACM (2016)Google Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  1. 1.LORIA, Inria Nancy - Grand-EstVillers-lès-NancyFrance

Personalised recommendations