Browse Source

Attempt to move closer to actual proofs.

tabularasa
Thomas Kerber 9 months ago
parent
commit
18797eea39
Signed by: Thomas Kerber <t.kerber@ed.ac.uk> GPG Key ID: 8489B911F9ED617B
4 changed files with 96 additions and 18 deletions
  1. 77
    3
      Yggdrasil/Examples/SecureChannel.agda
  2. 7
    2
      Yggdrasil/Probability.agda
  3. 1
    1
      Yggdrasil/Security.agda
  4. 11
    12
      Yggdrasil/World.agda

+ 77
- 3
Yggdrasil/Examples/SecureChannel.agda View File

@@ -3,7 +3,8 @@ module Yggdrasil.Examples.SecureChannel where
open import Data.Bool using (Bool; true; false; if_then_else_; _∧_)
open import Data.List using (List; []; _∷_; any)
open import Data.Maybe using (Maybe; just; nothing)
open import Data.Nat using (_*_)
open import Data.Nat using (_*_; zero; suc)
open import Data.Empty using (⊥-elim)
open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩)
open import Level using (Level; Lift; lift)
open import Relation.Binary.PropositionalEquality using (refl)
@@ -177,7 +178,80 @@ secure {ℓ} M C PK L l pk?= c?= m?= = record
}
; base-case = refl
; proof = λ
{ g σ O (call↓ ∈Γ x) Σ inv → ⟨ ? , ⟨ ? , ? ⟩ ⟩
; g σ O (call↯ ∈Γ Γ⊑ x) Σ inv → ⟨ ? , ⟨ ? , ? ⟩ ⟩
{ g σ O (call↓ here tt) ⟨
⟨ stnode (just m) [] , lift true ⟩ ,
stnode (just pk′) (
stnode (just ⟨ pk , log ⟩) [] ∷
stnode (just c) [] ∷
[])
⟩ inv → ⟨ ? , ⟨ ? , ? ⟩ ⟩
; g σ O (call↓ here tt) ⟨
⟨ stnode nothing [] , lift false ⟩ ,
stnode nothing (
stnode nothing [] ∷
stnode nothing [] ∷
[])
⟩ inv → ⟨ ? , ⟨ ? , ? ⟩ ⟩
; zero σ O (call↓ (there here) m) ⟨
⟨ stnode (just m′) [] , lift true ⟩ ,
stnode (just pk′) (
stnode (just ⟨ pk , log ⟩) [] ∷
stnode (just c) [] ∷
[])
⟩ inv → ⟨ ? , ⟨ ? , ? ⟩ ⟩
; (suc g) σ O (call↓ (there here) m) ⟨
⟨ stnode (just m′) [] , lift true ⟩ ,
stnode (just pk′) (
stnode (just ⟨ pk , log ⟩) [] ∷
stnode (just c) [] ∷
[])
⟩ inv → ⟨ ? , ⟨ ? , ? ⟩ ⟩
; g σ O (call↓ (there here) m) ⟨
⟨ stnode nothing [] , lift false ⟩ ,
stnode nothing (
stnode nothing [] ∷
stnode nothing [] ∷
[])
⟩ inv → ⟨ ? , ⟨ ? , ? ⟩ ⟩
; g σ O _ ⟨ ⟨ stnode nothing [] , lift true ⟩ , _ ⟩ inv → ⊥-elim ?
; g σ O _ ⟨
⟨ stnode _ [] , lift true ⟩ ,
stnode nothing _
⟩ ()
; g σ O _ ⟨
⟨ stnode _ [] , lift true ⟩ ,
stnode _ (stnode nothing [] ∷ _)
⟩ ()
; g σ O _ ⟨
⟨ stnode _ [] , lift true ⟩ ,
stnode _ (
stnode _ [] ∷
stnode nothing [] ∷
[])
⟩ ()
; g σ O _ ⟨ ⟨ stnode (just _) [] , lift false ⟩ , _ ⟩ inv → ⊥-elim ?
; g σ O _ ⟨
⟨ stnode _ [] , lift false ⟩ ,
stnode (just _) _
⟩ ()
; g σ O _ ⟨
⟨ stnode _ [] , lift false ⟩ ,
stnode _ (stnode (just _) [] ∷ _)
⟩ ()
; g σ O _ ⟨
⟨ stnode _ [] , lift false ⟩ ,
stnode _ (
stnode _ [] ∷
stnode (just _) [] ∷
[])
⟩ ()
; g σ O (call↓ (there (there ())) x) Σ inv
; g σ O (call↯ () here x) Σ inv
; g σ O (call↯ () (there here here) x) Σ inv
; g σ O (call↯ () (there (there here) here) x) Σ inv
; g σ O (call↯ ∈Γ (there (there (there ())) here) x) Σ inv
; g σ O (call↯ ∈Γ (there here (there () Γ⊑)) x) Σ inv
; g σ O (call↯ ∈Γ (there (there here) (there () Γ⊑)) x) Σ inv
; g σ O (call↯ ∈Γ (there (there (there ())) (there x₂ Γ⊑)) x) Σ inv
}
}

+ 7
- 2
Yggdrasil/Probability.agda View File

@@ -54,11 +54,16 @@ data Dist {ℓ : Level} : Set ℓ → Set (lsuc ℓ) where
sample : ∀ {n : ℕ} → Dist (PrFin {ℓ} n)
_>>=_ : ∀ {A B : Set ℓ} → Dist A → (A → Dist B) → Dist B

_>>=′_ : ∀ {ℓ A B} → Dist {ℓ} A → (A → Dist {ℓ} B) → Dist {ℓ} B
pure x >>=′ y = y x
sample >>=′ y = sample >>= y
(a >>= b) >>=′ y = (a >>= b) >>= y

dmap : ∀ {ℓ A B} → (A → B) → Dist {ℓ} A → Dist {ℓ} B
dmap f d = d >>= (λ x → pure (f x))
dmap f d = d >>= (λ x → pure (f x))

_*_ : ∀ {ℓ A B} → Dist {ℓ} A → Dist {ℓ} B → Dist {ℓ} (A × B)
a * b = a >>= (λ x → b >>= (λ y → pure ⟨ x , y ⟩))
a * b = a >>= (λ x → b >>= (λ y → pure ⟨ x , y ⟩))

lift : {ℓ₁ ℓ₂ : Level} {A : Set ℓ₁} → Dist A → Dist (Lift ℓ₂ A)
lift (pure x) = pure (llift x)

+ 1
- 1
Yggdrasil/Security.agda View File

@@ -17,7 +17,7 @@ open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl; con
open import Relation.Nullary.Decidable using (True; fromWitnessFalse)
open import Yggdrasil.List using (_∈_; here; there; with-proof; map≡-implies-∈≡)
open import Yggdrasil.World using (WorldType; WorldState; World; Oracle; Call; Strategy; Node; weaken; call; call↓; stnode; _∷_; []; _⊑_; Query; _∈↑_; abort; dist; _>>=_; call↯; query; path; strat; ⊤; tt; Action⊤; read; write; exec⊤; Result; out-of-gas; result; rmap; T)
open import Yggdrasil.Probability as Pr using (Dist; _>>=_; pure; _≈[_]≈_; dmap; _*_; Pr[_[_]]≡_)
open import Yggdrasil.Probability as Pr using (Dist; _>>=_; pure; _≈[_]≈_; dmap; _*_; Pr[_[_]]≡_)
open import Yggdrasil.Rational using (_÷_)
open WorldType
open Node

+ 11
- 12
Yggdrasil/World.agda View File

@@ -10,7 +10,7 @@ open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
open import Level using (Level; Lift) renaming (suc to lsuc; lift to llift)
open import Yggdrasil.Probability using (Dist; pure; _>>=_; lift)
open import Yggdrasil.Probability using (Dist; pure; _>>=_; lift)
open import Yggdrasil.List using (_∈_; here; there)

data ⊤ {ℓ : Level} : Set ℓ where
@@ -179,32 +179,31 @@ exec↑ : ∀ {ℓ S Γ₁ Γ₂ A} → Oracle S Γ₁ → Action↑ (node Γ₂
(S × WorldState {ℓ} Γ₁) → Γ₂ ⊑ Γ₁ → ℕ → Dist (Result (A × (S × WorldState {ℓ} Γ₁)))

-- NOTE: Gas is only used for termination here, it is NOT a computational model.
exec (strat S α O) Σ g = (exec⊤ O α ⟨ S , Σ ⟩ g) >>= (pure ∘ rmap (llift ∘ proj₁))
exec (strat S α O) Σ g = (exec⊤ O α ⟨ S , Σ ⟩ g) >>= (pure ∘ rmap (llift ∘ proj₁))

exec⊤ O read Σ g = pure (result ⟨ proj₁ Σ , Σ ⟩)
exec⊤ O (write σ) Σ g = pure (result ⟨ tt , ⟨ σ , proj₂ Σ ⟩ ⟩)
exec⊤ O (call↓ {f = f} ∈Γ x) Σ g = exec↑ O (Call.δ f x) Σ here g
exec⊤ O abort Σ g = pure abort
exec⊤ O (dist D) Σ g = lift D >>= λ{
exec⊤ O (dist D) Σ g = lift D >>= λ{
(llift x) → pure (result ⟨ x , Σ ⟩ ) }
exec⊤ O (call↯ {f = f} f∈ ⊑Γ x) Σ g = exec↑ O (Call.δ f x) Σ ⊑Γ g
exec⊤ O (α >>= β) Σ g = (exec⊤ O α Σ g) >>= λ{
exec⊤ O (α >>= β) Σ g = (exec⊤ O α Σ g) >>= λ{
(result ⟨ x , Σ′ ⟩) → exec⊤ O (β x) Σ′ g ;
abort → pure abort ;
out-of-gas → pure out-of-gas }
abort → pure abort ;
out-of-gas → pure out-of-gas }

exec↑ O read Σ ⊑Γ g = pure (result
⟨ get ⊑Γ (proj₂ Σ) , Σ ⟩)
exec↑ O (write σ) Σ ⊑Γ g = pure (result
⟨ tt , ⟨ proj₁ Σ , set ⊑Γ (proj₂ Σ) σ ⟩ ⟩)
exec↑ O abort Σ ⊑Γ g = pure abort
exec↑ O (dist D) Σ ⊑Γ g = lift D >>=
exec↑ O (dist D) Σ ⊑Γ g = lift D >>=
λ{ (llift x) → pure (result ⟨ x , Σ ⟩) }
exec↑ O (query {q = q} q∈ x) Σ ⊑Γ zero = pure out-of-gas
exec↑ O (query {q = q} q∈ x) Σ ⊑Γ (suc g) = exec⊤ O (O (path ⊑Γ q∈) x) Σ g
exec↑ O (call↓ {f = f} ∈Γ Γ∈ x) Σ ⊑Γ g = exec↑ O (Call.δ f x) Σ (⊑-right ⊑Γ Γ∈) g
exec↑ O (α >>= β) Σ ⊑Γ g = (exec↑ O α Σ ⊑Γ g)
>>= λ{
(result ⟨ x , Σ′ ⟩) → exec↑ O (β x) Σ′ ⊑Γ g ;
abort → pure abort ;
out-of-gas → pure out-of-gas }
exec↑ O (α >>= β) Σ ⊑Γ g = (exec↑ O α Σ ⊑Γ g) >>=′ λ{
(result ⟨ x , Σ′ ⟩) → exec↑ O (β x) Σ′ ⊑Γ g ;
abort → pure abort ;
out-of-gas → pure out-of-gas }

Loading…
Cancel
Save