Graham Steel holds a degree in Mathematics from the University of
Cambridge and a PhD in Informatics from the University of
Edinburgh. After post-doctoral research positions in Germany, Italy,
Scotland and France, he became an INRIA researcher at the
Specification and Verification Laboratory (LSV) of the ENS-Cachan in
2008. He specialises in the analysis of security of APIs for
cryptographic modules used in critical devices such as cash machines,
USB security tokens and smartcards.
International standards dictate that all processing of customer
Personal Identification Numbers (PINs) in the international cash
machine network must take place inside special tamper resistant
Hardware Security Modules (HSMs). These HSMs have a restricted API
designed so that even if an attacker is able to make arbitrary command
calls to the device, no customer PINs can be obtained. However, in
recent years, a number of attacks have been found on these APIs. Some
of them are so-called differential attacks, whereby an attacker makes
repeated calls to the API with slightly different parameters, and from
the pattern of error messages received, he is able to deduce the value
of a PIN. In this talk, I will present some of these attacks, and talk
about efforts to analyse them formally. This will include techniques
for proving the absence of such attacks in patched APIs, and a
practical proposal for improving the security of the network without
making large-scale changes to the current infrastructure.