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.
