Perfect hiding of the Pedersen commitment scheme #
A transliteration of section PedersenSecurity in EasyCrypt's examples/Pedersen.ec, kept as
close to the original as the DSL allows. EC, in full:
local module FakeCommit(U:Unhider) = {
proc main() : bool = {
var b, b', x, h, c, d;
var m0, m1 : exp;
(* Clearly, there are many useless lines, but their presence helps for the proofs *)
x <$ dt; h <- g^x; (m0, m1) <@ U.choose(h);
b <$ {0,1}; d <$ dt; c <- g^d; (* message independent - fake commitment *)
b' <@ U.guess(c);
return (b = b');
}
}.
local lemma hi_ll (U<:Unhider):
islossless U.choose => islossless U.guess => islossless FakeCommit(U).main.
local lemma fakecommit_half (U<:Unhider) &m:
islossless U.choose => islossless U.guess =>
Pr[FakeCommit(U).main() @ &m : res] = 1%r/2%r.
local lemma phi_hi (U<:Unhider) &m:
Pr[HidingExperiment(Pedersen,U).main() @ &m : res] = Pr[FakeCommit(U).main() @ &m : res].
lemma pedersen_perfect_hiding (U<:Unhider) &m:
islossless U.choose => islossless U.guess =>
Pr[HidingExperiment(Pedersen,U).main() @ &m : res] = 1%r/2%r.
Status. All four EC lemmas are proven, on standard axioms, except for one framework fact:
hidingGame_self_glob, the glob adversary rule. Everything cryptographic is closed; see that
theorem for exactly what is missing and where it belongs.
The point of this rewrite is that the theorems are about HidingExperiment and FakeCommit
as modules, exactly as EC states them. The previous version stated its results about
hand-inlined ProgramDenotations (realGame/fakeGame), which left the final theorem saying
nothing about HidingExperiment at all — the inlining was never justified against the module.
That justification is now hidingGame_inline/fakeGame_inline.
Deviations from EC, all forced and all local:
(m0, m1) <@ U.choose(h)becomes a pair-typed localmm— tuple assignment of locals does not elaborate (the ⚠ note inCommitment.lean). EC never readsm0/m1inFakeCommitanyway.- EC's
&m(an initial memory) becomes an explicitσ : State.
={glob U} is not a deviation: it is GlobEq below, which is exactly EC's notion — see the
comment there.
EC vocabulary #
Two abbreviations so the statements below read like the EC ones. Both are pure notation: they
unfold to the spellings already used in pedersen_correctness.
EC's Pr[M.main() @ σ : res] — the probability that a Bool-returning, argument-less
module procedure returns true, started in σ.
Equations
Instances For
The event res as a wp postcondition.
Equations
- GaudisCrypt.Examples.Pedersen.resIndicator = {r : Bool × GaudisCrypt.State | r.1 = true}.indicator fun (x : Bool × GaudisCrypt.State) => 1
Instances For
Pr as a wp — the bridge EC's byphoare/byequiv cross implicitly. wp p F σ is
(p σ).expected F definitionally, so this is expectation_indicator at c = 1.
EC's islossless P — P terminates with probability 1, from any state, on any argument.
Real content under a sub-probability semantics: a diverging adversary would make
fakecommit_half an inequality.
Equations
- GaudisCrypt.Examples.Pedersen.IsLossless p = ∀ (args : sig.ParamType) (σ : GaudisCrypt.State), (GaudisCrypt.procedureDenotation p args).wp (fun (x : sig.ret × GaudisCrypt.State) => 1) σ = 1
Instances For
EC's glob A, for a whole module A — the getter reading everything A may touch.
FVP.fvP A : Footprint State is the computed footprint of the module (FV.lean; it
decomposes over a moduletype's fields by FVP.fvP_pair), and Footprint.touched_getter
quotients the state by the complement footprint, so two states read equal exactly when they
differ only outside A — see Footprint.touched_getter in Language/Footprint.lean, whose
docstring names this as EC's glob.
Equations
Instances For
EC's ={glob A}. That this is the right notion is not a definition but a theorem:
Footprint.indistinguishable_of_touched_getter_eq says glob-equal states are separated by no
A-test, and Footprint.touched_getter_get_eq_of_mem says writes outside A preserve it.
Equations
- GaudisCrypt.Examples.Pedersen.GlobEq A σ₁ σ₂ = ((GaudisCrypt.Examples.Pedersen.glob A).get σ₁ = (GaudisCrypt.Examples.Pedersen.glob A).get σ₂)
Instances For
The two games #
HidingExperiment is declared in Commitment.lean (it is generic in the scheme, as in EC);
FakeCommit is EC's local module, transcribed line for line — including the "useless" h <- g^x
and c <- g^d, which EC keeps deliberately so that the two games line up statement by statement
for the relational proof.
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
HidingExperiment(Pedersen, U).main — the real game, as a module.
Equations
Instances For
FakeCommit(U).main — the fake game, as a module.
Equations
Instances For
Inlining (EC's inline*) #
The prhl2 rules consume >>=-chains, but a module procedure is a procWrap over a
programDenotation on its own local-state type — and the two games do not even have the same
locals (five against seven). These two lemmas are EC's inline*: each game as a module equals
a bind chain on State, with the adversary calls left as opaque denotations. Proven by
SubProbability.ext_of_expected, i.e. by checking the wp at an arbitrary postcondition, which
is the same reduction fakecommit_half runs.
FakeCommit(U).main, inlined.
HidingExperiment(Pedersen, U).main, inlined. Pedersen's own gen/commit are inlined too
(their internal samplings become the x and d draws), via wp_gen/wp_commit.
The algebraic heart of the coupling — EC's closing algebra: the real commitment at opening
key d is the fake one at d + x * m. g^d * (g^x)^m = g^d * g^(x*m) = g^(d + x*m).
EC's coupling argument, at equal initial states — the content of EC's
proc; inline*. call (_:true); wp;
rnd (fun d, (d + x * (b?m1:m0)){2}) (fun d, (d - x * (b?m1:m0)){2});
by wp; rnd; call (_: true); auto => />; progress; algebra.
Read bottom-up: couple the x draws by the identity, run U.choose on both sides (same program,
same argument — prhl2.refl), couple the coins by the identity, then couple the two d draws
by the translation d ↦ d + x * (b ? m1 : m0), under which commit_shift makes the real and
fake commitments coincide, and finally run U.guess on what is by then literally the same
argument.
The rcases eq_or_ne steps are bookkeeping EC does not need: a mid-condition of the form
x₀ = x₁ ∧ τ₁ = τ₂ has to be turned into an actual substitution before the two sides are
syntactically the same program.
The statements #
EC's four lemmas, in EC's order.
EC's
local lemma hi_ll (U<:Unhider):
islossless U.choose => islossless U.guess => islossless FakeCommit(U).main.
EC discharges this with islossless; (apply dt_ll || apply DBool.dbool_ll) — the game is a
straight-line composition of two lossless samplings and two lossless adversary calls.
EC's
local lemma fakecommit_half (U<:Unhider) &m:
islossless U.choose => islossless U.guess =>
Pr[FakeCommit(U).main() @ &m : res] = 1%r/2%r.
EC: byphoare; proc; wp; swap 4 3; rnd (pred1 b'); call ug_ll; wp; rnd; call uc_ll; auto.
The swap 4 3 moves the coin b past d and c so that it is drawn after U.guess has
fixed b'; a fresh fair coin then matches b' with probability exactly 1/2.
The one open proof: the glob adversary rule, at the whole game — two runs of the same
game from ={glob U} states agree on the result and stay ={glob U}.
This is the only place ={glob U} (rather than plain equality) is doing work, and it is a
framework fact, not a Pedersen one. The rule that discharges it is prhl2_self_of_orbit
(Lib/RO/GlobTransfer.lean — generic, despite the file): a program confined to F
self-couples across any zig-zag of Fᶜ-updates, and its orbit precondition is literally what
GlobEq unfolds to under Quotient.exact.
What is missing to feed it is (procedureDenotation A args).inFootprint (FVP.fvP_proc A),
which is not stated anywhere: the ingredients exist (procedureDenotation_inFootprint_reduce,
fvP_stmt_le_FVP, inFootprint_selfRange, and FVP.fvP_proc being exactly that
globalL-reduction) but are only ever assembled into the RO-specific
fvP_proc_le_roLift_compl. That lemma belongs next to FVP.fvP_proc in FV.lean.
The relational judgment behind EC's phi_hi — what byequiv reduces that lemma to:
equiv[ HidingExperiment(Pedersen,U).main ~ FakeCommit(U).main : ={glob U} ==> ={res} ]
Assembled the way Lib/RO/GlobTransfer.lean assembles its endpoint: relax the precondition from
Eq to ={glob U} by composing the same-program glob rule with the coupling proper,
real σ₁ ~[glob rule]~ real σ₂ ~[EC's coupling]~ fake σ₂
so that all the cryptographic content lives in phi_hi_equiv_eq and all the framework
content in hidingGame_self_glob.
EC's
local lemma phi_hi (U<:Unhider) &m:
Pr[HidingExperiment(Pedersen,U).main() @ &m : res] = Pr[FakeCommit(U).main() @ &m : res].
i.e. byequiv applied to phi_hi_equiv. relE.wp_eq is the byequiv bridge; the observable
resIndicator depends only on the result, so ={res} alone transfers it, and GlobEq.refl
supplies the precondition at the single memory σ (EC's &m against itself).
Perfect hiding. EC's
lemma pedersen_perfect_hiding (U<:Unhider) &m:
islossless U.choose => islossless U.guess =>
Pr[HidingExperiment(Pedersen,U).main() @ &m : res] = 1%r/2%r.
proof. by move => uc_ll ug_ll; rewrite (phi_hi U &m) (fakecommit_half U &m). qed.