Jan Jürjens
TU München
Germany

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 developing 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. In this paper, we propose an automated approach to determine
security goals provided by a protocol implementation based on control
flow graphs and automated theorem provers for first-order logic.

Keywords: code security, automated security analysis, cryptographic protocol, authentication, biometrics

Read Paper (in PDF)