AsmSecure.lean🔗

Tier 2 · definitions used by the symbolic proof 2 headline theorems depend on it 18 of 59 lines trusted trust banner B2, trusted: definitions used by the statement 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.

Hardware Attacker and Explained-Trace Security Queries

Trusted: definitions used by the statement.

Defines the hardware-level Dolev-Yao attacker (HwAttackerObserves, HwAttackerKnows) and instantiates Security.AllSecurityQueriesHold over explained CLI event traces (AllSecurityQueriesHoldOnHwTrace).

@[expose] public section

namespace DY.Libsignal.Composed.Refinement

open DY DY.Comparse

open CryptoProofLib.Refinement (ExternInterpretation)

open DY.Libsignal.HwEvents (CliEvent)

section

variable (r : ProtocolSetup) (vis : List VisEntry)

def HwAttackerObservesL36–43 ↗#

Terms observed by the hardware adversary under vis: public setup messages (setupSent r) and terms in .send, .recv, or .leak entries (excluding .pt, .rng, and .accept).

def HwAttackerObserves (t : DY.Bytes) : Prop :=
  t ∈ setupSent r ∨
  ∃ v ∈ vis, t ∈ v.terms ∧
    match v.kind with
    | .send | .recv | .leak => True
    | .pt | .rng | .accept => False

def HwAttackerKnowsL45–48 ↗#

Dolev-Yao deduction closure of HwAttackerObserves r vis.

def HwAttackerKnows (t : DY.Bytes) : Prop :=
  Fixpoint.mkLeastFixpoint
    (fun known b => AttackerKnowledge.attackerKnowledge.pred known b ∨ HwAttackerObserves r vis b) t

end

def AllSecurityQueriesHoldOnHwTraceL52–60 ↗#

Under every explanation (g, ss, vis) of CLI trace evs, all ten security queries hold on runTrace r ss against HwAttackerKnows r vis.

def AllSecurityQueriesHoldOnHwTrace (interpretation : ExternInterpretation) (r : ProtocolSetup)
    (S : OpaqueSymbolSemantics) (evs : List CliEvent) : Prop :=
  ∀ g ss vis, Explains interpretation r S g ss vis evs →
    Security.AllSecurityQueriesHold (runTrace r ss) (HwAttackerKnows r vis)

end DY.Libsignal.Composed.Refinement