AlphaProof Code: Verifying Signal’s Security at the Machine-Code Level

Paper › Symbolic/Specifications/Model/EquationalTheory › TrWireMsg.leanTier 2 · definitions

TrWireMsg.lean🔗

Tier 2 · definitions used by the symbolic proof 13 headline theorems depend on it 133 of 191 lines trusted source ↗

trust banner in the header: none; the closure computes B2 for the symbolic proof

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.

Declarations on this page (19)

Triple Ratchet SignalMessage Wire Terms

DyLean term algebra and attacker deduction rules for the MAC-authenticated portion of a Triple Ratchet SignalMessage (version byte plus protobuf body, parameterized by EncodingVariation for non-canonical prost encodings).

namespace DY.TrWire

inductive PbValueL27–34 ↗#

A protobuf wire value: varint (type 0), length-delimited bytes (type 2), or skipped payload (types 1, 3, and 5).

public inductive PbValue where | varint (n : Nat) | bytes (b : List (BitVec 8)) | unknown (wireType : Nat) (payload : List (BitVec 8)) deriving DecidableEq
@[expose] section

inductive FieldItemL38–45 ↗#

One field occurrence of the SignalMessage protobuf body in wire order.

public inductive FieldItem where /-- Known field `tag` (1 to 6) carrying its value from the message. -/ | known (tag keyPad valuePad : Nat) /-- Overridden, repeated, or unknown field carrying an explicit `PbValue`. -/ | extra (tag : Nat) (value : PbValue) (keyPad valuePad : Nat) deriving DecidableEq

def FieldItem.toNatsL47–53 ↗#

Injective List Nat encoding of a FieldItem.

public def FieldItem.toNats : FieldItem → List Nat | .known t kp vp => [0, t, kp, vp] | .extra t (.varint n) kp vp => [1, t, kp, vp, n] | .extra t (.bytes b) kp vp => 2 :: t :: kp :: vp :: b.map BitVec.toNat | .extra t (.unknown wt p) kp vp => 3 :: t :: kp :: vp :: wt :: p.map BitVec.toNat

structure EncodingVariationL55–68 ↗#

Non-canonical protobuf and version-byte encoding choices accepted by prost and libsignal relative to canonicalVariation.

public structure EncodingVariation where /-- Low 4 bits of byte 0 (ignored by libsignal). -/ versionLowNibble : Nat /-- Trailing bytes after the 32-byte key in field 1 (ignored by `PublicKey::deserialize`). -/ ratchetKeyTrailingBytes : List (BitVec 8) /-- High bits above bit 31 in `known 2` varints (truncated by `as u32`). -/ counterHigh : Nat /-- High bits above bit 31 in `known 3` varints (truncated by `as u32`). -/ previousCounterHigh : Nat fields : List FieldItem deriving DecidableEq
end

def canonicalVariationL72–76 ↗#

Canonical encoding emitted by SignalMessage::new: byte 0x44, fields 1 to 4 in order, minimal varints.

@[expose] public def canonicalVariation : EncodingVariation := ⟨4, [], 0, 0, [.known 1 0 0, .known 2 0 0, .known 3 0 0, .known 4 0 0]⟩

class CanTrWireMsgL78–81 ↗#

public class CanTrWireMsg (Bytes: Type u) where trWireMsg: (version: UInt8) → (senderRatchetKey: Bytes) → (counter previousCounter: UInt32) → (ciphertext pqRatchet: Bytes) → (encodingVariation: EncodingVariation) → Bytes
export CanTrWireMsg (trWireMsg)
namespace TrWireMsg

abbrev TrWireHeaderDataL87–88 ↗#

public abbrev TrWireHeaderData := UInt8 × UInt32 × UInt32 × EncodingVariation

def TrWireHeaderData.codeL90–94 ↗#

@[expose] public def TrWireHeaderData.code (d : TrWireHeaderData) : List (List Nat) := let (v, c, pc, ev) := d [v.toNat, c.toNat, pc.toNat, ev.versionLowNibble, ev.counterHigh, ev.previousCounterHigh] :: ev.ratchetKeyTrailingBytes.map BitVec.toNat :: ev.fields.map FieldItem.toNats

structure SubFL96–104 ↗#

public structure SubF (Bytes: Type) where version: UInt8 senderRatchetKey: Bytes counter: UInt32 previousCounter: UInt32 ciphertext: Bytes pqRatchet: Bytes encodingVariation: EncodingVariation

instanceL106–107 ↗#

public instance: ALaCarte.FunctorSizeOf SubF := .ternary SubF.senderRatchetKey SubF.ciphertext SubF.pqRatchet

instanceL109–149 ↗#

public instance: SubBytesFunctor SubF := .ternaryByCode TrWireHeaderData.code (fun {x y} hcode => x:TrWireHeaderDatay:TrWireHeaderDatahcode:x.code = y.code⊢ x = y x:TrWireHeaderDatay:TrWireHeaderDatahcode:x.code = y.codemap_bv:∀ {l₁ l₂ : List (BitVec 8)}, List.map BitVec.toNat l₁ = List.map BitVec.toNat l₂ → l₁ = l₂⊢ x = y x:TrWireHeaderDatay:TrWireHeaderDatahcode:x.code = y.codemap_bv:∀ {l₁ l₂ : List (BitVec 8)}, List.map BitVec.toNat l₁ = List.map BitVec.toNat l₂ → l₁ = l₂item_inj:∀ {a b : FieldItem}, a.toNats = b.toNats → a = b⊢ x = y x:TrWireHeaderDatay:TrWireHeaderDatahcode:x.code = y.codemap_bv:∀ {l₁ l₂ : List (BitVec 8)}, List.map BitVec.toNat l₁ = List.map BitVec.toNat l₂ → l₁ = l₂item_inj:∀ {a b : FieldItem}, a.toNats = b.toNats → a = bmap_item:∀ {l₁ l₂ : List FieldItem}, List.map FieldItem.toNats l₁ = List.map FieldItem.toNats l₂ → l₁ = l₂⊢ x = y y:TrWireHeaderDatamap_bv:∀ {l₁ l₂ : List (BitVec 8)}, List.map BitVec.toNat l₁ = List.map BitVec.toNat l₂ → l₁ = l₂item_inj:∀ {a b : FieldItem}, a.toNats = b.toNats → a = bmap_item:∀ {l₁ l₂ : List FieldItem}, List.map FieldItem.toNats l₁ = List.map FieldItem.toNats l₂ → l₁ = l₂v₁:UInt8c₁:UInt32pc₁:UInt32low₁:Nattr₁:List (BitVec 8)ch₁:Natpch₁:Natfs₁:List FieldItemhcode:TrWireHeaderData.code (v₁, c₁, pc₁, { versionLowNibble := low₁, ratchetKeyTrailingBytes := tr₁, counterHigh := ch₁, previousCounterHigh := pch₁, fields := fs₁ }) = y.code⊢ (v₁, c₁, pc₁, { versionLowNibble := low₁, ratchetKeyTrailingBytes := tr₁, counterHigh := ch₁, previousCounterHigh := pch₁, fields := fs₁ }) = y map_bv:∀ {l₁ l₂ : List (BitVec 8)}, List.map BitVec.toNat l₁ = List.map BitVec.toNat l₂ → l₁ = l₂item_inj:∀ {a b : FieldItem}, a.toNats = b.toNats → a = bmap_item:∀ {l₁ l₂ : List FieldItem}, List.map FieldItem.toNats l₁ = List.map FieldItem.toNats l₂ → l₁ = l₂v₁:UInt8c₁:UInt32pc₁:UInt32low₁:Nattr₁:List (BitVec 8)ch₁:Natpch₁:Natfs₁:List FieldItemv₂:UInt8c₂:UInt32pc₂:UInt32low₂:Nattr₂:List (BitVec 8)ch₂:Natpch₂:Natfs₂:List FieldItemhcode:TrWireHeaderData.code (v₁, c₁, pc₁, { versionLowNibble := low₁, ratchetKeyTrailingBytes := tr₁, counterHigh := ch₁, previousCounterHigh := pch₁, fields := fs₁ }) = TrWireHeaderData.code (v₂, c₂, pc₂, { versionLowNibble := low₂, ratchetKeyTrailingBytes := tr₂, counterHigh := ch₂, previousCounterHigh := pch₂, fields := fs₂ })⊢ (v₁, c₁, pc₁, { versionLowNibble := low₁, ratchetKeyTrailingBytes := tr₁, counterHigh := ch₁, previousCounterHigh := pch₁, fields := fs₁ }) = (v₂, c₂, pc₂, { versionLowNibble := low₂, ratchetKeyTrailingBytes := tr₂, counterHigh := ch₂, previousCounterHigh := pch₂, fields := fs₂ }) map_bv:∀ {l₁ l₂ : List (BitVec 8)}, List.map BitVec.toNat l₁ = List.map BitVec.toNat l₂ → l₁ = l₂item_inj:∀ {a b : FieldItem}, a.toNats = b.toNats → a = bmap_item:∀ {l₁ l₂ : List FieldItem}, List.map FieldItem.toNats l₁ = List.map FieldItem.toNats l₂ → l₁ = l₂v₁:UInt8c₁:UInt32pc₁:UInt32low₁:Nattr₁:List (BitVec 8)ch₁:Natpch₁:Natfs₁:List FieldItemv₂:UInt8c₂:UInt32pc₂:UInt32low₂:Nattr₂:List (BitVec 8)ch₂:Natpch₂:Natfs₂:List FieldItemhcode:(v₁.toNat = v₂.toNat ∧ c₁.toNat = c₂.toNat ∧ pc₁.toNat = pc₂.toNat ∧ low₁ = low₂ ∧ ch₁ = ch₂ ∧ pch₁ = pch₂) ∧ List.map BitVec.toNat tr₁ = List.map BitVec.toNat tr₂ ∧ List.map FieldItem.toNats fs₁ = List.map FieldItem.toNats fs₂⊢ (v₁, c₁, pc₁, { versionLowNibble := low₁, ratchetKeyTrailingBytes := tr₁, counterHigh := ch₁, previousCounterHigh := pch₁, fields := fs₁ }) = (v₂, c₂, pc₂, { versionLowNibble := low₂, ratchetKeyTrailingBytes := tr₂, counterHigh := ch₂, previousCounterHigh := pch₂, fields := fs₂ }) map_bv:∀ {l₁ l₂ : List (BitVec 8)}, List.map BitVec.toNat l₁ = List.map BitVec.toNat l₂ → l₁ = l₂item_inj:∀ {a b : FieldItem}, a.toNats = b.toNats → a = bmap_item:∀ {l₁ l₂ : List FieldItem}, List.map FieldItem.toNats l₁ = List.map FieldItem.toNats l₂ → l₁ = l₂v₁:UInt8c₁:UInt32pc₁:UInt32low₁:Nattr₁:List (BitVec 8)ch₁:Natpch₁:Natfs₁:List FieldItemv₂:UInt8c₂:UInt32pc₂:UInt32tr₂:List (BitVec 8)fs₂:List FieldItemhv:v₁.toNat = v₂.toNathc:c₁.toNat = c₂.toNathpc:pc₁.toNat = pc₂.toNathtr:List.map BitVec.toNat tr₁ = List.map BitVec.toNat tr₂hfs:List.map FieldItem.toNats fs₁ = List.map FieldItem.toNats fs₂⊢ (v₁, c₁, pc₁, { versionLowNibble := low₁, ratchetKeyTrailingBytes := tr₁, counterHigh := ch₁, previousCounterHigh := pch₁, fields := fs₁ }) = (v₂, c₂, pc₂, { versionLowNibble := low₁, ratchetKeyTrailingBytes := tr₂, counterHigh := ch₁, previousCounterHigh := pch₁, fields := fs₂ }) All goals completed! 🐙) (fun x => (x.version, x.counter, x.previousCounter, x.encodingVariation)) SubF.senderRatchetKey SubF.ciphertext SubF.pqRatchet (fun d rk ct pq => { version := d.1, senderRatchetKey := rk, counter := d.2.1, previousCounter := d.2.2.1, ciphertext := ct, pqRatchet := pq, encodingVariation := d.2.2.2 })

def SubF.lengthL151–153 ↗#

@[expose] public def SubF.length [BytesFunctor]: Bytes.PartialLength SubF := fun ⟨_, rk, _, _, ct, pq, _⟩ rec => 1 + rec rk + 4 + 4 + rec ct + rec pq
end TrWireMsg

#combineL157–158 ↗#

#combine into BytesFunctor, BytesLength from TrWireMsg,
variable [BytesFunctor] [BytesFunctor.Has SubF]

abbrev TrWireMsg.SubF.packL162–163 ↗#

public abbrev TrWireMsg.SubF.pack (x: TrWireMsg.SubF Bytes) := BytesView.pack x

instanceL165–170 ↗#

public instance: CanTrWireMsg Bytes where trWireMsg version senderRatchetKey counter previousCounter ciphertext pqRatchet encodingVariation := ({version, senderRatchetKey, counter, previousCounter, ciphertext, pqRatchet, encodingVariation}: TrWireMsg.SubF Bytes).pack

def trWireMsgFields?L172–173 ↗#

@[expose] public def trWireMsgFields? (b: Bytes): Option (TrWireMsg.SubF Bytes) := b.view? TrWireMsg.SubF

def trWireMsg.attackerKnowledgeL175–179 ↗#

@[expose] public def trWireMsg.attackerKnowledge: SubAttackerKnowledge SubF where pred p out := ∃ x: TrWireMsg.SubF Bytes, out = x.pack ∧ p x.senderRatchetKey ∧ p x.ciphertext ∧ p x.pqRatchet

def trWireMsgArg.attackerKnowledgeL181–185 ↗#

@[expose] public def trWireMsgArg.attackerKnowledge: SubAttackerKnowledge SubF where pred p out := ∃ x: TrWireMsg.SubF Bytes, p x.pack ∧ (out = x.senderRatchetKey ∨ out = x.ciphertext ∨ out = x.pqRatchet)

#combineL187–192 ↗#

#combine [BytesFunctor.Has SubF] into attackerKnowledge' from trWireMsg, trWireMsgArg,
end DY.TrWire