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.
Keywords for this software
References in zbMATH (referenced in 5 articles )
Showing results 1 to 5 of 5.
- Avalle, Matteo; Pironti, Alfredo; Sisto, Riccardo: Formal verification of security protocol implementations: a survey (2014) ioport
- Cadé, David; Blanchet, Bruno: Proved generation of implementations from computationally secure protocol specifications (2013)
- Blanchet, Bruno: Security protocol verification: symbolic and computational models (2012)
- Jager, Tibor; Kohlar, Florian; Schäge, Sven; Schwenk, Jörg: On the security of TLS-DHE in the standard model (2012)
- Fournet, Cédric; Bhargavan, Karthikeyan; Gordon, Andrew D.: Cryptographic verification by typing for a sample protocol implementation (2011)