Document Open Access Logo

Partial Order Reduction for Security Protocols

Authors David Baelde, Stéphanie Delaune, Lucca Hirschi

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2015.497.pdf
  • Filesize: 0.6 MB
  • 14 pages

Document Identifiers

Author Details

David Baelde
Stéphanie Delaune
Lucca Hirschi

Cite As Get BibTex

David Baelde, Stéphanie Delaune, and Lucca Hirschi. Partial Order Reduction for Security Protocols. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 497-510, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.CONCUR.2015.497

Abstract

Security protocols are concurrent processes that communicate using cryptography with the aim of achieving various security properties. Recent work on their formal verification has brought procedures and tools for deciding trace equivalence properties (e.g. anonymity, unlinkability, vote secrecy) for a bounded number of sessions. However, these procedures are based on a naive symbolic exploration of all traces of the considered processes which, unsurprisingly, greatly limits the scalability and practical impact of the verification tools.
 
In this paper, we mitigate this difficulty by developing partial order reduction techniques for the verification of security protocols. We provide reduced transition systems that optimally eliminate redundant traces, and which are adequate for model-checking trace equivalence properties of protocols by means of symbolic execution. We have implemented our reductions in the tool Apte, and demonstrated that it achieves the expected speedup on various protocols.

Subject Classification

Keywords
  • Cryptographic protocols
  • verification
  • process algebra
  • trace equivalence

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. M. Abadi and C. Fournet. Mobile values, new names, and secure communication. In Proceedings of POPL'01. ACM Press, 2001. Google Scholar
  2. J.-M. Andreoli. Logic programming with focusing proofs in linear logic. J. Log. Comput., 2(3), 1992. Google Scholar
  3. A.V. Anisimov and D.E. Knuth. Inhomogeneous sorting. International Journal of Computer & Information Sciences, 8(4):255-260, 1979. Google Scholar
  4. D. Baelde, S. Delaune, and L. Hirschi. A reduced semantics for deciding trace equivalence using constraint systems. In Proc. of POST'14. Springer, 2014. Google Scholar
  5. David Baelde, Stéphanie Delaune, and Lucca Hirschi. Partial order reduction for security protocols. CoRR, abs/1504.04768, 2015. Google Scholar
  6. C. Baier and J.-P. Katoen. Principles of Model Checking (Representation and Mind Series). The MIT Press, 2008. Google Scholar
  7. Mayla Bruso, K. Chatzikokolakis, and J. den Hartog. Formal verification of privacy for RFID systems. In Proc. of CSF'10, 2010. Google Scholar
  8. V. Cheval. Apte: an algorithm for proving trace equivalence. In Proc. TACAS'14, 2014. Google Scholar
  9. V. Cheval, H. Comon-Lundh, and S. Delaune. Trace equivalence decision: Negative tests and non-determinism. In Proc. of CCS'11. ACM Press, 2011. Google Scholar
  10. V. Cheval and L. Hirschi. sources of APTE, 2015. URL: https://github.com/APTE/APTE.
  11. E. Clarke, S. Jha, and W. Marrero. Efficient verification of security protocols using partial-order reductions. Int. Journal on Software Tools for Technology Transfer, 4(2), 2003. Google Scholar
  12. H. Comon-Lundh, V. Cortier, and E. Zalinescu. Deciding security properties for cryptographic protocols. Application to key cycles. ACM Transactions on Computational Logic (TOCL), 11(4), 2010. Google Scholar
  13. Cas JF Cremers and Sjouke Mauw. Checking secrecy by means of partial order reduction. In System Analysis and Modeling. Springer, 2005. Google Scholar
  14. Pierpaolo Degano, Rocco De Nicola, and Ugo Montanari. A partial ordering semantics for ccs. Theoretical Computer Science, 75(3):223-262, 1990. Google Scholar
  15. S. Delaune, S. Kremer, and M. Ryan. Verifying privacy-type properties of electronic voting protocols: A taster. In Towards Trustworthy Elections - New Directions in Electronic Voting, volume 6000. Springer, 2010. Google Scholar
  16. Patrice Godefroid. Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem, volume 1032 of Lecture Notes in Computer Science. Springer, 1996. Google Scholar
  17. L. Hirschi. APTE with POR. URL: http://www.lsv.ens-cachan.fr/~hirschi/apte_por.
  18. J. Millen and V. Shmatikov. Constraint solving for bounded-process cryptographic protocol analysis. In Proceedings of CCS'01. ACM Press, 2001. Google Scholar
  19. D. Miller and A. Saurin. From proofs to focused proofs: A modular proof of focalization in linear logic. In Proc. of CSL'07, volume 4646. Springer, 2007. Google Scholar
  20. S. Mödersheim, L. Viganò, and D. Basin. Constraint differentiation: Search-space reduction for the constraint-based analysis of security protocols. JCS, 18(4), 2010. Google Scholar
  21. D. Peled. Ten years of partial order reduction. In Proc. of CAV'98. Springer, 1998. Google Scholar
  22. A. Tiu. Spec: http://users.cecs.anu.edu.au/~tiu/spec/, 2010.
  23. A. Tiu and J. E. Dawson. Automating open bisimulation checking for the spi calculus. In Proc. of CSF'10. IEEE Comp. Soc. Press, 2010. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact