Browse Source

Slight reorganising.

tabularasa
Thomas Kerber 9 months ago
parent
commit
1a813a3c9e
Signed by: Thomas Kerber <t.kerber@ed.ac.uk> GPG Key ID: 8489B911F9ED617B
2 changed files with 10 additions and 8 deletions
  1. 4
    3
      Yggdrasil/Examples/SecureChannel.agda
  2. 6
    5
      Yggdrasil/Security.agda

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

@@ -3,6 +3,7 @@ module Yggdrasil.Examples.SecureChannel where
open import Data.Bool using (Bool; true; false; if_then_else_)
open import Data.List using (List; []; _∷_)
open import Data.Maybe using (Maybe; just; nothing)
open import Data.Nat using (_*_)
open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩)
open import Level using (Level; Lift; lift)
open import Relation.Binary.PropositionalEquality using (refl)
@@ -158,8 +159,8 @@ secure : {ℓ : Level} → (M C PK L : Set ℓ) → (l : M → L) →
(pk?= : PK → PK → Bool) → (c?= : C → C → Bool) →
πᵢ-SecureChannel M L l ≃ πᵣ-SecureChannel M C PK L l pk?= c?=
secure {ℓ} M C PK L l pk?= c?= = record
{ g-exec-min = ?
; g-sim-min = ?
{ sim-gas = λ _ → 1000
; gas-map = _* 10
; simulator = S-SecureChannel M C PK L l pk?= c?=
; proof = ?
; proof = λ{ g (strat α O) → ? }
}

+ 6
- 5
Yggdrasil/Security.agda View File

@@ -113,14 +113,15 @@ simulated-strategy S str g = strat
record Adv[_,_]≤_ {ℓ : Level} (πᵢ πᵣ : World ℓ) (ε : ℚ) :
Set (lsuc (lsuc ℓ)) where
field
g-exec-min :
g-sim-min :
sim-gas : Strategy (World.Γ πᵣ) Guess →
gas-map : ℕ →
simulator : Simulator πᵢ πᵣ
proof : (g-exec g-sim : ℕ) → g-exec-min ≤ g-exec → g-sim-min ≤ g-sim →
proof : (g : ℕ) →
(str : Strategy (World.Γ πᵣ) Guess) →
(⌊exec⌋ (simulated-strategy simulator str g-sim) (World.Σ πᵢ) g-exec)
(⌊exec⌋ (simulated-strategy simulator str (sim-gas str)) (World.Σ πᵢ)
(gas-map g))
≈[ ε ]≈
(⌊exec⌋ str (World.Σ πᵣ) g-exec)
(⌊exec⌋ str (World.Σ πᵣ) g)

_≃_ : {ℓ : Level} → (πᵢ πᵣ : World ℓ) → Set (lsuc (lsuc ℓ))
πᵢ ≃ πᵣ = Adv[ πᵢ , πᵣ ]≤ 0

Loading…
Cancel
Save