AnBx: Automatic Generation and Verification of Security Protocols Implementations
Paolo Modesti
International Symposium on Foundations & Practice of Security (FPS 2015), Clermont-Ferrand, France, 2015
Abstract
The AnBx compiler is a tool for automatic generation of Java implementations of security protocols specified in a simple and abstract model that can be formally verified. In our model-driven development approach, protocols are described in AnBx, an extension of the Alice & Bob notation. Along with the synthesis of consistency checks, the tool analyses the security goals and produces annotations that allow the verification of the generated implementation with ProVerif.
Links