Security Analysis of PKCS11

Experiments: Secure Configuration of PKCS11 - Eracom version of API.

Experiments with an symmetric key management API based on the Eracom ProtectServer implementation of PKCS#11

The model checker used is SATMC v3.0. These experiments are descibed in a paper entitled Analysing PKCS#11 Key Management APIs with Unbounded Fresh Data, by Sibylle Fröschle and Graham Steel, accepted to appear at ARSPA-WITS '09 For a short description, see this note

Experiment Summary Model file Results file
1 Property 1 - secrecy of sensistive keys property-1.if output
2 Property 2 - forward secrecy property-2.if output

Extra experiment

This doesn't appear in the submitted paper. Here, we analyse a revised version of the API and show it is robust to loss of session keys. An explanation here.
Experiment Summary Model file Results file
3 Property 2 - Forward secrecy of revised API revised-api.if output

Notes on the model checking

To rerun these experiments you will need not just SATMC v3.0 but also the customised prelude file which defines our typed theory. The fact that SATMC supports this easy customisation of the theory was one of our main motivations for choosing it. The other was that unlike many protocol model checkers, it supports mutable global state, and it is happy to allow protocols with loops.

We used the following parameters for SATMC:

--prelude=eracom/prelude.if --avispa=false --sc=true --solver=minisat --hash_table=true

You should substitue eracom/prelude.if with the location where you saved the prelude file

We would like to thank the SATMC team, and in particular Roberto Carbone, for their support during our experiments.

About LSV