Permalink
Browse files

sem-sec: generalize, cleanup...

  • Loading branch information...
1 parent c26185b commit cc47d7929628252cf2e2febb7f04010c7780ebd8 @np np committed May 24, 2012
Showing with 220 additions and 128 deletions.
  1. +2 −0 flipbased.agda
  2. +120 −58 one-time-semantic-security.agda
  3. +85 −61 otp-sem-sec.agda
  4. +11 −7 program-distance.agda
  5. +2 −2 vcomp.agda
View
@@ -22,6 +22,8 @@ module flipbased
(join↺ : ∀ {n₁ n₂ a} {A : Set a} → ↺ n₁ (↺ n₂ A) → ↺ (n₁ + n₂) A)
where
+Coins =
+
-- If you are not allowed to toss any coin, then you are deterministic.
Det : {a} Set a Set a
Det =0
@@ -3,94 +3,156 @@ module one-time-semantic-security where
open import Function
open import Data.Nat
open import flat-funs
-open import Data.Vec using (splitAt)
+open import Data.Vec using (splitAt; take; drop)
open import program-distance
open import Data.Bits
open import flipbased-implem
open import Data.Product
open import Relation.Binary.PropositionalEquality
-module AbsSemSec (|M| |C| : ℕ) {t} {T : Set t}
+record EncParams : Set where
+ constructor mk
+ field
+ |M| |C| |R|e : ℕ
+
+ M = Bits |M|
+ C = Bits |C|
+ Re = Bits |R|e
+
+ -- The type of the encryption function
+ Enc : Set
+ Enc = M ↺ |R|e C
+
+module AbsSemSec {t} {T : Set t}
(♭Funs : FlatFuns T) where
open FlatFuns ♭Funs
- M = `Bits |M|
- C = `Bits |C|
-
- record AbsSemSecAdv (|R| : Coins) : Set where
+ record SemSecAdv (ep : EncParams) |R|a : Set where
constructor mk
+ open EncParams ep hiding (M; C; Re)
+
field
{|S|} : ℕ
- S = `Bits |S|
- R = `Bits |R|
+ M = `Bits |M|
+ C = `Bits |C|
+ Re = `Bits |R|e
+ S = `Bits |S|
+
+ -- Randomness adversary
+ Ra = `Bits |R|a
field
- step₀ : R `→ (M `× M) `× S
+ step₀ : Ra `→ (M `× M) `× S
step₁ : C `× S `→ `Bit
- SemSecReduction : (f : Coins Coins) Set
- SemSecReduction f = {c} AbsSemSecAdv c AbsSemSecAdv (f c)
+ open EncParams ep public hiding (M; C; Re)
--- Here we use Agda functions for FlatFuns.
-module FunSemSec (prgDist : PrgDist) (|M| |C| : ℕ) where
- open PrgDist prgDist
- open AbsSemSec |M| |C| fun♭Funs
- open FlatFunsOps fun♭Ops
+ SemSecReduction : ep ep' (f : Coins Coins) Set
+ SemSecReduction ep ep' f = {c} SemSecAdv ep c SemSecAdv ep' (f c)
- M² = Bit M
- Enc : cc Set
- Enc cc = M ↺ cc C
- Tr : (cc₀ cc₁ : Coins) Set
- Tr cc₀ cc₁ = Enc cc₀ Enc cc₁
+-- Here we use Agda functions for FlatFuns.
+module FunSemSec (prgDist : PrgDist) where
+ open PrgDist prgDist
+ open AbsSemSec fun♭Funs
+ open FlatFunsOps fun♭Ops
- FunSemSecAdv : Coins Set
- FunSemSecAdv = AbsSemSecAdv
+ module FunSemSecAdv {ep : EncParams} {|R|a} (A : SemSecAdv ep |R|a) where
+ open SemSecAdv A public
- module FunSemSecAdv {|R|} (A : FunSemSecAdv |R|) where
- open AbsSemSecAdv A public
+ M² = Bit M
- step₀F : R (M² × S)
+ step₀F : Ra (M² × S)
step₀F = step₀ >>> proj *** idO
- step₀↺ : ↺ |R| (M² × S)
+ step₀↺ : ↺ |R|a (M² × S)
step₀↺ = mk step₀F
step₁F : S C Bit
step₁F s c = step₁ (c , s)
- -- Returing 0 means Chal wins, Adv looses
- -- 1 means Adv wins, Chal looses
- runSemSec : {cc ca} (E : Enc cc) (A : FunSemSecAdv ca) b ↺ (ca + cc) Bit
- runSemSec E A b
- = A-step₀ >>= λ { (m , s) map↺ (A-step₁ s) (E (m b)) }
- where open FunSemSecAdv A renaming (step₀↺ to A-step₀; step₁F to A-step₁)
-
- _⇄_ : {cc ca} (E : Enc cc) (A : FunSemSecAdv ca) b ↺ (ca + cc) Bit
- _⇄_ = runSemSec
-
- runAdv : {|R|} FunSemSecAdv |R| C Bits |R| (M × M) × Bit
- runAdv (mk A-step₀ A-step₁) C = A-step₀ >>> id *** (const C &&& id >>> A-step₁)
-
- _≗A_ : {p} (A₁ A₂ : FunSemSecAdv p) Set
- A₀ ≗A A₁ = C R runAdv A₀ C R ≡ runAdv A₁ C R
-
- change-adv : {cc ca} {E : Enc cc} {A₁ A₂ : FunSemSecAdv ca} A₁ ≗A A₂ (E ⇄ A₁) ≗⅁ (E ⇄ A₂)
- change-adv {ca = ca} {A₁ = _} {_} pf b R with splitAt ca R
- change-adv {E = E} {A₁} {A₂} pf b ._ | pre Σ., post , refl = trans (cong proj₂ (helper₀ A₁)) helper₂
- where open FunSemSecAdv
- helper₀ = λ A pf (run↺ (E (proj (proj₁ (step₀ A pre)) b)) post) pre
- helper₂ = cong (λ m step₁ A₂ (run↺ (E (proj (proj₁ m) b)) post , proj₂ (step₀ A₂ pre)))
- (helper₀ A₂)
-
- SafeSemSecReduction : (f : Coins Coins) {cc₀ cc₁} (E₀ : Enc cc₀) (E₁ : Enc cc₁) Set
- SafeSemSecReduction f E₀ E₁ =
- ∃ λ (red : SemSecReduction f)
- {c} A (E₀ ⇄ A) ⇓ (E₁ ⇄ red {c} A)
-
- SemSecTr : {cc₀ cc₁} (f : Coins Coins) (tr : Tr cc₀ cc₁) Set
- SemSecTr {cc₀} f tr = {E : Enc cc₀} SafeSemSecReduction f (tr E) E
+ module RunSemSec (ep : EncParams) where
+ open EncParams ep using (M; C; |R|e; Enc)
+
+ -- Returing 0 means Chal wins, Adv looses
+ -- 1 means Adv wins, Chal looses
+ runSemSec : {|R|a} (E : Enc) (A : SemSecAdv ep |R|a) b ↺ (|R|a + |R|e) Bit
+ runSemSec E A b
+ = A-step₀ >>= λ { (m , s) map↺ (A-step₁ s) (E (m b)) }
+ where open FunSemSecAdv A renaming (step₀↺ to A-step₀; step₁F to A-step₁)
+
+ _⇄_ : {|R|a} (E : Enc) (A : SemSecAdv ep |R|a) b ↺ (|R|a + |R|e) Bit
+ _⇄_ = runSemSec
+
+ runAdv : {|R|} SemSecAdv ep |R| C Bits |R| (M × M) × Bit
+ runAdv (mk A-step₀ A-step₁) C = A-step₀ >>> id *** (const C &&& id >>> A-step₁)
+
+ _≗A_ : {p} (A₁ A₂ : SemSecAdv ep p) Set
+ A₀ ≗A A₁ = C R runAdv A₀ C R ≡ runAdv A₁ C R
+
+ change-adv : {ca E} {A₁ A₂ : SemSecAdv ep ca} A₁ ≗A A₂ (E ⇄ A₁) ≗⅁ (E ⇄ A₂)
+ change-adv {ca = ca} {A₁ = _} {_} pf b R with splitAt ca R
+ change-adv {E = E} {A₁} {A₂} pf b ._ | pre Σ., post , refl = trans (cong proj₂ (helper₀ A₁)) helper₂
+ where open FunSemSecAdv
+ helper₀ = λ A pf (run↺ (E (proj (proj₁ (step₀ A pre)) b)) post) pre
+ helper₂ = cong (λ m step₁ A₂ (run↺ (E (proj (proj₁ m) b)) post , proj₂ (step₀ A₂ pre)))
+ (helper₀ A₂)
+
+ _≗E_ : (E₀ E₁ : Enc) Set
+ E₀ ≗E E₁ = m E₀ m ≗↺ E₁ m
+
+ ≗E→≗⅁ : {E₀ E₁} E₀ ≗E E₁ {c} (A : SemSecAdv ep c)
+ (E₀ ⇄ A) ≗⅁ (E₁ ⇄ A)
+ ≗E→≗⅁ E₀≗E₁ {c} A b R
+ rewrite E₀≗E₁ (proj (proj₁ (SemSecAdv.step₀ A (take c R))) b) (drop c R) = refl
+
+ ≗E→⇓ : {E₀ E₁} E₀ ≗E E₁ {c} (A : SemSecAdv ep c) (E₀ ⇄ A) ⇓ (E₁ ⇄ A)
+ ≗E→⇓ E₀≗E₁ A = extensional-reduction (≗E→≗⅁ E₀≗E₁ A)
+
+ module SemSecReductions (ep ep' : EncParams) where
+ module EP = EncParams ep
+ module EP' = EncParams ep'
+ open EP public using (Enc; |R|e; Re)
+ open RunSemSec ep public
+ open EP' public using () renaming (Enc to Enc'; |R|e to |R|e')
+ open RunSemSec ep' public using () renaming (_⇄_ to _⇄'_; _≗E_ to _≗E'_; ≗E→⇓ to ≗E→⇓')
+
+ Tr : Set
+ Tr = Enc Enc'
+
+ Tr⁻¹ : Set
+ Tr⁻¹ = Enc' Enc
+
+ private -- unused
+ SafeSemSecReduction : (f : Coins Coins) (_≈_ : Enc Enc' Set) Set
+ SafeSemSecReduction f _≈_ =
+ ∃ λ (red : SemSecReduction ep ep' f)
+ {E₀ : Enc} {E₁ : Enc'} {c} A E₀ ≈ E₁ (E₀ ⇄ A) ⇓ (E₁ ⇄' red {c} A)
+
+ SemSecTr : (f : Coins Coins) (tr : Tr) Set
+ SemSecTr f tr =
+ ∃ λ (red : SemSecReduction ep' ep f)
+ E {c} A (tr E ⇄' A) ⇓ (E ⇄ red {c} A)
+
+ SemSecTr⁻¹ : (f : Coins Coins) (tr⁻¹ : Tr⁻¹) Set
+ SemSecTr⁻¹ f tr⁻¹ =
+ ∃ λ (red : SemSecReduction ep' ep f)
+ E {c} A (E ⇄' A) ⇓ (tr⁻¹ E ⇄ red {c} A)
+
+ SemSecTr→SemSecTr⁻¹ : tr tr⁻¹ (tr-right-inv : E tr (tr⁻¹ E) ≗E' E)
+ {f} SemSecTr f tr SemSecTr⁻¹ f tr⁻¹
+ SemSecTr→SemSecTr⁻¹ _ tr⁻¹ tr-inv (red , pf) = red , helper
+ where helper : (E : Enc') {c} A (E ⇄' A) ⇓ (tr⁻¹ E ⇄ red {c} A)
+ helper E A A-breaks-E = pf (tr⁻¹ E) A A-breaks-trtr⁻¹E
+ where A-breaks-trtr⁻¹E = ≗E→⇓' (λ m R sym (tr-inv E m R)) A A-breaks-E
+
+ SemSecTr⁻¹→SemSecTr : tr tr⁻¹ (tr-left-inv : E tr⁻¹ (tr E) ≗E E)
+ {f} SemSecTr⁻¹ f tr⁻¹ SemSecTr f tr
+ SemSecTr⁻¹→SemSecTr tr _ tr-inv (red , pf) = red , helper
+ where helper : (E : Enc) {c} A (tr E ⇄' A) ⇓ (E ⇄ red {c} A)
+ helper E {c} A A-breaks-E = ≗E→⇓ (tr-inv E) (red A) (pf (tr E) A A-breaks-E)
+
View
@@ -20,6 +20,7 @@ open import forkable
open import flat-funs
open import program-distance
open import one-time-semantic-security
+import bit-guessing-game
module BitsExtra where
splitAt′ : k {n} Bits (k + n) Bits k × Bits n
@@ -31,79 +32,102 @@ module BitsExtra where
open BitsExtra
-Coins =
-module Guess (prgDist : PrgDist) where
- open PrgDist prgDist
- GuessAdv : Coins Set
- GuessAdv c = ↺ c Bit
- runGuess⅁ : {ca} (A : GuessAdv ca) (b : Bit) ↺ ca Bit
- runGuess⅁ A _ = A
- -- An oracle: an adversary who can break the guessing game.
- Oracle : Coins Set
- Oracle ca = ∃ (λ (A : GuessAdv ca) breaks (runGuess⅁ A))
- -- Any adversary cannot do better than a random guess.
- GuessSec : Coins Set
- GuessSec ca = (A : GuessAdv ca) ¬(breaks (runGuess⅁ A))
-module PostCompSec (prgDist : PrgDist) (|M| |C| : ℕ) where
- module PostCompRed {t} {T : Set t}
- {♭Funs : FlatFuns T}
- (♭ops : FlatFunsOpsFuns) where
+module CompRed {t} {T : Set t}
+ {♭Funs : FlatFuns T}
+ (♭ops : FlatFunsOpsFuns)
+ (ep ep' : EncParams) where
open FlatFunsOps ♭ops
- open AbsSemSec |M| |C| ♭Funs
+ open AbsSemSec ♭Funs
+
+ open EncParams ep using (|M|; |C|)
+ open EncParams ep' using () renaming (|M| to |M|'; |C| to |C|')
+
+ M = `Bits |M|
+ C = `Bits |C|
+ M' = `Bits |M|'
+ C' = `Bits |C|'
+
+ comp-red : (pre-E : M' `→ M)
+ (post-E : C `→ C') SemSecReduction ep' ep _
+ comp-red pre-E post-E (mk A₀ A₁) = mk (A₀ >>> (pre-E *** pre-E) *** idO) (post-E *** idO >>> A₁)
+
+module Comp (ep : EncParams) (|M|' |C|' : ℕ) where
+ open EncParams ep
+
+ ep' : EncParams
+ ep' = EncParams.mk |M|' |C|' |R|e
+
+ open EncParams ep' using () renaming (Enc to Enc'; M to M'; C to C')
+
+ Tr = Enc Enc'
+
+ open FlatFunsOps fun♭Ops
- post-comp-red : (post-E : C `→ C) SemSecReduction _
- post-comp-red post-E (mk A₀ A₁) = mk A₀ (post-E *** idO >>> A₁)
+ comp : (pre-E : M' M) (post-E : C C') Tr
+ comp pre-E post-E E = pre-E >>> E >>> {-weaken≤ |R|e≤|R|e' ∘-} map↺ post-E
+module CompSec (prgDist : PrgDist) (ep : EncParams) (|M|' |C|' : ℕ) where
open PrgDist prgDist
- open PostCompRed fun♭Ops
open FlatFunsOps fun♭Ops
- open FunSemSec prgDist |M| |C|
- open AbsSemSec |M| |C| fun♭Funs
-
- post-comp : {cc} (post-E : C C) Tr cc cc
- post-comp post-E E = E >>> map↺ post-E
-
- post-comp-pres-sem-sec : {cc} (post-E : C C)
- SemSecTr id (post-comp {cc} post-E)
- post-comp-pres-sem-sec post-E = post-comp-red post-E , (λ _ id)
-
- post-comp-pres-sem-sec' : (post-E post-E⁻¹ : C C)
- (post-E-inv : post-E⁻¹ ∘ post-E ≗ id)
- {cc} {E : Enc cc}
- SafeSemSecReduction id E (post-comp post-E E)
- post-comp-pres-sem-sec' post-E post-E⁻¹ post-E-inv {cc} {E} = red , helper where
- E' = post-comp post-E E
- red : SemSecReduction id
- red = post-comp-red post-E⁻¹
- helper : {p} A (E ⇄ A) ⇓ (E' ⇄ red {p} A)
- helper {c} A A-breaks-E = A'-breaks-E'
- where open FunSemSecAdv A renaming (step₀F to A₀F)
- A' = red {c} A
- same-games : (E ⇄ A) ≗⅁ (E' ⇄ A')
- same-games b R
- rewrite post-E-inv (run↺ (E (proj₁ (A₀F (take c R)) b))
- (drop c R)) = refl
- A'-breaks-E' : breaks (E' ⇄ A')
- A'-breaks-E' = extensional-reduction same-games A-breaks-E
-
- post-neg : {cc} Tr cc cc
- post-neg = post-comp vnot
-
- post-neg-pres-sem-sec : {cc} SemSecTr id (post-neg {cc})
- post-neg-pres-sem-sec {cc} {E} = post-comp-pres-sem-sec vnot {E}
-
- post-neg-pres-sem-sec' : {cc} {E : Enc cc}
- SafeSemSecReduction id E (post-neg E)
- post-neg-pres-sem-sec' {cc} {E} = post-comp-pres-sem-sec' vnot vnot vnot∘vnot {cc} {E}
+ open FunSemSec prgDist
+ open AbsSemSec fun♭Funs
+
+ open EncParams ep
+
+ ep' : EncParams
+ ep' = EncParams.mk |M|' |C|' |R|e
+
+ open EncParams ep' using () renaming (Enc to Enc'; M to M'; C to C')
+
+ module CompSec' (pre-E : M'M) (post-E : CC') where
+ open SemSecReductions ep ep'
+ open CompRed fun♭Ops ep ep' hiding (M; C)
+ open Comp ep |M|' |C|'
+
+ comp-pres-sem-sec : SemSecTr id (comp pre-E post-E)
+ comp-pres-sem-sec = comp-red pre-E post-E , λ E A id
+
+ open SemSecReductions ep ep'
+ open CompRed fun♭Ops ep ep' hiding (M; C)
+ open CompSec' public
+ module Comp' {x y z} = Comp x y z
+ open Comp' hiding (Tr)
+ comp-pres-sem-sec⁻¹ : pre-E pre-E⁻¹
+ (pre-E-right-inv : pre-E ∘ pre-E⁻¹ ≗ id)
+ post-E post-E⁻¹
+ (post-E-left-inv : post-E⁻¹ ∘ post-E ≗ id)
+ SemSecTr⁻¹ id (comp pre-E post-E)
+ comp-pres-sem-sec⁻¹ pre-E pre-E⁻¹ pre-E-inv post-E post-E⁻¹ post-E-inv =
+ SemSecTr→SemSecTr⁻¹
+ (comp pre-E⁻¹ post-E⁻¹)
+ (comp pre-E post-E)
+ (λ E m R trans (post-E-inv _) (cong (λ x run↺ (E x) R) (pre-E-inv _)))
+ (comp-pres-sem-sec pre-E⁻¹ post-E⁻¹)
+
+module PostNegSec (prgDist : PrgDist) ep where
+ open EncParams ep
+ open Comp ep |M| |C| hiding (Tr)
+ open CompSec prgDist ep |M| |C|
+ open FunSemSec prgDist
+ open SemSecReductions ep ep
+
+ post-neg : Tr
+ post-neg = comp id vnot
+
+ post-neg-pres-sem-sec : SemSecTr id post-neg
+ post-neg-pres-sem-sec = comp-pres-sem-sec id vnot
+
+ post-neg-pres-sem-sec⁻¹ : SemSecTr⁻¹ id post-neg
+ post-neg-pres-sem-sec⁻¹ = comp-pres-sem-sec⁻¹ id id (λ _ refl) vnot vnot vnot∘vnot
module Concrete k where
open program-distance.Implem k
- module Guess' = Guess prgDist
+ module Guess' = bit-guessing-game prgDist
module FunSemSec' = FunSemSec prgDist
- module PostCompSec' = PostCompSec prgDist
+ module CompSec' = CompSec prgDist
Oops, something went wrong.

0 comments on commit cc47d79

Please sign in to comment.