A bisimulation for dynamic sealing

Abstract

We define λ_seal, an untyped call-by-value λ-calculus with primitives for protecting abstract data by sealing, and develop a bisimulation proof method that is sound and complete with respect to contextual equivalence. This provides a formal basis for reasoning about data abstraction in open, dynamic settings where static techniques such as type abstraction and logical relations are not applicable.

References

1. Martín Abadi and Cédric Fournet. Mobile values, new names, and secure communication. In Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 104--115, 2001.
2. Martín Abadi and Andrew D. Gordon. A bisimulation method for cryptographic protocols. Nordic Journal of Computing, 5:267--303, 1998. Preliminary version appeared in Programming Languages and Systems -- ESOP'98, 7th European Symposium on Programming,phLecture Notes in Computer Science, Springer-Verlag, vol. 1381, pages 12--26, 1998.
3. Martín Abadi and Andrew D. Gordon. A calculus for cryptographic protocols: The spi calculus. Information and Computation, 148(1):1--70, 1999. Preliminary version appeared inphProceedings of the 4th ACM Conference on Computer and Communications Security, pp. 36--47, 1997.
4. Samson Abramsky. The lazy lambda calculus. In David A. Turner, editor, Research Topics in Functional Programming, pages 65--117. Addison Wesley, 1990.
5. Michele Boreale, Rocco De Nicola, and Rosario Pugliese. Proof techniques for cryptographic processes. SIAM Journal on Computing, 31(3):947--986, 2002. Preliminary version appeared in 14th Annual IEEE Symposium on Logic in Computer Science, pp. 157--166, 1999.
6. Johannes Borgström and Uwe Nestmann. On bisimulations for the spi calculus. In 9th International Conference on Algebraic Methodology and Software Technology, volume 2422 of Lecture Notes in Computer Science, pages 287--303. Springer-Verlag, 2002.
7. Derek Dreyer, Karl Crary, and Robert Harper. A type system for higher-order modules. In Proceedings of the 30th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 236--249, 2003.
8. Dan Grossman, Greg Morrisett, and Steve Zdancewic. Syntactic type abstraction. ACM Transactions on Programming Languages and Systems, 22(6):1037--1080, 2000.
9. Douglas J. Howe. Proving congruence of bisimulation in functional programming languages. Information and Computation, 124(2), 1996.
10. Alan Jeffrey and Julian Rathke. Towards a theory of bisimulation for local names. In 14th Annual IEEE Symposium on Logic in Computer Science, pages 56--66, 1999.
11. Alan Jeffrey and Julian Rathke. A theory of bisimulation for a fragment of concurrent ML with local names. Theoretical Computer Science, 2003. To appear. An extended abstract appeared inph15th Annual IEEE Symposium on Logic in Computer Science, pp. 311--321, 2000.
12. James J. Leifer, Gilles Peskine, Peter Sewell, and Keith Wansbrough. Global abstraction-safe marshalling with hash types. In Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, pages 87--98, 2003.
13. Barbara Liskov. A history of CLU. In The Second ACM SIGPLAN Conference on History of Programming Languages, pages 133--147, 1993.
14. Gavin Lowe. An attack on the Needham-Schroeder public-key authentication protocol. Information Processing Letters, 56(3):131--133, 1995.
15. John C. Mitchell. On the equivalence of data representations. In Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, pages 305--330. Academic Press, 1991.
16. John C. Mitchell and Gordon D. Plotkin. Abstract types have existential types. ACM Transactions on Programming Languages and Systems, 10(3):470--502, 1988. Preliminary version appeared in Proceedings of the 12th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pages 37--51, 1985.
17. James H. Morris Jr. Lambda-Calculus Models of Programming Languages. PhD thesis, Massachusetts Institute of Technology, 1968.
18. James H. Morris Jr. Protection in programming languages. Communications of the ACM, 16(1):15--21, 1973.
19. James H. Morris Jr. Types are not sets. In Proceedings of the 1st Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pages 120--124, 1973.
20. Roger Needham and Michael Schroeder. Using encryption for authentication in large networks of computers. Communications of the ACM, 21(12):993--999, 1978.
21. Benjamin Pierce and Eijiro Sumii. Relating cryptography and polymorphism, 2000. Manuscript. http://www.yl.is.s.u-tokyo.ac.jp/~sumii/pub/.
22. Andrew M. Pitts. Existential types: Logical relations and operational equivalence. In Proceedings of the 25th International Colloquium on Automata, Languages and Programming, volume 1443 of Lecture Notes in Computer Science, pages 309--326. Springer-Verlag, 1998.
23. Andrew M. Pitts. Parametric polymorphism and operational equivalence. Mathematical Structures in Computer Science, 10:321--359, 2000. Preliminary version appeared in HOOTS II Second Workshop on Higher-Order Operational Techniques in Semantics, Electronic Notes in Theoretical Computer Science, vol. 10, 1998.
24. Andrew M. Pitts and Ian Stark. Observable properties of higher order functions that dynamically create local names, or: what's new? In Mathematical Foundations of Computer Science, volume 711 of Lecture Notes in Computer Science, pages 122--141. Springer-Verlag, 1993.
25. John C. Reynolds. Types, abstraction and parametric polymorphism. In Information Processing 83, Proceedings of the IFIP 9th World Computer Congres, pages 513--523, 1983.
26. Andreas Rossberg. Generativity and dynamic opacity for abstract types. In Proceedings of the 5th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, pages 241--252, 2003.
27. Davide Sangiorgi and Robin Milner. The problem of "weak bisimulation up to". In CONCUR '92, Third International Conference on Concurrency Theory, volume 630 of Lecture Notes in Computer Science, pages 32--46. Springer-Verlag, 1992.
28. Peter Sewell. Modules, abstract types, and distributed versioning. In Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 236--247, 2001.
29. Ian Stark. Names and Higher-Order Functions. PhD thesis, University of Cambridge, 1994. http://www.dcs.ed.ac.uk/home/stark/publications/thesis.html.
30. Eijiro Sumii and Benjamin C. Pierce. Logical relations for encryption. In 14th IEEE Computer Security Foundations Workshop, pages 256--269, 2001. Long version to appear in the Journal of Computer Security.
31. Eijiro Sumii and Benjamin C. Pierce. A bisimulation for dynamic sealing. http://www.cis.upenn.edu/~sumii/, 2003.
32. Steve Zdancewic, Dan Grossman, and Greg Morrisett. Principals in programming languages: A syntactic proof technique. In Proceedings of the Fourth ACM SIGPLAN International Conference on Functional Programming, pages 197--207, 1999.

Index Terms

• Information systems

  • Data management systems

    • Data structures

      • Data layout

        • Data encryption

• Networks

  • Network protocols

    • Protocol correctness

      • Protocol testing and verification

• Security and privacy

  • Cryptography

• Software and its engineering

  • Software notations and tools

    • Formal language definitions

    • General programming languages

      • Language features

        • Abstract data types

• Theory of computation

  • Computational complexity and cryptography

  • Formal languages and automata theory

  • Logic

  • Semantics and reasoning