9.1. SCKA Definitions
Definition9.1.1
\todo
structure SCKAScheme (m : Type → Type u) [Monad m] (IK StA StB I Rho Rand : Type) where
/-- Samples the initial common value. -/
initKeyGen : m IK
/-- Initializes A's local state from the initial key. -/
initA : IK → m StA
/-- Initializes B's local state from the initial key. -/
initB : IK → m StB
/-- Party A's send: returns an optional (epoch,key) pair, the message sent to B,
the sending epoch, and A's next state. -/
sendA : StA → m (Option (Option (ℕ × I) × Rho × ℕ × StA))
/-- Party A's randomness-leaking send: also returns the randomness used for the send. -/
sendArleak : StA → m (Option (Option (ℕ × I) × Rho × ℕ × StA × Rand))
/-- Party A's receive: returns the optional derived (epoch,key) pair, the receiving
epoch, and A's next state. -/
recvA : StA → Rho → Option (Option (ℕ × I) × ℕ × StA)
/-- Party B's send: returns an optional (epoch,key) pair, the message sent to A,
the sending epoch, and B's next state. -/
sendB : StB → m (Option (Option (ℕ × I) × Rho × ℕ × StB))
/-- Party B's randomness-leaking send: also returns the randomness used for the send. -/
sendBrleak : StB → m (Option (Option (ℕ × I) × Rho × ℕ × StB × Rand))
/-- Party B's receive: returns the optional derived (epoch,key) pair, the receiving
epoch, and B's next state. -/
recvB : StB → Rho → Option (Option (ℕ × I) × ℕ × StB)
github #183
Lean code for Definition9.1.1●1 definition
Associated Lean declarations
-
SCKAScheme[complete]
Associated Lean declarations
-
SCKAScheme[complete]
-
structuredefined in SecureMessaging/SCKA/Defs.leancomplete
structure SCKAScheme.{u} (m : Type → Type u) [Monad m] (IK StA StB I Rho Rand : Type) : Type u
structure SCKAScheme.{u} (m : Type → Type u) [Monad m] (IK StA StB I Rho Rand : Type) : Type u
A sparse continuous key agreement scheme. - `IK`: initial common value, - `StA`: local state for party A, - `StB`: local state for party B, - `I`: epoch-key space, - `Rho`: protocol-message space, - `Rand`: randomness space used by sending algorithms.
Fields
initKeyGen : m IK
Samples the initial common value.
initA : IK → m StA
Initializes A's local state from the initial key.
initB : IK → m StB
Initializes B's local state from the initial key.
sendA : StA → m (Option (Option (ℕ × I) × Rho × ℕ × StA))
Party A's send: returns an optional (epoch,key) pair, the message sent to B, the sending epoch, and A's next state.
sendArleak : StA → m (Option (Option (ℕ × I) × Rho × ℕ × StA × Rand))
Party A's randomness-leaking send: also returns the randomness used for the send.
recvA : StA → Rho → Option (Option (ℕ × I) × ℕ × StA)
Party A's receive: returns the optional derived (epoch,key) pair, the receiving epoch, and A's next state.
sendB : StB → m (Option (Option (ℕ × I) × Rho × ℕ × StB))
Party B's send: returns an optional (epoch,key) pair, the message sent to A, the sending epoch, and B's next state.
sendBrleak : StB → m (Option (Option (ℕ × I) × Rho × ℕ × StB × Rand))
Party B's randomness-leaking send: also returns the randomness used for the send.
recvB : StB → Rho → Option (Option (ℕ × I) × ℕ × StB)
Party B's receive: returns the optional derived (epoch,key) pair, the receiving epoch, and B's next state.
Definition9.1.2
Group: SCKA. (3)
Used by 2
Associated Lean declarations
-
SCKAScheme.GameState[complete] -
SCKAScheme.oracleSendA[complete] -
SCKAScheme.oracleSendB[complete] -
SCKAScheme.oracleSendArleak[complete] -
SCKAScheme.oracleSendBrleak[complete] -
SCKAScheme.oracleRecvA[complete] -
SCKAScheme.oracleRecvB[complete] -
SCKAScheme.oracleChall[complete] -
SCKAScheme.oracleCorruptA[complete] -
SCKAScheme.oracleCorruptB[complete]
\mathsf{state}=
(\stA,\stB,\mathsf{Key},\mathsf{Msg},n_\A,n_\B,
t^\mathsf{cur}_\A,t^\mathsf{cur}_\B,
\mathsf{Exposed},\mathsf{Challenged},\mathsf{correct})
-
\stA,\stB: local protocol states for parties A and B. -
\mathsf{Key}[P,t]: partyP's key for epocht. -
\mathsf{Msg}[P,n]: partyP'snth message and its sending epoch. -
n_\A,n_\B: numbers of messages sent by A and B. -
t^\mathsf{cur}_\A,t^\mathsf{cur}_\B: current epochs of A and B. -
\mathsf{Exposed},\mathsf{Challenged}: exposed and challenged epochs. -
\mathsf{correct}: whether all correctness assertions have held.
structure GameState (StA StB I Rho : Type) where
/-- Local protocol state for party A. -/
stA : StA
/-- Local protocol state for party B. -/
stB : StB
/-- Key table for A: `Key[A, t]`. -/
keyA : ℕ → Option I
/-- Key table for B: `Key[B, t]`. -/
keyB : ℕ → Option I
/-- Transit array for A's messages: `Msg[A, n] = (ρ, t^snd)`. -/
msgA : ℕ → Option (Rho × ℕ)
/-- Transit array for B's messages: `Msg[B, n] = (ρ, t^snd)`. -/
msgB : ℕ → Option (Rho × ℕ)
/-- Number of messages A has sent. -/
nA : ℕ
/-- Number of messages B has sent. -/
nB : ℕ
/-- A's current epoch `t^cur_A`. -/
tcurA : ℕ
/-- B's current epoch `t^cur_B`. -/
tcurB : ℕ
/-- Epochs exposed through corruption or randomness leakage. -/
exposed : Finset ℕ
/-- Epochs already challenged. -/
challenged : Finset ℕ
/-- Whether all correctness asserts have held so far. -/
correct : Bool\OSendA
\begin{array}{l}
((t_{I_\A},I_\A),\rho,t^\mathsf{snd}_\A,\stA')
\sample \SendA(\stA); \\
\mathsf{assert}\;t^\mathsf{snd}_\A\ge t^\mathsf{cur}_\A; \\
t^\mathsf{cur}_\A\gets t^\mathsf{snd}_\A; \\
\pif\;(t_{I_\A},I_\A)\ne(\bot,\bot)\;\pthen \\
\quad\mathsf{assert}\;\mathsf{Key}[\A,t_{I_\A}]=\bot; \\
\quad\mathsf{assert}\;\mathsf{Key}[\B,t_{I_\A}]\in\{I_\A,\bot\}; \\
\quad\mathsf{Key}[\A,t_{I_\A}]\gets I_\A; \\
\mathsf{assert}\;\forall t\in\{1,\ldots,t^\mathsf{snd}_\A\},\;
\mathsf{Key}[\A,t]\ne\bot; \\
\mathsf{Msg}[\A,{+}{+}n_\A]\gets(\rho,t^\mathsf{snd}_\A); \\
\Return(t^\mathsf{snd}_\A,t_{I_\A},\rho)
\end{array}
def oracleSendA [DecidableEq I] (scka : SCKAScheme ProbComp IK StA StB I Rho Rand) :
QueryImpl (Unit →ₒ Option (ℕ × Option ℕ × Rho))
(StateT (GameState StA StB I Rho) ProbComp) :=
fun () => do
let state ← get
match ← liftM (scka.sendA state.stA) with
| none => pure none
| some (keyOpt, ρ, tsnd, stA') =>
let assertMonotonicity := state.tcurA ≤ tsnd
let assertKnownPrefix (keyA : ℕ → Option I) :=
(List.range (tsnd + 1)).all (fun t => t = 0 || (keyA t).isSome)
let nA' := state.nA + 1
let msgA' := Function.update state.msgA nA' (some (ρ, tsnd))
match keyOpt with
| none =>
set { state with
stA := stA', tcurA := tsnd, msgA := msgA', nA := nA',
correct := state.correct && assertMonotonicity && assertKnownPrefix state.keyA }
return some (tsnd, none, ρ)
| some (tI, key) =>
let assertUniqueEpochs := (state.keyA tI).isNone
let assertConsistentKeys := (state.keyB tI).isNone || state.keyB tI == some key
let keyA' := Function.update state.keyA tI (some key)
set { state with
stA := stA', tcurA := tsnd, keyA := keyA', msgA := msgA', nA := nA',
correct := state.correct
&& assertMonotonicity && assertUniqueEpochs
&& assertConsistentKeys && assertKnownPrefix keyA' }
return some (tsnd, some tI, ρ)\OSendB
\begin{array}{l}
((t_{I_\B},I_\B),\rho,t^\mathsf{snd}_\B,\stB')
\sample \SendB(\stB); \\
\mathsf{assert}\;t^\mathsf{snd}_\B\ge t^\mathsf{cur}_\B; \\
t^\mathsf{cur}_\B\gets t^\mathsf{snd}_\B; \\
\pif\;(t_{I_\B},I_\B)\ne(\bot,\bot)\;\pthen \\
\quad\mathsf{assert}\;\mathsf{Key}[\B,t_{I_\B}]=\bot; \\
\quad\mathsf{assert}\;\mathsf{Key}[\A,t_{I_\B}]\in\{I_\B,\bot\}; \\
\quad\mathsf{Key}[\B,t_{I_\B}]\gets I_\B; \\
\mathsf{assert}\;\forall t\in\{1,\ldots,t^\mathsf{snd}_\B\},\;
\mathsf{Key}[\B,t]\ne\bot; \\
\mathsf{Msg}[\B,{+}{+}n_\B]\gets(\rho,t^\mathsf{snd}_\B); \\
\Return(t^\mathsf{snd}_\B,t_{I_\B},\rho)
\end{array}
def oracleSendB [DecidableEq I] (scka : SCKAScheme ProbComp IK StA StB I Rho Rand) :
QueryImpl (Unit →ₒ Option (ℕ × Option ℕ × Rho))
(StateT (GameState StA StB I Rho) ProbComp) :=
fun () => do
let state ← get
match ← liftM (scka.sendB state.stB) with
| none => pure none
| some (keyOpt, ρ, tsnd, stB') =>
let assertMonotonicity := state.tcurB ≤ tsnd
let assertKnownPrefix (keyB : ℕ → Option I) :=
(List.range (tsnd + 1)).all (fun t => t = 0 || (keyB t).isSome)
let nB' := state.nB + 1
let msgB' := Function.update state.msgB nB' (some (ρ, tsnd))
match keyOpt with
| none =>
set { state with
stB := stB', tcurB := tsnd, msgB := msgB', nB := nB',
correct := state.correct && assertMonotonicity && assertKnownPrefix state.keyB }
return some (tsnd, none, ρ)
| some (tI, key) =>
let assertUniqueEpochs := (state.keyB tI).isNone
let assertConsistentKeys := (state.keyA tI).isNone || state.keyA tI == some key
let keyB' := Function.update state.keyB tI (some key)
set { state with
stB := stB', tcurB := tsnd, keyB := keyB', msgB := msgB', nB := nB',
correct := state.correct
&& assertMonotonicity && assertUniqueEpochs
&& assertConsistentKeys && assertKnownPrefix keyB' }
return some (tsnd, some tI, ρ)\OSendARLeak
\begin{array}{l}
V\gets\mathsf{vuln}_\A(\stA); \\
((t_{I_\A},I_\A),\rho,t^\mathsf{snd}_\A,\stA',r)
\sample \SendARLeak(\stA); \\
V'\gets\mathsf{vuln}_\A(\stA')\setminus V; \\
\req\;V'\cap\mathsf{Challenged}=\emptyset; \\
\mathsf{Exposed}\gets\mathsf{Exposed}\cup V'; \\
\mathsf{assert}\;t^\mathsf{snd}_\A\ge t^\mathsf{cur}_\A; \\
t^\mathsf{cur}_\A\gets t^\mathsf{snd}_\A; \\
\pif\;(t_{I_\A},I_\A)\ne(\bot,\bot)\;\pthen \\
\quad\mathsf{assert}\;\mathsf{Key}[\A,t_{I_\A}]=\bot; \\
\quad\mathsf{assert}\;\mathsf{Key}[\B,t_{I_\A}]\in\{I_\A,\bot\}; \\
\quad\mathsf{Key}[\A,t_{I_\A}]\gets I_\A; \\
\mathsf{assert}\;\forall t\in\{1,\ldots,t^\mathsf{snd}_\A\},\;
\mathsf{Key}[\A,t]\ne\bot; \\
\mathsf{Msg}[\A,{+}{+}n_\A]\gets(\rho,t^\mathsf{snd}_\A); \\
\Return(t^\mathsf{snd}_\A,t_{I_\A},\rho,r)
\end{array}
def oracleSendArleak [DecidableEq I] (vulnA : StA → Finset ℕ)
(scka : SCKAScheme ProbComp IK StA StB I Rho Rand) :
QueryImpl (Unit →ₒ Option (ℕ × Option ℕ × Rho × Rand))
(StateT (GameState StA StB I Rho) ProbComp) :=
fun () => do
let state ← get
let vulnOld := vulnA state.stA
match ← liftM (scka.sendArleak state.stA) with
| none => pure none
| some (keyOpt, ρ, tsnd, stA', rand) =>
let vuln' := vulnA stA' \ vulnOld
-- req vuln' ∩ Challenged = ∅
if vuln' ∩ state.challenged ≠ ∅ then pure none
else
let exposed' := state.exposed ∪ vuln'
let assertMonotonicity := state.tcurA ≤ tsnd
let assertKnownPrefix (keyA : ℕ → Option I) :=
(List.range (tsnd + 1)).all (fun t => t = 0 || (keyA t).isSome)
let nA' := state.nA + 1
let msgA' := Function.update state.msgA nA' (some (ρ, tsnd))
match keyOpt with
| none =>
set { state with
stA := stA', tcurA := tsnd, exposed := exposed',
msgA := msgA', nA := nA',
correct := state.correct && assertMonotonicity && assertKnownPrefix state.keyA }
return some (tsnd, none, ρ, rand)
| some (tI, key) =>
let assertUniqueEpochs := (state.keyA tI).isNone
let assertConsistentKeys := (state.keyB tI).isNone || state.keyB tI == some key
let keyA' := Function.update state.keyA tI (some key)
set { state with
stA := stA', tcurA := tsnd, exposed := exposed', keyA := keyA',
msgA := msgA', nA := nA',
correct := state.correct
&& assertMonotonicity && assertUniqueEpochs
&& assertConsistentKeys && assertKnownPrefix keyA' }
return some (tsnd, some tI, ρ, rand)\OSendBRLeak
\begin{array}{l}
V\gets\mathsf{vuln}_\B(\stB); \\
((t_{I_\B},I_\B),\rho,t^\mathsf{snd}_\B,\stB',r)
\sample \SendBRLeak(\stB); \\
V'\gets\mathsf{vuln}_\B(\stB')\setminus V; \\
\req\;V'\cap\mathsf{Challenged}=\emptyset; \\
\mathsf{Exposed}\gets\mathsf{Exposed}\cup V'; \\
\mathsf{assert}\;t^\mathsf{snd}_\B\ge t^\mathsf{cur}_\B; \\
t^\mathsf{cur}_\B\gets t^\mathsf{snd}_\B; \\
\pif\;(t_{I_\B},I_\B)\ne(\bot,\bot)\;\pthen \\
\quad\mathsf{assert}\;\mathsf{Key}[\B,t_{I_\B}]=\bot; \\
\quad\mathsf{assert}\;\mathsf{Key}[\A,t_{I_\B}]\in\{I_\B,\bot\}; \\
\quad\mathsf{Key}[\B,t_{I_\B}]\gets I_\B; \\
\mathsf{assert}\;\forall t\in\{1,\ldots,t^\mathsf{snd}_\B\},\;
\mathsf{Key}[\B,t]\ne\bot; \\
\mathsf{Msg}[\B,{+}{+}n_\B]\gets(\rho,t^\mathsf{snd}_\B); \\
\Return(t^\mathsf{snd}_\B,t_{I_\B},\rho,r)
\end{array}
def oracleSendBrleak [DecidableEq I] (vulnB : StB → Finset ℕ)
(scka : SCKAScheme ProbComp IK StA StB I Rho Rand) :
QueryImpl (Unit →ₒ Option (ℕ × Option ℕ × Rho × Rand))
(StateT (GameState StA StB I Rho) ProbComp) :=
fun () => do
let state ← get
let vulnOld := vulnB state.stB
match ← liftM (scka.sendBrleak state.stB) with
| none => pure none
| some (keyOpt, ρ, tsnd, stB', rand) =>
let vuln' := vulnB stB' \ vulnOld
if vuln' ∩ state.challenged ≠ ∅ then pure none
else
let exposed' := state.exposed ∪ vuln'
let assertMonotonicity := state.tcurB ≤ tsnd
let assertKnownPrefix (keyB : ℕ → Option I) :=
(List.range (tsnd + 1)).all (fun t => t = 0 || (keyB t).isSome)
let nB' := state.nB + 1
let msgB' := Function.update state.msgB nB' (some (ρ, tsnd))
match keyOpt with
| none =>
set { state with
stB := stB', tcurB := tsnd, exposed := exposed',
msgB := msgB', nB := nB',
correct := state.correct && assertMonotonicity && assertKnownPrefix state.keyB }
return some (tsnd, none, ρ, rand)
| some (tI, key) =>
let assertUniqueEpochs := (state.keyB tI).isNone
let assertConsistentKeys := (state.keyA tI).isNone || state.keyA tI == some key
let keyB' := Function.update state.keyB tI (some key)
set { state with
stB := stB', tcurB := tsnd, exposed := exposed', keyB := keyB',
msgB := msgB', nB := nB',
correct := state.correct
&& assertMonotonicity && assertUniqueEpochs
&& assertConsistentKeys && assertKnownPrefix keyB' }
return some (tsnd, some tI, ρ, rand)\ORecA(n)
\begin{array}{l}
\req\;\mathsf{Msg}[\B,n]\ne\bot; \\
(\rho,t^\mathsf{snd}_\B)\gets\mathsf{Msg}[\B,n]; \\
r\getsval\RecA(\stA,\rho); \\
\pif\;r=\bot\;\pthen\;
\mathsf{correct}\gets\mathsf{false};\;\Return\bot; \\
((t_{I_\B},I_\B),t^\mathsf{rcv}_\A,\stA')\gets r; \\
\mathsf{assert}\;t^\mathsf{rcv}_\A=t^\mathsf{snd}_\B; \\
t^\mathsf{cur}_\A\gets
\max(t^\mathsf{cur}_\A,t^\mathsf{rcv}_\A); \\
\pif\;(t_{I_\B},I_\B)\ne(\bot,\bot)\;\pthen \\
\quad\mathsf{assert}\;\mathsf{Key}[\A,t_{I_\B}]=\bot; \\
\quad\mathsf{assert}\;\mathsf{Key}[\B,t_{I_\B}]\in\{I_\B,\bot\}; \\
\quad\mathsf{Key}[\A,t_{I_\B}]\gets I_\B; \\
\mathsf{assert}\;\forall t\in\{1,\ldots,t^\mathsf{cur}_\A\},\;
\mathsf{Key}[\A,t]\ne\bot; \\
\Return(t^\mathsf{rcv}_\A,t_{I_\B})
\end{array}
def oracleRecvA [DecidableEq I] (scka : SCKAScheme ProbComp IK StA StB I Rho Rand) :
QueryImpl (ℕ →ₒ Option (ℕ × Option ℕ))
(StateT (GameState StA StB I Rho) ProbComp) :=
fun (n : ℕ) => do
let state ← get
-- req Msg[B, n] ≠ ⊥
match state.msgB n with
| none => pure none
| some (ρ, tsndB) =>
match scka.recvA state.stA ρ with
| none =>
-- honest delivery should succeed; failure is a correctness violation.
set { state with correct := false }
return none
| some (keyOpt, trcv, stA') =>
let tcurA' := max state.tcurA trcv
let assertMatchingEpoch := trcv == tsndB
let assertKnownPrefix (keyA : ℕ → Option I) :=
(List.range (tcurA' + 1)).all (fun t => t = 0 || (keyA t).isSome)
match keyOpt with
| none =>
set { state with
stA := stA', tcurA := tcurA',
correct := state.correct && assertMatchingEpoch && assertKnownPrefix state.keyA }
return some (trcv, none)
| some (tI, key) =>
let assertUniqueEpochs := (state.keyA tI).isNone
let assertConsistentKeys := (state.keyB tI).isNone || state.keyB tI == some key
let keyA' := Function.update state.keyA tI (some key)
set { state with
stA := stA', tcurA := tcurA', keyA := keyA',
correct := state.correct
&& assertMatchingEpoch && assertUniqueEpochs
&& assertConsistentKeys && assertKnownPrefix keyA' }
return some (trcv, some tI)\ORecB(n)
\begin{array}{l}
\req\;\mathsf{Msg}[\A,n]\ne\bot; \\
(\rho,t^\mathsf{snd}_\A)\gets\mathsf{Msg}[\A,n]; \\
r\getsval\RecB(\stB,\rho); \\
\pif\;r=\bot\;\pthen\;
\mathsf{correct}\gets\mathsf{false};\;\Return\bot; \\
((t_{I_\A},I_\A),t^\mathsf{rcv}_\B,\stB')\gets r; \\
\mathsf{assert}\;t^\mathsf{rcv}_\B=t^\mathsf{snd}_\A; \\
t^\mathsf{cur}_\B\gets
\max(t^\mathsf{cur}_\B,t^\mathsf{rcv}_\B); \\
\pif\;(t_{I_\A},I_\A)\ne(\bot,\bot)\;\pthen \\
\quad\mathsf{assert}\;\mathsf{Key}[\B,t_{I_\A}]=\bot; \\
\quad\mathsf{assert}\;\mathsf{Key}[\A,t_{I_\A}]\in\{I_\A,\bot\}; \\
\quad\mathsf{Key}[\B,t_{I_\A}]\gets I_\A; \\
\mathsf{assert}\;\forall t\in\{1,\ldots,t^\mathsf{cur}_\B\},\;
\mathsf{Key}[\B,t]\ne\bot; \\
\Return(t^\mathsf{rcv}_\B,t_{I_\A})
\end{array}
def oracleRecvB [DecidableEq I] (scka : SCKAScheme ProbComp IK StA StB I Rho Rand) :
QueryImpl (ℕ →ₒ Option (ℕ × Option ℕ))
(StateT (GameState StA StB I Rho) ProbComp) :=
fun (n : ℕ) => do
let state ← get
match state.msgA n with
| none => pure none
| some (ρ, tsndA) =>
match scka.recvB state.stB ρ with
| none =>
set { state with correct := false }
return none
| some (keyOpt, trcv, stB') =>
let tcurB' := max state.tcurB trcv
let assertMatchingEpoch := trcv == tsndA
let assertKnownPrefix (keyB : ℕ → Option I) :=
(List.range (tcurB' + 1)).all (fun t => t = 0 || (keyB t).isSome)
match keyOpt with
| none =>
set { state with
stB := stB', tcurB := tcurB',
correct := state.correct && assertMatchingEpoch && assertKnownPrefix state.keyB }
return some (trcv, none)
| some (tI, key) =>
let assertUniqueEpochs := (state.keyB tI).isNone
let assertConsistentKeys := (state.keyA tI).isNone || state.keyA tI == some key
let keyB' := Function.update state.keyB tI (some key)
set { state with
stB := stB', tcurB := tcurB', keyB := keyB',
correct := state.correct
&& assertMatchingEpoch && assertUniqueEpochs
&& assertConsistentKeys && assertKnownPrefix keyB' }
return some (trcv, some tI)\OChall(t)
\begin{array}{l}
\req\;t\notin\mathsf{Exposed}\cup\mathsf{Challenged}; \\
\pif\;\mathsf{Key}[\A,t]\ne\bot\;\pthen \\
\quad K\gets\mathsf{Key}[\A,t]; \\
\pelse \\
\quad K\gets\mathsf{Key}[\B,t]; \\
\req\;K\ne\bot; \\
\pif\;b=1\;\pthen\;K\sample I; \\
\mathsf{Challenged}\gets\mathsf{Challenged}\cup\{t\}; \\
\Return K
\end{array}
def oracleChall (isRandom : Bool) (StA StB I Rho : Type) [SampleableType I] :
QueryImpl (ℕ →ₒ Option I) (StateT (GameState StA StB I Rho) ProbComp) :=
fun (t : ℕ) => do
let state ← get
-- req t ∉ Exposed ∪ Challenged
if t ∈ state.exposed ∨ t ∈ state.challenged then pure none
else
let key? := match state.keyA t with
| some k => some k
| none => state.keyB t
match key? with
| none => pure none -- req K ≠ ⊥
| some k =>
let outK ← if isRandom then liftM ($ᵗ I : ProbComp I) else pure k
set { state with challenged := insert t state.challenged }
return some outK\OCorrA
\begin{array}{l}
V\gets\mathsf{vuln}_\A(\stA); \\
\req\;V\cap\mathsf{Challenged}=\emptyset; \\
\mathsf{Exposed}\gets\mathsf{Exposed}\cup V; \\
\Return\stA
\end{array}
def oracleCorruptA (vulnA : StA → Finset ℕ) (StB I Rho : Type) :
QueryImpl (Unit →ₒ Option StA) (StateT (GameState StA StB I Rho) ProbComp) :=
fun () => do
let state ← get
let vuln := vulnA state.stA
if vuln ∩ state.challenged ≠ ∅ then pure none
else
set { state with exposed := state.exposed ∪ vuln }
return some state.stA\OCorrB
\begin{array}{l}
V\gets\mathsf{vuln}_\B(\stB); \\
\req\;V\cap\mathsf{Challenged}=\emptyset; \\
\mathsf{Exposed}\gets\mathsf{Exposed}\cup V; \\
\Return\stB
\end{array}
def oracleCorruptB (vulnB : StB → Finset ℕ) (StA I Rho : Type) :
QueryImpl (Unit →ₒ Option StB) (StateT (GameState StA StB I Rho) ProbComp) :=
fun () => do
let state ← get
let vuln := vulnB state.stB
if vuln ∩ state.challenged ≠ ∅ then pure none
else
set { state with exposed := state.exposed ∪ vuln }
return some state.stB
uses Definition 9.1.1
Lean code for Definition9.1.2●10 definitions
Associated Lean declarations
-
SCKAScheme.GameState[complete]
-
SCKAScheme.oracleSendA[complete]
-
SCKAScheme.oracleSendB[complete]
-
SCKAScheme.oracleSendArleak[complete]
-
SCKAScheme.oracleSendBrleak[complete]
-
SCKAScheme.oracleRecvA[complete]
-
SCKAScheme.oracleRecvB[complete]
-
SCKAScheme.oracleChall[complete]
-
SCKAScheme.oracleCorruptA[complete]
-
SCKAScheme.oracleCorruptB[complete]
Associated Lean declarations
-
SCKAScheme.GameState[complete] -
SCKAScheme.oracleSendA[complete] -
SCKAScheme.oracleSendB[complete] -
SCKAScheme.oracleSendArleak[complete] -
SCKAScheme.oracleSendBrleak[complete] -
SCKAScheme.oracleRecvA[complete] -
SCKAScheme.oracleRecvB[complete] -
SCKAScheme.oracleChall[complete] -
SCKAScheme.oracleCorruptA[complete] -
SCKAScheme.oracleCorruptB[complete]
-
structuredefined in SecureMessaging/SCKA/Defs.leancomplete
structure SCKAScheme.GameState (StA StB I Rho : Type) : Type
structure SCKAScheme.GameState (StA StB I Rho : Type) : Type
Internal state of the SCKA game. - `stA`, `stB`: per-party protocol state. - `keyA`, `keyB`: tables with epoch keys derived by each party. - `msgA`, `msgB`: arrays storing sent messages and their epochs. - `nA`, `nB`: per-party send counters (number of messages sent so far). - `tcurA`, `tcurB`: per-party current epoch (latest usable epoch). - `exposed`: epochs exposed by corruption or randomness leakage. - `challenged`: epochs the adversary has challenged. - `correct`: whether all correctness properties have held so far.
Fields
stA : StA
Local protocol state for party A.
stB : StB
Local protocol state for party B.
keyA : ℕ → Option I
Key table for A: `Key[A, t]`.
keyB : ℕ → Option I
Key table for B: `Key[B, t]`.
msgA : ℕ → Option (Rho × ℕ)
Transit array for A's messages: `Msg[A, n] = (ρ, t^snd)`.
msgB : ℕ → Option (Rho × ℕ)
Transit array for B's messages: `Msg[B, n] = (ρ, t^snd)`.
nA : ℕ
Number of messages A has sent.
nB : ℕ
Number of messages B has sent.
tcurA : ℕ
A's current epoch `t^cur_A`.
tcurB : ℕ
B's current epoch `t^cur_B`.
exposed : Finset ℕ
Epochs exposed through corruption or randomness leakage.
challenged : Finset ℕ
Epochs already challenged.
correct : Bool
Whether all correctness asserts have held so far.
-
defdefined in SecureMessaging/SCKA/Defs.leancomplete
def SCKAScheme.oracleSendA {IK StA StB I Rho Rand : Type} [DecidableEq I] (scka : SCKAScheme ProbComp IK StA StB I Rho Rand) : QueryImpl (OracleSpec.ofFn fun x ↦ Option (ℕ × Option ℕ × Rho)) (StateT (SCKAScheme.GameState StA StB I Rho) ProbComp)
def SCKAScheme.oracleSendA {IK StA StB I Rho Rand : Type} [DecidableEq I] (scka : SCKAScheme ProbComp IK StA StB I Rho Rand) : QueryImpl (OracleSpec.ofFn fun x ↦ Option (ℕ × Option ℕ × Rho)) (StateT (SCKAScheme.GameState StA StB I Rho) ProbComp)
**O-Send-A** (plain, `rleak = 0`). ```text Send-A: ((tIA, IA), ρ, t^snd_A, stA) ←$ scka.sendA(stA) assert t^snd_A ≥ t^cur_A -- monotonicity t^cur_A ← t^snd_A if (tIA, IA) ≠ (⊥, ⊥): -- new key derived assert Key[A, tIA] = ⊥ -- unique epochs assert Key[B, tIA] ∈ {IA, ⊥} -- consistent keys Key[A, tIA] ← IA assert ∀ t ≤ t^snd_A : Key[A, t] ≠ ⊥ -- known prefix Msg[A, ++nA] ← (ρ, t^snd_A) return (t^snd_A, tIA, ρ) ``` -
defdefined in SecureMessaging/SCKA/Defs.leancomplete
def SCKAScheme.oracleSendB {IK StA StB I Rho Rand : Type} [DecidableEq I] (scka : SCKAScheme ProbComp IK StA StB I Rho Rand) : QueryImpl (OracleSpec.ofFn fun x ↦ Option (ℕ × Option ℕ × Rho)) (StateT (SCKAScheme.GameState StA StB I Rho) ProbComp)
def SCKAScheme.oracleSendB {IK StA StB I Rho Rand : Type} [DecidableEq I] (scka : SCKAScheme ProbComp IK StA StB I Rho Rand) : QueryImpl (OracleSpec.ofFn fun x ↦ Option (ℕ × Option ℕ × Rho)) (StateT (SCKAScheme.GameState StA StB I Rho) ProbComp)
**O-Send-B** (plain, `rleak = 0`). ```text Send-B: ((tIB, IB), ρ, t^snd_B, stB) ←$ scka.sendB(stB) assert t^snd_B ≥ t^cur_B -- monotonicity t^cur_B ← t^snd_B if (tIB, IB) ≠ (⊥, ⊥): -- new key derived assert Key[B, tIB] = ⊥ -- unique epochs assert Key[A, tIB] ∈ {IB, ⊥} -- consistent keys Key[B, tIB] ← IB assert ∀ t ≤ t^snd_B : Key[B, t] ≠ ⊥ -- known prefix Msg[B, ++nB] ← (ρ, t^snd_B) return (t^snd_B, tIB, ρ) ``` -
defdefined in SecureMessaging/SCKA/Defs.leancomplete
def SCKAScheme.oracleSendArleak {IK StA StB I Rho Rand : Type} [DecidableEq I] (vulnA : StA → Finset ℕ) (scka : SCKAScheme ProbComp IK StA StB I Rho Rand) : QueryImpl (OracleSpec.ofFn fun x ↦ Option (ℕ × Option ℕ × Rho × Rand)) (StateT (SCKAScheme.GameState StA StB I Rho) ProbComp)
def SCKAScheme.oracleSendArleak {IK StA StB I Rho Rand : Type} [DecidableEq I] (vulnA : StA → Finset ℕ) (scka : SCKAScheme ProbComp IK StA StB I Rho Rand) : QueryImpl (OracleSpec.ofFn fun x ↦ Option (ℕ × Option ℕ × Rho × Rand)) (StateT (SCKAScheme.GameState StA StB I Rho) ProbComp)
**O-Send-A-rleak** (`rleak = 1`). Like `O-Send-A`, but uses `sendArleak`, computes the newly vulnerable epochs `vuln' = vulnA stA' \ vulnA stA`, requires `vuln' ∩ Challenged = ∅`, adds `vuln'` to `Exposed`, and also returns the randomness. ```text Send-A-rleak: vuln ← stA.vuln ((tIA, IA), ρ, t^snd_A, stA) ←$ scka.sendArleak(stA) vuln' ← stA.vuln \ vuln -- newly vulnerable epochs req vuln' ∩ Challenged = ∅ Exposed ← Exposed ∪ vuln' assert t^snd_A ≥ t^cur_A -- monotonicity t^cur_A ← t^snd_A if (tIA, IA) ≠ (⊥, ⊥): assert Key[A, tIA] = ⊥ -- unique epochs assert Key[B, tIA] ∈ {IA, ⊥} -- consistent keys Key[A, tIA] ← IA assert ∀ t ≤ t^snd_A : Key[A, t] ≠ ⊥ -- known prefix Msg[A, ++nA] ← (ρ, t^snd_A) return (t^snd_A, tIA, ρ, rand) ``` -
defdefined in SecureMessaging/SCKA/Defs.leancomplete
def SCKAScheme.oracleSendBrleak {IK StA StB I Rho Rand : Type} [DecidableEq I] (vulnB : StB → Finset ℕ) (scka : SCKAScheme ProbComp IK StA StB I Rho Rand) : QueryImpl (OracleSpec.ofFn fun x ↦ Option (ℕ × Option ℕ × Rho × Rand)) (StateT (SCKAScheme.GameState StA StB I Rho) ProbComp)
def SCKAScheme.oracleSendBrleak {IK StA StB I Rho Rand : Type} [DecidableEq I] (vulnB : StB → Finset ℕ) (scka : SCKAScheme ProbComp IK StA StB I Rho Rand) : QueryImpl (OracleSpec.ofFn fun x ↦ Option (ℕ × Option ℕ × Rho × Rand)) (StateT (SCKAScheme.GameState StA StB I Rho) ProbComp)
**O-Send-B-rleak** (`rleak = 1`). Run B's randomness-leaking send, compute the newly vulnerable epochs `vuln' = vulnB stB' \ vulnB stB`, require `vuln' ∩ Challenged = ∅`, add `vuln'` to `Exposed`, and also return the randomness. ```text Send-B-rleak: vuln ← stB.vuln ((tIB, IB), ρ, t^snd_B, stB) ←$ scka.sendBrleak(stB) vuln' ← stB.vuln \ vuln -- newly vulnerable epochs req vuln' ∩ Challenged = ∅ Exposed ← Exposed ∪ vuln' assert t^snd_B ≥ t^cur_B -- monotonicity t^cur_B ← t^snd_B if (tIB, IB) ≠ (⊥, ⊥): assert Key[B, tIB] = ⊥ -- unique epochs assert Key[A, tIB] ∈ {IB, ⊥} -- consistent keys Key[B, tIB] ← IB assert ∀ t ≤ t^snd_B : Key[B, t] ≠ ⊥ -- known prefix Msg[B, ++nB] ← (ρ, t^snd_B) return (t^snd_B, tIB, ρ, rand) ``` -
defdefined in SecureMessaging/SCKA/Defs.leancomplete
def SCKAScheme.oracleRecvA {IK StA StB I Rho Rand : Type} [DecidableEq I] (scka : SCKAScheme ProbComp IK StA StB I Rho Rand) : QueryImpl (OracleSpec.ofFn fun x ↦ Option (ℕ × Option ℕ)) (StateT (SCKAScheme.GameState StA StB I Rho) ProbComp)
def SCKAScheme.oracleRecvA {IK StA StB I Rho Rand : Type} [DecidableEq I] (scka : SCKAScheme ProbComp IK StA StB I Rho Rand) : QueryImpl (OracleSpec.ofFn fun x ↦ Option (ℕ × Option ℕ)) (StateT (SCKAScheme.GameState StA StB I Rho) ProbComp)
**O-Recv-A n.** Deliver `Msg[B, n]` to A (`req Msg[B, n] ≠ ⊥`), run A's receive, check the matching epoch and key correctness asserts, and return `(t^rcv, t_I?)`. ```text Receive-A(n): 1 req Msg[B, n] ≠ ⊥ 2 (ρ, t^snd_B) ← Msg[B, n] 3 ((tIB, IB), t^rcv_A, stA) ← scka.recvA(stA, ρ) 4 assert t^rcv_A = t^snd_B -- matching epoch 5 t^cur_A ← max(t^cur_A, t^rcv_A) 6 if (tIB, IB) ≠ (⊥, ⊥): -- new key derived 7 assert Key[A, tIB] = ⊥ -- unique epochs 8 assert Key[B, tIB] ∈ {IB, ⊥} -- consistent keys 9 Key[A, tIB] ← IB 10 assert ∀ t ≤ t^cur_A : Key[A, t] ≠ ⊥ -- known prefix 11 return (t^rcv_A, tIB) ``` -
defdefined in SecureMessaging/SCKA/Defs.leancomplete
def SCKAScheme.oracleRecvB {IK StA StB I Rho Rand : Type} [DecidableEq I] (scka : SCKAScheme ProbComp IK StA StB I Rho Rand) : QueryImpl (OracleSpec.ofFn fun x ↦ Option (ℕ × Option ℕ)) (StateT (SCKAScheme.GameState StA StB I Rho) ProbComp)
def SCKAScheme.oracleRecvB {IK StA StB I Rho Rand : Type} [DecidableEq I] (scka : SCKAScheme ProbComp IK StA StB I Rho Rand) : QueryImpl (OracleSpec.ofFn fun x ↦ Option (ℕ × Option ℕ)) (StateT (SCKAScheme.GameState StA StB I Rho) ProbComp)
**O-Recv-B n.** Deliver `Msg[A, n]` to B (`req Msg[A, n] ≠ ⊥`), run B's receive, check the matching epoch and key correctness asserts, and return `(t^rcv, t_I?)`. ```text Receive-B(n): 1 req Msg[A, n] ≠ ⊥ 2 (ρ, t^snd_A) ← Msg[A, n] 3 ((tIA, IA), t^rcv_B, stB) ← scka.recvB(stB, ρ) 4 assert t^rcv_B = t^snd_A -- matching epoch 5 t^cur_B ← max(t^cur_B, t^rcv_B) 6 if (tIA, IA) ≠ (⊥, ⊥): 7 assert Key[B, tIA] = ⊥ -- unique epochs 8 assert Key[A, tIA] ∈ {IA, ⊥} -- consistent keys 9 Key[B, tIA] ← IA 10 assert ∀ t ≤ t^cur_B : Key[B, t] ≠ ⊥ -- known prefix 11 return (t^rcv_B, tIA) ``` -
defdefined in SecureMessaging/SCKA/Defs.leancomplete
def SCKAScheme.oracleChall (isRandom : Bool) (StA StB I Rho : Type) [SampleableType I] : QueryImpl (OracleSpec.ofFn fun x ↦ Option I) (StateT (SCKAScheme.GameState StA StB I Rho) ProbComp)
def SCKAScheme.oracleChall (isRandom : Bool) (StA StB I Rho : Type) [SampleableType I] : QueryImpl (OracleSpec.ofFn fun x ↦ Option I) (StateT (SCKAScheme.GameState StA StB I Rho) ProbComp)
**O-Chall t.** `req t ∉ Exposed ∪ Challenged`; take the recorded key for epoch `t`; return the real key (`isRandom = false`) or a freshly sampled uniform key (`isRandom = true`); record `t` as challenged. ```text Chall(t): 1 req t ∉ Exposed ∪ Challenged 2 if Key[A, t] ≠ ⊥: K ← Key[A, t] 4 else : K ← Key[B, t] 5 req K ≠ ⊥ 6 if b = 1: K ←$ I // replace with random key 8 Challenged ← Challenged ∪ {t} 9 return K ``` -
defdefined in SecureMessaging/SCKA/Defs.leancomplete
def SCKAScheme.oracleCorruptA {StA : Type} (vulnA : StA → Finset ℕ) (StB I Rho : Type) : QueryImpl (OracleSpec.ofFn fun x ↦ Option StA) (StateT (SCKAScheme.GameState StA StB I Rho) ProbComp)
def SCKAScheme.oracleCorruptA {StA : Type} (vulnA : StA → Finset ℕ) (StB I Rho : Type) : QueryImpl (OracleSpec.ofFn fun x ↦ Option StA) (StateT (SCKAScheme.GameState StA StB I Rho) ProbComp)
**O-Corrupt-A.** `req stA.vuln ∩ Challenged = ∅`; expose `stA.vuln`; return A's state. ```text Corr-A(): 1 req stA.vuln ∩ Challenged = ∅ // no challenge of a vulnerable epoch 2 Exposed ← Exposed ∪ stA.vuln 3 return stA ```
-
defdefined in SecureMessaging/SCKA/Defs.leancomplete
def SCKAScheme.oracleCorruptB {StB : Type} (vulnB : StB → Finset ℕ) (StA I Rho : Type) : QueryImpl (OracleSpec.ofFn fun x ↦ Option StB) (StateT (SCKAScheme.GameState StA StB I Rho) ProbComp)
def SCKAScheme.oracleCorruptB {StB : Type} (vulnB : StB → Finset ℕ) (StA I Rho : Type) : QueryImpl (OracleSpec.ofFn fun x ↦ Option StB) (StateT (SCKAScheme.GameState StA StB I Rho) ProbComp)
**O-Corrupt-B.** `req stB.vuln ∩ Challenged = ∅`; expose `stB.vuln`; return B's state. ```text Corr-B(): 1 req stB.vuln ∩ Challenged = ∅ // no challenge of a vulnerable epoch 2 Exposed ← Exposed ∪ stB.vuln 3 return stB ```
Definition9.1.3
Group: SCKA. (3)
Statement uses 2
Used by 5
Associated Lean declarations
-
SCKAScheme.sckaCorrectnessSpec[complete] -
SCKAScheme.sckaCorrectnessImpl[complete] -
SCKAScheme.SCKACorrectnessAdversary[complete] -
SCKAScheme.correctnessExp[complete]
\Ocor=\{\mathsf{O\text{-}Unif},\OSendA,\OSendB,
\ORecA(n),\ORecB(n)\}
Correctness oracle interface
def sckaCorrectnessSpec (Rho : Type) :=
unifSpec -- Uniform randomness
+ (Unit →ₒ Option (ℕ × Option ℕ × Rho)) -- O-Send-A
+ (Unit →ₒ Option (ℕ × Option ℕ × Rho)) -- O-Send-B
+ (ℕ →ₒ Option (ℕ × Option ℕ)) -- O-Recv-A
+ (ℕ →ₒ Option (ℕ × Option ℕ)) -- O-Recv-BCorrectness oracle implementation
def sckaCorrectnessImpl [DecidableEq I] (scka : SCKAScheme ProbComp IK StA StB I Rho Rand) :
QueryImpl (sckaCorrectnessSpec Rho)
(StateT (GameState StA StB I Rho) ProbComp) :=
oracleUnif StA StB I Rho
+ oracleSendA scka + oracleSendB scka
+ oracleRecvA scka + oracleRecvB sckaCorrectness adversary
abbrev SCKACorrectnessAdversary (Rho : Type) :=
OracleComp (sckaCorrectnessSpec Rho) Bool\Exp{\textsf{cor}}{\textsf{SCKA}}(\adv)
\begin{array}{l}
ik\sample\mathsf{InitKeyGen}(); \\
\stA\sample\InitA(ik);\quad\stB\sample\InitB(ik); \\
\mathsf{Key}[P,t]\gets\bot;\quad\mathsf{Msg}[P,n]\gets\bot; \\
n_\A,n_\B,t^\mathsf{cur}_\A,t^\mathsf{cur}_\B\gets0; \\
\mathsf{Exposed},\mathsf{Challenged}\gets\emptyset;\quad
\mathsf{correct}\gets\mathsf{true}; \\
(\_,\mathsf{state})\getsval\adv^{\Ocor}; \\
\Return\mathsf{state.correct}
\end{array}
Correctness experiment
def correctnessExp [DecidableEq I]
(scka : SCKAScheme ProbComp IK StA StB I Rho Rand)
(adversary : SCKACorrectnessAdversary Rho) : ProbComp Bool := do
let ik ← scka.initKeyGen
let stA ← scka.initA ik
let stB ← scka.initB ik
let (_, state) ← (simulateQ (sckaCorrectnessImpl scka) adversary).run
(initGameState stA stB)
return state.correct
uses Definition 9.1.1 · Definition 9.1.2 · github #184
Lean code for Definition9.1.3●4 definitions
Associated Lean declarations
-
SCKAScheme.sckaCorrectnessSpec[complete]
-
SCKAScheme.sckaCorrectnessImpl[complete]
-
SCKAScheme.SCKACorrectnessAdversary[complete]
-
SCKAScheme.correctnessExp[complete]
Associated Lean declarations
-
SCKAScheme.sckaCorrectnessSpec[complete] -
SCKAScheme.sckaCorrectnessImpl[complete] -
SCKAScheme.SCKACorrectnessAdversary[complete] -
SCKAScheme.correctnessExp[complete]
-
defdefined in SecureMessaging/SCKA/Defs.leancomplete
def SCKAScheme.sckaCorrectnessSpec (Rho : Type) : OracleSpec ((((ℕ ⊕ Unit) ⊕ Unit) ⊕ ℕ) ⊕ ℕ)
def SCKAScheme.sckaCorrectnessSpec (Rho : Type) : OracleSpec ((((ℕ ⊕ Unit) ⊕ Unit) ⊕ ℕ) ⊕ ℕ)
Oracle spec for the SCKA correctness game: uniform randomness, send and receive oracles.
-
defdefined in SecureMessaging/SCKA/Defs.leancomplete
def SCKAScheme.sckaCorrectnessImpl {IK StA StB I Rho Rand : Type} [DecidableEq I] (scka : SCKAScheme ProbComp IK StA StB I Rho Rand) : QueryImpl (SCKAScheme.sckaCorrectnessSpec Rho) (StateT (SCKAScheme.GameState StA StB I Rho) ProbComp)
def SCKAScheme.sckaCorrectnessImpl {IK StA StB I Rho Rand : Type} [DecidableEq I] (scka : SCKAScheme ProbComp IK StA StB I Rho Rand) : QueryImpl (SCKAScheme.sckaCorrectnessSpec Rho) (StateT (SCKAScheme.GameState StA StB I Rho) ProbComp)
Oracle set for the SCKA correctness game: uniform randomness, plain send oracles, and receive oracles.
-
abbrevdefined in SecureMessaging/SCKA/Defs.leancomplete
abbrev SCKAScheme.SCKACorrectnessAdversary (Rho : Type) : Type
abbrev SCKAScheme.SCKACorrectnessAdversary (Rho : Type) : Type
SCKA correctness adversary: access to the restricted send/receive oracles.
-
defdefined in SecureMessaging/SCKA/Defs.leancomplete
def SCKAScheme.correctnessExp {IK StA StB I Rho Rand : Type} [DecidableEq I] (scka : SCKAScheme ProbComp IK StA StB I Rho Rand) (adversary : SCKAScheme.SCKACorrectnessAdversary Rho) : ProbComp Bool
def SCKAScheme.correctnessExp {IK StA StB I Rho Rand : Type} [DecidableEq I] (scka : SCKAScheme ProbComp IK StA StB I Rho Rand) (adversary : SCKAScheme.SCKACorrectnessAdversary Rho) : ProbComp Bool
**Correctness experiment** (§3.1 of [SCKA]). Run the adversary against the restricted send/receive oracles and return whether all correctness invariants (Monotonicity, Matching epoch, Unique epochs, Consistent keys, Known prefix) held throughout.
Definition9.1.4
Group: SCKA. (3)
Statement uses 2
Used by 5
Associated Lean declarations
-
SCKAScheme.sckaSecuritySpec[complete] -
SCKAScheme.sckaSecurityImpl[complete] -
SCKAScheme.SCKAAdversary[complete] -
SCKAScheme.securityExp[complete] -
SCKAScheme.sckaGuessAdvantage[complete]
\Osec=\Ocor\cup
\{\OSendARLeak,\OSendBRLeak,\OChall(t),\OCorrA,\OCorrB\}
Security oracle interface
def sckaSecuritySpec (StA StB I Rho Rand : Type) :=
sckaCorrectnessSpec Rho
+ (Unit →ₒ Option (ℕ × Option ℕ × Rho × Rand)) -- O-Send-A-rleak
+ (Unit →ₒ Option (ℕ × Option ℕ × Rho × Rand)) -- O-Send-B-rleak
+ (ℕ →ₒ Option I) -- O-Chall t
+ (Unit →ₒ Option StA) -- O-Corrupt-A
+ (Unit →ₒ Option StB) -- O-Corrupt-BSecurity oracle implementation
def sckaSecurityImpl (isRandom : Bool) (vulnA : StA → Finset ℕ) (vulnB : StB → Finset ℕ)
[SampleableType I] [DecidableEq I] (scka : SCKAScheme ProbComp IK StA StB I Rho Rand) :
QueryImpl (sckaSecuritySpec StA StB I Rho Rand)
(StateT (GameState StA StB I Rho) ProbComp) :=
sckaCorrectnessImpl scka
+ oracleSendArleak vulnA scka + oracleSendBrleak vulnB scka
+ oracleChall isRandom StA StB I Rho
+ oracleCorruptA vulnA StB I Rho + oracleCorruptB vulnB StA I RhoSecurity adversary
abbrev SCKAAdversary (StA StB I Rho Rand : Type) :=
OracleComp (sckaSecuritySpec StA StB I Rho Rand) Bool\Exp{\textsf{sec}}{\textsf{SCKA}}(\adv)
\begin{array}{l}
ik\sample\mathsf{InitKeyGen}(); \\
\stA\sample\InitA(ik);\quad\stB\sample\InitB(ik); \\
\mathsf{Key}[P,t]\gets\bot;\quad\mathsf{Msg}[P,n]\gets\bot; \\
n_\A,n_\B,t^\mathsf{cur}_\A,t^\mathsf{cur}_\B\gets0; \\
\mathsf{Exposed},\mathsf{Challenged}\gets\emptyset;\quad
\mathsf{correct}\gets\mathsf{true}; \\
b\sample\{0,1\}; \\
(b',\_)\getsval\adv^{\Osec}; \\
\Return[b'=b]
\end{array}
Security experiment
def securityExp [SampleableType I] [DecidableEq I]
(scka : SCKAScheme ProbComp IK StA StB I Rho Rand)
(adversary : SCKAAdversary StA StB I Rho Rand)
(vulnA : StA → Finset ℕ) (vulnB : StB → Finset ℕ) : ProbComp Bool := do
let ik ← scka.initKeyGen
let stA ← scka.initA ik
let stB ← scka.initB ik
let b ← $ᵗ Bool
let (b', _) ← (simulateQ (sckaSecurityImpl b vulnA vulnB scka) adversary).run
(initGameState stA stB)
return (b == b')
\mathsf{Adv}^{\mathsf{guess}}_{\mathsf{SCKA}}(\adv)
=\left|\Pr\left[\Exp{\mathsf{sec}}{\mathsf{SCKA}}(\adv)=1\right]
-\frac12\right|
=\left|\Pr[b'=b]-\frac12\right|
Guessing advantage
noncomputable def sckaGuessAdvantage [SampleableType I] [DecidableEq I]
(scka : SCKAScheme ProbComp IK StA StB I Rho Rand)
(adversary : SCKAAdversary StA StB I Rho Rand)
(vulnA : StA → Finset ℕ) (vulnB : StB → Finset ℕ) : ℝ :=
|(Pr[= true | securityExp scka adversary vulnA vulnB]).toReal - 1 / 2|
uses Definition 9.1.1 · Definition 9.1.2 · github #185
Lean code for Definition9.1.4●5 definitions
Associated Lean declarations
-
SCKAScheme.sckaSecuritySpec[complete]
-
SCKAScheme.sckaSecurityImpl[complete]
-
SCKAScheme.SCKAAdversary[complete]
-
SCKAScheme.securityExp[complete]
-
SCKAScheme.sckaGuessAdvantage[complete]
Associated Lean declarations
-
SCKAScheme.sckaSecuritySpec[complete] -
SCKAScheme.sckaSecurityImpl[complete] -
SCKAScheme.SCKAAdversary[complete] -
SCKAScheme.securityExp[complete] -
SCKAScheme.sckaGuessAdvantage[complete]
-
defdefined in SecureMessaging/SCKA/Defs.leancomplete
def SCKAScheme.sckaSecuritySpec (StA StB I Rho Rand : Type) : OracleSpec (((((((((ℕ ⊕ Unit) ⊕ Unit) ⊕ ℕ) ⊕ ℕ) ⊕ Unit) ⊕ Unit) ⊕ ℕ) ⊕ Unit) ⊕ Unit)
def SCKAScheme.sckaSecuritySpec (StA StB I Rho Rand : Type) : OracleSpec (((((((((ℕ ⊕ Unit) ⊕ Unit) ⊕ ℕ) ⊕ ℕ) ⊕ Unit) ⊕ Unit) ⊕ ℕ) ⊕ Unit) ⊕ Unit)
Oracle spec for the SCKA security game: the correctness spec extended with the randomness-leaking send oracles, the challenge oracle, and the corruption oracles.
-
defdefined in SecureMessaging/SCKA/Defs.leancomplete
def SCKAScheme.sckaSecurityImpl {IK StA StB I Rho Rand : Type} (isRandom : Bool) (vulnA : StA → Finset ℕ) (vulnB : StB → Finset ℕ) [SampleableType I] [DecidableEq I] (scka : SCKAScheme ProbComp IK StA StB I Rho Rand) : QueryImpl (SCKAScheme.sckaSecuritySpec StA StB I Rho Rand) (StateT (SCKAScheme.GameState StA StB I Rho) ProbComp)
def SCKAScheme.sckaSecurityImpl {IK StA StB I Rho Rand : Type} (isRandom : Bool) (vulnA : StA → Finset ℕ) (vulnB : StB → Finset ℕ) [SampleableType I] [DecidableEq I] (scka : SCKAScheme ProbComp IK StA StB I Rho Rand) : QueryImpl (SCKAScheme.sckaSecuritySpec StA StB I Rho Rand) (StateT (SCKAScheme.GameState StA StB I Rho) ProbComp)
Oracle set for the SCKA security game (Fig. 1): the correctness oracles extended with randomness-leaking sends, challenge, and corruption.
-
abbrevdefined in SecureMessaging/SCKA/Defs.leancomplete
abbrev SCKAScheme.SCKAAdversary (StA StB I Rho Rand : Type) : Type
abbrev SCKAScheme.SCKAAdversary (StA StB I Rho Rand : Type) : Type
SCKA security adversary: access to all oracles of `sckaSecuritySpec`.
-
defdefined in SecureMessaging/SCKA/Defs.leancomplete
def SCKAScheme.securityExp {IK StA StB I Rho Rand : Type} [SampleableType I] [DecidableEq I] (scka : SCKAScheme ProbComp IK StA StB I Rho Rand) (adversary : SCKAScheme.SCKAAdversary StA StB I Rho Rand) (vulnA : StA → Finset ℕ) (vulnB : StB → Finset ℕ) : ProbComp Bool
def SCKAScheme.securityExp {IK StA StB I Rho Rand : Type} [SampleableType I] [DecidableEq I] (scka : SCKAScheme ProbComp IK StA StB I Rho Rand) (adversary : SCKAScheme.SCKAAdversary StA StB I Rho Rand) (vulnA : StA → Finset ℕ) (vulnB : StB → Finset ℕ) : ProbComp Bool
**Security experiment** (Fig. 1). Initialize both parties, sample a challenge bit, run the adversary with the full game oracles, and return whether it guessed the bit.
-
defdefined in SecureMessaging/SCKA/Defs.leancomplete
def SCKAScheme.sckaGuessAdvantage {IK StA StB I Rho Rand : Type} [SampleableType I] [DecidableEq I] (scka : SCKAScheme ProbComp IK StA StB I Rho Rand) (adversary : SCKAScheme.SCKAAdversary StA StB I Rho Rand) (vulnA : StA → Finset ℕ) (vulnB : StB → Finset ℕ) : ℝ
def SCKAScheme.sckaGuessAdvantage {IK StA StB I Rho Rand : Type} [SampleableType I] [DecidableEq I] (scka : SCKAScheme ProbComp IK StA StB I Rho Rand) (adversary : SCKAScheme.SCKAAdversary StA StB I Rho Rand) (vulnA : StA → Finset ℕ) (vulnB : StB → Finset ℕ) : ℝ
SCKA guess advantage: `|Pr[Win] - 1/2|`.