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 |
Old TLS versions:
| Extension | Type | Peer-reviewed | Reference |
|---|---|---|---|
| TLS Encrypted ClientHello | ProVerif model (symbolic) | Y | A Symbolic Analysis of Privacy for TLS 1.3 with Encrypted Client Hello |
| Exported Authenticators | TODO | ? | Exported Authenticators |
| KEMTLS (AuthKEM and Hybrid-KEX) | Computational | Y | KEMTLS |
| KEMTLS (AuthKEM and Hybrid-KEX) | Tamarin model (symbolic) | Y | A tale of two models: formal verification of KEMTLS via Tamarin |
| 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 |