ASPIER: An Automated Framework for Verifying Security Protocol Implementations
- 1 July 2009
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- Vol. 1 (10636900) , 172-185
- https://doi.org/10.1109/csf.2009.20
Abstract
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
This publication has 30 references indexed in Scilit:
- Protocol Composition Logic (PCL)Electronic Notes in Theoretical Computer Science, 2007
- Verified Interoperable Implementations of Security ProtocolsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2006
- Event-related potential noise reduction using the hidden Markov tree modelPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2004
- Abstractions from proofsPublished by Association for Computing Machinery (ACM) ,2004
- Athena: a new efficient automatic checker for security protocol analysisPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Proving properties of security protocols by inductionPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Lazy abstractionPublished by Association for Computing Machinery (ACM) ,2002
- The NRL Protocol Analyzer: An OverviewThe Journal of Logic Programming, 1996
- Model checking and abstractionPublished by Association for Computing Machinery (ACM) ,1992
- Security Policies and Security ModelsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1982