Conversation
…es, examples. Stages 4-6 of enabling (a*b)^x = a^x * b^x: core/public.v, the HeapLang primitives, lib/dh.v and the case studies. Lemmas whose base must now be an atom gained negb (is_mul _) / negb (is_inv _) premises; public_TExp, TExpA, TExpK, TExp_TMulN, TExp_TInv, minted_base_exps and twp_texp stay unconditional. New factor-level API, for protocols that exponentiate an attacker-supplied value and so cannot assume an atomic base: algebra.v is_inv_TExp, TExp_injl, invs_canceled_TExp, factors_TExp subterms.v subterm_factors, subterm_TExp_factors public.v public_TExp_factors The OPAQUE server exercises all of them. It also needs a group-membership check it never had: 1 ^ x = 1 drops the server's ephemeral secret out of the session key, so Server.session now rejects an identity X_u -- the check its own TODO was already asking for. CLAUDE.md records the endomorphism law, the atomic-base wf invariant, and both downstream consequences. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01E8khwa8zca1fMdMbwHLikG
PTMul is replaced by PTN of term_opN & list pre_term, mirroring PT0/PT1/PT2. term_opN currently has the single constructor ONMul, with the same derived eqType/choiceType/countType/orderType instances as the other operation types, and PTMul ts becomes a Notation for PTN ONMul ts (alongside PTInv/PTExp). Keeping PTMul as a notation means product-specific matches read as before and, once term_opN gains a constructor, become non-exhaustiveness errors rather than silently taking the product branch. The HeapLang encoding follows the arities too: outer TOpN_tag = 3, inner TMul_tag = 0, PTN o ts represented as (#TOpN_tag, (repr o, repr_list ...)). eq_term, leq_term, hl_is_mul, hl_one, hl_factors and hl_mul_aux are updated accordingly, with eq_term_opN / leq_term_opN and their specs. Order plumbing: leqE's PTN case compares the operation first, as PT1/PT2 do; with_stdpp.v gains int_of_term_opN / opN_le / opN_leE, and pt_order_mul becomes pt_order_N, quantified over the operation. Case patterns in the n-ary branch now destruct the operation -- [] rather than a binder, so is_mul and friends keep reducing as before, and a second n-ary operation fails loudly. Structural functions that ignore the operation (height, tsize, nonces_of_pre_term) match on PTN _ ts; product-specific ones (is_mul, factors, wf, normalize) stay on PTMul. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01E8khwa8zca1fMdMbwHLikG
`TMulN`/`TInv` served both as the Diffie-Hellman group operation (in the
base of `TExp`) and as the exponent operation. Those two roles cannot
share a carrier: with one structure, `a^1 = a`, `(a*b)^x = a^x*b^x` and
`(a^x)^y = a^(x*y)` together say that `x |-> (_^x)` is a monoid
homomorphism `(G,*) -> End(G) = (Z_n,x)`, i.e. a group homomorphism
`psi : G -> Z_n*`. Its image has order dividing `gcd(n, phi(n))`, and
`psi` is trivial on any large prime-order subgroup -- so in any group
where DLP is hard, the axioms force `a^x = a` and exponentiation
degenerates to the identity.
So give the two roles separate operations:
- `GMul`/`GInv` (`O1GInv`, `ONGMul`; `TGMulN`, `TGMul`, `TGInv`) --
the DH group, a symbolic model of a prime-order elliptic-curve
group. Validates `(a*b)^x = a^x*b^x`, `1^x = 1`,
`(a^-1)^x = (a^x)^-1`, and the abelian-group laws.
- `Mul`/`Inv` -- keep their names and the exponent laws:
`(g^a)^b = g^(a*b)`, `g^1 = g`, `(g^a)^(a^-1) = g`.
`TExp : G -> E -> G` now takes a group element and a scalar, so the
degeneracy argument no longer applies. A scalar product or scalar
inverse in a base is an atom: `(a*b)^x` does not distribute.
The group stack is a parallel copy of the exponent stack at the other
operation pair, reusing `SMS` at `(pt_order, ginv_aux)`. `exp` is
retargeted rather than rewritten: it distributes over `gfactors` and
pushes through `PTGInv`, while still merging exponents with the scalar
`mul`. `is_non_free` splits in two: the five heads `TNonFree`
represents, and the three `wf` forbids in an exponential base
(`is_gnon_free`). `is_mul_base`/`is_inv_base` become false and are
replaced by `is_gmul_base`/`is_ginv_base`, since `wf (PTExp (PTMul ts) e)`
is now legal.
`public` treats the group product and inverse exactly as it treats the
exponent ones: `decompose` gains `DGInv`, `public_pre_aux` gains an
`is_gmul` disjunct, and `public_TGInv`/`public_TGMulN`/`public_gfactors`
mirror their scalar counterparts. `primitives/attacker.v` exposes
`add_gmul`, `add_ginv` and `add_gmul_unit`, so the symbolic attacker can
build group products and inverses.
In OPAQUE, the identity the server rejects is now the *group* identity.
Four behavioural checks record what the split buys: `TExp_TGMulN`,
`TExp_TGInv`, `TExp_gunit`, and -- the negative one -- `tsize_TExp_TMulN`,
which says a scalar product in a base is a genuine atom.
All ten `*_secure` / `game_secure` theorems still report "Closed under
the global context".
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01E8khwa8zca1fMdMbwHLikG
`examples/opaque/impl.v` carried a `TODO: use the key exchange formula
from the OPAQUE paper`; `KE` hashed two independent DH values. OPAQUE
(Jarecki, Krawczyk and Xu, Eurocrypt 2018) instantiates its AKE with
HMQV, whose key is a single group element mixing static and ephemeral
keys:
d = H(X_u, IdS) e = H(X_s, IdU)
client: K = (X_s · P_s^e)^(x_u + d·p_u)
server: K = (X_u · P_u^d)^(x_s + e·p_s)
That needs a group product, which the term algebra only gained with the
GMul/GInv split, and an exponent sum, which it does not have. The sum
is avoidable: exponentiation distributes over the group product, so
`Y^(x + c)` becomes `Y^x · Y^c`. `KE` now takes the two multipliers as
parameters, so one definition serves both roles -- the client passes
`(d, e)` and the server `(e, d)` -- and `d`/`e` bind the ephemeral to the
peer's static public key, standing in for the paper's identities.
`hmqv_K_sym` records that both roles compute the same group element; the
expansion is the four-factor product
g^(x_s·x_u) · g^(p_s·e·x_u) · g^(x_s·d·p_u) · g^(p_s·e·d·p_u).
Secrecy. `public_gfactors` makes a group product public exactly when all
its group factors are, so one secret factor suffices. Both roles use the
static-static factor: the client has `opaque_public_private_pair p_u P_s`
from the envelope, the server `opaque_public_private_pair p_s P_u` from
its file. Two new pieces make that work:
- `gcount_TExp_eq0` (core/term/tsize.v) -- the occurs check. If an
exponent of `w` is bigger than all of `X`, no group factor of `X^c`
is `w` or its inverse. This is HMQV's own argument: the multiplier
`m_b` is a hash of the peer's ephemeral `X_b`, hence strictly bigger,
so `X_b` cannot contain it, and the attacker cannot cancel the
static-static factor out.
- `public_dh_secret_gen` (examples/iso_dh/proofs/base.v) -- the
`exps`-membership form of `public_dh_secret2`. The static-static
factor has four exponents, two of them public hash multipliers, so a
lemma concluding "some exponent is public" would be vacuous;
`exp_pred_inv_gen` already takes an arbitrary sublist of `exps`, so
instantiating at `[p_u; p_s]` skips the hashes.
`hmqv_key_gfactors` packages both group-factor memberships and the two
`exps` memberships the roles need. The server's freshness argument rides
on the second factor, `g^(p_u·d·x_s)`, by the same occurs check.
Both roles still prove exactly today's `SK_result`: `public SK <-> |>[]False`
and `SK` not in the fresh set. `game.v` is unchanged.
In OPAQUE the identity the server rejects stays the group identity, but
the check is no longer load-bearing -- the static-static factor survives
any `X_u`.
Also adds `all_minted_TMulN` / `all_minted_TGMulN` (with the `nonces`
subset lemmas they need) and moves `mem_factors_TMulN2` from `public.v`
to `algebra.v`, where `tsize.v` can reach it.
All ten `*_secure` / `game_secure` theorems and OPAQUE's `wp_game` still
report "Closed under the global context".
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01E8khwa8zca1fMdMbwHLikG
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
1 participant
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.
No description provided.