Extending the Input Language of Spi2Java
Cătălin Hriţcu, Alex Busenius, Violeta Ivanova · 2008
Automatic code generation from formal models is an important approach for the secure implementation of cryptographic protocols. We have extended Spi2Java, a tool that automatically generates interoperable protocols from spi calculus processes to use a more powerful input language. The new input language is the spi calculus with constructors and destructors defined in the paper of Abadi and Blanchet [1]. We have successfully implemented a generic type inference algorithm for the new language constructs and refactored the code significantly. Furthermore, we implemented a translation from the original input language to the spi calculus with constructors and destructors. This paper describes the steps we have taken for implementing this extension, our achievements