Verified Security Protocol Modeling and Implementation with AnBx

AnBx is an extension of the Alice & Bob notation for protocol narrations to serve as a specification language for a purely declarative modelling of distributed protocols. AnBx is built around a set of communication and data abstractions which provide primitive support for the high-level security guarantees, and help shield from the details of the underlying cryptographic infrastructure. Being implemented on top of the OFMC verification tool, AnBx serves not only for spec- ification and design, but also for security analysis of distributed protocols. Moreover the framework, keeping apart the protocol logic from the application logic, allow for automatic generation of Java source code of protocols specified in AnBx . We demonstrate the practical effectiveness of our approach with the specification and analysis of two real-life e-payment protocols, obtaining stronger and more scalable security guarantees than those offered by the original ones. In the second part of the thesis we formally analyze the Secure Vehicle Communication sys- tem (SeVeCom), using the AIF framework which is based on a novel set-abstraction technique. We report on two new attacks found and verify that under some reasonable assumptions, the system is secure