Computer Laboratory

Technical reports

Robbing the bank with a theorem prover

Paul Youn, Ben Adida, Mike Bond, Jolyon Clulow, Jonathan Herzog, Amerson Lin, Ronald L. Rivest, Ross Anderson

August 2005, 26 pages

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.

Full text

PDF (0.2 MB)

BibTeX record

@TechReport{UCAM-CL-TR-644,
  author =	 {Youn, Paul and Adida, Ben and Bond, Mike and Clulow, Jolyon
          	  and Herzog, Jonathan and Lin, Amerson and Rivest, Ronald L.
          	  and Anderson, Ross},
  title = 	 {{Robbing the bank with a theorem prover}},
  year = 	 2005,
  month = 	 aug,
  url = 	 {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-644.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-644}
}