First-order Verification of Crypto protocols
Dr. Ernie Cohen
Microsoft Research
Abstract: I'll describe a verification method for crypto protocols, based on
first-order invariants. For typical protocols, suitable invariants can be
generated automatically from the protocol text, allowing safety properties
to be proved by automatic first-order theorem proving. This approach has
been implemented in an automatic verifier (TAPS) that has proved properties
of over 100 protocols, and has found bugs missed in published model checking
analyses. If there's time, I'll also describe how the verifier has been
extended to prove safety from guessing attacks, and how the method can be
adapted to more faithful protocol models.
Short bio:
Ernie Cohen is a Test Architect at Microsoft, where he develops formal
methods for system software and security. Since his PhD at the University of
Texas at Austin, he has worked as a Senior Scientist at
Bellcore/Telcordia,
and a Visiting Researcher and Software Architect at Microsoft.