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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Abadi, M.: Secrecy by Typing in Security Protocols. Journal of the ACM 46, 749–786 (1999)
Abadi, M., Blanchet, B.: Secrecy types for asymmetric communication. Theoretical Computer Science 298, 387–415 (2003)
Abadi, M., Gordon, A.: A Calculus for Cryptographic Protocols: The Spi Calculus. Information and Computation 148, 1–70 (1999)
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)
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)
Backes, M., Pfitzmann, B.: Symmetric Encryption in a Simulatable Dolev-Yao Style Cryptographic Library. In: Proc. of CSFW 2004, pp. 204–218 (2004)
Canetti, R.: Universally Composable Security: A New Paradigm for Cryptographic Protocols. In: Proc. of FOCS 2001, pp. 136–145 (2001)
Denning, D.: A Lattice Model of Secure Information Flow. Communications of the ACM 19, 236–243 (1976)
Denning, D., Denning, P.: Certification of Programs for Secure Information Flow. Communications of the ACM 20, 504–513 (1977)
Dolev, D., Yao, A.: On the security of public key protocols. IEEE Transactions on Information Theory IT-29, 198–208 (1983)
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)
Laud, P.: Encryption Cycles and Two Views of Cryptography. In: Proc. of Nordsec 2002, pp. 85–100 (2002)
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)
Laud, P., Vene, V.: A Type System for Computationally Secure Information Flow. Tech. Report IT-LU-O-043-050307, Cybernetica AS, March 7th (2005)
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)
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)
Lindholm, T., Yellin, F.: The Java Virtual Machine Specification. Addison-Wesley, Reading (1999)
Myers, A.C.: JFlow: Practical Mostly-Static Information Flow Control. In: Proc. of POPL 1999, pp. 228–241 (1999)
Sabelfeld, A., Myers, A.C.: Language-Based Information-Flow Security. IEEE Journal on Selected Areas in Communications 21, 5–19 (2003)
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)
Smith, G., Volpano, D.: Secure Information Flow in a Multi-threaded Imperative Language. In: Proc. of POPL 1998, pp. 355–364 (1998)
Volpano, D.: Secure Introduction of One-way Functions. In: Proc. of CSFW 2000, pp. 246–254 (2000)
Volpano, D., Smith, G., Irvine, C.: A Sound Type System for Secure Flow Analysis. Journal of Computer Security 4, 167–187 (1996)
Volpano, D.M., Smith, G.: Eliminating Covert Flows with Minimum Typings. In: Proc. of CSFW 1997, pp. 156–169 (1997)
Volpano, D., Smith, G.: Probabilistic Noninterference in a Concurrent Language. In: Proc. of CSFW 1998, pp. 34–43 (1998)
Volpano, D., Smith, G.: Verifying Secrets and Relative Secrecy. In: Proc. of POPL 2000, pp. 268–276 (2000)
Yao, A.: Theory and applications of trapdoor functions (extended abstract). In: Proc. of FOCS 1982, pp. 80–91 (1982)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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)