06080416

a

06080416 Fr\"oschle, Sibylle Sommer, Nils Concepts and proofs for configuring PKCS\#11. Barthe, Gilles (ed.) et al., Formal aspects of security and trust. 8th international workshop, FAST 2011, Leuven, Belgium, September 12--14, 2011. Revised selected papers. Berlin: Springer (ISBN 978-3-642-29419-8/pbk). Lecture Notes in Computer Science 7140, 131-147 (2012). 2012 Berlin: Springer EN

doi:10.1007/978-3-642-29420-4_9

Summary: We have recently put forward several ideas of how to specify, model, and verify security APIs centered around the slogan `security APIs are also like programs' and first-order linear time logic extended by past operators. We have developed these ideas based on an investigation of PKCS \#11, a standard widely adopted in industry, and presented preliminary results at FAST'10. In this paper, we present several novel results about PKCS \#11 that we have obtained based on the full implementation of this approach. In particular, this concerns an analysis of the `wrap with trusted feature', a full analysis of which has been out of reach for the previous models. At the same time we provide concepts and terminology that connect to Bond and Clulow's `Types of Intention' and devise an informal method of configuring and understanding PKCS \#11.