Reasoning with past to prove pkcs#11 keys secure

Publikationstyp
Conference Paper
Date Issued
2011-03-18
Sprache
English
Author(s)
Fröschle, Sibylle B.  orcid-logo
Sommer, Nils  
TORE-URI
http://hdl.handle.net/11420/11273
First published in
Lecture notes in computer science  
Number in series
6561 LNCS
Start Page
96
End Page
110
Citation
Lecture Notes in Computer Science (6561 LNCS): 96-110 (2011-03-18)
Contribution to Conference
7th International Workshop on Formal Aspects of Security and Trust, FAST 2010  
Publisher DOI
10.1007/978-3-642-19751-2_7
Scopus ID
2-s2.0-79952605484
Publisher
Springer
PKCS#11 is a widely adopted standard that defines a security API for accessing devices such as smartcards and hardware security modules. Motivated by experiments on several devices we develop an approach that allows us to formally establish security properties of keys stored on such devices. We use first-order linear time logic extended by past operators. The expressiveness of a first-order language allows us to model the security API and its features close to how it is specified while the past operators enable proof by backwards analysis. We apply this approach to prove that keys that initially have the attribute extractable set to false are secure.
DDC Class
004: Informatik
530: Physik
600: Technik