LSV Seminar

The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.

The seminar is open to public and does not require any form of registration.

Past Seminars

Formal Analysis of Security APIs

Tuesday, November 13 2007 at 11:00AM
Salle de Conférence (Pavillon des Jardins)
Graham Steel (University of Edinburgh)

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 obtain personal identification numbers (PINs). These HSMs have a restricted API that is designed to prevent malicious intruders from gaining access to the data. However, several attacks have been found on these APIs, as the result of painstaking manual analysis by experts such as Mike Bond and Jolyon Clulow.

I have been carrying out research aimed at formalising and mechanising the analysis of these APIs. This talk will present some API attacks, and some automated formal analysis using theorem provers, protocol analysis tools, and the PRISM probabilistic model checker.

About LSV