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.
The Spi2Java project is mantained on its own website. Please browse to the Spi2Java home page for further information.
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.