Concrete UC Emulation #
UC emulation in which the environment's distinguishing advantage is bounded by
a function of the adversary and of the environment, in the style of concrete
security (EasyCrypt, EasyUC: Canetti, Stoughton, Varia, CSF 2019). A bound
such as bound A Z = DDH_Advantage (B A Z), for an explicit reduction B,
constrains every adversary and environment individually.
UCEmulates ε bounds sdist, the supremum over all distinguishers. The
concrete form is pointwise: UCEmulatesC with a constant bound is exactly
UCEmulates (UCEmulatesC_const_iff), so statistical results embed.
Main definitions #
Env— an environment for a Kleisli morphismα → SPComp β: an input, an initial heap and a distinguisher.Env.gap— the distinguishing gap of one environment between two morphisms.DistC f g bound— the gap of every environmentZis at mostbound Z.UCEmulatesC spec π F bound— for every adversaryAthere is a simulatorSwhose ideal run isbound A-close to the real run withA.UCEmulatesCSim spec π F sim bound— the same with the simulator given by an explicit mapsimfrom adversaries to simulators.fixHeap,PureGame,GameAdvBoundC,gameUCBound,UCFromGameC— the route from a concrete game bound to concrete UC emulation.
Main results #
DistC_const_iff,UCEmulatesC_const_iff,UCEmulatesCSim_const_iff— constant bounds are the numeric notionssdist ≤ ε,UCEmulates ε,UCEmulatesAlg ε.DistC.comp_right,DistC.comp_left,DistC.mapSum,DistC.triangle— post-processing, pre-composition, parallel composition, game hops, with the reductions visible in the bound.UCEmulatesCSim.trans— transitivity, the second bound evaluated at the simulator produced by the first.UCEmulatesCSim_compile,UCEmulatesCSim_par— concrete subroutine and parallel composition.DistC_of_isPure_advantageA,ucFromGameC_of_pure_adv— concrete game bound to concrete UC emulation, withS = A.
Simulator quantifier #
UCEmulatesCSim records the simulator as a map sim of the adversary; it is
the primary form because transitivity evaluates the second bound at the
simulator of the first (b₂ (sim₁ A)), which cannot be named when the
simulator is only existential. UCEmulatesC keeps Canetti's ∀ A ∃ S shape
and is equivalent to ∃ sim, UCEmulatesCSim … sim …
(UCEmulatesC_iff_exists_sim).
Environment #
The environment is the triple of input, initial heap and distinguisher, the
three quantities over which sdist takes its supremum. A bound may depend on
all three: the IND-CPA reduction to DDH embeds the environment's messages.
Environments and concrete distance #
An environment for Kleisli morphisms α → SPComp β: it chooses the input,
the initial heap, and the distinguisher run on the output.
- input : α
Input fed to the morphism.
- heap : Core.Heap
Initial heap.
- dist : β → Core.SPComp Bool
Distinguisher run on the output.
Instances For
Distinguishing gap of the environment Z between f and g.
Equations
- CatCrypt.Crypto.UCConcrete.Env.gap f g Z = CatCrypt.Crypto.absDiff (CatCrypt.Crypto.prTrue ((f Z.input).bind Z.dist) Z.heap) (CatCrypt.Crypto.prTrue ((g Z.input).bind Z.dist) Z.heap)
Instances For
Concrete distance: every environment Z distinguishes f from g with
gap at most bound Z.
Equations
- CatCrypt.Crypto.UCConcrete.DistC f g bound = ∀ (Z : CatCrypt.Crypto.UCConcrete.Env α β), CatCrypt.Crypto.UCConcrete.Env.gap f g Z ≤ bound Z
Instances For
The environment Z precomposed with the post-processing k: same input
and heap, distinguisher k followed by Z.dist. This is the reduction
used by the right post-processing lemma.
Equations
Instances For
Every morphism has concrete distance 0 from itself.
Symmetry.
Right post-processing: running k after both morphisms is bounded by the
bound of the environment that runs k inside its distinguisher.
Pre-composition with a common computation: the bound is the supremum of the continuation bound over intermediate values and heaps, with the distinguisher unchanged.
Case split of a bound on sum-typed environments: an environment on input
.inl a is sent to the left bound with the distinguisher restricted to
.inl, and symmetrically on the right.
Equations
- CatCrypt.Crypto.UCConcrete.Env.sumCase b₁ b₂ { input := Sum.inl a, heap := h, dist := D } = b₁ { input := a, heap := h, dist := fun (y : β₁) => D (Sum.inl y) }
- CatCrypt.Crypto.UCConcrete.Env.sumCase b₁ b₂ { input := Sum.inr a, heap := h, dist := D } = b₂ { input := a, heap := h, dist := fun (y : β₂) => D (Sum.inr y) }
Instances For
Parallel composition on Sum: each input activates one component, so the
bound is the component bound of the activated side.
Concrete UC emulation #
Concrete UC emulation: for every adversary A there is a simulator S
such that every environment Z distinguishes the real run of π with A
from the ideal run of F with S with gap at most bound A Z.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Concrete UC emulation with the simulator given by the map sim.
Equations
- One or more equations did not get rendered due to their size.
Instances For
An explicit simulator map yields concrete UC emulation.
∀ A ∃ S is equivalent to the existence of a simulator map.
A constant concrete bound is numeric UC emulation.
A constant concrete bound with an explicit simulator map is algebraic UC emulation.
Monotonicity in the bound.
Monotonicity in the bound, simulator map fixed.
Reflexivity with the identity simulator map and bound 0.
Transitivity: the simulator maps compose, and the second bound is evaluated at the simulator produced by the first.
Transitivity of the existential form when the second bound does not depend on the adversary.
Same interface (composition plumbing): a concrete distance between π
and F gives concrete UC emulation with the adversary as simulator; the
bound runs the adversary inside the environment's distinguisher.
Subroutine and parallel composition #
Concrete subroutine composition: replacing π by F and ρ_real by
ρ_ideal costs the subroutine bound, taken at the intermediate values
and heaps with the distinguisher restricted to .inr, plus the protocol
bound at the environment that runs ρ_ideal inside its distinguisher.
Concrete UC subroutine composition (composition plumbing), same interface with the adversary as simulator.
Concrete UC parallel composition (composition plumbing): the output of
mapSum π₁ π₂ is exposed on the adversary channel, and each environment is
charged the bound of the component its input activates.
Concrete game route #
The distinguisher D with its initial heap fixed to h₀: it ignores the
heap it is run on. For a heap-independent game G, running D after G
from h₀ equals running fixHeap h₀ D after G from Heap.empty.
Equations
- CatCrypt.Crypto.UCConcrete.fixHeap h₀ D b x✝ = D b h₀
Instances For
Concrete distance from a per-distinguisher advantage bound on
heap-independent games: the environment Z is charged the game bound at
its input and its distinguisher with the heap fixed to Z.heap.
A family of heap-independent games.
- isPure (x : hon) : (G x).IsPure
Instances
Concrete game bound: the advantage of every distinguisher D on input x
is at most bound x D, where bound is typically the advantage of an
explicit reduction built from D against a primitive.
bound is an explicit index, fixed by the goal.
Instances
The distinguisher that the game bound receives from adversary A and UC
environment Z: run A on the game output, pass its view to Z.dist on
the adversary channel, with the heap fixed to Z.heap.
Equations
- CatCrypt.Crypto.UCConcrete.envReduction A Z = CatCrypt.Crypto.UCConcrete.fixHeap Z.heap fun (o : leak) => (A o).bind fun (v : V) => Z.dist (Sum.inr v)
Instances For
UC bound induced by a concrete game bound: the game bound at the
environment's input and at envReduction A Z.
Equations
- CatCrypt.Crypto.UCConcrete.gameUCBound bound A Z = bound Z.input (CatCrypt.Crypto.UCConcrete.envReduction A Z)
Instances For
Running a game wrapped by UCProtocol.ofGame, then the adversary, then a
distinguisher, is running the game followed by the adversary and the
distinguisher on the adversary channel.
Concrete UC emulation of a game pair from heap-independence and a concrete
game bound (composition plumbing, simulator S = A).
Concrete UC emulation of UCProtocol.ofGame G_real by
UCProtocol.ofGame G_ideal with view type V, simulator S = A, and the
bound induced by the game bound bound.
- uc : UCEmulatesCSim (UCDSL.UCSpec.ofGame hon leak V) (UCDSL.UCProtocol.ofGame G_real) (UCDSL.UCProtocol.ofGame G_ideal) id (gameUCBound bound)
Instances
Heap-independent games with a concrete game bound give concrete UC emulation (composition plumbing).