@TechReport{YABCx05,
  author = 	 { Paul Youn and Ben Adida and Mike Bond and Jolyon Clulow and Jonathan Herzog and Amerson Lin and Ronald L. Rivest
                   and Ross Anderson },
  title = 	 { Robbing the bank with a theorem prover },
  institution =  { University of Cambridge Computer Laboratory },
  date =         { 2005-08 },                  
  OPTyear = 	 { 2005 },
  OPTmonth = 	 { August },
  url =          { http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-644.pdf },                  
  htmlnote = 	 { Technical Report UCAM-CL-TR-644. Also see <a href="#YABCx07">YABCx07</a>. },
  abstract =     {
        We present the first methodology for analysis and automated detection of attacks on
        security application programming interfaces (security APIs) --- the interfaces to
        hardware cryptographic services used by developers of critical security systems,
        such as banking applications.  Taking a cue from previous work on the formal analysis
        of security protocols, we model APIs purely according to specifications, under
        the assumption of ideal encryption primitives. We use a theorem prover tool and
        adapt it to the security API context. We develop specific formalization and automation
        techniques that allow us to fully harness the power of a theorem prover. We show how,
        using these techniques, we were able to automatically re-discover all of the pure API
        attacks originally documented by Bond and Anderson against banking payment networks,
        since their discovery of this type of attack in 2000.  We conclude with a note of
        encouragement: the complexity and unintuiveness of the modelled attacks make a very 
        strong case for continued focus on automated formal analysis of cryptographic APIs.                  
                 },
}