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
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
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.
The project included some research into finding ways to reason
effectively about key-management APIs that use bitwise XOR, like 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
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-ARSPA
workshop 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.