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 |
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. 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