Defending the Bank with a Proof Assistant

Abstract

Abstract. We show how the proof-assistant Coq helped us formally verify security properties of an API. As far as we know, this is the first mathematical proof of security properties of an API. The API we veri-fied is a fixed version of Bond's modelization of IBM's Common Cryp-tographic Architecture. We explain the methodology we followed, sketch our proof and explain the points the formal verification raised.