structure Cryptlib.Primitives.NIKE.NIKE.NIKE : Type 1

• PrivateKey : Type
• PublicKey : Type
• SharedSecret : Type
• name : String
• privateKeySize : Nat
• publicKeySize : Nat
• sharedSecretSize : Nat
• Safe : self.PublicKey → Prop
• decSafe : DecidablePred self.Safe
• privateKeyFromSeed : Vector UInt8 32 → self.PrivateKey
• derivePublicKey : self.PrivateKey → self.PublicKey
• groupAction : self.PrivateKey → { pk : self.PublicKey // self.Safe pk } → self.SharedSecret
• encodePrivateKey : self.PrivateKey → Vector UInt8 self.privateKeySize
• decodePrivateKey : Vector UInt8 self.privateKeySize → Option self.PrivateKey
• encodePublicKey : self.PublicKey → Vector UInt8 self.publicKeySize
• decodePublicKey : Vector UInt8 self.publicKeySize → Option self.PublicKey
• encodeSharedSecret : self.SharedSecret → Vector UInt8 self.sharedSecretSize
• derive_safe (sk : self.PrivateKey) : self.Safe (self.derivePublicKey sk)
• decode_encode_priv (sk : self.PrivateKey) : self.decodePrivateKey (self.encodePrivateKey sk) = some sk
• decode_encode_pub (pk : self.PublicKey) : self.decodePublicKey (self.encodePublicKey pk) = some pk
• decodePrivateKey_total (v : Vector UInt8 self.privateKeySize) : ∃ (sk : self.PrivateKey), self.decodePrivateKey v = some sk

  Every byte string of the right width decodes to a private key.

• encode_decode_pub (v : Vector UInt8 self.publicKeySize) (pk : self.PublicKey) : self.decodePublicKey v = some pk → self.encodePublicKey pk = v
• commutes (sk₁ sk₂ : self.PrivateKey) : self.groupAction sk₁ ⟨self.derivePublicKey sk₂, ⋯⟩ = self.groupAction sk₂ ⟨self.derivePublicKey sk₁, ⋯⟩
• reinterpret : self.SharedSecret → self.PublicKey

  Reinterpret a shared secret as a public key.

• reinterpret_safe (sk : self.PrivateKey) (spk : { pk : self.PublicKey // self.Safe pk }) : self.Safe (self.reinterpret (self.groupAction sk spk))

  The group action maps safe elements to safe elements.

• groupAction_comm (sk₁ sk₂ : self.PrivateKey) (spk : { pk : self.PublicKey // self.Safe pk }) : self.groupAction sk₁ ⟨self.reinterpret (self.groupAction sk₂ spk), ⋯⟩ = self.groupAction sk₂ ⟨self.reinterpret (self.groupAction sk₁ spk), ⋯⟩

  Group actions by two private keys commute on any safe element, not only on derived public keys as in commutes.

• publicKeySize_eq_sharedSecretSize : self.publicKeySize = self.sharedSecretSize

  Public keys and shared secrets have the same encoded size.

• encodePublicKey_reinterpret (ss : self.SharedSecret) : Util.Bytes.ofVector (self.encodePublicKey (self.reinterpret ss)) = Util.Bytes.ofVector (self.encodeSharedSecret ss)

  reinterpret preserves the encoding.

Iterated group action

Acting on a base public key with f 0, ..., f (n-1) and then targetSk gives the same result as acting on targetSk's public key with the base key and then f 0, ..., f (n-1).

def Cryptlib.Primitives.NIKE.NIKE.telescopeElem (nike : NIKE) (baseSk : nike.PrivateKey) (f : Nat → nike.PrivateKey) : Nat → { pk : nike.PublicKey // nike.Safe pk }

The base public key after n group actions by f 0, ..., f (n-1).

Equations

• Cryptlib.Primitives.NIKE.NIKE.telescopeElem nike baseSk f 0 = ⟨nike.derivePublicKey baseSk, ⋯⟩
• Cryptlib.Primitives.NIKE.NIKE.telescopeElem nike baseSk f n.succ = ⟨nike.reinterpret (nike.groupAction (f n) (Cryptlib.Primitives.NIKE.NIKE.telescopeElem nike baseSk f n)), ⋯⟩

def Cryptlib.Primitives.NIKE.NIKE.telescopeSecret (nike : NIKE) (baseSk targetSk : nike.PrivateKey) (f : Nat → nike.PrivateKey) : Nat → { ss : nike.SharedSecret // nike.Safe (nike.reinterpret ss) }

The base key's shared secret with targetSk, then n group actions by f 0, ..., f (n-1).

Equations

• One or more equations did not get rendered due to their size.
• Cryptlib.Primitives.NIKE.NIKE.telescopeSecret nike baseSk targetSk f 0 = ⟨nike.groupAction baseSk ⟨nike.derivePublicKey targetSk, ⋯⟩, ⋯⟩

theorem Cryptlib.Primitives.NIKE.NIKE.telescope_agree (nike : NIKE) (baseSk targetSk : nike.PrivateKey) (f : Nat → nike.PrivateKey) (n : Nat) : nike.groupAction targetSk (telescopeElem nike baseSk f n) = (telescopeSecret nike baseSk targetSk f n).val

targetSk acting on telescopeElem n equals telescopeSecret n.