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.