Using contextual equivalence (a.k.a. observational equivalence) to specify security properties is an important idea in the field of formal verification of cryptographic protocols. While contextual equivalence is difficult to prove in general, in typed lambda calculi, one is usually able to deduce it using so-called logical relations.
We apply this technique on the cryptographic metalanguage, an extension of Moggi's computational lambda calculus. To explore the difficult aspect of dynamic key generation, we use Stark's name creation monad. The general construction of logical relations for monadic types (by Goubault-Larrecq et al.) then allows us to derive logical relations on Stark's semantic model.
This study also leads us to an exploration of what should be the right definition of contextual equivalence for cryptographic protocols. We argue that contextual equivalence defined over Stark's model cannot represent honestly the power of contexts or attackers. Actually, although Stark's category is a perfectly adequate model of dynamic key generation, it lacks in some aspects when we study relations between programs in the metalanguage. We then propose a refined category for studying contextual equivalence and defining logical relations in the cryptographic metalanguage. We show that the cryptographic logical relation derived over this category is sound, and complete for a certain subset of types up to first order. We explore questions of decidability of cryptographic logical relations relating two given terms in certain cases.
We then extend our soundness and completeness results at all higher-order types, which requires us to switch from logical relations to lax logical relations. We define logical relations which are lax at function types but strict (non-lax) at various other types, and show that they are sound and complete for contextual equivalence at all types.
The thesis from where this work is taken can be found there.