Skip to main content

Technical Reports: CMU-CyLab-08-012

Title:ASPIER: An Automated Framework for Verifying Security Protocol Implementations
Authors:Sagar Chaki, Anupam Datta
Publication Date:October 14, 2008


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. ASPIERincorporates a standard symbolic attacker model and provides analogous guarantees about protocol implementations as previous work does for protocol specifications. We have implemented ASPIERand 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.

Full Report: CMU-CyLab-08-012