miTLS is a verified reference implementation of the TLS protocol. Our code fully supports its wire formats, ciphersuites, sessions and connections, re-handshakes and resumptions, alerts and errors, and data fragmentation, as prescribed in the RFCs; it interoperates with mainstream web browsers and servers.
Spi2Java is a model driven development (MDD) framework to semi-automatically generate Java security protocol implementations from verified Spi Calculus formal specifications of such protocols. The aim of the framework is to provide high correctness confidence on the generated code, thus making a step towards bridging the gap between the verified abstract formal models, and their concrete implementations.
Get more details on the Spi2Java home page.
On this page you can find online material regarding the black-box monitoring approach for security protocol implementations.
Download: monPV tool, along with SSL and SSH-TLP examples. Contains a README file with furhter instructions on compilation and usage.
Black-Box Monitoring of Security Protocols, Revision 1, : Politecnico di Torino (Italy), Microsoft Research Cambridge (UK) and Open University (UK), 2009.