[7-18]Cryptographic logical relations

Date:2008-07-15

Title：Cryptographic logical relations
Speaker：Dr. Yu ZHANG（MACAU University of Science and Technology）
Time：3:00 pm, Jul. 18
Venue：Lecture room of SKLCS

Abstract：

Formal verification of cryptographic protocols has been a very active research field for over a decade and it has been well accepted that many security properties, e.g., the secrecy property, can be formalized using the notion of contextual equivalence (a.k.a. observational equivalence) of programs. In typed lambda-calculi, contextual equivalence can usually be proved through a technique called logical relations. However, applying logical relations in the setting of protocol verification is not straightforward. We have in particular concentrated on the dynamic key (nonce) generation, which plays an important role in protocols but is unfortunately detoured by informal conventions in most models. Our work is based on the general model of deriving logical relations for monadic types (by Goubault-Larrecq et al.) and we propose a new categorical model Set^{PI->} based on Stark’s name creation monad. We argue that this should be the right category for defining cryptographic logical relations. Interestingly, this research also leads us to an exploration of what should be the correct definition of contextual equivalence in the framework. We finally arrive at a definition also based on the new category, where represent faithfully the capability of adversaries, and we prove that our cryptographic logical relations are sound w.r.t. the contextual equivalence. The approach is applied to proving the correctness of the Needham-Schroeder-Lowe protocol in the Dolev-Yao model.