Skip to main content
SpringerLink
Log in

Automating Security Analysis: Symbolic Equivalence of Constraint Systems

  • Conference paper
  • First Online:
Automated Reasoning (IJCAR 2010)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 6173))

Included in the following conference series:

Abstract

We consider security properties of cryptographic protocols, that are either trace properties (such as confidentiality or authenticity) or equivalence properties (such as anonymity or strong secrecy).

Infinite sets of possible traces are symbolically represented using deducibility constraints. We give a new algorithm that decides the trace equivalence for the traces that are represented using such constraints, in the case of signatures, symmetric and asymmetric encryptions. Our algorithm is implemented and performs well on typical benchmarks. This is the first implemented algorithm, deciding symbolic trace equivalence.

This work has been partially supported by the ANR project SeSur AVOTÉ.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abadi, M., Cortier, V.: Deciding knowledge in security protocols under equational theories. Theoretical Computer Science 367(1-2), 2–32 (2006)

    Article  MathSciNet  Google Scholar 

  2. Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Proc. of 28th ACM Symposium on Principles of Programming Languages, POPL’01 (2001)

    Google Scholar 

  3. Baudet, M.: Deciding security of protocols against off-line guessing attacks. In: Proc. of 12th ACM Conference on Computer and Communications Security (2005)

    Google Scholar 

  4. Baudet, M.: YAPA, Yet Another Protocol Analyzer (2008), http://www.lsv.ens-cachan.fr/~baudet/yapa/index.html

  5. Baudet, M., Cortier, V., Delaune, S.: YAPA: A generic tool for computing intruder knowledge. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 148–163. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  6. Blanchet, B.: An automatic security protocol verifier based on resolution theorem proving (invited tutorial). In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, Springer, Heidelberg (2005)

    Google Scholar 

  7. Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. Journal of Logic and Algebraic Programming 75(1), 3–51 (2008)

    Article  MathSciNet  Google Scholar 

  8. Cheval, V., Comon-Lundh, H., Delaune, S.: Automating security analysis: symbolic equivalence of constraint systems. Technical report (2010), http://www.lsv.ens-cachan.fr/~cheval/programs/technical-report_OnlinePDF.pdf

  9. Chevalier, Y., Rusinowitch, M.: Decidability of symbolic equivalence of derivations (unpublished draft) (2009)

    Google Scholar 

  10. Ciobâcă, Ş.: Kiss (2009), http://www.lsv.ens-cachan.fr/~ciobaca/kiss

  11. Comon-Lundh, H.: Challenges in the automated verification of security protocols. In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 396–409. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  12. Comon-Lundh, H., Cortier, V., Zalinescu, E.: Deciding security properties of cryptographic protocols. application to key cycles. Transaction on Computational Logic 11(2) (2010)

    Google Scholar 

  13. Corin, R., Doumen, J., Etalle, S.: Analysing password protocol security against off-line dictionary attacks. Electr. Notes Theor. Comput. Sci. 121, 47–63 (2005)

    Article  Google Scholar 

  14. Cortier, V., Delaune, S.: A method for proving observational equivalence. In: Proc. of 22nd Computer Security Foundations Symposium (CSF’09), pp. 266–276. IEEE Comp. Soc. Press, Los Alamitos (2009)

    Google Scholar 

  15. Delaune, S., Kremer, S., Ryan, M.D.: Verifying privacy-type properties of electronic voting protocols. Journal of Computer Security 17(4), 435–487 (2009)

    Article  Google Scholar 

  16. Fendrup, U., Hüttel, H., Jensen, J.N.: Modal logics for cryptographic processes. Theoretical Computer Science 68 (2002)

    Google Scholar 

  17. Huttel, H.: Deciding framed bisimulation. In: 4th International Workshop on Verification of Infinite State Systems, INFINITY’02, pp. 1–20 (2002)

    Google Scholar 

  18. Meadows, C.: The NRL protocol analyzer: An overview. Journal of Logic Programming 26(2), 113–131 (1996)

    Article  MathSciNet  Google Scholar 

  19. Millen, J., Shmatikov, V.: Constraint solving for bounded-process cryptographic protocol analysis. In: Proc. of 8th ACM Conference on Computer and Communications Security (2001)

    Google Scholar 

  20. Rusinowitch, M., Turuani, M.: Protocol insecurity with finite number of sessions is np-complete. In: Proc. of 14th Computer Security Foundations Workshop (2001)

    Google Scholar 

  21. Weidenbach, C.: Towards an automatic analysis of security protocols in first-order logic. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 314–328. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LSV, ENS Cachan & CNRS & INRIA Saclay Île-de-France, France

    Vincent Cheval, Hubert Comon-Lundh & Stéphanie Delaune

Authors
  1. Vincent Cheval
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Hubert Comon-Lundh
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Stéphanie Delaune
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. RWTH Aachen, LuFG Informatik, 2, Ahornstr. 55, 52074, Aachen, Germany

    Jürgen Giesl

  2. Department of Computer Science, Chalmers University of Technology, 41296, Gothenburg, Sweden

    Reiner Hähnle

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Cheval, V., Comon-Lundh, H., Delaune, S. (2010). Automating Security Analysis: Symbolic Equivalence of Constraint Systems. In: Giesl, J., Hähnle, R. (eds) Automated Reasoning. IJCAR 2010. Lecture Notes in Computer Science(), vol 6173. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14203-1_35

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-14203-1_35

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-14202-4

  • Online ISBN: 978-3-642-14203-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation