Cryptographic logical relations
--- What is the contextual equivalence for cryptographic protocols
and how to prove it?

  • This thesis was done under the direction of David Nowak and Jean Goubault-Larrecq, in the framework of the SECSI project.

  • Rapporteurs: Pierre-Louis Curien and Martin Hyland.

  • The draft of my thesis is available in PS and PDF.


    ABSTRACT:

    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 model SetI.

    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 SetI 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 SetI→, 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 SetPI→. We find the proper notion of contextual equivalence based on this category.

    Next, we show that the cryptographic logical relation defined on SetPI→ 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. This requires us to shift from logical relations to lax logical relations, still on the category SetPI→. We then 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 was defended on October 21, 2005, before the jury: