VeriSec: Automated Verification of Security-Critical Software

In the context of this Industrial Fellowship, an approach was developed to verify implementations of cryptographic protocols against their specifications, which in turn are verified against security requirements, so that the verification chain results in verification of the implementation against the security requirements. In particular, the Industrial Fellowship developed compositional techniques for security verification in this context. The approach was applied to existing implementations of cryptographic protocols.