In addition to our original experiments, here we analyse for the first time extensions to the standard API made by nCipher and Eracom (now SafeNet) in their HSMs. In summary, we found that both permitted secure configurations to be found, but both require careful attention to other details in order to avoid vulnerabilities. However, we examined only small bounded models permitted by our naive encoding of the problem for NuSMV. Deatils are in the paper, to appear in the Journal of Computer Security. For more comprehensive results on the eracom fixes, see the third paper on P11.
| Experiment | Summary | Model file | Results file |
| 1 | three symmetic keys, Clulow's wrap/decrypt attack (Fig 1 in paper) | experiment1.smv | experiment1.out |
| 2 | three symmetic keys, new encrypt/unwrap attack (Fig 3 in paper) | experiment2.smv | experiment2.out |
| 3 | three symmetic keys, two asym keypairs, new wrap/unwrap attack (Fig 4 in paper) | experiment3.smv | experiment3.out |
| 4 | three symmetic keys, four handles for each, restriction of dec/wrap, enc/unwrap and wrap/unwrap attribute pairs - (Fig 5 in paper) | experiment-4.smv | experiment-4.out |
| 5 | three symmetic keys, two asym keypairs, Clulow's trojan wrapped key attack (Fig 6 in our paper - S3.5 in Clulow's paper) | experiment5.smv | experiment5.out |
| 6 | three symmetic keys, two asym keypairs, new attack on trusted key (Fig 7 in paper) | experiment6.smv | experiment6.out |
| 7 | three symmetic keys, two asym keypair, closed graph of trusted keys - no attack | experiment7.smv | experiment7.out |
| 8 | three symmetic keys, two asym keypairs, closed cycle of trusted keys including one of the asym keypairs - no attack | experiment8.smv | experiment8.out |
| 9 | three symmetic keys, two double length keys, ECB, Clulow's weaker key attack (Fig 9 - S2.4 in Clulow paper) | experiment9.smv | experiment9.out |
| 10 | three symmetic keys, two double length keys, ECB, Clulow's ECB key attack (Fig 10 - S2.2 in Clulow paper) | experiment10.smv | experiment10.out |
| 11 | Full nCipher SAM, no attack | experiment11.smv | experiment11.out |
| 12 | nCipher SAM with import, no attribute restrictions, Clulow's wrap/decrypt attack (Fig 1 in paper) | experiment12.smv | experiment12.out |
| 13 | nCipher SAM with import, restriction of dec/wrap, enc/unwrap and wrap/unwrap attribute pairs, no attack | experiment13.smv | experiment13.out |
| 14 | nCipher SAM switched off, Clulow's trojan wrapped key attack (Fig 6 in our paper - S3.5 in Clulow's paper) | experiment14.smv | experiment14.out |
| 15 | ERACOM wrap mechanism, no attack | experiment15.smv | experiment15.out |
| 16 | ERACOM wrap mechanism no attribute restrictions, Clulow's wrap/decrypt attack (Fig 1 in paper) | experiment16.smv | experiment16.out |