A Usable Formal Methods Sample Problem from TEEP

Status of This Memo

This Internet-Draft is submitted in full conformance with the provisions of BCP 78 and BCP 79.¶

Internet-Drafts are working documents of the Internet Engineering Task Force (IETF). Note that other groups may also distribute working documents as Internet-Drafts. The list of current Internet-Drafts is at https://datatracker.ietf.org/drafts/current/.¶

Internet-Drafts are draft documents valid for a maximum of six months and may be updated, replaced, or obsoleted by other documents at any time. It is inappropriate to use Internet-Drafts as reference material or to cite them other than as "work in progress."¶

This Internet-Draft will expire on 8 May 2024.¶

Copyright Notice

Copyright (c) 2023 IETF Trust and the persons identified as the document authors. All rights reserved.¶

This document is subject to BCP 78 and the IETF Trust's Legal Provisions Relating to IETF Documents (https://trustee.ietf.org/license-info) in effect on the date of publication of this document. Please review these documents carefully, as they describe your rights and restrictions with respect to this document.¶

Table of Contents

1. Introduction

In this draft we take the Trusted Execution Environment Provisioning protocol [I-D.ietf-teep-protocol] to be a good domain from which to draw a sample modeling problem for slightly different reasons than those proposed in [I-D.farrell-ufmrg-sample].¶

1. TEEP is a proposed standard under active development, at working-group consensus as of this writing. Formal modeling, even for demonstration or training purposes, can therefore increase familiarity with the TEEP protocol, including outside of the SUIT and TEEP working groups directly involed in its development.¶

2. The TEEP protocol is expressly concerned with security, so it has security properties amenable to formal description, modeling, and analysis. Any findings may have valuable security implications.¶

3. The TEEP protocol has well-defined use cases and includes a number of options for flexibility, including provisions for constrained environments. Modeling the entire protocol, including all its options, is a reasonable challenge for a learning or training exercise. By contrast, [I-D.farrell-ufmrg-sample] limits itself to just the SEARCH command of [RFC9051].¶

4. The TEEP protocol follows a typical protocol design in the IETF where various already-standardized technologies are reused. In this case, protocols from the Software Updates for Internet of Things (SUIT) architecture [RFC9019] and the Remote Attestation Procedures (RATS) architecture [RFC9334] are incorporated into the design.¶

5. The architecture of the TEEP protocol is also representative for IETF protocol development since more than two parties are involved in the protocol communication even in a single, self-contined deployment. Whether a formal model must consider all parties or can limit itself to a subset is a worthwhile question about the scope of this sample problem.¶

2. Conventions and Definitions

The key words "MUST", "MUST NOT", "REQUIRED", "SHALL", "SHALL NOT", "SHOULD", "SHOULD NOT", "RECOMMENDED", "NOT RECOMMENDED", "MAY", and "OPTIONAL" in this document are to be interpreted as described in BCP 14 [RFC2119] [RFC8174] when, and only when, they appear in all capitals, as shown here.¶

3. The Trusted Execution Environment Provisioning (TEEP) Protocol

The Trusted Execution Environment Provisioning protocol [I-D.ietf-teep-protocol] specifies communication between a Trusted Application Manager (TAM) [RFC9397] (Section 2) and a TEEP Agent. Importantly, this communication is relayed by an untrusted TEEP Broker [RFC9397] (Section 6.1). Two security-sensitive payloads are communicated via the TEEP protocol, namely:¶

• Trusted Applications (TAs) and Trusted Components (TCs) [RFC9397] (Section 2); and¶

• attestation evidence.¶

A Trusted Application is an application (or, in some implementations, an application component) that runs in a TEE.¶

A Trusted Component is a set of code and/or data in a TEE that is managed as a unit by a TAM. Trusted Applications and Personalization Data [RFC9397] (Section 2) are thus managed by being included in Trusted Components.¶

TCs are provided by developers or authors, which TEEP calls "Trusted Component Signers" [RFC9397] (Section 2). SUIT manifests protect TCs' integrity and may optionally protect their confidentiality as well. Neither the TAM nor the TEEP Broker should be able to modify TCs. TEEP Agents only install TCs from sources they trust.¶

Attestation evidence is typically communicated from the TEEP Agent to the TAM, although there is the option to offer attestation capabilities in both directions. In the description below, we focus only on attestation of the Device [RFC9397] (Section 2) containing the TEEP Agent to the TAM, rather than attestation in the other direction.¶

The description below illustrates the basic communication interaction, with details of the TEEP protocol abstracted away.¶

TAM -> Verifier: NonceRequest

TAM <- Verifier: NonceResponse
Nonce

TAM -> TEEP Agent: QueryRequest
{token, challenge, supported-teep-cipher-suites,
supported-suit-cose-profiles, data-item-requested(trusted-components,
attestation)}SK_TAM

TEEP Agent -> Attester: EvidenceRequest
challenge

TEEP Agent <- Attester: EvidenceResponse
{challenge, claims}SK_ATTESTER

TAM <- TEEP Agent: QueryResponse
{token, selected-teep-cipher-suite, attestation-payload-format(EAT),
attestation-payload({challenge, claims}SK_ATTESTER), tc-list}SK_AGENT

Author -> TAM: SoftwareUpdate
{manifest, sequence_nr, TC}SK_AUTHOR

TAM -> TEEP Agent: Update
{token2, {manifest, sequence_nr, software}SK_AUTHOR}SK_TAM

TAM <- TEEP Agent: Success
{token2}SK_AGENT

4. Security Considerations

This document has no security considerations of its own, although it may contribute indirectly to the development of new security considerations for the TEEP protocol.¶

5. IANA Considerations

This document has no IANA actions.¶

Authors' Addresses