Skip to main content
SpringerLink
Log in

A Type System for Computationally Secure Information Flow

  • Conference paper
Fundamentals of Computation Theory (FCT 2005)

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

Included in the following conference series:

Abstract

The paper presents a novel type system for checking the security of information flow in programs containing operations of symmetric encryption. The type system is correct with respect to the complexity-theoretic security definitions of the encryption primitive.

Partially supported by Estonian Science Foundation, grant #6095.

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.: Secrecy by Typing in Security Protocols. Journal of the ACM 46, 749–786 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  2. Abadi, M., Blanchet, B.: Secrecy types for asymmetric communication. Theoretical Computer Science 298, 387–415 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  3. Abadi, M., Gordon, A.: A Calculus for Cryptographic Protocols: The Spi Calculus. Information and Computation 148, 1–70 (1999)

    Article  MATH  MathSciNet  Google Scholar 

  4. 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)

    Google Scholar 

  5. 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)

    Google Scholar 

  6. Backes, M., Pfitzmann, B.: Symmetric Encryption in a Simulatable Dolev-Yao Style Cryptographic Library. In: Proc. of CSFW 2004, pp. 204–218 (2004)

    Google Scholar 

  7. Canetti, R.: Universally Composable Security: A New Paradigm for Cryptographic Protocols. In: Proc. of FOCS 2001, pp. 136–145 (2001)

    Google Scholar 

  8. Denning, D.: A Lattice Model of Secure Information Flow. Communications of the ACM 19, 236–243 (1976)

    Article  MATH  MathSciNet  Google Scholar 

  9. Denning, D., Denning, P.: Certification of Programs for Secure Information Flow. Communications of the ACM 20, 504–513 (1977)

    Article  MATH  Google Scholar 

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

    Google Scholar 

  11. Laud, P.: Semantics and Program Analysis of Computationally Secure Information Flow. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, pp. 77–91. Springer, Heidelberg (2001)

    Google Scholar 

  12. Laud, P.: Encryption Cycles and Two Views of Cryptography. In: Proc. of Nordsec 2002, pp. 85–100 (2002)

    Google Scholar 

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

    Google Scholar 

  14. Laud, P., Vene, V.: A Type System for Computationally Secure Information Flow. Tech. Report IT-LU-O-043-050307, Cybernetica AS, March 7th (2005)

    Google Scholar 

  15. Lincoln, P., Mitchell, J., Mitchell, M., Scedrov, A.: A Probabilistic Poly-Time Framework for Protocol Analysis. In: Proc. of ACM CCS 1998, pp. 112–121 (1998)

    Google Scholar 

  16. Lincoln, P., Mitchell, J., Mitchell, M., Scedrov, A.: Probabilistic Polynomial-Time Equivalence and Security Analysis. In: Wing, J.M., Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 776–793. Springer, Heidelberg (1999)

    Google Scholar 

  17. Lindholm, T., Yellin, F.: The Java Virtual Machine Specification. Addison-Wesley, Reading (1999)

    Google Scholar 

  18. Myers, A.C.: JFlow: Practical Mostly-Static Information Flow Control. In: Proc. of POPL 1999, pp. 228–241 (1999)

    Google Scholar 

  19. Sabelfeld, A., Myers, A.C.: Language-Based Information-Flow Security. IEEE Journal on Selected Areas in Communications 21, 5–19 (2003)

    Article  Google Scholar 

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

    Google Scholar 

  21. Smith, G., Volpano, D.: Secure Information Flow in a Multi-threaded Imperative Language. In: Proc. of POPL 1998, pp. 355–364 (1998)

    Google Scholar 

  22. Volpano, D.: Secure Introduction of One-way Functions. In: Proc. of CSFW 2000, pp. 246–254 (2000)

    Google Scholar 

  23. Volpano, D., Smith, G., Irvine, C.: A Sound Type System for Secure Flow Analysis. Journal of Computer Security 4, 167–187 (1996)

    Google Scholar 

  24. Volpano, D.M., Smith, G.: Eliminating Covert Flows with Minimum Typings. In: Proc. of CSFW 1997, pp. 156–169 (1997)

    Google Scholar 

  25. Volpano, D., Smith, G.: Probabilistic Noninterference in a Concurrent Language. In: Proc. of CSFW 1998, pp. 34–43 (1998)

    Google Scholar 

  26. Volpano, D., Smith, G.: Verifying Secrets and Relative Secrecy. In: Proc. of POPL 2000, pp. 268–276 (2000)

    Google Scholar 

  27. Yao, A.: Theory and applications of trapdoor functions (extended abstract). In: Proc. of FOCS 1982, pp. 80–91 (1982)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Tartu University,  

    Peeter Laud & Varmo Vene

Authors
  1. Peeter Laud
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Varmo Vene
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institut für Theoretische Informatik, Universität zu Lübeck, Germany

    Maciej Liśkiewicz

  2. Institut für Theoretische Informatik, Universität zu Lübeck, Ratzeburger Allee 160, 23538, Lübeck, Germany

    Rüdiger Reischuk

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Laud, P., Vene, V. (2005). A Type System for Computationally Secure Information Flow. In: Liśkiewicz, M., Reischuk, R. (eds) Fundamentals of Computation Theory. FCT 2005. Lecture Notes in Computer Science, vol 3623. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11537311_32

Download citation

  • DOI: https://doi.org/10.1007/11537311_32

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-28193-1

  • Online ISBN: 978-3-540-31873-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation