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

`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

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

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

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

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

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

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

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...

record FunPack : Set₁ where
  field
    `Set : Set
    funU : FunUniverse `Set
    funO : FunOps funU

Cost models are universe instances! (time)

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)

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!

AdvTr = ∀ (fp : FunPack) → Adv fp → Adv fp

• Security analysis: agdaFunPack
• Complexity analysis: spaceCostModel and timeCostModel
• Running the code: circuitPack