A bisimulation for dynamic sealing

DOI10.1016/j.tcs.2006.12.032zbMath1111.68034OpenAlexW2096216741MaRDI QIDQ5899331

Eijiro Sumii, Benjamin C. Pierce

Publication date: 11 May 2007

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2006.12.032

zbMATH Keywords

securitybisimulation\(\lambda\)-calculuscryptographic protocolsencryptioninformation hidingdata abstractioncontextual equivalencedynamic sealing

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Data encryption (aspects in computer science) (68P25)

Related Items (9)

A bisimulation-like proof method for contextual properties in untyped \(\lambda \)-calculus with references and deallocation ⋮ Non-parametric parametricity ⋮ First-order reasoning for higher-order concurrency ⋮ Automated type-based analysis of injective agreement in the presence of compromised principals ⋮ From Applicative to Environmental Bisimulation ⋮ Unnamed Item ⋮ Full Abstraction at Package Boundaries of Object-Oriented Languages ⋮ A Complete Characterization of Observational Equivalence in Polymorphic λ-Calculus with General References ⋮ Unnamed Item

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• An attack on the Needham-Schroeder public-key authentication protocol
• Full abstraction in the lazy lambda calculus
• A calculus for cryptographic protocols: The spi calculus
• A theory of bisimulation for a fragment of concurrent ML with local names
• Proving congruence of bisimulation in functional programming languages
• Proof Techniques for Cryptographic Processes
• Principals in programming languages
• A type system for higher-order modules
• On Bisimulations for the Spi Calculus*
• Using encryption for authentication in large networks of computers
• Parametric polymorphism and operational equivalence
• Mobile values, new names, and secure communication
• Modules, abstract types, and distributed versioning
• Barbed bisimulation
• Global abstraction-safe marshalling with hash types
• A bisimulation for type abstraction and recursion
• Protection in programming languages

This page was built for publication: A bisimulation for dynamic sealing