Minute Takers: Hannes Tschofenig, Muhammad Usama Sardar
Slides:
https://datatracker.ietf.org/meeting/125/materials/slides-125-seat-chairs-slides-00
Henk: Is use cases draft going to be published?
Yaroslav: No
total participants: 50
Is use cases draft ready for adoption?
Yes: 6
No: 0
No opinion: 13
Have you read the latest revision of early attestation draft?
(authors should not vote)
yes: 7
no: 19
No opinion: 0
Slides:
https://datatracker.ietf.org/meeting/125/materials/slides-125-seat-security-analysis-00
Usama presented his slides.
Slide 11/11: Summary of analysis so far
• Pre-handshake attestation: replay and diversion attacks
• Intra-handshake attestation: diversion and relay
attacks
• Post-handshake attestation: no known attacks
* Slide 11/11: Unless one re-establishes connection each time
attestation is required, post-handshake attestation is required, and
hence, intra-handshake only adds unnecessary complexity.
Jun raised a question whether we can be certain about the correctness of
the formal model.
Usama responded by saying that there are several ways:
The research work has been submitted for review in a top security
conference, where artifacts are evaluated as part of the review.
Markus Rudy: Think of DHE as a counter-example to "if private keys are
leaked, everything is lost".Jonathan Hoyland: You can prove that a compromised key is used
honestly if you have other uncompromised keys.Ionuț Mihalcea: Right, but it might just leak the other key and not
priv_EK, why only look at the case where priv_EK is leakedMuhammad Usama Sardar: Sure, that's where we have the attack. We are
not denying that the other case is not possible.
Transient key leakage is possible too. If provisioned at runtime, the
problem could be in provisioning protocol. So there are several
possibilities.Hannes Tschofenig: Maybe the use case draft should also talk a bit
about our attacker assumptions. I have been puzzeled also in the TLS
group with regards to key attestation about what people assume
attackers can and cannot do.Paul Wouters: hannes: agreed on the user cases and attack
explanations. also knowing real world limitations of things like tees
deployed with identical keys and other expected deployment
characteristicsHannes Tschofenig: Formal methods are not perfect but they certainly
help. If nothing else, they help you look at the solution from a
different angle.Deirdre Connolly: Formal analysis is broad collection of techniques
applicable to 'formalizable' schemes, protocols, etc, including
cryptographic ones; techniques include different approaches of
pen-and-paper proofs, game based or otherwise; formal methods
techniques such as the symbolic models in Tamarin and ProVerif, or
computational models such as EasyCrypt; or 'other', like Squirrel,
that try to straddle those two worlds; other techniques include formal
verification of executable programs that they correctly implement a
reference model/spec of an algorithm
Slides:
https://datatracker.ietf.org/meeting/125/materials/slides-125-seat-facts-seat-ietf-125-slides-00
Nathanael presented his new solution.
Usama: Thank you for using our formal models. I believe that attested
TLS is quite a complicated problem and formal analysis is critical to
get to a secure solution. So your formal modeling work is highly
appreciated.
Also, huge thank you for independent verification of our expat draft.
Nathanael explained his background and his motivation for participating
in the work as a new participant in the group.
Chairs noted that the use case document needs to be adopted first. Then,
solutions will have to be compared against the use cases. Then,
solutions can be adopted.
Slides:
https://datatracker.ietf.org/meeting/125/materials/slides-125-seat-seat-expat-00
Community interest:
5 tech giants in this field are developing implementations of
draft-fossati-seat-expat
5 I-Ds using our protocol
The only attested TLS draft cited in CCC’s response to NIST RFI
(NIST-2025-0035)
Tiru presented the protocol and Usama presented the ongoing formal
analysis.
Jonathan noted that his formal analysis on the exported authenticators
showed that EAs do not bind to each other, i.e. if multiple EAs are sent
(e.g. in a re-attestation) EAs provide no guarantee that the
attestations are from the same device. You know the TLS server shares
state with the first attester and that the TLS server shares state with
the second attester but you have no guarantee from the EA protocol
that the first attester shares state with the second attester. If you
want that property, you need to guarantee that some other way.
Usama thanks Jonathan for sharing his insights and believes that the
runtime measurements via TPM should provide that guarantee. In ProVerif,
they are currently modeled as constants.
Clarification question for Jonathan: The above statement is for TLS
Client as RATS Attester, right? and sharing "state" means sharing some
secrets (like exporter values) that the adversary does not know, right?
Thomas Fossati: I believe that before asking adoption we should
clarify what the scope of expat is: see
https://github.com/tls-attestation/exported-attestation/issues/56Usama: This is an implementation detail. We will see how the
discussions go as more developers implement it. In CCC Attestation
SIG, as you know, there is clear interest in SHIM layer.
Slides:
https://datatracker.ietf.org/meeting/125/materials/slides-125-seat-early-attestation-01
Yaron requested call for adoption of the draft since he believes the
draft is now within the scope of the charter.
Usama believes it is still out of charter because of modifying the key
schedule. (mailing list discussion)
Usama: If there is no external or resumption PSK, the inputs for Early
Secret is a constant and it is still a "secret" in TLS 1.3 key schedule.
Key can be constant.
Discussion about terminology.
Usama: Option a: EKU has lots of problems with the threat model. (See
https://github.com/tlswg/tls-key-update/issues/100) Option c does not
cover server as Attester. Option b requires reconnections.
Chairs highlight the work on the use cases. Asks group to review the use
case draft.