Complete Lax Logical Relations for Cryptographic Lambda-Calculi

Abstract Security properties are profitably expressed using notions of contextual equivalence, and logical relations are a powerful proof technique to establish contextual equivalence in typed lambda calculi, see e. g. Sumii and Pierce’s logical relation for a cryptographic lambda-calculus. We clarify Sumii and Pierce’s approach, showing that the right tool is prelogical relations, or lax logical relations in general: relations should be lax at encryption types, notably. To explore the difficult aspect of fresh name creation, we use Moggi’s monadic lambda-calculus with constants for cryptographic primitives, and Stark’s name creation monad. We define logical relations which are lax at encryption and function types but strict (non-lax) at various other types, and show that they are sound and complete for contextual equivalence at all types.

Authors

• Jean Goubault-Larrecq
• Slawomir Lasota 0001
• David Nowak
• Yu Zhang

Keywords

No keywords are indexed for this paper.