From f03e7f99b27612da73950bf0ccdf4c026a6e661c Mon Sep 17 00:00:00 2001 From: Douglas Stebila Date: Wed, 22 Jul 2026 21:05:38 -0400 Subject: [PATCH] Website updates for 0.6.0 release Add the 0.6.0 news item and refresh the CFRG hybrid KEM case study for the report, bounds companion, and per-proof `bound:` clauses the release adds. This is a partial update: the rest of the 0.6.0 website work is specified in extras/docs/plans/todo/2026-07-22-website-update-0.6.0.md in the engine repo. Notably, limitations.md, canonicalization.md, and researchers/soundness.md still state that ProofFrog does not track quantitative advantage bounds, which 0.6.0 makes false. Co-Authored-By: Claude Opus 4.8 (1M context) --- examples.md | 6 +++++- index.md | 1 + 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/examples.md b/examples.md index dfc64a3..b9077b1 100644 --- a/examples.md +++ b/examples.md @@ -157,7 +157,11 @@ The [KEMPRF](https://github.com/ProofFrog/examples/blob/main/Schemes/KEM/KEMPRF. A ProofFrog formalization of the four hybrid PQ/T KEM combiners specified in the IRTF CFRG draft [*Hybrid PQ/T Key Encapsulation Mechanisms*](https://datatracker.ietf.org/doc/html/draft-irtf-cfrg-hybrid-kems-10). Each framework combines a post-quantum KEM with a "traditional" component — either another KEM or a nominal group — via a key-derivation function: **UG** and **CG** use a nominal group, **UK** and **CK** use a second KEM; **U**(niversal) and **C**(2PRI) name the two combiner constructions. Each is modelled in two variants (a seed-form matching the draft's primary definition and an expanded-form cache), giving machine-checked proofs of correctness, IND-CCA security (for both the post-quantum and traditional branches), and the LEAK-BIND and HON-BIND binding properties. -This case study motivated much of the new lazy-map random-oracle and group-exponent machinery in the 0.5.0 engine. The [full README](https://github.com/ProofFrog/examples/blob/main/applications/cfrg-hybrid-kems/README.md) documents the modelling choices, the mapping from draft sections to files, and the assumptions each proof relies on (including important caveats about implicit rejection and the absence of a quantum-attacker model). +This case study motivated much of the lazy-map random-oracle and group-exponent machinery added to the engine in 0.5.0. The [full README](https://github.com/ProofFrog/examples/blob/main/applications/cfrg-hybrid-kems/README.md) documents the modelling choices, the mapping from draft sections to files, and the assumptions each proof relies on (including important caveats about implicit rejection and the absence of a quantum-attacker model). + +As of ProofFrog 0.6.0, the case study also carries a **report of its findings** and a **companion document summarizing the advantage bound and assumptions of each of the 57 proofs**, both alongside the rewritten README in the same directory. Every proof now declares a [`bound:` clause]({% link manual/language-reference/proofs.md %}), so `prove` checks the concrete advantage bound the proof claims as well as the sequence of hops. + +Ten of those proofs reduce a hop to a statistical fact about reprogramming a random oracle, stated as one of six helper games in [`games/ROM/`](https://github.com/ProofFrog/examples/tree/main/applications/cfrg-hybrid-kems/games/ROM), each carrying a declared `advantage <= ...;` clause. Each of those six games ships with an EasyCrypt proof of the bound it declares (`games/ROM/*.ec`), so the numbers the helper games assert are checked by a second tool rather than taken on trust. These EasyCrypt files are written directly rather than produced by any exporter, and they cover the six helper games only — not the hybrid KEM theorems that use them. See the [`applications/cfrg-hybrid-kems/`](https://github.com/ProofFrog/examples/tree/main/applications/cfrg-hybrid-kems) directory for all scheme definitions, games, and proofs. diff --git a/index.md b/index.md index ff16a3d..56e284c 100644 --- a/index.md +++ b/index.md @@ -38,6 +38,7 @@ See the [installation instructions]({% link manual/installation.md %}) for detai ## Recent updates +- **Jul. 22, 2026: Release of [ProofFrog version 0.6.0](https://github.com/ProofFrog/ProofFrog/releases/tag/v0.6.0)** featuring concrete advantage bounds (the engine now synthesizes the bound a verified proof establishes, and checks a bound the proof claims), a preliminary LaTeX export backend, tuple-destructuring bindings, an Emacs mode for FrogLang, and a substantial wave of soundness fixes to the canonicalization and equivalence layers — anyone relying on a proof checked by 0.5.0 should re-run it under this release - **Jun. 7, 2026: Release of [ProofFrog version 0.5.0](https://github.com/ProofFrog/ProofFrog/releases/tag/v0.5.0)** featuring a large new case study (machine-checked proofs of the [CFRG hybrid KEM combiners](https://datatracker.ietf.org/doc/html/draft-irtf-cfrg-hybrid-kems-10) and a Hashed ElGamal KEM), new FrogLang features for random-oracle and group-based proofs (lazy-map random oracles, collection iteration, sampling with exclusions, and a `requires:` block), expanded canonicalization power, and several engine correctness fixes - Jun. 7, 2026: Release of [ProofFrog VS Code Extension version 0.1.1](https://marketplace.visualstudio.com/items?itemName=ProofFrog.prooffrog) on VS Code Extension Marketplace - **Apr. 16, 2026: Release of [ProofFrog version 0.4.1](https://github.com/ProofFrog/ProofFrog/releases/tag/v0.4.1)** featuring proof engine improvements