Session Date/Time: 04 Nov 2025 14:30

UFMRG

Summary

The UFMRG session featured three presentations. Felix extended his work on usable formal methods for Attested TLS, highlighting issues with existing definitions like Lois hierarchy in this context and presenting a cyclic redundancy problem that makes strong cryptographic binding challenging for pre/intra-handshake attestation. Corey Myers and Felix Linker presented a co-design and formal analysis of a new end-to-end encrypted messaging protocol for SecureDrop, detailing why Signal/MLS protocols were unsuitable for their specific requirements and how they integrated computational and symbolic proofs to identify vulnerabilities. Finally, Deirdre Connolly introduced the "Crypto Proof Ladders" project, an initiative to help cryptographers learn and compare various computer-aided proof tools by focusing on different proof techniques. The session concluded with a proposal for a new IRTF Research Group on Confidential Computing and Formal Methods.

Key Discussion Points

Usable Formal Methods for Attested TLS (Felix Linker):
- Approach: Emphasized making formal methods more accessible to engineers through English explanations, visualization of valid/invalid traces, and actively involving protocol designers in the loop.
- Correlation Property: Introduced a "correlation property" to describe agreement between parties on multiple parameters, which did not neatly fit existing hierarchies.
- Critique of Lois Hierarchy: Argued that Lois hierarchy's "weak agreement" definition is not suitable for attestation protocols, particularly in one-way authentication scenarios, as it implies agreement on an initiator's identity that may not be authenticated or known (e.g., anonymous TLS client). Jonathan Hood clarified that Lois's "identity" could refer to the "same person" via shared secret rather than a named identity.
- Attested TLS Formal Analysis: Presented a detailed analysis covering remote attestation goals, TLS goals, and novel composition goals that cryptographically bind attestation to the TLS connection at various levels (general, handshake traffic secret, application traffic secret).
- Challenges with Strong Binding: Identified a significant cyclic redundancy problem when attempting to achieve the strongest binding (application traffic secret) within attestation evidence for pre- and intra-handshake attestation. Including the application traffic secret in the evidence would require it to be sent after the TLS Finished message, making it impossible to include in the Finished message's HMAC, which is necessary for the binding. This problem is considered "really hard, if not impossible," for standardization without significant TLS protocol changes.
- Key Insights: Stressed the need for infrastructure identity to prevent diversion attacks and a cryptographic binding between remote attestation and TLS to prevent relay attacks.
Co-design Analysis of SecureDrop Protocol (Corey Myers & Felix Linker):
- Motivation for E2E: SecureDrop's original design relied on physical security, which became a burden and unsuitable for third-party hosting (e.g., cloud), necessitating an end-to-end encrypted design.
- Limitations of Existing Protocols: Signal and MLS were found unsuitable due to their reliance on persistent client-side state for key ratcheting (SecureDrop sources are stateless) and the unacceptable metadata leakage from storing session bundles on the server in a low-volume, high-stakes context.
- Iterative Design & Analysis: Described an iterative co-design process involving security requirements, threat modeling, protocol design, and both computational (pen-and-paper) and symbolic (Tamarin) formal analysis to refine the protocol.
- Protocol Overview: Uses standard Public Key Encryption (PKE) for metadata and Authenticated Public Key Encryption (APKE) for the actual message, combined with a novel message delivery protocol over Tor designed for anonymity and undetectability.
- Formal Analysis Methodology: For confidentiality and authentication, they split proofs into primitive-level (computational) and protocol-level (symbolic). They employed an axiomatization approach in Tamarin to directly model computational guarantees, providing a more accurate cryptographic model and separation of concerns.
- Findings: The analysis uncovered a previously unnoticed attack on the message delivery protocol. It also revealed that protocol-level replay protection could not be formally guaranteed from the cryptographic primitives, and that the protocol is not post-quantum secure for anonymity and undetectability due to reliance on elliptic curve Diffie-Hellman.
- Benefits: The formal analysis led to a faster iteration cycle on design and provided confidence in security decisions.
Crypto Proof Ladders Project (Deirdre Connolly):
- Objective: To help cryptographers learn and compare various computer-aided proof tools (e.g., EasyCrypt, ProVerif, Tamarin) by providing a collection of "ladders" that ramp up in proof technique difficulty rather than just construction complexity.
- Ladders: Includes ladders for symmetric, asymmetric, and protocol constructions, with a focus on demonstrating different proof techniques across multiple tools.
- Target Audience: Primarily working cryptographers who write proofs and want to explore how computer-aided tools can improve their work. The project is less focused on training engineers without prior proof-writing experience.
- Community Engagement: The project is open to community contributions of new problems, tools, or proofs.

Decisions and Action Items

Attested TLS Work: Feedback is requested on the shared preprint. Discussions will continue in the SEED working group.
New IRTF Research Group Proposal: Samu will send a pointer to the mailing list regarding a proposal for a new IRTF Research Group on Confidential Computing and Formal Methods. An additional side meeting was scheduled for the same day.
Trusted Computing Son of Excellence (TCES): TCES is seeking contributions and help to promote formal methods adoption in critical infrastructure and the business community; interested parties are encouraged to reach out via the mailing list.

Next Steps

Attested TLS: Further development and discussion of the formal analysis, particularly around the challenges of strong cryptographic binding, are expected within the SEED working group.
SecureDrop Protocol: The Freedom of the Press Foundation aims to couple their implementation with verification to the formal model and reuse the existing proving work.
Crypto Proof Ladders: Continue to expand the collection of proofs, tools, and problems on the ladders, actively seeking and integrating community contributions.
Confidential Computing RG: Advance the proposal for the new IRTF Research Group, engage interested parties, and refine the scope and charter.