Warning: fopen(/public/southbridge/dream/web/projects/data/stats.txt): failed to open stream: Permission denied in /afs/inf.ed.ac.uk/group/dreamers/websites/dream.inf.ed.ac.uk/web/projects/count.php on line 16

Warning: fwrite() expects parameter 1 to be resource, boolean given in /afs/inf.ed.ac.uk/group/dreamers/websites/dream.inf.ed.ac.uk/web/projects/count.php on line 24

Warning: fclose() expects parameter 1 to be resource, boolean given in /afs/inf.ed.ac.uk/group/dreamers/websites/dream.inf.ed.ac.uk/web/projects/count.php on line 27
Automated Analysis of Security Critical Systems  
MRG home page Research Publications Software People

University of Edinburgh

Automated Analysis of Security Critical Systems

Project Description

This project investigated the application of formal tools to the problem of analysing the APIs of the hardware security modules used in electronic payment systems (i.e. cash machine networks, point of sale devices, etc.).

The project ran from 1st October 2004 to 30th September 2007. You can read a summary of the whole project in the Final Report, submitted to EPSRC in December 2007. The project was rated Outstanding by EPSRC's review panel, and given the top rating in all 7 categories. You can read the EPSRC assessment here.


All publications are listed below.


Our industrial collaborators on the project were nCipher plc., a manufacturer of cryptographic hardware security modules, and CESG, the information assurance arm of GCHQ.


The project was funded by EPSRC (grant number GR/S98139/01).


The project was designed and proposed by Graham Steel, who was the principal R.A.

Alan Bundy was the PI 

Jacques Fleuriot was a Co-Investigator 

Gavin Keighren was an MSc student who carried out the experiments using Cl-Atse.


  • A Formal Theory of Key Conjuring. Véronique Cortier, Stéphanie Delaune and Graham Steel. In Proceedings of the 20th IEEE Computer Security Foundations Symposium (CSF 20), pages 79-93.
  • Automatic Analysis of the Security of XOR-based Key Management Schemes. Véronique Cortier, Gavin Keighren and Graham Steel. In proceedings of TACAS 2007, pages 538-552.
  • On the Decidability of a Class of XOR-based Key-management APIs, with Véronique Cortier. To appear at the FCS-ARSPA workshop at FLoC'06.
  • Computer Science Strikes Back Against Fraud. Graham Steel. Shortlisted for the EPSRC 2007 Computer Science Writing Prize.
  • Formal Analysis of PIN Block Attacks. Graham Steel. In Theoretical Computer Science, volume 367 (1-2), pages 257-270, November 2006. ©Elsevier
  • Deduction with XOR Constraints in Security API Modelling. Graham Steel. In Proceedings of the 20th Conference on Automated Deduction (CADE 20), July 2005, pages 322-336. ©Springer-Verlag
  • Visualising First-Order Proof Search. Graham Steel. Appeared in Proceedings of the 2005 Workshop on User Interfaces for Theorem Provers (UITP '05), pages 179-189.
  • Links

    AnaBlock homepage.

    Other researchers in the field of API analysis include:

    Related groups and projects in the University of Edinburgh: