LibsignalAead.lean🔗

Tier 2 · definitions used by the computational proof 2 headline theorems depend on it 11 of 58 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-encoding and identity-key types for libsignal's per-message AEAD

Trusted in part. The theorems of Computational/Theorems/ use only SerializedIdentityKeys and addressCheckPasses from this file: read them. The rest is checked by Lean. See Computational/docs/TRUSTED_BASE.md.

Defines the fixed-block wire encoding WireEnc (for n-block CBC bodies, DEV-AEAD2), the concatenated 66-byte sender/receiver identity keys SerializedIdentityKeys authenticated by compute_mac, and the address check addressCheckPasses of verify_mac_with_addresses (DEV-AEAD11). The raw-byte wire AEAD used by the session bounds is in WireAeadDefs.lean.

@[expose] public section

namespace CryptoGames

namespace LibsignalAead

open CBC HMAC

1 declaration not shown (lines 36–42): theorems, which Lean checks, or definitions that no headline statement uses

CryptoGames.LibsignalAead.WireEnc.parse, CryptoGames.LibsignalAead.WireEnc, CryptoGames.LibsignalAead.WireEnc.encode

abbrev SerializedIdentityKeysL44–46 ↗#

Concatenated sender and receiver serialized public identity keys (33 bytes each: type byte 0x05 followed by 32 key bytes) authenticated by SignalMessage::compute_mac.

abbrev SerializedIdentityKeys := List.Vector (BitVec 8) 66

def addressCheckPassesL48–55 ↗#

Address check of SignalMessage::verify_mac_with_addresses, given the message's addresses field (present) and locally serialized expected addresses (expected): accept if present is none, reject if present is some _ and expected is none, otherwise test equality.

def addressCheckPasses (present expected : Option (List (BitVec 8))) : Bool :=
  match present, expected with
  | none, _ => true
  | some _, none => false
  | some a, some e => a == e

end LibsignalAead

end CryptoGames