PqxdhSessionModel.lean🔗

Tier 2 · definitions used by the computational proof 3 headline theorems depend on it 4 of 130 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.

Wire-Level send / recv Models and Reachable PQXDH Sessions

Trusted in part. Computational/Theorems/ uses ReachablePqxdhSession, firstMessageBody, wirePrekey, and wireWhisper (via SignalSession/PqDir.lean); sendWirePending, sendModelPq, recvModelPq, and honestBundle are checked by Lean. See Computational/docs/TRUSTED_BASE.md.

Defines the CLI's one-byte wire framing (2 ‖ SignalMessage vs 3 ‖ PreKeySignalMessage), the pending-session send model sendWirePending over V1 SPQR (pqxdhSpqrSession), the inductive closure ReachablePqxdhSession of PQXDH-initialized sessions under pqxdhSessionParams, and untagged proof-target helpers (sendModelPq, recvModelPq, honestBundle).

@[expose] public section

set_option autoImplicit false

namespace CryptoVerification.E2E

open CryptoGames CryptoGames.LibsignalSession CryptoGames.LibsignalSessionApi

open CryptoVerification.LibsignalProtoCodec

Wire tags

def wireWhisperL38–39 ↗#

WIRE_WHISPER: the tag of a bare SignalMessage on the wire.

def wireWhisper : BitVec 8 := 2#8

def wirePrekeyL41–42 ↗#

WIRE_PREKEY: the tag of a PreKeySignalMessage on the wire.

def wirePrekey : BitVec 8 := 3#8

6 declarations not shown (lines 46–131): theorems, which Lean checks, or definitions that no headline statement uses

CryptoVerification.E2E.firstMessageBody, CryptoVerification.E2E.sendWirePending, CryptoVerification.E2E.ReachablePqxdhSession.recvPrekey, CryptoVerification.E2E.ReachablePqxdhSession.send, CryptoVerification.E2E.ReachablePqxdhSession.recv, CryptoVerification.E2E.ReachablePqxdhSession.initiate, CryptoVerification.E2E.ReachablePqxdhSession, CryptoVerification.E2E.sendModelPq, CryptoVerification.E2E.recvModelPq, CryptoVerification.E2E.honestBundle

end CryptoVerification.E2E