Final Report of Grant GR/S98139/01: Automated Analysis of Security Critical Systems
Graham Steel, Alan Bundy, Jacques Fleuriot · 2007
The aim of the project was to investigate the application of security protocol analysis techniques to security APIs. Security protocols are short programs that describe the secure exchange of information over an insecure network, using cryptography. Security APIs are the Application Program Interfaces of tamper-resistant hardware security modules, commonly used in security critical applications such as cash machines (ATMs). Security protocol analysis has been the subject of intensive research by the formal methods community over the last 20 years, but the use of these techniques for analysing APIs had not been attempted prior to our proposal. In the early 2000s, a number of powerful attacks on APIs currently in use in the banking network were discovered as the result of pain-staking manual analysis by expert researchers. Hence the aim of this project was to develop techniques to automate the analysis of APIs, taking security protocol analysis as a starting point.