CTL
4 May 2010 - 14h00
Formal Analysis of Key Management APIs
by Graham Steel from LSV Laboratoire Spécification et Vérification
Abstract: Designing an cryptographic key management interface for a tamper
resistant device is a difficult problem. The interface should be
designed so that no matter what sequence of commands is called, the
key management policy continues to hold: sensitive keys remain secret,
keys can only be used for their designated purposes, keys are be
exported and imported from the device securely, etc. Most commercial
key management APIs are based around the RSA standard PKCS#11. In this
talk, we will show how implementing this standard without a great deal
of care can lead to multiple security vulnerabilities. We will look at
a number of examples of attacks and see why they are difficult to fix.
We will discuss a formal framework for the analysis of such APIs.
Finally, we will discuss new standards being developed by OASIS and
IEEE to try to improve the situation.
Slides of the Presentation.
