Department of Computer Science and Technology

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

DOI: 10.48456/tr-644

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 = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-644.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-644},
  number = 	 {UCAM-CL-TR-644}
}