Automated Security Verification for Crypto Protocol Implementations: Verifying the Jessie Project

An important missing link in the construction of secure systems is finding a practical way to establish a correspondence between a software specification and its implementation. We address this problem for the case of crypto-based Java implementations (such as crypto protocols) with an approach using automated theorem provers for first-order logic, by linking the implementation to a specification model. In this paper, we present details on an application of this approach to the open-source Java implementation Jessie of the SSL protocol. We also shortly comment on how these results can be transferred to the standard Java Secure Sockets Extension (JSSE) library that was recently open-sourced by Sun.