Repository navigation
Conversation
bgregoir
marked this pull request as draft
November 10, 2026 18:08
…ting Following mathcomp (algebra/poly.v), with `peval` for `horner` and `deg` (degree + 1) for `size`: - PolyComRing: evaluation lemmas (pevalC, pevalD, pevalM, peval_exp, pevalXsubC, ...), the remainder theorem (peval_factor), root lemmas (root0, rootC, rootX, rootN, root_XsubC), factor_theorem, divisibility of polynomials (clone of Ideal.IdealComRing) and root_factor_theorem; - Poly (integral domain): rootM, rootZ, factor_theorem_deg, roots_finite, max_poly_roots, and the probability that a nonzero polynomial vanishes at a sampled point (mu_root_le, mu_root_uni). PolyReduce reuses the divisibility clone inherited from PolyComRing instead of its own copy.
This was referenced Nov 10, 2026
…FC 8439 poly1305_prime.ec: 2^130 - 5 is prime, by a chain of Pocklington certificates. poly1305_field.ec: polynomials over Z/(2^130 - 5). poly1305_msg.ec: the Poly1305 message polynomial of RFC 8439 and its injectivity. poly1305_clamp.ec: for r made of 16 uniform bytes and clamped as in RFC 8439, each value of r has probability at most 2^-106 (dr1E). For distinct (a, c) of valid sizes, the difference of the two message polynomials evaluated at r hits a given field element with probability at most max(nblocks)/2^106 (pr_topol_diff), and a given difference modulo 2^128 with probability at most 8 * max(nblocks)/2^106 (pr_tag_diff). chacha_poly_rfc.ec clones chacha_poly.ec with the Poly1305 polynomial over Z/(2^130 - 5), tags modulo 2^128 and the RFC 8439 sizes, and proves the axioms topol_inj, pr_zeropol_spec, ge0_pr_zeropol and poly_out_*. Bytes stay abstract, with to_uint/of_uint and three axioms. chacha_poly.ec: the proof clause of the TPoly clone named the axiom before renaming and was dropped, leaving ge0_poly_size an axiom (EasyCrypt issue #1236); realize it after the clone instead.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Stacked on #1233 (Pocklington, itself on #1238), and depends on #1232 (root counting in
Poly.ec), whose commit is included here until it is merged; only the last commit is new.Replaces the Poly1305 axioms of the ChaCha20-Poly1305 example by proofs.
examples/ChaChaPoly/poly1305_prime.ec,poly1305_field.ec,poly1305_msg.ec(moved from #1233)prime_p1305 : prime (2^130 - 5), as a chain of 9 Pocklington certificates checked bycbv delta hint +powmod +gcd;Z/(2^130 - 5)and its polynomial ring;le(b) + 2^128), its degree, and its injectivity (topol_inj) for lengths< 2^64.examples/ChaChaPoly/poly1305_clamp.ec(abstract theoryClamp, parameterised by a byte distribution withmu1 = 1/256)r; each clamped value has probability at most 2^-106 (dr1E).pr_topol_diff: for distinct(a, c)of valid sizes,Pr_r[P2(r) - P1(r) = t] <= max(nblocks)/2^106(viamu_root_le).pr_tag_diff: the same difference modulo 2^128 is hit with probability at most8 * max(nblocks)/2^106.examples/ChaChaPoly/chacha_poly_rfc.ecchacha_poly.ecwith the polynomial over Z/(2^130 - 5), tags modulo 2^128, a 32-bit counter, and maximal sizesmax_ad/max_cipherfor the associated data and the ciphertext, as parameters within the RFC 8439 limits (max_ad_rg,max_cipher_rg); the bound grows linearly with them.topol_inj,pr_zeropol_spec,ge0_pr_zeropoland the fourpoly_out_*axioms;pr_zeropol = 8 * max_nblocks / 2^106andpr1_poly_out = 2^-128.to_uint_rg,to_uint_inj,of_uintK; the finite type of bytes is built from them (enumdefined,enum_specproved).chacha_poly_rfc_security: for a nonce-respecting adversary,|Pr[real] - Pr[IdealAEAD]| <= |Pr[ChaCha20] - Pr[random function]| + qdec * 8 * max_nblocks / 2^106 + qdec / 2^128.examples/ChaChaPoly/chacha_poly.ecge0_poly_sizeaxiom of theTPolyclone is now realized (its proof clause was silently dropped because of therename, see clone: proof clause on a renamed axiom is checked but the axiom remains #1236).IdealAEAD: the ideal oracles as a single module (random ciphertexts and tags, decryption only of the ciphertexts returned by encryption), equal toCCA_CPA_AdvaroundEncRnd(CCA_CPA_IdealAEAD);conclusion_idealrestatesconclusionwith it.conclusion_ideal_abs: the same bound on the absolute value of the advantage, by applyingconclusion_idealto the adversary that negates its output (with losslessness of the four games).