University of Surrey

Test tubes in the lab Research in the ATI Dance Research

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.

[img]
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 :
NameEmailORCID
Wesemeyer, SteveS.Wesemeyer@surrey.ac.uk
Newton, Christopherc.newton@surrey.ac.uk
Treharne, HelenH.Treharne@surrey.ac.uk
Chen, Liqunliqun.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 View Item

Downloads

Downloads per month over past year


Information about this web site

© The University of Surrey, Guildford, Surrey, GU2 7XH, United Kingdom.
+44 (0)1483 300800