RefinementPreservation.lean🔗

Tier 2 · definitions used by the symbolic proof 1 headline theorem depend on it 4 of 41 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.

Refinement Preservation over libsignal-cli Runs

Trusted: definitions used by the statement.

States CompRefinementPreservationCli: if the ten symbolic security queries (Security.AllModelSecurityQueriesHold) hold and runs under (Agree, R) refine the symbolic model (CompRefinesCli Agree R), then those ten security properties hold on guarded, coin-fresh hardware traces (SignalSessionSecureFor Agree R).

@[expose] public section

set_option autoImplicit false

namespace DY.Libsignal.Composed.Refinement.Cli

open CryptoProofLib.Refinement (ExternInterpretation)

open DY.Libsignal.Composed DY.Libsignal.Composed.Refinement

open DY.Libsignal.Composed.Security (SignalSessionSecureFor)

open CryptoVerification.SignalSession (Inputs Outcome)

def CompRefinementPreservationCliL36–42 ↗#

Preservation of the composed security bundle across trace refinement for run relation R.

def CompRefinementPreservationCli {ω : Type} (Agree : ExternInterpretation → ω → Prop)
    (R : ExternInterpretation → ω → Inputs → Option Outcome → Prop) : Prop :=
  Security.AllModelSecurityQueriesHold → CompRefinesCli Agree R → SignalSessionSecureFor Agree R

end DY.Libsignal.Composed.Refinement.Cli