University of Surrey

Test tubes in the lab Research in the ATI Dance Research

A Symbolic Analysis of ECC-based Direct Anonymous Attestation

Whitefield, Jorden, Chen, Liqun, Sasse, Ralf, Schneider, Steve, Treharne, Helen and Wesemeyer, Stephan (2019) A Symbolic Analysis of ECC-based Direct Anonymous Attestation In: 4th IEEE European Symposium on Security and Privacy, 17-19 Jun 2019, Stockholm, Sweden.

[img]
Preview
Text
A Symbolic Analysis of ECC-based Direct Anonymous Attestation.pdf - Accepted version Manuscript

Download (486kB) | Preview

Abstract

Direct Anonymous Attestation (DAA) is a cryptographic scheme that provides Trusted Platform Module (TPM)- backed anonymous credentials. We develop TAMARIN modelling of the ECC-based version of the protocol as it is standardised and provide the first mechanised analysis of this standard. Our analysis confirms that the scheme is secure when all TPMs are assumed honest, but reveals a break in the protocol’s expected authentication and secrecy properties for all TPMs even if only one is compromised. We propose and formally verify a minimal fix to the standard. In addition to developing the first formal analysis of ECC-DAA, the paper contributes to the growing body of work demonstrating the use of formal tools in supporting standardisation processes for cryptographic protocols.

Item Type: Conference or Workshop Item (Conference Paper)
Divisions : Faculty of Engineering and Physical Sciences > Computing Science
Authors :
NameEmailORCID
Whitefield, Jordenj.whitefield@surrey.ac.uk
Chen, Liqunliqun.chen@surrey.ac.uk
Sasse, Ralf
Schneider, SteveS.Schneider@surrey.ac.uk
Treharne, HelenH.Treharne@surrey.ac.uk
Wesemeyer, Stephan
Date : 17 June 2019
Copyright Disclaimer : © 2019 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.
Uncontrolled Keywords : Direct Anonymous Attestation; Symbolic verification; TAMARIN PROVER; Authentication; Secrecy
Related URLs :
Depositing User : Clive Harris
Date Deposited : 25 Apr 2019 09:56
Last Modified : 17 Jun 2019 02:08
URI: http://epubs.surrey.ac.uk/id/eprint/851685

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