SchemeModel.lean🔗

Tier 2 · definitions used by the computational proof 2 headline theorems depend on it 20 of 167 lines trusted trust banner B3, trusted in part 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.

Fixed Two-Party Configuration and SPQR-Off Session Outcomes

Trusted in part. Computational/Theorems/ uses serializedPartyAddresses, partyDeviceId, partyIdentityKeyBytes, partyIdentityKey, and partyAddressName; spqrOffSessionParams, initKeysE, Reach, sendModelSpqrOff, and recvModelSpqrOff are checked by Lean. See Computational/docs/TRUSTED_BASE.md and Computational/docs/DEVIATIONS.md (DEV-M3, DEV-M4, DEV-M5, DEV-M10, DEV-E8).

@[expose] public section

set_option autoImplicit false

namespace CryptoVerification.E2E

open CryptoGames CryptoGames.LibsignalSession CryptoGames.Ratchet CryptoGames.Ratchet.LibsignalInst

open CryptoVerification.LibsignalTripleRatchetRepr CryptoVerification.LibsignalProtoCodec

The parties (constants of the image)

def partyAddressNameL37–45 ↗#

The protocol address name of each party: a fixed hyphenated UUID.

DEV-M3 (libsignal): the parties' addresses are constants. ACD19 Def. 6 has two parties A and B and no addresses. libsignal MACs both parties' addresses, and the wrapper fixes them: these two UUID names and device 1 (partyDeviceId). Why: the image is one fixed configuration. Effect: w.l.o.g., argued: the session model's bound holds for every address blob.

def partyAddressName : Party → String
  | .A => "8a6f1c2e-3b4d-4e5f-9a0b-1c2d3e4f5a6b"
  | .B => "5d3e2f10-7a8b-4c9d-8e0f-a1b2c3d4e5f6"

2 declarations not shown (lines 47–69): theorems, which Lean checks, or definitions that no headline statement uses

CryptoVerification.E2E.partyIdentityKeyBytes, CryptoVerification.E2E.partyIdentityKey

def partyDeviceIdL71–72 ↗#

Every party uses device 1.

def partyDeviceId : BitVec 8 := 1#8

def serializedPartyAddressesL74–82 ↗#

serialize_addresses(sender, recipient) of the two parties' addresses (names partyAddressName, device 1) under the UUID parser uuidParse: none if a name does not parse (then libsignal MACs without addresses, in the binary and in the session model alike). The scheme uses it at the trusted model uuidTryParse of Uuid::try_parse (spqrOffSessionParams), under which both names parse.

def serializedPartyAddresses (uuidParse : UuidParser) (sender recipient : Party) : Option (List (BitVec 8)) := do
  let s ← serviceIdParse uuidParse (utf8 (partyAddressName sender))
  let r ← serviceIdParse uuidParse (utf8 (partyAddressName recipient))
  return addrBytes s partyDeviceId ++ addrBytes r partyDeviceId

5 declarations not shown (lines 86–165): theorems, which Lean checks, or definitions that no headline statement uses

CryptoVerification.E2E.spqrOffSessionParams, CryptoVerification.E2E.initKeysE, CryptoVerification.E2E.Reach.recv, CryptoVerification.E2E.Reach.send, CryptoVerification.E2E.Reach, CryptoVerification.E2E.Reach.initB, CryptoVerification.E2E.Reach.initA, CryptoVerification.E2E.sendModelSpqrOff, CryptoVerification.E2E.recvModelSpqrOff

end CryptoVerification.E2E