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.