PKCS#11, is a security API for cryptographic tokens. It is known to be vulnerable to attacks which can directly extract, as cleartext, the value of sensitive keys. Fixes proposed in the literature, or implemented in real devices, impose policies restricting key roles and token functionalities. In [7] we have presented a type-based analysis to prove, on abstract API specifications, that the secrecy of sensitive keys is preserved under a certain policy. In this paper we discuss how this type system might be extended to type-check a real security policy implemented in the opencryptoki PKCS#11 software token. This is a first step towards a type-based analysis of real PKCS#11 devices.
Towards a type-based analysis of real PKCS#11 devices
FOCARDI, Riccardo;LUCCIO, Flaminia
2012-01-01
Abstract
PKCS#11, is a security API for cryptographic tokens. It is known to be vulnerable to attacks which can directly extract, as cleartext, the value of sensitive keys. Fixes proposed in the literature, or implemented in real devices, impose policies restricting key roles and token functionalities. In [7] we have presented a type-based analysis to prove, on abstract API specifications, that the secrecy of sensitive keys is preserved under a certain policy. In this paper we discuss how this type system might be extended to type-check a real security policy implemented in the opencryptoki PKCS#11 software token. This is a first step towards a type-based analysis of real PKCS#11 devices.File | Dimensione | Formato | |
---|---|---|---|
ASA12.pdf
non disponibili
Tipologia:
Abstract
Licenza:
Accesso chiuso-personale
Dimensione
191.03 kB
Formato
Adobe PDF
|
191.03 kB | Adobe PDF | Visualizza/Apri |
I documenti in ARCA sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.