Formal Analysis and Implementation of a TPM 2.0-based Direct Anonymous Attestation Scheme
Wesemeyer, Steve, Newton, Christopher, Treharne, Helen, Chen, Liqun, Sasse, Ralf and Whitefield, Jordan (2019) Formal Analysis and Implementation of a TPM 2.0-based Direct Anonymous Attestation Scheme In: 15th ACM ASIA Conference on Computer and Communications Security, 5-9 Oct 2020, Virtual Conference.
|
Text
main.pdf - Accepted version Manuscript Download (1MB) | Preview |
Abstract
Direct Anonymous Attestation (Daa) is a set of cryptographic schemes used to create anonymous digital signatures. To provide additional assurance, Daa schemes can utilise a Trusted Platform Module (Tpm) that is a tamper-resistant hardware device embedded in a computing platform and which provides cryptographic primitives and secure storage. We extend Chen and Li’s Daa scheme to support: 1) signing a message anonymously, 2) self-certifying Tpm keys, and 3) ascertaining a platform’s state as recorded by the Tpm’s platform configuration registers (PCR) for remote attestation, with explicit reference to Tpm 2.0 API calls.We perform a formal analysis of the scheme and are the first symbolic models to explicitly include the low-level Tpm call details. Our analysis reveals that a fix proposed by Whitefield et al. to address an authentication attack on an Ecc-Daa scheme is also required by our scheme. Developing a finegrained, formal model of a Daa scheme contributes to the growing body of work demonstrating the use of formal tools in supporting security analyses of cryptographic protocols. We additionally provide and benchmark an open-source C++ implementation of this Daa scheme supporting both a hardware and a software Tpm and measure its performance.
Item Type: | Conference or Workshop Item (Conference Abstract) | |||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Divisions : | Faculty of Engineering and Physical Sciences > Computer Science | |||||||||||||||||||||
Authors : |
|
|||||||||||||||||||||
Date : | 25 October 2019 | |||||||||||||||||||||
Uncontrolled Keywords : | Formal Verification, Security Protocols, TPM, DAA | |||||||||||||||||||||
Additional Information : | Embargo OK Metadata Pending | |||||||||||||||||||||
Depositing User : | James Marshall | |||||||||||||||||||||
Date Deposited : | 17 Jul 2020 11:14 | |||||||||||||||||||||
Last Modified : | 05 Oct 2020 02:08 | |||||||||||||||||||||
URI: | http://epubs.surrey.ac.uk/id/eprint/858231 |
Actions (login required)
![]() |
View Item |
Downloads
Downloads per month over past year