Understanding security goals provided by crypto-protocol implementations

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 presence 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 source code analysis of legacy crypto-protocol implementations, for which specifications are often not available. This is an important challenge since it is non-trivial to determine from a given protocol implementation exactly which security goals are achieved, which is necessary for a reliable maintenance of security-critical systems. In this paper, we propose an approach to determine security goals provided by an implemented protocol based on control flow graphs and automated theorem provers for first-order logic.