KEY: Shared Key Management Game #

The KEY game manages shared keys indexed by session identifiers (SID).

Overview #

Two variants parameterized by b : Bool:

b = false (real): stores actual shared keys provided by the caller
b = true (ideal): replaces honest keys with freshly sampled random keys

Oracles #

kset: Honest key set — stores actual key (real) or random key (ideal)
kcset: Corrupt key set — always stores the provided key directly
kget: Retrieve the stored shared key for a session
khon: Check whether a session's key was set honestly

References #

Rocq SSProve: theories/Cryptobox/KEY.v
Dupressoir et al., CSF 2022 (Section 4.2)

Heap Locations #

State is stored in the global heap via typed locations. Locations are @[reducible] so that .ty reduces for type checking.

source

@[reducible]

noncomputable def CatCrypt.Examples.Cryptobox.keyStoreLoc [CT : CryptoTypes] :

Core.Location

Shared key storage: SID → SharedKey. Default: all default.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[reducible]

noncomputable def CatCrypt.Examples.Cryptobox.keyHonestLoc [CT : CryptoTypes] :

Core.Location

Honesty flags for shared keys: SID → Bool. Default: all false (unset).

Equations

CatCrypt.Examples.Cryptobox.keyHonestLoc = { id := 201, ty := CatCrypt.Examples.Cryptobox.SID → Bool, fintype := Pi.instFintype, inhabited := Pi.instInhabited }

Instances For

Oracle Definitions #

Each oracle is an SPComp computation that reads/writes heap locations. The b : Bool parameter in keySetOracle switches between real and ideal behavior.

source

noncomputable def CatCrypt.Examples.Cryptobox.keySetOracle [CT : CryptoTypes] (b : Bool) (sid : SID) (k : CryptoTypes.SharedKey) :

Core.SPComp Unit

KSET oracle: set the shared key for a session. If the session already has a key set (honest or corrupt), fails. If b = false (real): stores the provided key k. If b = true (ideal): samples a fresh random key and stores that instead.

Equations