Skip to main content
SpringerLink
Log in

Application of Dependency Graphs to Security Protocol Analysis

  • Conference paper
Trustworthy Global Computing (TGC 2007)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 4912))

Included in the following conference series:

Abstract

We present a computationally sound technique of static analysis for confidentiality in cryptographic protocols. The technique is a combination of the dependency flow graphs presented by Beck and Pingali and our earlier works – we start with the protocol representation as a dependency graph indicating possible flows of data in all possible runs of the protocol and replace the cryptographic operations with constructions which are “obviously secure”. Transformations are made in such a way that the semantics of the resulting graph remains computationally indistinguishable from the semantics of the original graph. The transformed graphs are analysed again; the transformations are applied until no more transformations are possible. A protocol is deemed secure if its transformed version is secure; the transformed versions are amenable to a very simple security analysis. The framework is well-suited for producing fully automated (with zero user input) proofs for protocol security.

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 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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., Rogaway, P.: Reconciling Two Views of Cryptography (The Computational Soundness of Formal Encryption). In: Watanabe, O., Hagiya, M., Ito, T., van Leeuwen, J., Mosses, P.D. (eds.) TCS 2000. LNCS, vol. 1872, pp. 3–22. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  2. Abadi, M., Jürjens, J.: Formal Eavesdropping and its Computational Interpretation. In: Kobayashi, N., Pierce, B.C. (eds.) TACS 2001. LNCS, vol. 2215, pp. 82–94. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  3. Adão, P., Bana, G., Herzog, J., Scedrov, A.: Soundness of formal encryption in the presence of key-cycles. In: di Vimercati, S.d.C., Syverson, P.F., Gollmann, D. (eds.) ESORICS 2005. LNCS, vol. 3679, pp. 374–396. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  4. Backes, M., Pfitzmann, B., Waidner, M.: A Composable Cryptographic Library with Nested Operations. In: 10th ACM Conference on Computer and Communications Security (CCS 2003), October 2003, pp. 220–230 (2003)

    Google Scholar 

  5. Backes, M., Laud, P.: Computationally Sound Secrecy Proofs by Mechanized Flow Analysis. In: 13th ACM Conference on Computer and Communications Security (CCS 2006), pp. 370–379 (2006)

    Google Scholar 

  6. Bellare, M., Desai, A., Pointcheval, D., Rogaway, P.: Relations among Notions of Security for Public-Key Encryption Schemes. In: Krawczyk, H. (ed.) CRYPTO 1998. LNCS, vol. 1462, pp. 26–45. Springer, Heidelberg (1998)

    Google Scholar 

  7. Bellare, M., Namprempre, C.: Authenticated Encryption: Relations among notions and analysis of the generic composition paradigm. In: Okamoto, T. (ed.) ASIACRYPT 2000. LNCS, vol. 1976, pp. 531–545. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  8. Bellare, M., Rogaway, P.: The Security of Triple Encryption and a Framework for Code-Based Game-Playing Proofs. In: Vaudenay, S. (ed.) EUROCRYPT 2006. LNCS, vol. 4004, pp. 409–426. Springer, Heidelberg (2006), http://eprint.iacr.org

    Chapter  Google Scholar 

  9. Blanchet, B.: A computationally sound mechanized prover for security protocols. In: Proc. 27th IEEE Symposium on Security & Privacy (2006)

    Google Scholar 

  10. Blanchet, B., Pointcheval, D.: Automated Security Proofs with Sequences of Games. In: Dwork, C. (ed.) CRYPTO 2006. LNCS, vol. 4117, pp. 537–554. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  11. Blanchet, B.: Computationally Sound Mechanized Proofs of Correspondence Assertions. In: Proc. 20th IEEE Computer Security Foundations Symposium (2007)

    Google Scholar 

  12. Canetti, R.: Universally Composable Security: A New Paradigm for Cryptographic Protocols. In: 42nd Annual Symposium on Foundations of Computer Science (FOCS 2001), October 2001, pp. 136–145 (2001)

    Google Scholar 

  13. Cortier, V., Warinschi, B.: Computationally Sound, Automated Proofs for Security Protocols. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 157–171. Springer, Heidelberg (2005)

    Google Scholar 

  14. Cramer, R., Gennaro, R., Schoenmakers, B.: A Secure and Optimally Efficient Multi-Authority Election Scheme. In: Fumy, W. (ed.) EUROCRYPT 1997. LNCS, vol. 1233, pp. 103–118. Springer, Heidelberg (1997)

    Google Scholar 

  15. Dolev, D., Yao, A.C.: On the security of public key protocols. IEEE Transactions on Information Theory IT-29(12), 198–208 (1983)

    Article  MathSciNet  Google Scholar 

  16. Joshua, D., Guttman, F.: Javier Thayer, and Lenore D. Zuck. The Faithfulness of Abstract Protocol Analysis: Message Authentication. In: 8th ACM Conference on Computer and Communications Security (CCS 2001), November 2001, pp. 186–195 (2001)

    Google Scholar 

  17. Laud, P.: Handling Encryption in Analysis for Secure Information Flow. In: Degano, P. (ed.) ESOP 2003. LNCS, vol. 2618, pp. 159–173. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  18. Laud, P.: Symmetric encryption in automatic analyses for confidentiality against active adversaries. In: 2004 IEEE Symposium on Security and Privacy, May 2004, pp. 71–85 (2004)

    Google Scholar 

  19. Laud, P.: Secrecy Types for a Simulatable Cryptographic Library. In: 12th ACM Conference on Computer and Communications Security (CCS 2005), pp. 26–35 (2005)

    Google Scholar 

  20. Lowe, G.: A Hierarchy of Authentication Specification. In: 10th Computer Security Foundations Workshop, pp. 31–44 (1997)

    Google Scholar 

  21. Janvier, R., Lakhnech, Y., Mazaré, L.: Completing the Picture: Soundness of Formal Encryption in the Presence of Active Adversaries. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 172–185. Springer, Heidelberg (2005)

    Google Scholar 

  22. Micciancio, D., Panjwani, S.: Adaptive Security of Symbolic Encryption. In: Kilian, J. (ed.) TCC 2005. LNCS, vol. 3378, pp. 169–187. Springer, Heidelberg (2005)

    Google Scholar 

  23. Micciancio, D., Warinschi, B.: Completeness Theorems for the Abadi-Rogaway Logic of Encrypted Expressions. In: Workshop in Issues in the Theory of Security (WITS 2002), January 2002 (2002)

    Google Scholar 

  24. Riis Nielson, H., Nielson, F.: Semantics with Applications: A Formal Introduction. Wiley, Chichester (1992)

    MATH  Google Scholar 

  25. Pfitzmann, B., Waidner, M.: A Model for Asynchronous Reactive Systems and its Application to Secure Message Transmission. In: 2001 IEEE Symposium on Security and Privacy (IEEE S&P 2001), pp. 184–200 (2001)

    Google Scholar 

  26. Pingali, K., Beck, M., Johnson, R., Moudgill, M., Stodghill, P.: Dependence Flow Graphs: an Algebraic Approach to Program Dependencies. In: Advances in Languages and Compilers for Parallel Processing, pp. 445–467. MIT Press, Cambridge (1991)

    Google Scholar 

  27. Tšahhirov, I., Laud, P.: Digital Signature in Automatic Analyses for Confidentiality against Active Adversaries. In: Nordsec 2005 10th Nordic Workshop on Secure IT Systems, Tartu, Estonia, October 20-21, 2005, pp. 29–41 (2005)

    Google Scholar 

  28. Yao, A.C.: Theory and Applications of Trapdoor Functions (extended abstract). In: 23rd Annual Symposium on Foundations of Computer Science, November 1982, pp. 80–91 (1982)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Tallinn University of Technology,  

    Ilja Tšahhirov

  2. Tartu University,  

    Peeter Laud

  3. Cybernetica AS,  

    Peeter Laud

Authors
  1. Ilja Tšahhirov
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Peeter Laud
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Gilles Barthe Cédric Fournet

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Tšahhirov, I., Laud, P. (2008). Application of Dependency Graphs to Security Protocol Analysis. In: Barthe, G., Fournet, C. (eds) Trustworthy Global Computing. TGC 2007. Lecture Notes in Computer Science, vol 4912. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78663-4_20

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-78663-4_20

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-78662-7

  • Online ISBN: 978-3-540-78663-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation