StatementIdsModel.lean🔗

Tier 2 · definitions used by the computational proof 2 headline theorems depend on it 19 of 67 lines trusted trust banner B2, trusted: definitions used by the statement source ↗

Read the definitions shown. Only the declarations that the headline statements use are shown, with the namespace, section, open and variable commands needed to read them. The collapsed runs are theorems, which Lean checks, and definitions that no headline statement uses.

Session parameters at arbitrary identity keys and the leaked-pre-key session scheme

Trusted: definitions used by the statement. The theorems of Computational/Theorems/ use idsOf, paramsIdsWithSpqr and sessionSchemeFixedSpk. The statements SessionSecureIds, SessionSecureUIds, SessionSecureSpkIds and SessionSecureSpkIdsWithSpqr, and paramsIds, are in Computational/Proofs/SpecLemmas/Session/StatementIdsModel.lean, checked by Lean. See Computational/docs/TRUSTED_BASE.md.

Defines session parameters for caller-chosen identity keys idA, idB (which enter the wire MACs) and the leaked-pre-key session scheme sessionSchemeFixedSpk, where Bob's signed-pre-key scalar s is fixed externally while the remaining initial keys are sampled via SampledSessionKey.

@[expose] public section

set_option autoImplicit false

open OracleComp OracleSpec ENNReal

namespace CryptoVerification.E2E

open CryptoGames CryptoGames.LibsignalSM Ratchet LibsignalInst LibsignalSession
  HMAC HKDF CBC LibsignalAead SM SM.Construction CKA AEADScheme MACScheme WireAEAD FSAEAD
  CryptoVerification.LibsignalProtoCodec CryptoVerification.LibsignalSession

Session parameters

def paramsIdsWithSpqrL43–49 ↗#

Session parameters for SPQR instance spqr and party identity keys idA, idB, with protoSignalCodec and serialized UUID party addresses (uuidTryParse).

def paramsIdsWithSpqr (C : Crypto) {PQC : Type} (spqr : Spqr Bytes PQC)
    (idA idB : IdentityKey) : Params Bytes PQC :=
  ⟨C, protoSignalCodec, spqr, idA, idB,
    serializedPartyAddresses LibsignalTripleRatchetRepr.uuidTryParse .A .B,
    serializedPartyAddresses LibsignalTripleRatchetRepr.uuidTryParse .B .A⟩

def idsOfL51–54 ↗#

Assigns identity key idA to .A and idB to .B.

def idsOf (idA idB : IdentityKey) : Party → IdentityKey
  | .A => idA
  | .B => idB

Leaked-pre-key session scheme

def sessionSchemeFixedSpkL58–65 ↗#

Single-session SMSchemeR with Bob's signed-pre-key coins fixed to s, keyed by SampledSessionKey via initKeysOfSampled s with plaintexts fitted to ℓ bytes.

def sessionSchemeFixedSpk {PQ PQC : Type} [Inhabited PQ] (P : Params PQ PQC) (ℓ : ℕ) (s : BitVec 256) :
    SMSchemeR SampledSessionKey (GhostState PQ) (Plain ℓ) PQC (BitVec 256) Bytes where
  initA k := P.initA (initKeysOfSampled s k)
  initB k := P.initB (initKeysOfSampled s k)
  send g m r := P.send g m.toList r
  receive g c rc := (P.receive g c rc).map fun x => (x.1, x.2.1, x.2.2.1, padOrTruncatePlain ℓ x.2.2.2)

end CryptoVerification.E2E