NIKE: Non-Interactive Key Exchange Game

The NIKE game captures the security of the shared key exchange component of Cryptobox. It has two variants parameterized by b : Bool:

• b = false (real): the shared key is computed via N.sharedkey
• b = true (ideal): for honest-honest pairs the shared key is sampled uniformly at random; for pairs involving a corrupt key the real shared key is returned

The NIKE game builds on top of the PKEY oracles (key generation, corruption tracking, secret key retrieval, and honesty checks).

References

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

Heap Locations

State specific to the NIKE game. Location IDs start at 400 to avoid collisions with PKEY locations (100-range).

@[reducible]

noncomputable def CatCrypt.Examples.Cryptobox.nikeKeysLoc [CT : CryptoTypes] : Core.Location

Stored shared keys indexed by canonical session ID.

Equations

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

@[reducible]

noncomputable def CatCrypt.Examples.Cryptobox.nikeHonestLoc [CT : CryptoTypes] : Core.Location

Honesty flags for sessions: whether both parties are honest.

Equations

• CatCrypt.Examples.Cryptobox.nikeHonestLoc = { id := 401, ty := CatCrypt.Examples.Cryptobox.SID → Bool, fintype := Pi.instFintype, inhabited := Pi.instInhabited }

Oracle Definitions

noncomputable def CatCrypt.Examples.Cryptobox.sharedkeyOracle [CT : CryptoTypes] [LinearOrder CryptoTypes.PK] (N : NIKEScheme) (b : Bool) (pkeyO : PKEYOracles) (pk_s pk_r : CryptoTypes.PK) : Core.SPComp CryptoTypes.SharedKey

Shared key oracle for the NIKE game.

Given sender and receiver public keys:

1. Check honesty of both keys via pkeyO.honpk
2. Retrieve sender's secret key via pkeyO.getsk
3. Compute the canonical session ID via sortSID
4. Look up whether a key was already stored for this session
5. If b = false (real) or either party is corrupt: compute the real shared key via N.sharedkey
6. If b = true (ideal) and both parties are honest: sample a uniformly random shared key
7. Store and return the key

Equations

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

Oracle Record

structure CatCrypt.Examples.Cryptobox.NIKEOracles [CT : CryptoTypes] : Type

Oracle interface for the NIKE game.

• sharedkey : CryptoTypes.PK → CryptoTypes.PK → Core.SPComp CryptoTypes.SharedKey

NIKE Game

noncomputable def CatCrypt.Examples.Cryptobox.GNIKE [CT : CryptoTypes] [LinearOrder CryptoTypes.PK] (N : NIKEScheme) (b : Bool) (pkeyO : PKEYOracles) (A : PKEYOracles → NIKEOracles → Core.SPComp Bool) : Core.SPComp Bool

NIKE game parameterized by b:

• b = false: real shared keys
• b = true: ideal (random) shared keys for honest pairs

The adversary receives both PKEY oracles (for key management) and the NIKE oracle (for shared key queries).

Equations

• CatCrypt.Examples.Cryptobox.GNIKE N b pkeyO A = A pkeyO { sharedkey := CatCrypt.Examples.Cryptobox.sharedkeyOracle N b pkeyO }

NIKE Advantage

noncomputable def CatCrypt.Examples.Cryptobox.nikeAdvantage [CT : CryptoTypes] [LinearOrder CryptoTypes.PK] (N : NIKEScheme) (pkeyO : PKEYOracles) (A : PKEYOracles → NIKEOracles → Core.SPComp Bool) : ENNReal

NIKE advantage: distinguishing real from ideal shared keys.

Equations

• CatCrypt.Examples.Cryptobox.nikeAdvantage N pkeyO A = CatCrypt.Crypto.Advantage (CatCrypt.Examples.Cryptobox.GNIKE N false pkeyO A) (CatCrypt.Examples.Cryptobox.GNIKE N true pkeyO A)