% fun-universe: Tracking space and time through a restricted universe
% Nicolas Pouillard and Daniel Gustafsson (ITU, IT University of Copenhagen)
% 2012-10-08, AIM16 in Copenhagen
# crypto-agda
* Formalizing cryptography in Type Theory (Agda)
* Started in April 2012 within the DemTech project
* Short term target: foundations and basic results
* Medium term target: verify voting protocols
* Long term impact: the end of paper proof in crypto
# Formalizing cryptography?
* Bit strings, bit-wise operations, and laws
* Number theory
* Group theory
# Provably secure cryptography, what′s needed?
* Information theory
* Probability theory
* Game theory
* Complexity theory
# (1×) Semantic Security
## Parameters
```{.haskell}
`Bits : ℕ → `Set
`Bits = `Vec `Bit
|M| |C| |R| : ℕ -- Parameters
M = `Bits |M| -- The message space
C = `Bits |C| -- The cipher-text space
R = `Bits |R| -- Randomness needed to encrypt
Enc = M `× R `→ C -- Encryption
E : Enc -- Parameter
```
# (1×) Semantic Security
```
advantageSS G = | Pr[G 0 ≡ 1] - Pr[G 1 ≡ 1] |
```
Encryption `E` is semantically secure iff forall "efficient" adversary
`A`, `advantageSS (E ⇆ A)` is "negligible".
# The adversary
```{.haskell}
Rₐ = Bits |Rₐ| -- Adv′s randomness
-- AdvCont = Rₐ → (M × M) × (C → Bit)
Adv = (Rₐ `→ M `× M)
× (Rₐ `× C `→ Bit)
_⇆_ : Enc → Adv → Bit → Rₐ × R → Bit
(E ⇆ (A₀ , A₁)) b (rₐ , r) = d
where
m = A₀ rₐ
c = E (m b , r)
d = A₁ (rₐ , c)
```
# Transformers
```{.haskell}
EncTr = Enc → Enc
AdvTr = Adv → Adv
encTr : EncTr
advTr : AdvTr
⟨E⟩ = encTr E
⟨A⟩ = advTr A
advantageSS (⟨E⟩ ⇆ A) ≈ advantageSS (E ⇆ ⟨A⟩)
```
# A universe for simple data
```{.haskell}
record Universe (`Set : Set) : Set where
constructor mk
field
`⊤ : `Set
`Bit : `Set
_`×_ : `Set → `Set → `Set
`Vec : `Set → ℕ → `Set
`Bits = `Vec `Bit
```
# Instances of this universe
```{.haskell}
Set-U : Universe Set
Set-U = mk ⊤ Bit _×_ Vec
Bits-U : Universe ℕ
Bits-U = mk 0 1 _+_ (flip _*_)
Fin-U : Universe ℕ
Fin-U = mk 1 2 _*_ _^_
⊤-U : Universe ⊤
⊤-U = _ -- Agda figures out that there
-- is only one such universe
```
# A universe of functions over simple data
```{.haskell}
record FunUniverse (`Set : Set) : Set₁ where
constructor _,_
field
universe : Universe `Set
_`→_ : `Set → `Set → Set
i `→ᵇ o = `Bits i `→ `Bits o
`Endo A = A `→ A
```
# Instances of this universe
```{.haskell}
agdaFunU : FunUniverse Set
agdaFunU = Set-U , λ A B → A → B
bitsFunU : FunUniverse ℕ
bitsFunU = Bits-U , λ i o → Bits i → Bits o
finFunU : FunUniverse ℕ
finFunU = Fin-U , λ i o → Fin i → Fin o
constFunU : Set → FunUniverse ⊤
constFunU A = ⊤-U , λ _ _ → A
circuitFunU : FunUniverse ℕ
circuitFunU = Bits-U , _⌥_
```
# Circuit syntax
```{.haskell}
data _⌥_ : ℕ → ℕ → Set where
rewire : ∀ {i o} → (Fin o → Fin i) → i ⌥ o
-- cost: 0 time, o space
_∘_ : ∀ {m n o} → n ⌥ o → m ⌥ n → m ⌥ o
-- cost: sum time and space
<_×_> : ∀ {m n o p} →
m ⌥ o → n ⌥ p → (m + n) ⌥ (o + p)
-- cost: max time and sum space
cond : ∀ {n} → (1 + (n + n)) ⌥ n
-- cost: 1 time, 1 space
bits : ∀ {n _⊤} → Bits n → _⊤ ⌥ n
-- cost: 0 time, n space
xor : ∀ {n} → Bits n → n ⌥ n
-- cost: 1 time, n space
```
# Circuit pictures
# Circuit pictures
# Circuit pictures
# Circuit pictures
# Packing up...
```{.haskell}
record FunPack : Set₁ where
field
`Set : Set
funU : FunUniverse `Set
funO : FunOps funU
```
# Cost models are universe instances! (time)
```{.haskell}
Time = ℕ
timeCostModel : FunPack
timeCostModel = record
{ `Set = Time
; funU = constFunU Time
; funO = record { rewire = const 0
; _∘_ = _+_
; <_×_> = _⊔_
; cond = 1
; bits = const 0
; xor = const 1 } }
```
# Cost models are universe instances! (space)
```{.haskell}
Space = ℕ
spaceCostModel : FunPack
spaceCostModel = record
{ `Set = Space
; funU = constFunU Space
; funO = record { rewire = λ {i} {o} _ → o
; _∘_ = _+_
; <_×_> = _+_
; cond = 1
; bits = λ {n} _ → n
; xor = λ {n} _ → n } }
```
# Wrapping up: polymorphic adversary transformers!
```{.haskell}
AdvTr = ∀ (fp : FunPack) → Adv fp → Adv fp
```
* Security analysis: `agdaFunPack`
* Complexity analysis: `spaceCostModel` and `timeCostModel`
* Running the code: `circuitPack`
#
Tak.