3.1. CKA Definitions🔗

Definition3.1.1

uses 0

Used by 9

Reverse dependency previews

Preview

Definition 3.1.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

\todo

structure CKAScheme (m : Type → Type u) [Monad m] (IK St I Rho Rand : Type) where
  /-- samples initial shared key -/
  initKeyGen : m IK
  /-- initializes A's local state from the initial key -/
  initA : IK → m St
  /-- initializes B's local state from the initial key -/
  initB : IK → m St
  /-- Party A's send: returns the fresh epoch key, message sent to B, and A's next state. -/
  sendA : St → m (Option (I × Rho × St))
  /-- Party A's randomness-leaking send: also returns the randomness used for the send. -/
  sendArleak : St → m (Option (I × Rho × St × Rand))
  /-- Party A's receive: returns the derived epoch key and A's next state. -/
  recvA : St → Rho → Option (I × St)
  /-- Party B's send: returns the fresh epoch key, message sent to A, and B's next state. -/
  sendB : St → m (Option (I × Rho × St))
  /-- Party B's randomness-leaking send: also returns the randomness used for the send. -/
  sendBrleak : St → m (Option (I × Rho × St × Rand))
  /-- Party B's receive: returns the derived epoch key and B's next state. -/
  recvB : St → Rho → Option (I × St)

github #195

Lean code for Definition3.1.1●1 definition

structure(9 fields)defined in SecureMessaging/CKA/Defs.lean

complete

structure CKAScheme.{u} (m : Type → Type u) [Monad m] (IK St I Rho Rand : Type) :
  Type u

structure CKAScheme.{u} (m : Type → Type u)
  [Monad m] (IK St I Rho Rand : Type) :
  Type u

A continuous key agreement (CKA) protocol with initial-key space `IK`,
per-party state space `St`, epoch-key space `I`, protocol-message space `Rho`,
and send-randomness space `Rand`.

Fields

initKeyGen : m IK

samples initial shared key

initA : IK → m St

initializes A's local state from the initial key

initB : IK → m St

initializes B's local state from the initial key

sendA : St → m (Option (I × Rho × St))

Party A's send: returns the fresh epoch key, message sent to B, and A's next state.

sendArleak : St → m (Option (I × Rho × St × Rand))

Party A's randomness-leaking send: also returns the randomness used for the send.

recvA : St → Rho → Option (I × St)

Party A's receive: returns the derived epoch key and A's next state.

sendB : St → m (Option (I × Rho × St))

Party B's send: returns the fresh epoch key, message sent to A, and B's next state.

sendBrleak : St → m (Option (I × Rho × St × Rand))

Party B's randomness-leaking send: also returns the randomness used for the send.

recvB : St → Rho → Option (I × St)

Party B's receive: returns the derived epoch key and B's next state.

Definition3.1.2

uses 1

Used by 2

Reverse dependency previews

Preview

Definition 3.1.3

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

\todo

Game state (\stA, \stB, \rho_\mathsf{A}, \rho_\mathsf{B}, K_\mathsf{A}, K_\mathsf{B}, \mathsf{correct}, \mathsf{last}, t_\mathsf{A}, t_\mathsf{B})

\stA, \stB: local protocol states for parties A and B.
\rho_\mathsf{A}, \rho_\mathsf{B}: pending messages sent by A and B.
K_\mathsf{A}, K_\mathsf{B}: sender keys associated with pending sent messages.
\mathsf{correct}: records whether all delivered epoch keys have matched so far.
\mathsf{last}: the last oracle action, used to enforce alternating communication.
t_\mathsf{A}, t_\mathsf{B}: per-party epoch counters.

structure GameState (St I Rho : Type) where
  /-- Local protocol state for party A. -/
  stA : St
  /-- Local protocol state for party B. -/
  stB : St
  /-- Latest undelivered message sent from A to B. -/
  rhoA : Option Rho
  /-- Latest undelivered message sent from B to A. -/
  rhoB : Option Rho
  /-- Sender key corresponding to `rhoA`. -/
  keyA : Option I
  /-- Sender key corresponding to `rhoB`. -/
  keyB : Option I
  /-- Whether delivered epoch keys have agreed so far. -/
  correct : Bool
  /-- Last oracle action, used to enforce alternating communication. -/
  lastAction : Option CKAAction
  /-- Epoch counter for A, incremented on A-side send, challenge, or receive. -/
  tA : ℕ
  /-- Epoch counter for B, incremented on B-side send, challenge, or receive. -/
  tB : ℕ

Game parameters (t^*, \Delta_\mathsf{FS}, \Delta_\mathsf{PCS}, \mathsf{chall})

t^*: challenge epoch selected for the security experiment.
\Delta_\mathsf{FS}: forward-secrecy delay after which post-challenge corruption is allowed.
\Delta_\mathsf{PCS}: post-compromise-security delay before the challenge during which corruption is disallowed.
\mathsf{chall}: party selected for the challenge oracle.

structure GameParams where
  /-- Epoch challenged by the adversary. -/
  challengeEpoch : ℕ
  /-- Forward-secrecy delay after which state corruption is allowed. -/
  ΔFS : ℕ
  /-- Post-compromise-security delay before the challenge during which corruption is disallowed. -/
  ΔPCS : ℕ
  /-- Party selected for the challenge oracle. -/
  challengedParty : CKAParty

Predicates

\allow(t_\mathsf{A},t_\mathsf{B},t^*,\Delta_\mathsf{FS},\Delta_\mathsf{PCS},P) \;\Leftrightarrow\; \max(t_\mathsf{A},t_\mathsf{B})+\Delta_\mathsf{PCS}\leq t^* \;\vee\; t^*+\Delta_\mathsf{FS}\leq t_P

def allowCorrPCS (gp : GameParams) (state : GameState St I Rho) : Bool :=
  (max state.tA state.tB) + gp.ΔPCS ≤ gp.challengeEpoch

abbrev allowCorrFS (gp : GameParams) (state : GameState St I Rho) : CKAParty → Bool
  | .A => gp.challengeEpoch + gp.ΔFS ≤ state.tA
  | .B => gp.challengeEpoch + gp.ΔFS ≤ state.tB

def allowCorr (gp : GameParams) (state : GameState St I Rho) : CKAParty → Bool
  | p => allowCorrPCS gp state || allowCorrFS gp state p

\OSendA

\begin{array}{l} t_\mathsf{A}\gets t_\mathsf{A}+1; \\ (K_\mathsf{A},\rho_\mathsf{A},\stA) \sample \SendA(\stA); \\ \Return(\rho_\mathsf{A},K_\mathsf{A}) \end{array}

def oracleSendA (cka : CKAScheme ProbComp IK St I Rho Rand) :
    QueryImpl (Unit →ₒ Option (Rho × I)) (StateT (GameState St I Rho) ProbComp) :=
  fun () => do
    let state ← get
    -- Only allow A to send if it is A's turn in alternating communication.
    if validStep state.lastAction .sendA then
      -- Increment A's epoch counter.
      let state := { state with tA := state.tA + 1 }
      -- Run A's send algorithm on the current A-state.
      match ← liftM (cka.sendA state.stA) with
      | none => pure none
      | some (key, ρ, stA') =>
        -- Update game state.
        set { state with
          stA := stA', rhoA := some ρ, keyA := some key,
          lastAction := some .sendA }
        -- Return the message and key to the adversary.
        return some (ρ, key)
    else pure none

\OSendB

\begin{array}{l} t_\mathsf{B}\gets t_\mathsf{B}+1; \\ (K_\mathsf{B},\rho_\mathsf{B},\stB) \sample \SendB(\stB); \\ \Return(\rho_\mathsf{B},K_\mathsf{B}) \end{array}

def oracleSendB (cka : CKAScheme ProbComp IK St I Rho Rand) :
    QueryImpl (Unit →ₒ Option (Rho × I)) (StateT (GameState St I Rho) ProbComp) :=
  fun () => do
    let state ← get
    -- Only allow B to send if it is B's turn in alternating communication.
    if validStep state.lastAction .sendB then
      -- Increment B's epoch counter.
      let state := { state with tB := state.tB + 1 }
      -- Run B's send algorithm on the current B-state.
      match ← liftM (cka.sendB state.stB) with
      | none => pure none
      | some (key, ρ, stB') =>
        -- Update game state.
        set { state with
          stB := stB', rhoB := some ρ, keyB := some key,
          lastAction := some .sendB }
        -- Return the message and key to the adversary.
        return some (ρ, key)
    else pure none

\OSendARLeak

\begin{array}{l} \req\;\max(t_\mathsf{A}+1,t_\mathsf{B})+\Delta_\mathsf{PCS}\leq t^*; \\ (K_\mathsf{A},\rho_\mathsf{A},\stA,r) \sample \SendARLeak(\stA); \\ t_\mathsf{A}\gets t_\mathsf{A}+1; \\ \Return(\rho_\mathsf{A},K_\mathsf{A},r) \end{array}

def oracleSendArleak (gp : GameParams) (cka : CKAScheme ProbComp IK St I Rho Rand) :
    QueryImpl (Unit →ₒ Option (Rho × I × Rand)) (StateT (GameState St I Rho) ProbComp) :=
  fun () => do
    let state ← get
    if validStep state.lastAction .sendA then
      let state := { state with tA := state.tA + 1 }
      if allowCorrPCS gp state then
        match ← liftM (cka.sendArleak state.stA) with
        | none => pure none
        | some (key, ρ, stA', rand) =>
          set { state with
            stA := stA', rhoA := some ρ, keyA := some key,
            lastAction := some .sendA }
          return some (ρ, key, rand)
      else pure none
    else pure none

\OSendBRLeak

\begin{array}{l} \req\;\max(t_\mathsf{A},t_\mathsf{B}+1)+\Delta_\mathsf{PCS}\leq t^*; \\ (K_\mathsf{B},\rho_\mathsf{B},\stB,r) \sample \SendBRLeak(\stB); \\ t_\mathsf{B}\gets t_\mathsf{B}+1; \\ \Return(\rho_\mathsf{B},K_\mathsf{B},r) \end{array}

def oracleSendBrleak (gp : GameParams) (cka : CKAScheme ProbComp IK St I Rho Rand) :
    QueryImpl (Unit →ₒ Option (Rho × I × Rand)) (StateT (GameState St I Rho) ProbComp) :=
  fun () => do
    let state ← get
    if validStep state.lastAction .sendB then
      let state := { state with tB := state.tB + 1 }
      if allowCorrPCS gp state then
        match ← liftM (cka.sendBrleak state.stB) with
        | none => pure none
        | some (key, ρ, stB', rand) =>
          set { state with
            stB := stB', rhoB := some ρ, keyB := some key,
            lastAction := some .sendB }
          return some (ρ, key, rand)
      else pure none
    else pure none

\ORecA

\begin{array}{l} t_\mathsf{A}\gets t_\mathsf{A}+1; \\ (K,\stA) \getsval \RecA(\stA,\rho_\mathsf{B}); \\ \mathsf{correct} \gets \mathsf{correct}\wedge(K_\mathsf{B}{=}K) \end{array}

def oracleRecvA [DecidableEq I] (cka : CKAScheme ProbComp IK St I Rho Rand) :
    QueryImpl (Unit →ₒ Unit) (StateT (GameState St I Rho) ProbComp) :=
  fun () => do
    let state ← get
    -- Only allow A to receive if it is A's turn in alternating communication.
    if validStep state.lastAction .recvA then
      -- Increment A's epoch counter.
      let state := { state with tA := state.tA + 1 }
      match state.rhoB with
      | none => pure () -- No pending message.
      | some ρ =>
        -- Run A's receive algorithm on the current A-state and B's message.
        match cka.recvA state.stA ρ with
        | none =>
          set { state with
            rhoB := none, keyB := none,
            correct := false, lastAction := some .recvA }
        | some (keyA, stA') =>
          let ok := state.keyB == some keyA
          set { state with
            -- Update game state.
            stA := stA', rhoB := none, keyB := none,
            -- Update correctness flag.
            correct := state.correct && ok, lastAction := some .recvA }
    else pure ()

\ORecB

\begin{array}{l} t_\mathsf{B}\gets t_\mathsf{B}+1; \\ (K,\stB) \getsval \RecB(\stB,\rho_\mathsf{A}); \\ \mathsf{correct} \gets \mathsf{correct}\wedge(K_\mathsf{A}{=}K) \end{array}

def oracleRecvB [DecidableEq I] (cka : CKAScheme ProbComp IK St I Rho Rand) :
    QueryImpl (Unit →ₒ Unit) (StateT (GameState St I Rho) ProbComp) :=
  fun () => do
    let state ← get
    -- Only allow B to receive if it is B's turn in alternating communication.
    if validStep state.lastAction .recvB then
      -- Increment B's epoch counter.
      let state := { state with tB := state.tB + 1 }
      match state.rhoA with
      | none => pure () -- No pending message.
      | some ρ =>
        -- Run B's receive algorithm on the current B-state and A's message.
        match cka.recvB state.stB ρ with
        | none =>
          set { state with
            rhoA := none, keyA := none,
            correct := false, lastAction := some .recvB }
        | some (keyB, stB') =>
          let ok := state.keyA == some keyB
          set { state with
            -- Update game state.
            stB := stB', rhoA := none, keyA := none,
            -- Update correctness flag.
            correct := state.correct && ok, lastAction := some .recvB }
    else pure ()

\OChallA

\begin{array}{l} t_\mathsf{A}\gets t_\mathsf{A}+1; \\ \req\;\mathsf{chall}{=}\mathsf{A}\wedge t_\mathsf{A}=t^*; \\ (K_\mathsf{A},\rho_\mathsf{A},\stA) \sample \SendA(\stA); \\ \mathsf{if}\;b\;\mathsf{then}\;K \sample \mathcal K\;\mathsf{else}\;K \gets K_\mathsf{A}; \\ \Return(\rho_\mathsf{A},K) \end{array}

def oracleChallA (gp : GameParams) (isRandom : Bool) [SampleableType I]
    (cka : CKAScheme ProbComp IK St I Rho Rand) :
    QueryImpl (Unit →ₒ Option (Rho × I)) (StateT (GameState St I Rho) ProbComp) :=
  fun () => do
    let state ← get
    if validStep state.lastAction .challA then
    -- Increment A's epoch counter.
      let state := { state with tA := state.tA + 1 }
    -- Enforce correct challenge party and epoch.
      if gp.challengedParty == .A && isChallengeEpoch gp state then
        -- Run A's send algorithm on the current A-state.
        match ← liftM (cka.sendA state.stA) with
        | none => pure none
        | some (key, ρ, stA') =>
          -- Real or random key for the adversary.
          let outKey ← if isRandom then liftM ($ᵗ I : ProbComp I) else pure key
          -- Update game state.
          set { state with
            stA := stA', rhoA := some ρ, keyA := some key,
            lastAction := some .challA }
          -- Return the message and key to the adversary.
          return some (ρ, outKey)
      else pure none
    else pure none

\OChallB

\begin{array}{l} t_\mathsf{B}\gets t_\mathsf{B}+1; \\ \req\;\mathsf{chall}{=}\mathsf{B}\wedge t_\mathsf{B}=t^*; \\ (K_\mathsf{B},\rho_\mathsf{B},\stB) \sample \SendB(\stB); \\ \mathsf{if}\;b\;\mathsf{then}\;K \sample \mathcal K\;\mathsf{else}\;K \gets K_\mathsf{B}; \\ \Return(\rho_\mathsf{B},K) \end{array}

def oracleChallB (gp : GameParams) (isRandom : Bool) [SampleableType I]
    (cka : CKAScheme ProbComp IK St I Rho Rand) :
    QueryImpl (Unit →ₒ Option (Rho × I)) (StateT (GameState St I Rho) ProbComp) :=
  fun () => do
    let state ← get
    if validStep state.lastAction .challB then
      -- Increment B's epoch counter.
      let state := { state with tB := state.tB + 1 }
      -- Enforce correct challenge party and epoch.
      if gp.challengedParty == .B && isChallengeEpoch gp state then
        -- Run B's send algorithm on the current B-state.
        match ← liftM (cka.sendB state.stB) with
        | none => pure none
        | some (key, ρ, stB') =>
          let outKey ← if isRandom then liftM ($ᵗ I : ProbComp I) else pure key
          -- Update game state.
          set { state with
            stB := stB', rhoB := some ρ, keyB := some key,
            lastAction := some .challB }
          -- Return the message and key to the adversary.
          return some (ρ, outKey)
      else pure none
    else pure none

\OCorrA

\begin{array}{l} \req\;\allow(t_\mathsf{A},t_\mathsf{B},t^*,\Delta_\mathsf{FS},\Delta_\mathsf{PCS},\mathsf{A}); \\ \Return\stA \end{array}

def oracleCorruptA (gp : GameParams) (St I Rho : Type) :
    QueryImpl (Unit →ₒ Option St) (StateT (GameState St I Rho) ProbComp) :=
  fun () => do
    let state ← get
    if allowCorr gp state .A then return some state.stA
    else return none

\OCorrB

\begin{array}{l} \req\;\allow(t_\mathsf{A},t_\mathsf{B},t^*,\Delta_\mathsf{FS},\Delta_\mathsf{PCS},\mathsf{B}); \\ \Return\stB \end{array}

def oracleCorruptB (gp : GameParams) (St I Rho : Type) :
    QueryImpl (Unit →ₒ Option St) (StateT (GameState St I Rho) ProbComp) :=
  fun () => do
    let state ← get
    if allowCorr gp state .B then return some state.stB
    else return none

uses Definition 3.1.1

Lean code for Definition3.1.2●16 definitions

structure(10 fields)defined in SecureMessaging/CKA/Defs.lean

complete

structure CKAScheme.GameState (St I Rho : Type) : Type

structure CKAScheme.GameState (St I Rho : Type) :
  Type

Internal state of the CKA game.
- `stA`, `stB`: per-party protocol state.
- `rhoA, rhoB`: undelivered messages sent by A or B.
- `keyA, keyB`: keys derived by A or B upon executing the send algorithm.
- `correct`: tracks whether A and B agree on derived keys at all epochs.
- `lastAction`: enforces alternating communication.
- `tA`, `tB`: per-party epoch counters.

Fields

stA : St

Local protocol state for party A.

stB : St

Local protocol state for party B.

rhoA : Option Rho

Latest undelivered message sent from A to B.

rhoB : Option Rho

Latest undelivered message sent from B to A.

keyA : Option I

Sender key corresponding to `rhoA`.

keyB : Option I

Sender key corresponding to `rhoB`.

correct : Bool

Whether delivered epoch keys have agreed so far.

lastAction : Option CKAScheme.CKAAction

Last oracle action, used to enforce alternating communication.

tA : ℕ

Epoch counter for A, incremented on A-side send, challenge, or receive.

tB : ℕ

Epoch counter for B, incremented on B-side send, challenge, or receive.

structure(4 fields)defined in SecureMessaging/CKA/Defs.lean

complete

structure CKAScheme.GameParams : Type

structure CKAScheme.GameParams : Type

Game parameters fixed at the start of the security experiment.

Fields

challengeEpoch : ℕ

Epoch challenged by the adversary.

ΔFS : ℕ

Forward-secrecy delay after which state corruption is allowed.

ΔPCS : ℕ

Post-compromise-security delay before the challenge during which corruption is disallowed.

challengedParty : CKAScheme.CKAParty

Party selected for the challenge oracle.

defdefined in SecureMessaging/CKA/Defs.lean

complete

def CKAScheme.isChallengeEpoch {St I Rho : Type} (gp : CKAScheme.GameParams)
  (state : CKAScheme.GameState St I Rho) : Bool

def CKAScheme.isChallengeEpoch
  {St I Rho : Type}
  (gp : CKAScheme.GameParams)
  (state : CKAScheme.GameState St I Rho) :
  Bool

Challenge allowed only when the challenged party's counter is at `challengeEpoch`.

defdefined in SecureMessaging/CKA/Defs.lean

complete

def CKAScheme.allowCorrPCS {St I Rho : Type} (gp : CKAScheme.GameParams)
  (state : CKAScheme.GameState St I Rho) : Bool

def CKAScheme.allowCorrPCS {St I Rho : Type}
  (gp : CKAScheme.GameParams)
  (state : CKAScheme.GameState St I Rho) :
  Bool

Pre-challenge PCS gate:
`max(tA, tB) ≤ challengeEpoch - ΔPCS`, equivalently
`max(tA, tB) + ΔPCS ≤ challengeEpoch`.

abbrevdefined in SecureMessaging/CKA/Defs.lean

complete

abbrev CKAScheme.allowCorrFS {St I Rho : Type} (gp : CKAScheme.GameParams)
  (state : CKAScheme.GameState St I Rho) : CKAScheme.CKAParty → Bool

abbrev CKAScheme.allowCorrFS {St I Rho : Type}
  (gp : CKAScheme.GameParams)
  (state : CKAScheme.GameState St I Rho) :
  CKAScheme.CKAParty → Bool

Post-challenge FS gate for party `p`:
party `p` has advanced `ΔFS` epochs past the challenge.

defdefined in SecureMessaging/CKA/Defs.lean

complete

def CKAScheme.allowCorr {St I Rho : Type} (gp : CKAScheme.GameParams)
  (state : CKAScheme.GameState St I Rho) : CKAScheme.CKAParty → Bool

def CKAScheme.allowCorr {St I Rho : Type}
  (gp : CKAScheme.GameParams)
  (state : CKAScheme.GameState St I Rho) :
  CKAScheme.CKAParty → Bool

Corruption gate for party `p`. This is the disjunction of the two allowed
corruption windows: both party counters are `ΔPCS` epochs before the challenge,
or party `p` has advanced `ΔFS` epochs past the challenge.

defdefined in SecureMessaging/CKA/Defs.lean

complete

def CKAScheme.oracleSendA {IK St I Rho Rand : Type}
  (cka : CKAScheme ProbComp IK St I Rho Rand) :
  QueryImpl (OracleSpec.ofFn fun x ↦ Option (Rho × I))
    (StateT (CKAScheme.GameState St I Rho) ProbComp)

def CKAScheme.oracleSendA
  {IK St I Rho Rand : Type}
  (cka :
    CKAScheme ProbComp IK St I Rho Rand) :
  QueryImpl
    (OracleSpec.ofFn fun x ↦
      Option (Rho × I))
    (StateT (CKAScheme.GameState St I Rho)
      ProbComp)

**O-Send-A.**
Increment epoch counter, trigger send by A, return message and key.
`tA++; (key, ρ, stA') ← sendA(stA)`; return `(ρ, key)`.

defdefined in SecureMessaging/CKA/Defs.lean

complete

def CKAScheme.oracleSendB {IK St I Rho Rand : Type}
  (cka : CKAScheme ProbComp IK St I Rho Rand) :
  QueryImpl (OracleSpec.ofFn fun x ↦ Option (Rho × I))
    (StateT (CKAScheme.GameState St I Rho) ProbComp)

def CKAScheme.oracleSendB
  {IK St I Rho Rand : Type}
  (cka :
    CKAScheme ProbComp IK St I Rho Rand) :
  QueryImpl
    (OracleSpec.ofFn fun x ↦
      Option (Rho × I))
    (StateT (CKAScheme.GameState St I Rho)
      ProbComp)

**O-Send-B.**
Increment epoch counter, trigger send by B, return message and key.
`tB++; (key, ρ, stB') ← sendB(stB)`; return `(ρ, key)`.

defdefined in SecureMessaging/CKA/Defs.lean

complete

def CKAScheme.oracleSendArleak {IK St I Rho Rand : Type}
  (gp : CKAScheme.GameParams)
  (cka : CKAScheme ProbComp IK St I Rho Rand) :
  QueryImpl (OracleSpec.ofFn fun x ↦ Option (Rho × I × Rand))
    (StateT (CKAScheme.GameState St I Rho) ProbComp)

def CKAScheme.oracleSendArleak
  {IK St I Rho Rand : Type}
  (gp : CKAScheme.GameParams)
  (cka :
    CKAScheme ProbComp IK St I Rho Rand) :
  QueryImpl
    (OracleSpec.ofFn fun x ↦
      Option (Rho × I × Rand))
    (StateT (CKAScheme.GameState St I Rho)
      ProbComp)

**O-Send-A-rleak.** Like `O-Send-A`, but returns the randomness used by
A's send when the post-increment epoch is before the `ΔPCS` challenge window.

defdefined in SecureMessaging/CKA/Defs.lean

complete

def CKAScheme.oracleSendBrleak {IK St I Rho Rand : Type}
  (gp : CKAScheme.GameParams)
  (cka : CKAScheme ProbComp IK St I Rho Rand) :
  QueryImpl (OracleSpec.ofFn fun x ↦ Option (Rho × I × Rand))
    (StateT (CKAScheme.GameState St I Rho) ProbComp)

def CKAScheme.oracleSendBrleak
  {IK St I Rho Rand : Type}
  (gp : CKAScheme.GameParams)
  (cka :
    CKAScheme ProbComp IK St I Rho Rand) :
  QueryImpl
    (OracleSpec.ofFn fun x ↦
      Option (Rho × I × Rand))
    (StateT (CKAScheme.GameState St I Rho)
      ProbComp)

**O-Send-B-rleak.** Like `O-Send-B`, but returns the randomness used by
B's send when the post-increment epoch is before the `ΔPCS` challenge window.

defdefined in SecureMessaging/CKA/Defs.lean

complete

def CKAScheme.oracleRecvA {IK St I Rho Rand : Type} [DecidableEq I]
  (cka : CKAScheme ProbComp IK St I Rho Rand) :
  QueryImpl (OracleSpec.ofFn fun x ↦ Unit)
    (StateT (CKAScheme.GameState St I Rho) ProbComp)

def CKAScheme.oracleRecvA
  {IK St I Rho Rand : Type}
  [DecidableEq I]
  (cka :
    CKAScheme ProbComp IK St I Rho Rand) :
  QueryImpl (OracleSpec.ofFn fun x ↦ Unit)
    (StateT (CKAScheme.GameState St I Rho)
      ProbComp)

**O-Recv-A.**
Increment epoch counter, run A's receive on B's pending message, and update
the internal `correct` flag.
`tA++; (keyA, stA') ← recvA(stA, ρB); correct := correct ∧ (keyA == keyB)`.

defdefined in SecureMessaging/CKA/Defs.lean

complete

def CKAScheme.oracleRecvB {IK St I Rho Rand : Type} [DecidableEq I]
  (cka : CKAScheme ProbComp IK St I Rho Rand) :
  QueryImpl (OracleSpec.ofFn fun x ↦ Unit)
    (StateT (CKAScheme.GameState St I Rho) ProbComp)

def CKAScheme.oracleRecvB
  {IK St I Rho Rand : Type}
  [DecidableEq I]
  (cka :
    CKAScheme ProbComp IK St I Rho Rand) :
  QueryImpl (OracleSpec.ofFn fun x ↦ Unit)
    (StateT (CKAScheme.GameState St I Rho)
      ProbComp)

**O-Recv-B.**
Increment epoch counter, run B's receive on A's pending message, and update
the internal `correct` flag.
`tB++; (keyB, stB') ← recvB(stB, ρA); correct := correct ∧ (keyB == keyA)`.

defdefined in SecureMessaging/CKA/Defs.lean

complete

def CKAScheme.oracleChallA {IK St I Rho Rand : Type}
  (gp : CKAScheme.GameParams) (isRandom : Bool) [SampleableType I]
  (cka : CKAScheme ProbComp IK St I Rho Rand) :
  QueryImpl (OracleSpec.ofFn fun x ↦ Option (Rho × I))
    (StateT (CKAScheme.GameState St I Rho) ProbComp)

def CKAScheme.oracleChallA
  {IK St I Rho Rand : Type}
  (gp : CKAScheme.GameParams)
  (isRandom : Bool) [SampleableType I]
  (cka :
    CKAScheme ProbComp IK St I Rho Rand) :
  QueryImpl
    (OracleSpec.ofFn fun x ↦
      Option (Rho × I))
    (StateT (CKAScheme.GameState St I Rho)
      ProbComp)

**O-Chall-A.**
Increment epoch counter, trigger send by A, return message and key.
Like `O-Send-A` but returns `b ? $ᵗ I : key` (real or
random key). Only fires when `challengedParty = A` and `tA = challengeEpoch`.

defdefined in SecureMessaging/CKA/Defs.lean

complete

def CKAScheme.oracleChallB {IK St I Rho Rand : Type}
  (gp : CKAScheme.GameParams) (isRandom : Bool) [SampleableType I]
  (cka : CKAScheme ProbComp IK St I Rho Rand) :
  QueryImpl (OracleSpec.ofFn fun x ↦ Option (Rho × I))
    (StateT (CKAScheme.GameState St I Rho) ProbComp)

def CKAScheme.oracleChallB
  {IK St I Rho Rand : Type}
  (gp : CKAScheme.GameParams)
  (isRandom : Bool) [SampleableType I]
  (cka :
    CKAScheme ProbComp IK St I Rho Rand) :
  QueryImpl
    (OracleSpec.ofFn fun x ↦
      Option (Rho × I))
    (StateT (CKAScheme.GameState St I Rho)
      ProbComp)

**O-Chall-B.**
Increment epoch counter, trigger send by B, return message and key.
Like `O-Send-B` but returns `b ? $ᵗ I : key` (real or
random key). Only fires when `challengedParty = B` and `tB = challengeEpoch`.

defdefined in SecureMessaging/CKA/Defs.lean

complete

def CKAScheme.oracleCorruptA (gp : CKAScheme.GameParams) (St I Rho : Type) :
  QueryImpl (OracleSpec.ofFn fun x ↦ Option St)
    (StateT (CKAScheme.GameState St I Rho) ProbComp)

def CKAScheme.oracleCorruptA
  (gp : CKAScheme.GameParams)
  (St I Rho : Type) :
  QueryImpl
    (OracleSpec.ofFn fun x ↦ Option St)
    (StateT (CKAScheme.GameState St I Rho)
      ProbComp)

**O-Corrupt-A.** Return `stA` if either the `ΔPCS` pre-challenge gate holds,
or A has advanced `ΔFS` epochs past the challenge.

defdefined in SecureMessaging/CKA/Defs.lean

complete

def CKAScheme.oracleCorruptB (gp : CKAScheme.GameParams) (St I Rho : Type) :
  QueryImpl (OracleSpec.ofFn fun x ↦ Option St)
    (StateT (CKAScheme.GameState St I Rho) ProbComp)

def CKAScheme.oracleCorruptB
  (gp : CKAScheme.GameParams)
  (St I Rho : Type) :
  QueryImpl
    (OracleSpec.ofFn fun x ↦ Option St)
    (StateT (CKAScheme.GameState St I Rho)
      ProbComp)

**O-Corrupt-B.** Return `stB` if either the `ΔPCS` pre-challenge gate holds,
or B has advanced `ΔFS` epochs past the challenge.

Definition3.1.3

Statement uses 2

Statement dependency previews

Preview

Definition 3.1.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 3

Reverse dependency previews

Preview

Theorem 3.2.3

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

\todo

Let \O = \{\OSendA, \ORecA, \OSendB, \ORecB\}.

specification for oracle interfaces

def ckaCorrectnessSpec (Rho I : Type) :=
  unifSpec                        -- Uniform randomness
  + (Unit →ₒ Option (Rho × I))   -- O-Send-A (outputs message and key)
  + (Unit →ₒ Unit)               -- O-Recv-A (no adversary I/O; delivers the pending sent message)
  + (Unit →ₒ Option (Rho × I))   -- O-Send-B (outputs message and key)
  + (Unit →ₒ Unit)               -- O-Recv-B (no adversary I/O; delivers the pending sent message)

oracle set \O

def ckaCorrectnessImpl [DecidableEq I] (cka : CKAScheme ProbComp IK St I Rho Rand) :
    QueryImpl (ckaCorrectnessSpec Rho I) (StateT (GameState St I Rho) ProbComp) :=
  oracleUnif St I Rho
    + oracleSendA cka + oracleRecvA cka
    + oracleSendB cka + oracleRecvB cka

type of adversaries with oracle access to \O

abbrev CKACorrectnessAdversary (Rho I : Type) := OracleComp (ckaCorrectnessSpec Rho I) Bool

\Exp{\textsf{cor}}{\textsf{CKA}}(\adv)

\lcka \sample \mathsf{Init\text{-}KeyGen}(1^\lambda);\quad \stA \getsval \InitA(\lcka);\quad \stB \getsval \InitB(\lcka)

b' \getsval \adv^{\O};\quad \Return \mathsf{correct}

def correctnessExp [DecidableEq I] (cka : CKAScheme ProbComp IK St I Rho Rand)
    (adversary : CKACorrectnessAdversary Rho I) : ProbComp Bool := do
  let ik ← cka.initKeyGen
  let stA ← cka.initA ik
  let stB ← cka.initB ik
  let (_, state) ←
    (simulateQ (ckaCorrectnessImpl cka) adversary).run (initGameState stA stB)
  return state.correct

uses Definition 3.1.1 · Definition 3.1.2 · github #196

Lean code for Definition3.1.3●3 definitions

defdefined in SecureMessaging/CKA/Defs.lean

complete

def CKAScheme.correctnessExp {IK St I Rho Rand : Type} [DecidableEq I]
  (cka : CKAScheme ProbComp IK St I Rho Rand)
  (adversary : CKAScheme.CKACorrectnessAdversary Rho I) : ProbComp Bool

def CKAScheme.correctnessExp
  {IK St I Rho Rand : Type}
  [DecidableEq I]
  (cka :
    CKAScheme ProbComp IK St I Rho Rand)
  (adversary :
    CKAScheme.CKACorrectnessAdversary Rho
      I) :
  ProbComp Bool

**Correctness experiment** `Expᶜᵒʳʳ(cka, 𝒜)`

Initialize both parties from common initial key material, then run the
adversary with access to the honest send/receive oracles. The experiment
returns whether all delivered epoch keys matched.

  `ik   ←$ cka.initKeyGen()`
  `stA  ← cka.initA(ik); stB ← cka.initB(ik)`
  `σ_0  := initGameState(stA, stB)`
  `(_,σ_f)  ← 𝒜^O(σ_0)`,        where `O = (O-Send-A, O-Recv-A, O-Send-B, O-Recv-B)`
  `output σ_f.correct`

defdefined in SecureMessaging/CKA/Defs.lean

complete

def CKAScheme.ckaCorrectnessImpl {IK St I Rho Rand : Type} [DecidableEq I]
  (cka : CKAScheme ProbComp IK St I Rho Rand) :
  QueryImpl (CKAScheme.ckaCorrectnessSpec Rho I)
    (StateT (CKAScheme.GameState St I Rho) ProbComp)

def CKAScheme.ckaCorrectnessImpl
  {IK St I Rho Rand : Type}
  [DecidableEq I]
  (cka :
    CKAScheme ProbComp IK St I Rho Rand) :
  QueryImpl
    (CKAScheme.ckaCorrectnessSpec Rho I)
    (StateT (CKAScheme.GameState St I Rho)
      ProbComp)

Oracle set for the correctness game.

abbrevdefined in SecureMessaging/CKA/Defs.lean

complete

abbrev CKAScheme.CKACorrectnessAdversary (Rho I : Type) : Type

abbrev CKAScheme.CKACorrectnessAdversary
  (Rho I : Type) : Type

Correctness adversary: send + recv oracles only.

Definition3.1.4

Statement uses 2

Statement dependency previews

Preview

Definition 3.1.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

Used by 4

Reverse dependency previews

Preview

Definition 3.1.5

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

\todo

Let \O = \{\OSendA, \ORecA, \OChallA, \OCorrA, \OSendARLeak, \OSendB, \ORecB, \OChallB, \OCorrB, \OSendBRLeak\}.

specification for oracle interfaces

def ckaSecuritySpec (St Rho I Rand : Type) :=
  ckaCorrectnessSpec Rho I
  + (Unit →ₒ Option (Rho × I))   -- O-Chall-A (outputs message and key)
  + (Unit →ₒ Option (Rho × I))   -- O-Chall-B (outputs message and key)
  + (Unit →ₒ Option St)           -- O-Corrupt-A (outputs party state)
  + (Unit →ₒ Option St)           -- O-Corrupt-B (outputs party state)
  + (Unit →ₒ Option (Rho × I × Rand)) -- O-Send-A-rleak
  + (Unit →ₒ Option (Rho × I × Rand)) -- O-Send-B-rleak

oracle set \O

def ckaSecurityImpl (gp : GameParams) (isRandom : Bool) [SampleableType I] [DecidableEq I]
    (cka : CKAScheme ProbComp IK St I Rho Rand) :
    QueryImpl (ckaSecuritySpec St Rho I Rand) (StateT (GameState St I Rho) ProbComp) :=
  ckaCorrectnessImpl cka
    + oracleChallA gp isRandom cka + oracleChallB gp isRandom cka
    + oracleCorruptA gp St I Rho + oracleCorruptB gp St I Rho
    + oracleSendArleak gp cka + oracleSendBrleak gp cka

type of adversaries with oracle access to \O

abbrev CKAAdversary (St Rho I Rand : Type) := OracleComp (ckaSecuritySpec St Rho I Rand) Bool

\Exp{\textsf{sec}}{\textsf{CKA}}(\adv)

\lcka \sample \mathsf{Init\text{-}KeyGen}(1^\lambda);\quad \stA \getsval \InitA(\lcka);\quad \stB \getsval \InitB(\lcka);\quad t_\mathsf{A},t_\mathsf{B} \getsval 0;\quad b \sample \{0,1\}

b' \getsval \adv^{\O};\quad \Return[b'=b]

def securityExp [SampleableType I] [DecidableEq I] (cka : CKAScheme ProbComp IK St I Rho Rand)
  (adversary : CKAAdversary St Rho I Rand)
    (gp : GameParams) : ProbComp Bool := do
  let ik ← cka.initKeyGen
  let stA ← cka.initA ik
  let stB ← cka.initB ik
  let b ← $ᵗ Bool
  let (b', _) ← (simulateQ (ckaSecurityImpl gp b cka) adversary).run (initGameState stA stB)
  return (b == b')

uses Definition 3.1.1 · Definition 3.1.2 · github #197

Lean code for Definition3.1.4●3 definitions

defdefined in SecureMessaging/CKA/Defs.lean

complete

def CKAScheme.securityExp {IK St I Rho Rand : Type} [SampleableType I]
  [DecidableEq I] (cka : CKAScheme ProbComp IK St I Rho Rand)
  (adversary : CKAScheme.CKAAdversary St Rho I Rand)
  (gp : CKAScheme.GameParams) : ProbComp Bool

def CKAScheme.securityExp
  {IK St I Rho Rand : Type}
  [SampleableType I] [DecidableEq I]
  (cka :
    CKAScheme ProbComp IK St I Rho Rand)
  (adversary :
    CKAScheme.CKAAdversary St Rho I Rand)
  (gp : CKAScheme.GameParams) :
  ProbComp Bool

**Security experiment** `Expˢᵉᶜ(cka, 𝒜, gp)`.

Initialize both parties, sample a challenge bit, then run the adversary with
access to the send, receive, challenge, and corruption oracles. The experiment
returns whether the adversary guesses the challenge bit.

  `ik   ←$ KeyGen()`
  `stA  ← initA(ik); stB ← initB(ik)`
  `b    ←$ {0,1}`
  `σ_0  := initGameState(stA, stB)`
  `(b', σ_f) ← 𝒜^{O_b}(σ_0)`,
    where `O_b` is `ckaSecurityImpl gp b cka`
  `output (b = b')`

As in [ACD19, Def. 13, Fig. 3].

defdefined in SecureMessaging/CKA/Defs.lean

complete

def CKAScheme.ckaSecurityImpl {IK St I Rho Rand : Type}
  (gp : CKAScheme.GameParams) (isRandom : Bool) [SampleableType I]
  [DecidableEq I] (cka : CKAScheme ProbComp IK St I Rho Rand) :
  QueryImpl (CKAScheme.ckaSecuritySpec St Rho I Rand)
    (StateT (CKAScheme.GameState St I Rho) ProbComp)

def CKAScheme.ckaSecurityImpl
  {IK St I Rho Rand : Type}
  (gp : CKAScheme.GameParams)
  (isRandom : Bool) [SampleableType I]
  [DecidableEq I]
  (cka :
    CKAScheme ProbComp IK St I Rho Rand) :
  QueryImpl
    (CKAScheme.ckaSecuritySpec St Rho I
      Rand)
    (StateT (CKAScheme.GameState St I Rho)
      ProbComp)

Oracle set for the security game.

abbrevdefined in SecureMessaging/CKA/Defs.lean

complete

abbrev CKAScheme.CKAAdversary (St Rho I Rand : Type) : Type

abbrev CKAScheme.CKAAdversary
  (St Rho I Rand : Type) : Type

Security adversary: send + recv + challenge + corruption + rleak oracles.

Definition3.1.5

uses 1used by 0✓L∃∀N

\todo

\Adv{\textsf{guess}}(\adv, gp) \;=\; \Bigl|\, \Pr\bigl[\,\Exp{\textsf{sec}}{\textsf{CKA}}(\adv,gp) = 1\,\bigr] - \tfrac12 \,\Bigr| \;=\; \Bigl|\, \Pr[\,b' = b\,] - \tfrac12 \,\Bigr|

noncomputable def ckaGuessAdvantage [SampleableType I] [DecidableEq I]
    (cka : CKAScheme ProbComp IK St I Rho Rand) (adversary : CKAAdversary St Rho I Rand)
    (gp : GameParams) : ℝ :=
  |(Pr[= true | securityExp cka adversary gp]).toReal - 1 / 2|

uses Definition 3.1.4

Lean code for Definition3.1.5●1 definition

defdefined in SecureMessaging/CKA/Defs.lean

complete

def CKAScheme.ckaGuessAdvantage {IK St I Rho Rand : Type} [SampleableType I]
  [DecidableEq I] (cka : CKAScheme ProbComp IK St I Rho Rand)
  (adversary : CKAScheme.CKAAdversary St Rho I Rand)
  (gp : CKAScheme.GameParams) : ℝ

def CKAScheme.ckaGuessAdvantage
  {IK St I Rho Rand : Type}
  [SampleableType I] [DecidableEq I]
  (cka :
    CKAScheme ProbComp IK St I Rho Rand)
  (adversary :
    CKAScheme.CKAAdversary St Rho I Rand)
  (gp : CKAScheme.GameParams) : ℝ

CKA guess advantage: `|Pr[Win] - 1/2|`.