Advertisement

Efficiently Deciding Equivalence for Standard Primitives and Phases

  • Véronique Cortier
  • Antoine Dallon
  • Stéphanie Delaune
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11098)

Abstract

Privacy properties like anonymity or untraceability are now well identified, desirable goals of many security protocols. Such properties are typically stated as equivalence properties. However, automatically checking equivalence of protocols often yields efficiency issues.

We propose an efficient algorithm, based on graph planning and SAT-solving. It can decide equivalence for a bounded number of sessions, for protocols with standard cryptographic primitives and phases (often necessary to specify privacy properties), provided protocols are well-typed, that is encrypted messages cannot be confused. The resulting implementation, SAT-Equiv, demonstrates a significant speed-up w.r.t. other existing tools that decide equivalence, covering typically more than 100 sessions. Combined with a previous result, SAT-Equiv can now be used to prove security, for some protocols, for an unbounded number of sessions.

References

  1. 1.
    Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Proceedings of 28th ACM Symposium on Principles of Programming Languages, POPL 2001, pp. 104–115. ACM (2001)Google Scholar
  2. 2.
    Arapinis, M., Chothia, T., Ritter, E., Ryan, M.: Analysing unlinkability and anonymity using the applied pi calculus. In: Proceedings of 23rd Computer Security Foundations Symposium (CSF 2010), pp. 107–121. IEEE Computer Society Press (2010)Google Scholar
  3. 3.
    Armando, A., Compagna, L.: Sat-based model-checking for security protocols analysis. Int. J. Inf. Secur. 7, 3–32 (2008)CrossRefGoogle Scholar
  4. 4.
    Bhargavan, K., Blanchet, B., Kobeissi, N.: Verified models and reference implementations for the TLS 1.3 standard candidate. In: Proceedings of 38th IEEE Symposium on Security and Privacy (S&P 2017). IEEE Computer Society Press (2017)Google Scholar
  5. 5.
    Blanchet, B.: Symbolic and computational mechanized verification of the ARINC823 avionic protocols. In: Proceedings of 30th IEEE Computer Security Foundations Symposium (CSF 2017), pp. 68–82. IEEE Computer Society Press (2017)Google Scholar
  6. 6.
    Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. J. Logic Algebr. Program. 75(1), 3–51 (2008)MathSciNetCrossRefGoogle Scholar
  7. 7.
    Blum, A., Furst, M.: Fast planning through planning graph analysis. Artif. Intell. 90, 281–300 (1997)CrossRefGoogle Scholar
  8. 8.
    Chadha, R., Ciobâcă, Ş., Kremer, S.: Automated verification of equivalence properties of cryptographic protocols. In: Seidl, H. (ed.) ESOP 2012. LNCS, vol. 7211, pp. 108–127. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-28869-2_6CrossRefGoogle Scholar
  9. 9.
    Cheval, V.: APTE: an algorithm for proving trace equivalence. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 587–592. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-642-54862-8_50CrossRefGoogle Scholar
  10. 10.
    Cheval, V., Cortier, V., Delaune, S.: Deciding equivalence-based properties using constraint solving. Theoret. Comput. Sci. 492, 1–39 (2013)MathSciNetCrossRefGoogle Scholar
  11. 11.
    Cheval, V., Kremer, S., Rakotonirina, I.: DEEPSEC: deciding equivalence properties in security protocols - theory and practice. In: Proceedings of 39th IEEE Symposium on Security and Privacy (S&P 2018), pp. 525–542. IEEE Computer Society Press (2018)Google Scholar
  12. 12.
    Chrétien, R., Cortier, V., Delaune, S.: Typing messages for free in security protocols: the case of equivalence properties. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 372–386. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-662-44584-6_26CrossRefGoogle Scholar
  13. 13.
    Chrétien, R., Cortier, V., Delaune, S.: Decidability of trace equivalence for protocols with nonces. In: Proceedings of the 28th IEEE Computer Security Foundations Symposium (CSF 2015). IEEE Computer Society Press (2015)Google Scholar
  14. 14.
    Chrétien, R., Cortier, V., Dallon, A., Delaune, S.: Typing messages for free in security protocols. Technical report (2018)Google Scholar
  15. 15.
    Compagna, L.: SAT-based model-checking of security protocols. Ph.D. thesis, Università degli Studi di Genova and the University of Edinburgh (joint programme), September 2005Google Scholar
  16. 16.
    Cortier, V., Dallon, A., Delaune, S.: SAT-equiv: an efficient tool for equivalence properties. In: Proceedings of the 30th IEEE Computer Security Foundations Symposium (CSF 2017). IEEE Computer Society Press, August 2017Google Scholar
  17. 17.
    Cortier, V., Dallon, A., Delaune, S.: Efficiently deciding equivalence for standard primitives and phases. Research report, June 2018. https://hal.archives-ouvertes.fr/hal-01819366
  18. 18.
    Cortier, V., Grimm, N., Lallemand, J., Maffei, M.: A type system for privacy properties. In: Proceedings of 24th ACM Conference on Computer and Communications Security (CCS 2017), pp. 409–423. ACM (2017)Google Scholar
  19. 19.
    Cortier, V., Grimm, N., Lallemand, J., Maffei, M.: Equivalence properties by typing in cryptographic branching protocols. In: Bauer, L., Küsters, R. (eds.) POST 2018. LNCS, vol. 10804, pp. 160–187. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-89722-6_7CrossRefGoogle Scholar
  20. 20.
    Cremers, C., Horvat, M., Hoyland, J., Scott, S., van der Merwe, T.: A comprehensive symbolic analysis of TLS 1.3. In: Proceedings of 24th ACM Conference on Computer and Communications Security (CCS 2017), pp. 1773–1788. ACM (2017)Google Scholar
  21. 21.
    Delaune, S., Kremer, S., Ryan, M.: Verifying privacy-type properties of electronic voting protocols. J. Comput. Secur. 4, 435–487 (2008)zbMATHGoogle Scholar
  22. 22.
    Escobar, S., Meadows, C., Meseguer, J.: A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties. Theoret. Comput. Sci. 367(1–2), 162–202 (2006)MathSciNetCrossRefGoogle Scholar
  23. 23.
    Kautz, H., Selman, B.: Planning as satisfiability. In: Proceedings 10th European Conference on Artificial Intelligence (ECAI 1992), pp. 359–363 (1992)Google Scholar
  24. 24.
    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_48CrossRefGoogle Scholar
  25. 25.
    Tiu, A., Dawson, J.: Automating open bisimulation checking for the spi calculus. In: Proceedings of 23rd IEEE Computer Security Foundations Symposium (CSF 2010), pp. 307–321. IEEE Computer Society Press (2010)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Véronique Cortier
    • 1
  • Antoine Dallon
    • 1
    • 2
    • 3
  • Stéphanie Delaune
    • 3
  1. 1.LORIA, CNRSNancyFrance
  2. 2.LSV, CNRS and ENS Paris-SaclayCachanFrance
  3. 3.Univ Rennes, CNRS, IRISARennesFrance

Personalised recommendations