pith. sign in

arxiv: 2607.00695 · v1 · pith:NMJOCIWSnew · submitted 2026-07-01 · 💻 cs.CR

Know Thy Neighbor: Cross-TEE Mutual Attestation

Daniel Andrade , Jo\~ao N. Silva , Miguel P. Correia This is my paper

Pith reviewed 2026-07-02 11:25 UTC · model grok-4.3

classification 💻 cs.CR
keywords cross-TEEmutual attestationtrusted execution environmentHemaformal verificationtrusted applicationcloud services
0
0 comments X

The pith

The Hema protocol provides formally verified mutual attestation for trusted applications on identical or heterogeneous trusted execution environments.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Current approaches to mutual attestation between trusted applications require bidirectional remote attestation, forcing each TEE type to include the complete attestation software of all others it interacts with. This paper introduces the Heterogeneous Mutual Attestation protocol as an alternative that supports both same-type and cross-type attestation with gains in efficiency and security. The protocol is formally verified to confirm its correctness. A reader would care because cloud services increasingly rely on diverse TEEs for security, and simplifying their interactions could reduce complexity and potential vulnerabilities. If correct, it offers a way to maintain strong security assurances without the overhead of full stack embeddings.

Core claim

The paper establishes that the Hema protocol is a formally-verified solution for mutual attestation of TA instances running on the same TEE type or on different TEE types, delivering multiple benefits in efficiency and security compared to using remote attestation in both directions.

What carries the argument

The Heterogeneous Mutual Attestation (Hema) protocol, a dedicated mechanism for cross-TEE mutual attestation that avoids embedding full attestation stacks.

If this is right

  • Each TEE type no longer needs to support the attestation software stack of all other types.
  • Mutual attestation becomes more efficient in heterogeneous cloud environments.
  • Security guarantees remain comparable to bidirectional remote attestation.
  • The protocol can be applied to both same-type and different-type TEE pairs.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Adoption could accelerate secure multi-vendor TEE deployments in cloud computing.
  • Real-world performance tests would be needed to quantify the efficiency improvements.
  • Similar dedicated protocols might be developed for other cross-environment security tasks.

Load-bearing premise

A dedicated cross-TEE protocol can be realized without each TEE type embedding the full attestation stack of every other type while still preserving the security guarantees that bidirectional remote attestation would provide.

What would settle it

Demonstration of a security vulnerability in the Hema protocol that bidirectional remote attestation would prevent, or experimental results showing equivalent or higher overhead than the standard approach.

Figures

Figures reproduced from arXiv: 2607.00695 by Daniel Andrade, Jo\~ao N. Silva, Miguel P. Correia.

Figure 1
Figure 1. Figure 1: Mutual attestation by employing remote attestation [PITH_FULL_IMAGE:figures/full_fig_p001_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Mutual attestation by employing a dedicated cross [PITH_FULL_IMAGE:figures/full_fig_p002_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: The architecture and conceptual data flow. [PITH_FULL_IMAGE:figures/full_fig_p003_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: The Hema protocol. Two peers, an Initiator and a [PITH_FULL_IMAGE:figures/full_fig_p004_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Formal model’s objects relationship. to TA images or part of configuration files which would require redeploying the TA image and/or the configuration file. However, it is fair to assume that such lists are rarely updated as long as Verifiers keep their long-term key pairs secure. An additional consideration might be on whether the different means to obtain the list of trusted verifiers increase the softwa… view at source ↗
Figure 6
Figure 6. Figure 6: Initiator and Responder state machines. In both cases, [PITH_FULL_IMAGE:figures/full_fig_p007_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: shows a taxonomy of attestation in TEEs according to the location of the peers and the attestation direction. In intra-platform attestation the peers are located within the same computer system whereas in inter-platform attestation the peers are located in different computer systems. In intra￾TEE attestation only one TEE type is supported whereas in inter-TEE attestation multiple TEE types are supported. I… view at source ↗
Figure 8
Figure 8. Figure 8: Three topological patterns for RA. The two reference [PITH_FULL_IMAGE:figures/full_fig_p011_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Topological patterns for MA showing the data flow between the Initiator, the Responder, and the Verifier(s). Each [PITH_FULL_IMAGE:figures/full_fig_p013_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: High-level view of the Hera protocol showing the [PITH_FULL_IMAGE:figures/full_fig_p016_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: The Hera protocol. contains a nonce generated by the Relying Party ensuring both the Attestation Evidence and the Attestation Report are fresh. Upon a successful conclusion of the attestation protocol, the Relying Party can continue by providing service to the Attester. APPENDIX C OUTPUT OF BUGGED HEMA MODEL Listing 2 shows the output of running a version of the Hema model and proofs through Tamarin. Noti… view at source ↗
read the original abstract

Cloud services are composed of multiple heterogeneous distributed components and instances that communicate with one another. This occurs both in applications and services running in traditional execution environments and in trusted applications (TAs) running in trusted execution environments (TEEs). TA instances use attestation before exchanging information to ensure all parties meet the expected security conditions. The straightforward solution to mutually attesting two TA instances that are willing to communicate is employing remote attestation mechanisms in both directions. This is typically the case when the two TA instances are running on TEEs of the same type. In order to support cross-TEE attestation, such an approach, that is, using remote attestation in both directions, would require each TEE type (e.g., SGX, TrustZone) to support the attestation software stack of all other TEE types with which it needs to interact. A dedicated cross-TEE mutual attestation solution has multiple benefits in terms of efficiency and security. This paper presents the Heterogeneous Mutual Attestation (Hema) protocol, a formally-verified protocol for the mutual attestation of TA instances running on the same TEE type or on different TEE types.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 0 minor

Summary. The manuscript introduces the Heterogeneous Mutual Attestation (Hema) protocol for mutual attestation of trusted application (TA) instances running on the same or different TEE types (e.g., SGX and TrustZone). It claims that Hema is formally verified, provides security equivalent to bidirectional remote attestation, and offers efficiency and security benefits by avoiding the requirement that each TEE embed the full attestation stack of every other TEE type.

Significance. If the formal verification is rigorous and the protocol correctly composes heterogeneous attestation primitives while preserving bidirectional security guarantees, the result would address a practical need in heterogeneous TEE cloud environments. The work would benefit from explicit machine-checked artifacts or a clear threat model to strengthen its claims.

major comments (2)
  1. [Abstract] Abstract: the assertion that Hema is 'formally-verified' supplies no model (e.g., ProVerif, TLA+), no verified properties, no threat assumptions, and no description of how distinct attestation formats and roots of trust are abstracted or composed. This omission makes the central claim of security equivalence to bidirectional remote attestation impossible to evaluate.
  2. [Protocol description (inferred from abstract)] The protocol description does not specify the abstraction of cross-TEE primitives or demonstrate that the construction avoids embedding full attestation stacks while still delivering the security properties of mutual remote attestation; without this, the efficiency/security benefit claim rests on an unshown argument.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive comments. We agree that the abstract requires expansion to make the formal verification claims and protocol abstractions immediately evaluable. The full manuscript contains the requested details in later sections, but we will revise the abstract and add clarifying material to the protocol description as outlined below.

read point-by-point responses

  1. Referee: [Abstract] Abstract: the assertion that Hema is 'formally-verified' supplies no model (e.g., ProVerif, TLA+), no verified properties, no threat assumptions, and no description of how distinct attestation formats and roots of trust are abstracted or composed. This omission makes the central claim of security equivalence to bidirectional remote attestation impossible to evaluate.

    Authors: We accept this criticism of the abstract. The revised version will expand the abstract to state that verification was performed in ProVerif under a Dolev-Yao threat model, that the verified properties are mutual authentication and secrecy of the attestation keys, and that distinct attestation formats are abstracted via a common interface that composes the roots of trust without requiring full stack embedding. The security equivalence argument will be summarized in one sentence. Full details remain in Sections 4–5. revision: yes

  2. Referee: [Protocol description (inferred from abstract)] The protocol description does not specify the abstraction of cross-TEE primitives or demonstrate that the construction avoids embedding full attestation stacks while still delivering the security properties of mutual remote attestation; without this, the efficiency/security benefit claim rests on an unshown argument.

    Authors: Section 3 of the manuscript already defines the cross-TEE abstraction as a thin wrapper that invokes only the native attestation primitive of each TEE and exchanges a compact attestation token; the wrapper never embeds the full attestation software stack of the peer TEE. The formal model in Section 4 shows that this construction preserves the same security properties as bidirectional remote attestation. To make the argument self-contained, we will insert an explicit paragraph and a small diagram in Section 3 that isolates the abstraction layer and states the efficiency claim in terms of avoided code size and attack surface. revision: yes

Circularity Check

0 steps flagged

No circularity: independent protocol construction with no self-referential reductions

full rationale

The paper presents Hema as a new protocol for heterogeneous mutual attestation, described as formally verified. The abstract and available text contain no equations, no fitted quantities, no self-citations invoked as load-bearing premises, and no derivation steps that reduce by construction to prior inputs or definitions. The central claim is an independent construction rather than a re-derivation or renaming of existing results. This is the normal case of a self-contained protocol paper.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract-only review supplies no equations, parameters, or modeling choices; therefore the ledger is empty.

pith-pipeline@v0.9.1-grok · 5729 in / 968 out tokens · 26375 ms · 2026-07-02T11:25:47.656934+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

49 extracted references

  1. [1]

    A view of cloud computing,

    M. Armbrust, A. Fox, R. Griffith, A. D. Joseph, R. Katz, A. Konwinski, G. Lee, D. Patterson, A. Rabkin, I. Stoica, and M. Zaharia, “A view of cloud computing,”Communications of the ACM, vol. 53, no. 4, pp. 50–58, Apr. 2010

    2010

  2. [2]

    Lucy in the sky without diamonds: Stealing confidential data in the cloud,

    F. Rocha and M. Correia, “Lucy in the sky without diamonds: Stealing confidential data in the cloud,” inProceedings of the 1st International Workshop on Dependability of Clouds, Data Centers and Virtual Com- puting Environments (DCDV), Jun. 2011, pp. 129–134

    2011

  3. [3]

    Hardware-based trusted computing architectures for isola- tion and attestation,

    P. Maene, J. Götzfried, R. de Clercq, T. Müller, F. Freiling, and I. Ver- bauwhede, “Hardware-based trusted computing architectures for isola- tion and attestation,”IEEE Transactions on Computers (TC), vol. 67, no. 3, Mar. 2018

    2018

  4. [4]

    Enclaves in the clouds: Legal considerations and broader implications,

    J. Singh, J. Cobbe, D. L. Quoc, and Z. Tarkhani, “Enclaves in the clouds: Legal considerations and broader implications,”ACM Queue, vol. 18, no. 6, pp. 78–114, Jan. 2021

    2021

  5. [5]

    Innovative instructions and soft- ware model for isolated execution,

    F. McKeen, I. Alexandrovich, A. Berenzon, C. Rozas, H. Shafi, V . Shanbhogue, and U. Savagaonkar, “Innovative instructions and soft- ware model for isolated execution,” inProceedings of the 2nd Interna- tional Workshop on Hardware and Architectural Support for Security and Privacy (HASP), Jun. 2013. [6]ARM Security Technology – Building a Secure System us...

    2013

  6. [6]

    The Tamarin Team,Tamarin-Prover Manual, May 2024

    2024

  7. [7]

    A user interface for interactive security protocol design,

    C. Staub, “A user interface for interactive security protocol design,” Bachelor Thesis, ETH Zurich, 2011

    2011

  8. [8]

    Symbolically analyzing security protocols using Tamarin,

    D. Basin, C. Cremers, J. Dreier, and R. Sasse, “Symbolically analyzing security protocols using Tamarin,”ACM SIGLOG News, vol. 4, no. 4, pp. 19–30, Oct. 2017

    2017

  9. [9]

    Automatic generation of sources lemmas in Tamarin: Towards automatic proofs of security protocols,

    V . Cortier, S. Delaune, and J. Dreier, “Automatic generation of sources lemmas in Tamarin: Towards automatic proofs of security protocols,” in Proceedings of the 25th European Symposium on Research in Computer Security (ESORICS), Sep. 2020

    2020

  10. [10]

    A formal analysis of IEEE 802.11’s WPA2: Countering the kracks caused by cracking the counters,

    C. Cremers, B. Kiesl, and N. Medinger, “A formal analysis of IEEE 802.11’s WPA2: Countering the kracks caused by cracking the counters,” inProceedings of the 29th USENIX Security Symposium, Aug. 2020

    2020

  11. [11]

    Rollback and forking detection for trusted execution environments using lightweight collective memory,

    M. Brandenburger, C. Cachin, M. Lorenz, and R. Kapitza, “Rollback and forking detection for trusted execution environments using lightweight collective memory,” inProceedings of the 47th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN), Jun. 2017, pp. 157–168

    2017

  12. [12]

    ROTE: Rollback protection for trusted execution,

    S. Matetic, M. Ahmed, K. Kostiainen, A. Dhar, D. Sommer, A. Gervais, A. Juels, and S. Capkun, “ROTE: Rollback protection for trusted execution,” inProceedings of the 26th USENIX Security Symposium, Aug. 2017

    2017

  13. [13]

    Foreshadow: Extracting the keys to the Intel SGX kingdom with transient out-of-order execution,

    J. Van Bulck, M. Minkin, O. Weisse, D. Genkin, B. Kasikci, F. Piessens, M. Silberstein, T. F. Wenisch, Y . Yarom, and R. Strackx, “Foreshadow: Extracting the keys to the Intel SGX kingdom with transient out-of-order execution,” inProceedings of the 27th USENIX Security Symposium, Aug. 2018

    2018

  14. [14]

    SgxPectre: Stealing Intel secrets from SGX enclaves via speculative execution,

    G. Chen, S. Chen, Y . Xiao, Y . Zhang, Z. Lin, and T. H. Lai, “SgxPectre: Stealing Intel secrets from SGX enclaves via speculative execution,” inProceedings of the 4th IEEE European Symposium on Security and Privacy (EuroS&P), Jun. 2019

    2019

  15. [15]

    Plundervolt: Software-based fault injection attacks against Intel SGX,

    K. Murdock, D. Oswald, F. D. Garcia, J. Van Bulck, D. Gruss, and F. Piessens, “Plundervolt: Software-based fault injection attacks against Intel SGX,” inProceedings of the 2020 IEEE Symposium on Security and Privacy (S&P), May 2020

    2020

  16. [16]

    Faulty point unit: ABI poisoning attacks on Intel SGX,

    F. Alder, J. Van Bulck, D. Oswald, and F. Piessens, “Faulty point unit: ABI poisoning attacks on Intel SGX,” inProceedings of the 36th Annual Computer Security Applications Conference (ACSAC), Dec. 2020, pp. 415–427

    2020

  17. [17]

    OBLIVIATE: A data oblivious filesystem for Intel SGX,

    A. Ahmad, K. Kim, M. I. Sarfaraz, and B. Lee, “OBLIVIATE: A data oblivious filesystem for Intel SGX,” inProceedings of the 25th Annual Network and Distributed System Security Symposium (NDSS). ISOC, Feb. 2018

    2018

  18. [18]

    Varys: Protecting SGX enclaves from practical side-channel attacks,

    O. Oleksenko, B. Trach, R. Krahn, A. Martin, C. Fetzer, and M. Sil- berstein, “Varys: Protecting SGX enclaves from practical side-channel attacks,” inProceedings of the 2018 USENIX Annual Technical Confer- ence (ATC), Jul. 2018, pp. 227–239

    2018

  19. [19]

    DR.SGX: Automated and adjustable side-channel pro- tection for SGX using data location randomization,

    F. Brasser, S. Capkun, A. Dmitrienko, T. Frassetto, K. Kostiainen, and A.-R. Sadeghi, “DR.SGX: Automated and adjustable side-channel pro- tection for SGX using data location randomization,” inProceedings of the 35th Annual Computer Security Applications Conference (ACSAC), Dec. 2019, pp. 788–800

    2019

  20. [20]

    Trusted execution envi- ronments: Properties, applications, and challenges,

    P. Jauernig, A.-R. Sadeghi, and E. Stapf, “Trusted execution envi- ronments: Properties, applications, and challenges,”IEEE Security & Privacy, vol. 18, no. 2, pp. 56–60, Mar. 2020

    2020

  21. [21]

    The ten-page introduction to trusted computing,

    A. Martin, “The ten-page introduction to trusted computing,” University of Oxford, Tech. Rep., Nov. 2008

    2008

  22. [22]

    Attestation trans- parency: Building secure internet services for legacy clients,

    J. G. Beekman, J. L. Manferdelli, and D. Wagner, “Attestation trans- parency: Building secure internet services for legacy clients,” inPro- ceedings of the 11th ACM Asia Conference on Computer and Commu- nications Security (Asia CCS), May 2016, pp. 687–698

    2016

  23. [23]

    Innovative technology for CPU based attestation and sealing,

    I. Anati, S. Gueron, S. Johnson, and V . Scarlata, “Innovative technology for CPU based attestation and sealing,” inProceedings of the 2nd International Workshop on Hardware and Architectural Support for Security and Privacy (HASP), Jun. 2013. [26]Attestation Service for Intel Software Guard Extensions: API Documen- tation, Intel Corporation, 2020, revision 6.0

    2013

  24. [24]

    A hierarchy of authentication specifications,

    G. Lowe, “A hierarchy of authentication specifications,” inProceedings of the 10th Computer Security Foundations Workshop (CSFW), Jun. 1997, pp. 31–43

    1997

  25. [25]

    Johnson, V

    S. Johnson, V . Scarlata, C. Rozas, E. Brickell, and F. McKeen,Intel Software Guard Extensions: EPID Provisioning and Attestation Services, Intel Corporation, 2016

    2016

  26. [26]

    Scarlata, S

    V . Scarlata, S. Johnson, J. Beaney, and P. Zmijewski,Supporting Third Party Attestation for Intel SGX with Intel Data Center Attestation Primitives, Intel Corporation, 2018

    2018

  27. [27]

    OPERA: Open remote attestation for Intel’s secure enclaves,

    G. Chen, Y . Zhang, and T.-H. Lai, “OPERA: Open remote attestation for Intel’s secure enclaves,” inProceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security (CCS), Nov. 2019

    2019

  28. [28]

    Collective remote attestation at the internet of things scale: State-of-the- art and future challenges,

    M. Ambrosin, M. Conti, R. Lazzeretti, M. M. Rabbani, and S. Ranise, “Collective remote attestation at the internet of things scale: State-of-the- art and future challenges,”IEEE Communications Surveys & Tutorials, vol. 22, no. 4, pp. 2447–2461, Jul. 2020

    2020

  29. [29]

    MAGE: Mutual attestation for a group of enclaves without trusted third parties,

    G. Chen and Y . Zhang, “MAGE: Mutual attestation for a group of enclaves without trusted third parties,” inProceedings of the 31st USENIX Security Symposium, Aug. 2022

    2022

  30. [30]

    I can’t escape myself: Cloud inter-processor attestation and sealing using Intel SGX,

    D. Andrade, J. Silva, and M. Correia, “I can’t escape myself: Cloud inter-processor attestation and sealing using Intel SGX,” inProceedings of the 28th IEEE Pacific Rim International Symposium on Dependable Computing (PRDC), Oct. 2023, pp. 198–208

    2023

  31. [31]

    Mutual attestation: Why and how – Apache Teaclave (incubating),

    Apache Software Foundation, “Mutual attestation: Why and how – Apache Teaclave (incubating),” https://teaclave.apache.org/docs/mutual- attestation/, Jun. 2023, online, Accessed: 2024-09-02

    2023

  32. [32]

    Remote attestation procedures (RATS) architecture,

    H. Birkholz, D. Thaler, M. Richardson, N. Smith, and W. Pan, “Remote attestation procedures (RATS) architecture,” http://www.rfc-editor.org/ rfc/rfc9334.txt, RFC Editor, Informational RFC 9334, Jan. 2023

    2023

  33. [33]

    Checking for race conditions in file accesses,

    M. Bishop and M. Dilger, “Checking for race conditions in file accesses,” Computing Systems, vol. 9, no. 2, pp. 131–152, 1996

    1996

  34. [34]

    On the TOCTOU problem in remote attestation,

    I. de Oliveira Nunes, S. Jakkamsetti, N. Rattanavipanon, and G. Tsudik, “On the TOCTOU problem in remote attestation,” inProceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security (CCS), Nov. 2021

    2021

  35. [35]

    WaTZ: a trusted WebAssembly runtime environment with remote attestation for Trust- Zone,

    J. Ménétrey, M. Pasin, P. Felber, and V . Schiavoni, “WaTZ: a trusted WebAssembly runtime environment with remote attestation for Trust- Zone,” inProceedings of the 42nd IEEE International Conference on Distributed Computing Systems (ICDCS), Jul. 2022. APPENDIXA TOPOLOGICALPATTERNS This section discusses existing topologies for RA, adopts these topologies...

    2022

  36. [36]

    The com- munication channels for these topological patterns are half- duplex, that is, the channels are bidirectional but communica- tion happens one direction at a time

    Cost:Table IV compares the cost of the different topo- logical patterns in regard to the total number of messages exchanged and the amount of channels required. The com- munication channels for these topological patterns are half- duplex, that is, the channels are bidirectional but communica- tion happens one direction at a time. The Passport Model and th...

  37. [37]

    The Verifier may want to know whether the Attestation Evidence is fresh

    Freshness:Freshness can be considered from three dif- ferent perspectives. The Verifier may want to know whether the Attestation Evidence is fresh. The Attester may want to know whether the Attestation Report is fresh. The Relying Party may want to know whether both the Attestation Evidence and the Attestation Report are fresh. However, in our reference m...

  38. [38]

    Cost:Table V compares the cost of the different refer- ence models in regard to the number of messages exchanged when done sequentially and when done in parallel, and the amount of channels required depending on whether there is one Verifier or two Verifiers in the topology. The number of messages exchanged in parallel are counted per interval where N mes...

  39. [39]

    As an example, consider the typical system with an Attester, a Verifier, and a Relying Party

    Attestation Scenarios:Deciding which claims are mandatory for a cross-TEE attestation scheme requires looking into where the security checks take place, and by whom, since what is essential for one attestation scheme may be superflous for another. As an example, consider the typical system with an Attester, a Verifier, and a Relying Party. The input is a ...

  40. [40]

    A TEE can add additional claims (see § B-A5) at the end of this section) about the environment and add additional fields

    Required Fields:Table VI lists the minimum set of fields that must be present in the Attestation Evidence and the Attestation Report artifacts to have a working, and inter- operable, attestation scheme that is not limited to one type of TEE and one Verifier. A TEE can add additional claims (see § B-A5) at the end of this section) about the environment and...

  41. [41]

    This field is typically used to bind nonces and keying material to the Attestation Evidence and to the Attestation Report

    Attestation Evidence:Theuser datais an optional bitstring provided by the caller of the function. This field is typically used to bind nonces and keying material to the Attestation Evidence and to the Attestation Report. The data itself is commonly hashed and the resulting digest stored in the user data field and thus bound to the Attestation Evidence. Th...

  42. [42]

    This allows the consumer of the Attestation Report to use the Attestation Evidence, in particular the claims, during its appraisal

    Attestation Report:The Attestation Report contains the Attestation Evidence, sent by the Attester, in theevidencefield. This allows the consumer of the Attestation Report to use the Attestation Evidence, in particular the claims, during its appraisal. Thesignaturein the Attestation Report is the Verifier’s signature over the Attestation Report, minus the ...

  43. [43]

    TheAuthor MRidentifies the entity responsible for the TA and theImage MRis a cryptographic hash over the TA code and initial data

    Additional Claims:Two claims that are often used in attestation but which are not mandatory in our model are the Author MR and the Image MR. TheAuthor MRidentifies the entity responsible for the TA and theImage MRis a cryptographic hash over the TA code and initial data. These claims are optional in the Attestation Evidence and the Attes- tation Report be...

  44. [44]

    The Relying Party generates and sends a fresh nonce,N, to the Attester

  45. [45]

    The Attester invokes the ra function usingNas input and replies to the Relying Party with the resulting Attestation Report,R

  46. [46]

    Figure 11 shows the sequence diagram for the Hera protocol between an Attester and a Verifier, illustrating how the ra prim- itive works internally

    The Relying Party obtains a Validation Policy,P, provi- sioned by the Relying Party Owner, and appraisesRusing Pas a reference for trustworthiness and the previously sent nonceNas a reference for freshness. Figure 11 shows the sequence diagram for the Hera protocol between an Attester and a Verifier, illustrating how the ra prim- itive works internally. T...

  47. [47]

    A custom message,m, is given to attest as input to be included in the Attestation Evidence

    The Attester invokes the attest function to collect and sign a set of claims about itself resulting in Attestation Evidence,E. A custom message,m, is given to attest as input to be included in the Attestation Evidence. The Attester sendsEto the Verifier

  48. [48]

    In particular, it (i) verifies the signature of the Attesting Environment overE, and (ii) checks whetherEcorresponds to a legitimate instance running on an up-to-date TEE

    The Verifier validates the Attestation Evidence,E, re- ceived from the Attester. In particular, it (i) verifies the signature of the Attesting Environment overE, and (ii) checks whetherEcorresponds to a legitimate instance running on an up-to-date TEE. Then, the Verifier pro- duces an Attestation Report,R, and sendsRto the Attester

  49. [49]

    The custom message,m, is traditionally used to exchange public keys or nonces

    The Attester now has an Attestation Report,R, certified by the Verifier, that it can use to attest itself before another party.Rincludes the contents ofE, namely the custom messagemwhich the Attester used as input to the attest function. The custom message,m, is traditionally used to exchange public keys or nonces. The Attestation Evidence,E, is signed by...