ASPIER: An Automated Framework for Verifying Security Protocol Implementations

Abstract. We present aspier – the first framework that combines software model checking with a standard protocol security model to analyze authentication and secrecy properties of protocol implementations in an automated manner. aspier incorporates a standard symbolic attacker model and provides analogous guarantees about protocol implementations as previous work does for protocol specifications. We have implemented aspier and used it to verify authentication and secrecy properties of a part of an industrial strength protocol implementation – the handshake in OpenSSL 0.9.6c – for configurations consisting of up to 3 servers and 3 clients. We have also implemented two distinct methods for reasoning about attacker message derivations, and evaluated them in the context of OpenSSL verification. Finally, aspier detected the “versionrollback” vulnerability in OpenSSL 0.9.6c source code.

• Type: Conference
• Year: 2009
• Where: CSFW
• Authors: Sagar Chaki, Anupam Datta
• Keywords: CSFW 2009, Protocol Implementation, Protocol Security Model, Secrecy Properties, Security Privacy