15/06/2012, 16:15 — 17:15 — Room P3.10, Mathematics Building
Rohit Chadha, INRIA and ENS-Cachan
Automated Verification of Equivalence Properties of Cryptographic
Protocols
Indistinguishability properties are essential in formal
verification of cryptographic protocols. They are needed to model
anonymity properties, strong versions of confidentiality and
resistance to offline guessing attacks, and can be conveniently
modeled using process equivalences. We present a novel procedure to
verify equivalence properties for bounded number of sessions. Our
procedure is able to verify trace equivalence for determinate
cryptographic protocols. On determinate protocols, trace
equivalence coincides with observational equivalence which can
therefore be automatically verified for such processes. When
protocols are not determinate our procedure can be used for both
under- and over-approximations of trace equivalence, which proved
successful on examples. The procedure can handle a large set of
cryptographic primitives, namely those which can be modeled by an
optimally reducing convergent rewrite system. Although, we were
unable to prove its termination, it has been implemented in a
prototype tool and has been effectively tested on examples, some of
which were outside the scope of existing tools.
