 What is the contextual equivalence for cryptographic protocols and how to prove it?
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 socalled 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 GoubaultLarrecq et al.) then allows us to derive logical relations on Stark's model Set^{I}. 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 Set^{I} is a perfectly adequate model of dynamic key generation, it lacks in some aspects when we study relations between programs in the metalanguage. We show that, to define contextual equivalence and logical relations in the cryptographic metalanguage, a better choice of category is Set^{I→}, where I^{→} is a category we define. This category is still lacking in some subtler aspects, and we eventually show that the proper category to consider is one called Set^{PI→}. We find the proper notion of contextual equivalence based on this category. Next, we show that the cryptographic logical relation defined on Set^{PI→} 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 higherorder types. This requires us to shift from logical relations to lax logical relations, still on the category Set^{PI→}. We then define logical relations which are lax at function types but strict (nonlax) at various other types, and show that they are sound and complete for contextual equivalence at all types.
