POR for Security Protocol Equivalences

Beyond Action-Determinism
  • David Baelde
  • Stéphanie DelauneEmail author
  • Lucca Hirschi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11098)


Formal methods have proved effective to automatically analyse protocols. Recently, much research has focused on verifying trace equivalence on protocols, which is notably used to model interesting privacy properties such as anonymity or unlinkability. Several tools for checking trace equivalence rely on a naive and expensive exploration of all interleavings of concurrent actions, which calls for partial-order reduction (POR) techniques. In this paper, we present the first POR technique for protocol equivalences that does not rely on an action-determinism assumption: we recast trace equivalence as a reachability problem, to which persistent and sleep set techniques can be applied, and we show how to effectively apply these results in the context of symbolic execution. We report on a prototype implementation, improving the tool DeepSec.


  1. 1.
    Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Proceedings of the 28th Symposium on Principles of Programming Languages (POPL 2001), pp. 104–115. ACM Press (2001)Google Scholar
  2. 2.
    Abadi, M., Fournet, C.: Private authentication. Theor. Comput. Sci. 322(3), 427–476 (2004)MathSciNetCrossRefGoogle Scholar
  3. 3.
    Abdulla, P., Aronis, S., Jonsson, B., Sagonas, K.: Optimal dynamic partial order reduction. ACM SIGPLAN Not. 49(1), 373–384 (2014)zbMATHGoogle Scholar
  4. 4.
    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
  5. 5.
    Armando, A., Carbone, R., Compagna, L., Cuellar, J., Abad, L.T.: Formal analysis of SAML 2.0 web browser single sign-on: breaking the SAML-based single sign-on for Google apps. In: Proceedings of the 6th ACM Workshop on Formal Methods in Security Engineering (FMSE 2008), pp. 1–10 (2008)Google Scholar
  6. 6.
    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). Scholar
  7. 7.
    Baelde, D., Delaune, S., Hirschi, L.: Porridge, an OCaml library implementing POR techniques for checking trace equivalence of security protocols.
  8. 8.
    Baelde, D., Delaune, S., Hirschi, L.: Partial order reduction for security protocols. In: Proceedings of the 26th International Conference on Concurrency Theory (CONCUR 2015). LIPIcs, Madrid, Spain, vol. 42, pp. 497–510. Leibniz-Zentrum für Informatik (2015)Google Scholar
  9. 9.
    Baelde, D., Delaune, S., Hirschi, L.: A reduced semantics for deciding trace equivalence. Log. Methods Comput. Sci. 13(2:8), 1–48 (2017)MathSciNetzbMATHGoogle Scholar
  10. 10.
    Baelde, D., Delaune, S., Hirschi, L.: POR for security protocols equivalences: beyond action-determinism. Technical report (2018).
  11. 11.
    Baier, C., Katoen, J.-P.: Principles of Model Checking (Representation and Mind Series). The MIT Press, Cambridge (2008)zbMATHGoogle Scholar
  12. 12.
    Baldoni, R., Coppa, E., D’Elia, D.C., Demetrescu, C., Finocchi, I.: A survey of symbolic execution techniques. ACM Comput. Surv. 51(3), 50:1–50:39 (2018). ISSN 0360-0300CrossRefGoogle Scholar
  13. 13.
    Basin, D., Cremers, C., Meier, S.: Provably repairing the ISO/IEC 9798 standard for entity authentication. J. Comput. Secur. 21(6), 817–846 (2013)CrossRefGoogle Scholar
  14. 14.
    Basin, D., Dreier, J., Sasse, R.: Automated symbolic proofs of observational equivalence. In: Proceedings of the 22nd ACM Conference on Computer and Communications Security (CCS 2015), pp. 1144–1155. ACM (2015)Google Scholar
  15. 15.
    Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: Proceedings of the 14th Computer Security Foundations Workshop (CSFW 2001), pp. 82–96. IEEE Computer Society Press (2001)Google Scholar
  16. 16.
    Bruso, M., Chatzikokolakis, K., den Hartog, J.: Formal verification of privacy for RFID systems. In: Proceedings of the 23rd IEEE Computer Security Foundations Symposium (CSF 2010). IEEE Computer Society Press (2010)Google Scholar
  17. 17.
    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). Scholar
  18. 18.
    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). Scholar
  19. 19.
    Cheval, V., Comon-Lundh, H., Delaune, S.: Trace equivalence decision: negative tests and non-determinism. In: Proceedings of the 18th Conference on Computer and Communications Security (CCS 2011). ACM Press (2011)Google Scholar
  20. 20.
    Cheval, V., Cortier, V., Delaune, S.: Deciding equivalence-based properties using constraint solving. Theor. Comput. Sci. 492, 1–39 (2013)MathSciNetCrossRefGoogle Scholar
  21. 21.
    Cheval, V., Kremer, S., Rakotonirina, I.: DEEPSEC: deciding equivalence properties in security protocols - theory and practice. In: Proceedings of the 39th IEEE Symposium on Security and Privacy (S&P 2018). IEEE Computer Society Press (2018)Google Scholar
  22. 22.
    Clarke, E., Jha, S., Marrero, W.: Partial order reductions for security protocol verification. In: Graf, S., Schwartzbach, M. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 503–518. Springer, Heidelberg (2000). Scholar
  23. 23.
    Cremers, C.J.F., Mauw, S.: Checking secrecy by means of partial order reduction. In: Amyot, D., Williams, A.W. (eds.) SAM 2004. LNCS, vol. 3319, pp. 171–188. Springer, Heidelberg (2005). Scholar
  24. 24.
    Delaune, S., Hirschi, L.: A survey of symbolic methods for establishing equivalence-based properties in cryptographic protocols. J. Log. Algebraic Methods Program. 87, 127–144 (2017)MathSciNetCrossRefGoogle Scholar
  25. 25.
    Delaune, S., Kremer, S., Ryan, M.D.: Verifying privacy-type properties of electronic voting protocols. J. Comput. Secur. 4, 435–487 (2008)zbMATHGoogle Scholar
  26. 26.
    Feldhofer, M., Dominikus, S., Wolkerstorfer, J.: Strong authentication for RFID systems using the AES algorithm. In: Joye, M., Quisquater, J.-J. (eds.) CHES 2004. LNCS, vol. 3156, pp. 357–370. Springer, Heidelberg (2004). Scholar
  27. 27.
    Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. ACM SIGPLAN Not. 40, 110–121 (2005)CrossRefGoogle Scholar
  28. 28.
    Godefroid, P.: Partial-order methods for the verification of concurrent systems. Ph.D. thesis, Université de Liège (1995)Google Scholar
  29. 29.
    Hirschi, L., Baelde, D., Delaune, S.: A method for verifying privacy-type properties: the unbounded case. In: Proceedings of the 37th IEEE Symposium on Security and Privacy (S&P 2016), San Jose, California, USA, pp. 564–581, May 2016Google Scholar
  30. 30.
    Lowe, G.: Breaking and fixing the needham-schroeder public-key protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 147–166. Springer, Heidelberg (1996). 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). Scholar
  32. 32.
    Mödersheim, S., Viganò, L., Basin, D.: Constraint differentiation: search-space reduction for the constraint-based analysis of security protocols. J. Comput. Secur. 18(4), 575–618 (2010)CrossRefGoogle Scholar
  33. 33.
    Peled, D.: Ten years of partial order reduction. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 17–28. Springer, Heidelberg (1998). Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • David Baelde
    • 1
  • Stéphanie Delaune
    • 2
    Email author
  • Lucca Hirschi
    • 3
  1. 1.LSV, ENS Paris-Saclay & CNRS, InriaUniversité Paris-SaclayCachanFrance
  2. 2.Univ Rennes, CNRS, IRISARennesFrance
  3. 3.Department of Computer ScienceETH ZurichZurichSwitzerland

Personalised recommendations