Analysing PKCS#11 key management APIs with unbounded fresh data

Abstract. We extend Delaune, Kremer and Steel’s framework for anal-ysis of PKCS#11-based APIs from bounded to unbounded fresh data. We achieve this by: formally defining the notion of an attribute policy; showing that a well-designed API should have a certain class of policy we call complete; showing that APIs with complete policies may be safely abstracted to APIs where the attributes are fixed; and proving that these static APIs can be analysed in a small bounded model such that secu-rity properties will hold for the unbounded case. We automate analysis in our framework using the SAT-based security protocol model checker SATMC. We show that a symmetric key management subset of the Era-com PKCS#11 API, used in their ProtectServer product, preserves the secrecy of sensitive keys for unbounded numbers of fresh keys and han-dles, i.e. pointers to keys. We also show that this API is not robust: if an encryption key is lost to the intruder, SATMC finds an attack whereby all the keys may be compromised.