Verifying Cryptoprotocol Implementations in First-Order Logic

Jan Juerjens

(The Open University, Milton Keynes)

Understanding the security goals provided by cryptographic protocol
implementations is known to be difficult, since security requirements
such as secrecy, integrity and authenticity of data are notoriously
hard to establish, especially in the context of cryptographic
interactions. A lot of research has been devoted to develop formal
techniques to analyze abstract specifications of cryptographic
protocols. Less attention has been paid to the analysis of
cryptoprotocol implementations, for which a formal link to
specifications is often not available. We present work towards
verifying crypto protocol implementation against security
requirements using automated theorem provers for first-order
logic, and discuss some interesting aspects of its underlying
model-theoretic foundations.
Thursday 14th December 2006, 14:00
Board Room
Department of Computer Science