Information Security Seminar 

18/01/2013, 16:15 — 17:15 — Room P3.10, Mathematics Building
Bruno Montalto, ETH Zurich

Symbolic Probabilistic Analysis of Off-line Guessing

Much work has been devoted to strengthening the guarantees provided by symbolic methods for protocol analysis, either by automatically obtaining proofs of computational security or by proving that security with respect to a symbolic model implies computational security. These results require strong assumptions on the security of the cryptographic primitives used. Such assumptions are often not verified by real-world implementations.

In this talk we present a fundamentally new approach to this problem. We introduce a symbolic framework for the analysis of protocol security against a stronger attacker than that considered in existing symbolic methods.

We provide a general method for expressing properties of cryptographic primitives. It allows modeling, for instance, message redundancy, weak random generation algorithms, or the leakage of partial information about a plaintext by an encryption scheme. These properties can be used to automatically find attacks and estimate their success probability. Under assumptions about the accuracy of the properties considered, we show that our estimates differ negligibly from the real-world success probability.

As case studies, we model non-trivial properties of RSA encryption and estimate the probability of off-line guessing attacks on the EKE protocol. These attacks are outside the scope of existing symbolic methods.