swMATH ID: 9852
Software Authors: Chaki, S. ;Datta, A.
Description: ASPIER: An Automated Framework for Verifying Security Protocol Implementations. We present ASPIER - the first framework that combines software model checking with a standard protocol security model to automatically analyze authentication and secrecy properties of protocol implementations in C. The technical approach extends the iterative abstraction-refinement methodology for software model checking with a domain-specific protocol and symbolic attacker model. We have implemented the ASPIER tool and used it to verify authentication and secrecy properties of a part of an industrial strength protocol implementation - the handshake in OpenSSL - 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. ASPIER detected the ”version-rollback” vulnerability in OpenSSL 0.9.6c source code and successfully verified the implementation when clients and servers are only willing to run SSL 3.0.
Homepage: http://ieeexplore.ieee.org/xpl/login.jsp?tp=&arnumber=5230617
Related Software: EasyCrypt; NAXOS; Spi2Java; HMQV; ZKPDL; MJ; JavaSPI; JML; AGVI; Coq; CryptoVerif; OCaml; ProVerif; TulaFale; F*; VCC
Referenced in: 5 Publications

Referenced in 1 Serial

1 Journal of Cryptology

Referencing Publications by Year