These experiments relate to the paper Formal Analysis of Key Integrity in PKCS#11, by Andrea Falcone and Riccardo Focardi, to be presented at ARSPA-WITS '10. The model checker used is SATMC v3.0.
We give two model files here. They relate to a real PKCS#11 device that we have tested (but will not name for the moment). The device has been patched to prevent some attacks that we found in earlier work. Specifically, sensitive keys cannot be wrapped.
The first model does not support key replacement. Running it with SATMC, we find no attacks. The second is exactly the same with the addition of an unwrap mode that replaces existing keys, a disconnection operation, and the modelling of an honest user (see the paper for details). Running it with SATMC we find an attack. Times taken on an Intel CPU 3.20GHz
| Experiment | Summary | Model file | Results file |
| 1 | Patched device, no replacement. No attacks found. 22 sec | replace1.if | output |
| 2 | Patched device with replacement modelled. Attack found in 41 sec | replace2.if | output |
We used the following parameters for SATMC:
--prelude=prelude.if --avispa=false --sc=true --solver=minisat --hash_table=true