Robbing the Bank with a Theorem Prover

So it’s a fairly provocative title, how did we get to that? Well automated tools have been successfully applied to modelling security protocols and finding attacks, and some good examples here are Gavin Lowe’s work, using FDR to model the Needham-Shroeder protocols, and Larry Paulson’s work using Isabella to prove the SET protocol secure. Now we come to the observation that security protocols, and security application programming interfaces are very closely related. So just to define what we mean by a security API here. We’re talking devices that offer security services, that will obviously have some interface, typically the application programming interface, and unlike a normal API it also has to enforce policy onto the user, it has to make sure that keys remain secret, that PINs aren’t revealed, and that users can’t generally do things that would violate the security policy.