Browse Source

Start thinking about security definition.

gas-move-test
Thomas Kerber 10 months ago
parent
commit
1d3de4eac2
Signed by: Thomas Kerber <t.kerber@ed.ac.uk> GPG Key ID: 8489B911F9ED617B
3 changed files with 47 additions and 2 deletions
  1. 0
    1
      Yggdrasil/List.agda
  2. 40
    0
      Yggdrasil/Security.agda
  3. 7
    1
      Yggdrasil/World.agda

+ 0
- 1
Yggdrasil/List.agda View File

@@ -6,4 +6,3 @@ open import Level using (Level)
data _∈_ {ℓ : Level} {A : Set ℓ} : A → List A → Set ℓ where
here : {x : A} {xs : List A} → x ∈ (x ∷ xs)
there : {x y : A} {xs : List A} → y ∈ xs → y ∈ (x ∷ xs)


+ 40
- 0
Yggdrasil/Security.agda View File

@@ -0,0 +1,40 @@
module Yggdrasil.Security where

open import Data.List using (map)
open import Data.Product using (_×_; Σ; Σ-syntax; proj₁; proj₂; ∃; ∃-syntax)
open import Level using (Level) renaming (suc to lsuc)
open import Relation.Binary.PropositionalEquality using (_≡_)
open import Yggdrasil.List using (_∈_)
open import Yggdrasil.World using (WorldType; World; Call; Strategy; weaken)
open WorldType

data Guess {ℓ : Level} : Set ℓ where
real? ideal? : Guess

data Outcome : Set where
↯ ✔ : Outcome

record RouterConfig {ℓ : Level} : Set (lsuc ℓ) where
field
ref : Guess {ℓ}
real : World ℓ
ideal : World ℓ
sim : Σ[ σ ∈ Set ℓ ] (σ × (∀ {c} → σ → c ∈ adv (proj₁ ideal) →
σ × (Σ (Call ℓ (node (proj₁ real))) (_∈ adv (proj₁ real)))))
hon-≡ : map weaken (hon (proj₁ ideal)) ≡ map weaken (hon (proj₁ real))

open RouterConfig

router-world-type : ∀ {ℓ} → RouterConfig {ℓ} → WorldType ℓ
router-world-type = ?

router-world : ∀ {ℓ} → RouterConfig {ℓ} → Guess {ℓ} → World ℓ
router-world = ?

router-strategy : ∀ {ℓ A} → (rc : RouterConfig {ℓ}) →
Strategy (proj₁ (ideal rc)) A → Strategy (router-world-type rc) A
router-strategy = ?

yggdrasil-game : ∀ {ℓ} → (rc : RouterConfig {ℓ}) →
Strategy (proj₁ (ideal rc)) Guess → Guess {ℓ} → Outcome
yggdrasil-game = ?

+ 7
- 1
Yggdrasil/World.agda View File

@@ -5,7 +5,7 @@ open import Data.Empty using (⊥-elim)
open import Data.List using (List; _∷_; []; map)
open import Data.Maybe using (Maybe; nothing; just)
open import Data.Nat using (ℕ; zero; suc)
open import Data.Product using (_×_; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
open import Data.Product using (_×_; Σ; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
open import Level using (Level) renaming (suc to lsuc)
@@ -43,6 +43,9 @@ record Call (ℓ : Level) (N : Node ℓ) : Set (lsuc ℓ) where
B : A → Set ℓ
δ : (state N) → (x : A) → (state N) × Action↑ N (B x)

weaken : ∀ {ℓ N} → Call ℓ N → Query ℓ
weaken c = record { A = Call.A c; B = Call.B c }

record WorldType ℓ where
inductive
field
@@ -84,6 +87,9 @@ data WorldStates {ℓ} where
data WorldState {ℓ} Γ where
stnode : state (node Γ) → WorldStates (chld (node Γ)) → WorldState Γ

World : (ℓ : Level) → Set (lsuc ℓ)
World ℓ = Σ (WorldType ℓ) WorldState

data _∈↑_ {ℓ : Level} (q : Query ℓ) (Γ : WorldType ℓ) : Set (lsuc ℓ) where
path : ∀ {Γ′} → Γ′ ⊑ Γ → q ∈ qry (node Γ′) → q ∈↑ Γ


Loading…
Cancel
Save