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.
One deviation from EC, forced and local: EC's &m (an initial memory) becomes an explicit
σ : VariableAssignment (the globals).
={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.VariableAssignment | r.1 = true}.indicator fun (x : Bool × GaudisCrypt.VariableAssignment) => 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
- One or more equations did not get rendered due to their size.
Instances For
EC's glob A, for a whole module A — the getter reading everything A may touch.
FVP.fvP A : Footprint VariableAssignment 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.
The module declared by module FakeCommit, abstracted over its single parameter U, which it takes as one right-nested tuple: Module.Arr (T₁ ×ₘ (… ×ₘ Tₙ)) M, with M the anonymous product of the procedures' own types, the declaration naming no module type.
Applied to such a tuple it is the record of its procedures FakeCommit.main, each applied to the parameters that procedure itself uses — which is what the @[simp] lemma FakeCommit.apply_simp says.
Equations
Instances For
@[simp]: applying FakeCommit.main to the parameters proc main uses (U) is Module.proc (FakeCommit.main.procedure.instantiate …) — the procedure with its holes filled by the callees they were made from, each written as it was in the body (with the arguments in place of the module parameters) and turned into a Procedure by Module.Proc.procedure.
Instantiating the holes of FakeCommit.main.procedure with a tuple holeArgs of procedures: the body of proc main as written, with each hole call replaced by the matching holeArgs.lookup (HoleIndex.zero being the first hole the body declared). True by rfl.
Deliberately not @[simp], unlike the other apply_simp lemmas: its right-hand side is the whole body written out, so letting it fire on its own would turn any goal mentioning an instantiated procedure into that body. Inlining a procedure is a step to ask for by name (simp [FakeCommit.main.procedure.apply_simp]).
@[simp]: applying FakeCommit to a tuple of its single parameter U — the record of its procedures FakeCommit.main, each applied to the parameters it uses.
This is the lemma that unfolds a module use: simp rewrites with it, then with the field lemmas of the module type (N.f.mk_simp) to get at the one procedure the goal is about, and then with FakeCommit.main.apply_simp to fill that procedure's holes.
proc main of module FakeCommit as a module, abstracted over the module parameters it uses (U, in declaration order): Module.Arr … (Module.Proc (procsig …)).
Apply it with the @[simp] lemma FakeCommit.main.apply_simp, which fills the holes of FakeCommit.main.procedure with the callees the body called.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The body of proc main of module FakeCommit, as a procedure of its own: the 2 calls it makes to module parameters (U) are its holes, in the order the body makes them.
A hole stands for a call whose callee is not known here — a module parameter is supplied only when the module is applied — so the body is a ProcedureWithHoles, to be instantiated (see FakeCommit.main.procedure.apply_simp) rather than run. Use FakeCommit.main for this procedure as a module.
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
- One or more equations did not get rendered due to their size.
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 the program state, globals and its own frame of locals — and the two games
do not even have the same locals (seven against eight, differently typed). These two lemmas are
EC's inline*: each game as a module equals
a bind chain on the globals, 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.