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) | Y | Sardar, Fossati, Frost, Xiong. Formal Specification and Verification of Architecturally-defined Attestation in Arm CCA and Intel TDX |
ProVerif model (symbolic) | N | Sardar, Fossati, Frost. SoK: Attestation in Confidential Computing |
Type | Peer-reviewed | Reference |
---|---|---|
CPSA model | Y | Burgin, Rowe, Guttman: Details of Attacks and Fix for EAP-AKA’ |