Options
Concepts and proofs for configuring PKCS#11
Publikationstyp
Conference Paper
Date Issued
2012-07-23
Sprache
English
Author(s)
First published in
Number in series
7140 LNCS
Start Page
131
End Page
147
Citation
Lecture Notes in Computer Science (7140 LNCS): 131-147 (2012-07-23)
Contribution to Conference
Publisher DOI
Scopus ID
Publisher
Springer
ISBN of container
978-3-642-29420-4
978-3-642-29419-8
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.
DDC Class
004: Informatik
530: Physik
600: Technik