Verification of low-level crypto-protocol implementations using automated theorem proving

Designing and implementing cryptographic protocols is known to be difficult. A lot of research has been devoted to developing formal techniques to analyze abstract designs of cryptographic protocols. Less attention has been paid to the verification of implementation-relevant aspects of cryptographic protocols. This is an important challenge since it is non-trivial to securely implement secure designs, because a specification by its nature is more abstract than the corresponding implementation, and the additional information may introduce attacks not present on the design level. In this paper, we address aspects of crypto protocol implementations close to the hardware level. More concretely, we consider the industrial cryptographic token interface standard PKCS 11 which defines how software on untrustworthy hardware can make use of tamper-proof hardware such as smart-cards to perform cryptographic operations on sensitive data. We propose an approach for automated security analysis with first-order logic theorem provers of crypto protocol implementations making use of this standard.