Cryptographic logical relations

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 directly, one is usually able to deduce it using the so-called logical relations in typed λ-calculi. We apply this technique to the cryptographic metalanguage—an extension of Moggi’s computational λ-calculus, where we use Stark’s model for name creation to explore the difficult aspect of dynamic key generation. The categorical construction of logical relations for monadic types (by Goubault-Larrecq et al.) then allows us to derive logical relations over the category SetI. Although SetI is a perfectly adequate model of dynamic key generation, it lacks in some aspects when we study relations between programs in the metalanguage. This leads us to an interesting exploration of what should be the proper category to consider. We show that, to define logical relations in the cryptographic metalanguage, a better choice of category is SetI→ that we proposed in [Y. Zhang, D. Nowak, Logical relations for dynamic name creation, in: Proceedings of the 17th International Workshop of Computer Science Logic and the 8th Kurt Gödel Colloqium, CSL & KGL, in: Lecture Notes in Computer Science, vol. 2803, Springer-Verlag, 2003, pp. 575–588]. However, this category is still lacking in some subtler aspects and we propose a refined category SetPI→ to fix the flaws, but our final choice is SetI×I, which is equivalent to SetPI→. We define the contextual equivalence based on SetI×I and show that the cryptographic logical relation derived over SetI×I is sound and can be used to verify protocols in practice.