NIKE to KEM adapter: hashed ElGamal

ENCAPSULATE(pk_static):
    eph_sk, eph_pk := GEN_KEYPAIR(RNG)
    ss             := DH(eph_sk, pk_static)
    ct             := ENCODE_PUBKEY(eph_pk)
    shared_key     := KEYED(deriveKey(ss), ENCODE(pk_static) || ENCODE(eph_pk))
    return ct, shared_key

DECAPSULATE(sk_static, ct):
    eph_pk     := DECODE_PUBKEY(ct)
    ss         := DH(sk_static, eph_pk)
    shared_key := KEYED(deriveKey(ss), ENCODE(pub(sk_static)) || ENCODE(eph_pk))
    return shared_key

The key is a PRF keyed by ss over the static key then the ephemeral key. Encapsulation and decapsulation reject public keys that are not NIKE.Safe.

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.Adapter.Bytes32 : Type

Equations

• Cryptlib.Primitives.KEM.Adapter.Bytes32 = Vector UInt8 32

def Cryptlib.Primitives.KEM.Adapter.toBytes {n : Nat} (v : Vector UInt8 n) : ByteArray

Equations

• Cryptlib.Primitives.KEM.Adapter.toBytes v = { data := v.toArray }

structure Cryptlib.Primitives.KEM.Adapter.PRF : Type

Shared-key derivation: derive ss pkStatic pkEph outLen returns outLen bytes.

• name : String

  Identifier used in test vectors, e.g. "sha256-v1".

• derive : ByteArray → ByteArray → ByteArray → (outLen : Nat) → Vector UInt8 outLen

@[reducible, inline]

abbrev Cryptlib.Primitives.KEM.Adapter.St : Type

Counter plus an inexhaustible seed stream.

Equations

• Cryptlib.Primitives.KEM.Adapter.St = (Nat × (Nat → Cryptlib.Primitives.KEM.Adapter.Bytes32))

def Cryptlib.Primitives.KEM.Adapter.nextSeed : EStateM KEM.KEMError St Bytes32

Equations

• Cryptlib.Primitives.KEM.Adapter.nextSeed (i, str) = EStateM.Result.ok (str i) (i + 1, str)

def Cryptlib.Primitives.KEM.Adapter.initWith (str : Nat → Bytes32) : St

Initial state over a caller-supplied seed stream, which must be unpredictable.

Equations

• Cryptlib.Primitives.KEM.Adapter.initWith str = (0, str)

def Cryptlib.Primitives.KEM.Adapter.derive (F : PRF) (nike : NIKE.NIKE.NIKE) (ss : Vector UInt8 nike.sharedSecretSize) (staticPk ephPk : Vector UInt8 nike.publicKeySize) : Vector UInt8 nike.sharedSecretSize

The shared key: the PRF over the static then ephemeral public key, at the NIKE's shared-secret width.

Equations

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

def Cryptlib.Primitives.KEM.Adapter.encapM (F : PRF) (nike : NIKE.NIKE.NIKE) (pk : nike.PublicKey) : EStateM KEM.KEMError St (nike.PublicKey × Vector UInt8 nike.sharedSecretSize)

Equations

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

def Cryptlib.Primitives.KEM.Adapter.decapM (F : PRF) (nike : NIKE.NIKE.NIKE) (sk : nike.PrivateKey) (ct : nike.PublicKey) : EStateM KEM.KEMError St (Vector UInt8 nike.sharedSecretSize)

Equations

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

theorem Cryptlib.Primitives.KEM.Adapter.nextSeed_consumes (i : Nat) (str : Nat → Bytes32) : nextSeed (i, str) = EStateM.Result.ok (str i) (i + 1, str)

nextSeed advances the counter by exactly one and leaves the stream alone.

theorem Cryptlib.Primitives.KEM.Adapter.encapM_consumes (F : PRF) (nike : NIKE.NIKE.NIKE) (pk : nike.PublicKey) (i : Nat) (str : Nat → Bytes32) : (∃ (r : nike.PublicKey × Vector UInt8 nike.sharedSecretSize), encapM F nike pk (i, str) = EStateM.Result.ok r (i + 1, str)) ∨ encapM F nike pk (i, str) = EStateM.Result.error KEM.KEMError.unsafePublicKey (i + 1, str)

theorem Cryptlib.Primitives.KEM.Adapter.encap_seeds_distinct (i : Nat) (str : Nat → Bytes32) (hinj : ∀ (m n : Nat), m ≠ n → str m ≠ str n) : str i ≠ str (i + 1)

Consecutive encapsulations use different seeds if the stream is injective.

theorem Cryptlib.Primitives.KEM.Adapter.roundTrip (F : PRF) (nike : NIKE.NIKE.NIKE) (sk : nike.PrivateKey) (s : St) : True → ∀ (c : nike.PublicKey) (k : Vector UInt8 nike.sharedSecretSize) (s' : St), encapM F nike (nike.derivePublicKey sk) s = EStateM.Result.ok (c, k) s' → ∀ (t : St), ∃ (t' : St), decapM F nike sk c t = EStateM.Result.ok k t'

Decapsulation recovers the encapsulated key for derivePublicKey sk. The True hypothesis is kemOfNike's Reliable.

def Cryptlib.Primitives.KEM.Adapter.kemOfNike (F : PRF) (nike : NIKE.NIKE.NIKE) : KEM.KEM

Equations

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