CISPA
Browse
cispa_all_2895.pdf (524.54 kB)

How to wrap it up - A formally verified proposal for the use of authenticated wrapping in PKCS#11

Download (524.54 kB)
conference contribution
posted on 2023-11-29, 18:10 authored by Alexander DaxAlexander Dax, Sven Tangermann, Robert KünnemannRobert Künnemann, Michael BackesMichael Backes
Being the most widely used and comprehensive standard for hardware security modules, cryptographic tokens and smart cards, PKCS#11 has been the subject of academic study for years. PKCS#11 provides a key store that is separate from the application, so that, ideally, an application never sees a key in the clear. Again and again, researchers have pointed out the need for an import/export mechanism that ensures the integrity of the permissions associated to a key. With version 2.40, for the first time, the standard included authenticated deterministic encryption schemes. The interface to this operation is insecure, however, so that an application can get the key in the clear, subverting the purpose of using a hardware security module. This work proposes a formal model for the secure use of authenticated deterministic encryption in PKCS#11, including concrete API changes to allow for secure policies to be implemented. Owing to the authenticated encryption mechanism, the policy we propose provides more functionality than any policy proposed so far and can be implemented without access to a random number generator. Our results cover modes of operation that rely on unique initialisation vectors (IVs), like GCM or CCM, but also modes that generate synthetic IVs. We furthermore provide a proof for the deduction soundness of our modelling of deterministic encryption in Böhl et.al.'s composable deduction soundness framework.

History

Preferred Citation

Alexander Dax, Sven Tangermann, Robert Künnemann and Michael Backes. How to wrap it up - A formally verified proposal for the use of authenticated wrapping in PKCS#11. In: IEEE Computer Security Foundations Symposium (CSF). 2019.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

IEEE Computer Security Foundations Symposium (CSF)

Legacy Posted Date

2019-06-07

Open Access Type

  • Unknown

BibTeX

@inproceedings{cispa_all_2895, title = "How to wrap it up - A formally verified proposal for the use of authenticated wrapping in PKCS#11", author = "Dax, Alexander and Tangermann, Sven and Künnemann, Robert and Backes, Michael", booktitle="{IEEE Computer Security Foundations Symposium (CSF)}", year="2019", }

Usage metrics

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC