Automated Verification of Security Protocol Implementations (CMU-CyLab-08-002)

We present a method that combines software model checking with a standard protocol security model to provide meaningful security analysis of protocol implementations in a completely automated manner. Our approach incorporates a standard symbolic attacker model and provides analogous guarantees about protocol implementations as previous work does for protocol specifications. We have implemented our approach and verified authentication and secrecy properties of an industrial strength protocol implementation – 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 present their comparison in the context of OpenSSL verification.