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.

Preview

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 :	Name Email ORCID Wesemeyer, Steve S.Wesemeyer@surrey.ac.uk Newton, Christopher c.newton@surrey.ac.uk Treharne, Helen H.Treharne@surrey.ac.uk Chen, Liqun liqun.chen@surrey.ac.uk Sasse, Ralf Whitefield, Jordan
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