Project Details

Key findings

Synopsis: The 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.).
Results: The project included some research into finding ways to reason effectively about key-management APIs that use bitwise XOR, such as the IBM 4758 CCA API.
- Early results on rediscovering known attacks in a formal model were presented at CADE-20 in Tallinn. This involved extending the superposition calculus with XOR unification constraints.
- We proved some theoretical results about the decidability of XOR-based key-management schemes, in collaboration with Véronique Cortier. This work was presented at the FCS-ARSPAworkshop in August 2006.
- We devised an efficient way to implement the decision procedure arising from these results, and obtained some verification results for the revised versions of the IBM CCA API. Details appeared at TACAS 2007.
- We proposed a formalisation for "Key Conjuring", the process by which the attacker obtains a valid but unknown key for an API. This was published at CSF 2007 in Venice.
- We developed a formal model for PIN-guessing attacks with information leakage, employing the PRISM probabilistic model checker to optimise attacks. Many APIs are vulnerable to these kinds of attacks.
Effective start/end date1/10/0430/09/07


  • EPSRC: £183,665.00


Explore the research topics touched on by this project. These labels are generated based on the underlying awards/grants. Together they form a unique fingerprint.
  • A Formal Theory of Key Conjuring

    Cortier, V., Delaune, S. & Steel, G., 2007, Computer Security Foundations Symposium, 2007. CSF '07. 20th IEEE. Institute of Electrical and Electronics Engineers (IEEE), p. 79-96 18 p.

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Automatic Analysis of the Security of XOR-Based Key Management Schemes

    Cortier, V., Keighren, G. & Steel, G., 2007, Tools and Algorithms for the Construction and Analysis of Systems: 13th International Conference, TACAS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24 - April 1, 2007. Proceedings. Grumberg, O. & Huth, M. (eds.). Springer-Verlag GmbH, p. 538-552 15 p. (Lecture Notes in Computer Science; vol. 4424).

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • Computer Science Strikes Back Against Fraud

    Steel, G., 2007.

    Research output: Working paper