Root-of-trust abstractions for symbolic analysis: application to attestation protocols

Georgios Fotiadis, Jose Moreira-Sanchez, Thanassis Giannetsos, Liqun Chen, Peter B. Ronne, Mark Ryan, Peter Y.A. Ryan

Research output: Chapter in Book/Report/Conference proceedingConference contribution

54 Downloads (Pure)


A key component in building trusted computing services is a highly secure anchor that serves as a Root-of-Trust (RoT). There are several works that conduct formal analysis on the security of such commodity RoTs (or parts of it), and also a few ones devoted to verifying the trusted computing service as a whole. However, most of the existing schemes try to verify security without differentiating the internal cryptography mechanisms of the underlying hardware token from the client application cryptography. This approach limits, to some extent, the reasoning that can be made about the level of assurance of the overall system by automated reasoning tools. In this work, we present a methodology that enables the use of formal verification tools towards verifying complex protocols using trusted computing. The focus is on reasoning about the overall application security, provided from the integration of the RoT services, and how these can translate to larger systems when the underlying cryptographic engine is considered perfectly secure. Using the Tamarin prover, we demonstrate the feasibility of our approach by instantiating it for a TPM-based remote attestation service, which is one of the core security services needed in today's increased attack landscape.
Original languageEnglish
Title of host publicationSecurity and Trust Management
Subtitle of host publication17th International Workshop, STM 2021, Darmstadt, Germany, October 8, 2021, Proceedings
EditorsRodrigo Roman, Jianying Zhou
PublisherSpringer, Cham
Number of pages22
ISBN (Electronic)9783030918590
ISBN (Print)9783030918583
Publication statusPublished - 8 Dec 2021

Publication series

NameLecture Notes in Computer Science
PublisherSpringer, Cham
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Bibliographical note

Publisher Copyright:
© 2021, Springer Nature Switzerland AG.


  • Formal verification
  • Remote attestation
  • SAPiC
  • TPM modelling
  • Tamarin prover
  • Trusted computing

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Root-of-trust abstractions for symbolic analysis: application to attestation protocols'. Together they form a unique fingerprint.

Cite this