This is the wiki page for the ufm rg.
Please feel free to add content however you think best, and we'll discuss how to organise that during IETF 116.
| Type | Peer-reviewed | Reference |
|---|---|---|
| Tamarin model (symbolic) | No | https://github.com/cloudflare/ohttp-analysis |
| Type | Peer-reviewed | Reference |
|---|---|---|
| Tamarin model (symbolic) | ? | https://github.com/cloudflare/odoh-analysis |
| Type | Peer-reviewed | Reference | TLS Draft | Artifacts |
|---|---|---|---|---|
| TODO | Y | Beurdouche et al. - 2015 - A Messy State of the Union: Taming the Composite State Machines of TLS | TODO | TODO |
| Tamarin model (symbolic) | Y | Cremers, Horvat, Hoyland, Scott, van der Merwe - 2017 - A Comprehensive Symbolic Analysis of TLS 1.3 | draft 21 | webpage, repo |
| Symbolic (ProVerif) and Computational (CryptoVerif) | Y | Bhargavan et al. 2018 - Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate | draft 18 | repo |
| TODO | Y | Patton et al. - 2018 - Partially Specified Channels | draft 23 | TODO |
Old TLS versions:
| Extension | Type | Peer-reviewed | Reference | Artifacts |
|---|---|---|---|---|
| TLS Encrypted ClientHello | ProVerif model (symbolic) | Y | A Symbolic Analysis of Privacy for TLS 1.3 with Encrypted Client Hello | repo |
| Exported Authenticators | TODO | ? | Exported Authenticators | TODO |
| KEMTLS (AuthKEM and Hybrid-KEX) | Computational | Y | KEMTLS | TODO |
| KEMTLS (AuthKEM and Hybrid-KEX) | Tamarin model (symbolic) | Y | A tale of two models: formal verification of KEMTLS via Tamarin | TODO |
| Type | Peer-reviewed | Reference |
|---|---|---|
| TODO | ? | [Bruni18] Bruni, A., Sahl Jørgensen, T., Grønbech Petersen, T., and C. Schürmann, "Formal Verification of Ephemeral Diffie-Hellman Over COSE (EDHOC)", November 2018, https://www.springerprofessional.de/en/formal-verification-of-ephemeral-diffie-hellman-over-cose-edhoc/16284348 |
| TODO | ? | [Norrman20] Norrman, K., Sundararajan, V., and A. Bruni, "Formal Analysis of EDHOC Key Establishment for Constrained IoT Devices", September 2020, https://arxiv.org/abs/2007.11427 |
| TODO | ? | [CottierPointcheval22] Cottier, B. and D. Pointcheval, "Security Analysis of the EDHOC protocol", September 2022, https://arxiv.org/abs/2209.03599 |
| TODO | ? | [Jacomme23] Jacomme, C., Klein, E., Kremer, S., and M. Racouchot, "A comprehensive, formal and automated analysis of the EDHOC protocol", October 2022, https://hal.inria.fr/hal-03810102/ |
| TODO | ? | [GuentherIlunga22] Günther, F. and M. Ilunga, "Careful with MAc-then-SIGn: A Computational Analysis of the EDHOC Lightweight Authenticated Key Exchange Protocol", December 2022, https://eprint.iacr.org/2022/1705 |
| Type | Peer-reviewed | Reference |
|---|---|---|
| TODO | ? | OPAQUE |
| Type | Peer-reviewed | Reference |
|---|---|---|
| TODO | ? | CPACE |
| Type | Peer-reviewed | Reference |
|---|---|---|
| WIM (symbolic) | Y | Fett, Küsters, Schmitz. A Comprehensive Formal Security Analysis of OAuth 2.0 |
| WIM (symbolic) | Y | OAuth 2.0 + extensions (PKCE, mTLS, etc). Fett, Hosseyni, Küsters. An Extensive Formal Security Analysis of the OpenID Financial-grade API |
| Type | Peer-reviewed | Reference |
|---|---|---|
| DY* model (symbolic) | Y | Bhargavan, Bichhawat, Do, Hosseyni, Küsters, Schmitz, Würtele. An In-Depth Symbolic Security Analysis of the ACME Standard |
| Type | Peer-reviewed | Reference |
|---|---|---|
| ProVerif model (symbolic) | N | Sardar, Fossati, Frost. SoK: Attestation in Confidential Computing |