In this first set of experiments, we examine key separation attacks, similar to those in Jolyon Clulow's 2003 CHES paper. We constrain our PKCS#11 API by repeatedly banning certain combinations of key attributes, each time obtaining a new (longer) attack. Finally we investigate some solutions involving for example the "trusted keys" mechanism, which requires that certain keys, for example wrapping and unwrapping keys, are marked as trusted by the Security Officer. For a further explanation of these experiments, see the paper Formal Analysis of PKCS#11, by S. Delaune, S. Kremer and G. Steel, presented at IEEE CSF-20 in 2008.
| 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 - no attack | experiment4.smv | experiment4.out |
| 5 | three symmetic keys, two asym keypairs, Clulow's trojan wrapped key attack (S3.5 in Clulow's paper) | experiment5.smv | experiment5.out |
| 6 | three symmetic keys, two asym keypairs, new attack on trusted key (Fig 5 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 (section 2.4 in Clulow paper) | experiment9.smv | experiment9.out |
| 10 | three symmetic keys, two double length keys, ECB, Clulow's ECB key attack (section 2.2 in Clulow paper) | experiment10.smv | experiment10.out |