Graham J. Steel, University of Edinburgh


Formalised PIN Cracking


Cash machines (ATMs) and other critical parts of the electronic payment infrastructure contain tamper-proof hardware security modules (HSMs), which protect highly sensitive data such as the keys used to encrypt personal identification numbers (PINs). Recently, several attacks have been found on the APIs of these HSMs, which would allow an attacker to obtain a customer's PIN. In this talk, I'll present some of these attacks, and talk about ongoing work at the University of Edinburgh, where we are analysing formal models of these APIs to check for further attacks, and to guarantee the success of measures taken to thwart them.