Options
Reasoning with past to prove pkcs#11 keys secure
Publikationstyp
Conference Paper
Date Issued
2011-03-18
Sprache
English
Author(s)
First published in
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
Publisher DOI
Scopus ID
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