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.
|Name||Lecture Notes in Computer Science|
|Conference||8th International Symposium on Foundations and Practice of Security|
|Abbreviated title||FPS 2015|
|Period||26/10/15 → 28/10/15|