Information Security Seminar 

18/03/2008, 16:30 — 17:30 — Room P3.10, Mathematics Building
Gergei Bana, Tulane University

Computational Soundness of First-Order-Logic-based SymbolicAnalysis of Cryptographic Protocols

In the past few years it has become a central question of cryptography how relevant purely symbolic analysis of security protocols are to reality. This question can be analyzed by linking the symbolic approach to the so-called computational approach as the latter is a more detailed description of reality, involving probability and complexity theory. Several attempts have been made to link these two approaches. Unfortunately, most of them are not done with sufficient mathematical rigor, and some of the results are questionable. This time, we look at the case when symbolic analysis is done via first order logic. We review some of the basic notions, look at problems with a recent attempt (Computational PCL by Datta et al.) to provide computational semantics to the syntax, and suggest a new way of defining the semantics to avoid those problems, making use of standard notions of the theory of stochastic processes.