LibsignalSessionApi.lean
Declarations on this page (8)
libsignal's public session API over abstract stores
Trusted in part. The theorems of Computational/ use only key, PreKeySignalMessage, new, ProtoPreKeySignalMessage, encode, PendingPreKey, PendingKyberPreKey, KyberPayload, varint, uint32Field, bytesField from this file (the pre-key message types and the Prost field encoders): read them. Everything else here (the session API, its errors and store calls) and every proof is checked by Lean. See Computational/.
Models the public entry points messageEncrypt (session_management.rs:43–151) and messageDecryptSignal (session_management.rs:297–354) over the core session model of LibsignalSession.lean:
-
Time and staleness:
SystemTime(checkedAddSecs,lt) and the 30-day unacknowledged session limitmaxUnacknowledgedSessionAge. -
Session records and
PreKeySignalMessage:PendingPreKey,PendingKyberPreKey,Session,SessionRecord,KyberPayload,ProtoPreKeySignalMessage,PreKeySignalMessage,CiphertextMessage, and concreteProstwire encoders (varint,key,uint32Field,bytesField). -
Stores and errors:
Direction,IdentityChange,StoreAnswers,StoreCall,ApiError,Api,storeCall,liftProtocol, andexecOk. Each entry point invokes at most the four store methods (loadSession,isTrustedIdentity,saveIdentity,storeSession) in fixed order, taking their answers viaStoreAnswersand emitting the executedStoreCalltrace. -
Scope and panics: single current session (
previous_sessions = []),log::max_level() = Off, distinct local and remote identity keys (self_session = false), canonical 33-byte stored keys, andApiError.modelingpanic panic = "abort"non-termination (SystemTimeoverflow or session-modelu32::MAXoverflow).
@[expose] public sectionnamespace CryptoGamesnamespace LibsignalSessionApiopen LibsignalSession5 declarations not shown (lines 53–88): theorems, which Lean checks, or definitions that no headline statement uses
CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames.
The session record (state/, proto/)
structure PendingPreKey
session_structure::PendingPreKey (proto/), as unacknowledged_ reads it (state/).
structure PendingPreKey where
/-- `pre_key_id` (`optional uint32`; `PreKeyId`). -/
preKeyId : Option (BitVec 32)
/-- `signed_pre_key_id` (stored as `int32`, read back `as u32`, the same 32 bits;
`SignedPreKeyId`). -/
signedPreKeyId : BitVec 32
/-- `base_key`, deserialized (see "Deviations"). -/
baseKey : PublicKey
/-- `timestamp` (`uint64`): seconds since the Unix epoch when the session was created. -/
timestamp : BitVec 64
deriving DecidableEqstructure PendingKyberPreKey
session_structure::PendingKyberPreKey (proto/): the Kyber pre-key id (KyberPreKeyId) and the KEM (key encapsulation mechanism) ciphertext of an unacknowledged PQXDH session.
structure PendingKyberPreKey where
/-- `pre_key_id` (`uint32`). -/
preKeyId : BitVec 32
/-- `ciphertext` (bytes). -/
ciphertext : List (BitVec 8)
deriving DecidableEq4 declarations not shown (lines 116–156): theorems, which Lean checks, or definitions that no headline statement uses
CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames.
structure ProtoPreKeySignalMessage
prost's proto::wire::PreKeySignalMessage (proto/, proto2: every field is optional).
structure ProtoPreKeySignalMessage where
/-- Field 5. -/
registrationId : Option (BitVec 32)
/-- Field 1. -/
preKeyId : Option (BitVec 32)
/-- Field 6. -/
signedPreKeyId : Option (BitVec 32)
/-- Field 7. -/
kyberPreKeyId : Option (BitVec 32)
/-- Field 8. -/
kyberCiphertext : Option (List (BitVec 8))
/-- Field 2. -/
baseKey : Option (List (BitVec 8))
/-- Field 3. -/
identityKey : Option (List (BitVec 8))
/-- Field 4 (the serialized inner `SignalMessage`). -/
message : Option (List (BitVec 8))
deriving DecidableEqnamespace Prostdef varint
encode_varint (prost/): base-128 (LEB128), 7 bits per byte, least significant group first, the high bit set on every byte but the last.
def varint (n : ℕ) : List (BitVec 8) :=
if h : n < 128 then [BitVec.ofNat 8 n] else BitVec.ofNat 8 (n % 128 + 128) :: varint (n / 128)
termination_by n
decreasing_by All goals completed! 🐙def key
encode_key (prost/): the varint of tag << 3 | wire_type.
def key (tag wireType : ℕ) : List (BitVec 8) := varint (8 * tag + wireType)def uint32Field
An optional uint32 field (uint32::encode: the varint! macro, prost/, at :356): nothing for None; else key (wire type 0, varint) and the value as a varint.
def bytesField
An optional bytes field (bytes::encode, prost/): nothing for None; else key (wire type 2, length-delimited), the length as a varint, the bytes.
end Prost
def ProtoPreKeySignalMessage.
prost's encoder for proto::wire::PreKeySignalMessage (Message::encode, infallible into a Vec: expect("can always append to a Vec")): the fields in ascending tag order (prost-derive sorts the fields by tag, prost-derive/), each Some field emitted, each None omitted. Concrete, unlike the session model's abstract SignalMessage codec; checked byte-exactly by the KATs (known-answer tests).
def ProtoPreKeySignalMessage.encode (m : ProtoPreKeySignalMessage) : List (BitVec 8) :=
Prost.uint32Field 1 m.preKeyId ++
Prost.bytesField 2 m.baseKey ++
Prost.bytesField 3 m.identityKey ++
Prost.bytesField 4 m.message ++
Prost.uint32Field 5 m.registrationId ++
Prost.uint32Field 6 m.signedPreKeyId ++
Prost.uint32Field 7 m.kyberPreKeyId ++
Prost.bytesField 8 m.kyberCiphertext17 declarations not shown (lines 224–447): theorems, which Lean checks, or definitions that no headline statement uses
CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames., CryptoGames.
end LibsignalSessionApiend CryptoGames