Examples.Ratchet.Proof

source

class DY.Example.Ratchet.HasProofTrace extends DY.Example.Ratchet.HasExecTrace :

Type 1

Instances

source

def DY.Example.Ratchet.transcriptToHash [HasProofTrace] (transcript : Transcript) :

Bytes

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem DY.Example.Ratchet.computeTranscriptHash_neq_initialTranscriptHash [HasProofTrace] (previousTxHash : Bytes) (elem : TranscriptElement) :

initialTranscriptHash ≠ computeTranscriptHash previousTxHash elem

source

theorem DY.Example.Ratchet.computeTranscriptHash_inj [HasProofTrace] (previousTxHash1 : Bytes) (elem1 : TranscriptElement) (previousTxHash2 : Bytes) (elem2 : TranscriptElement) :

computeTranscriptHash previousTxHash1 elem1 = computeTranscriptHash previousTxHash2 elem2 → previousTxHash1 = previousTxHash2 ∧ elem1 = elem2

source

theorem DY.Example.Ratchet.transcriptToHash_inj [HasProofTrace] :

Function.Injective transcriptToHash

source

def DY.Example.Ratchet.stateLabel [HasProofTrace] (me : Participant) (transcript : Transcript) :

Label

Equations

DY.Example.Ratchet.stateLabel me transcript = { isCorrupt := fun (tr : DY.ExecTrace) => DY.Example.Ratchet.StateCompromised me transcript tr, isCorruptLater := ⋯ }

Instances For

source

def DY.Example.Ratchet.stateTxHashLabel [HasProofTrace] (txHash : Bytes) :

Label

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem DY.Example.Ratchet.stateTxHashLabel_eq [HasProofTrace] (transcript : Transcript) (h : 2 ≤ List.length transcript) :

stateTxHashLabel (transcriptToHash transcript) = (stateLabel transcript[0].recipient transcript).join (stateLabel transcript[1].recipient transcript)

source

@[instance_reducible]

instance DY.Example.Ratchet.instKdfExpandInvariant_examples [HasProofTrace] :

KdfExpand.KdfExpandInvariant

Equations

One or more equations did not get rendered due to their size.

source

def DY.Example.Ratchet.isKeyMyTurn [HasProofTrace] (l : Transcript) (k : Bytes) :

Prop

Equations

One or more equations did not get rendered due to their size.
DY.Example.Ratchet.isKeyMyTurn [] k = (k = DY.Example.Ratchet.firstKey)
DY.Example.Ratchet.isKeyMyTurn [head] k = (k = DY.Example.Ratchet.firstKey)

Instances For

source

def DY.Example.Ratchet.isKeyOtherTurn [HasProofTrace] (l : Transcript) (k : Bytes) :

Prop

Equations

One or more equations did not get rendered due to their size.
DY.Example.Ratchet.isKeyOtherTurn [] k = (k = DY.Example.Ratchet.firstKey)
DY.Example.Ratchet.isKeyOtherTurn [head] k = (k = DY.Example.Ratchet.firstKey)

Instances For

source

theorem DY.Example.Ratchet.isKeyMyTurn_isKeyOtherTurn [HasProofTrace] (l : Transcript) (k1 k2 : Bytes) :

isKeyMyTurn l k1 → isKeyOtherTurn l k2 → k1 = k2

source

def DY.Example.Ratchet.labelBeforeTimestamp [HasProofTrace] (l : Label) (i : Nat) :

Label

Equations

DY.Example.Ratchet.labelBeforeTimestamp l i = { isCorrupt := fun (tr : DY.ExecTrace) => l.isCorrupt (DY.Trace.prefix tr i), isCorruptLater := ⋯ }

Instances For

source

def DY.Example.Ratchet.labelBeforeEvent [HasProofTrace] (l : Label) (me other : Participant) (transcript : Transcript) :

Label

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem DY.Example.Ratchet.labelBeforeEvent_canFlow_labelBeforeTimestamp [HasProofTrace] (l : Label) (me other : Participant) (transcript : Transcript) (i : Nat) (tr : ExecTrace) :

i ≤ Trace.length tr → (∃ (k : Bytes ), Trace.EventLogged (RatchetEvent.ReceiveUpdate me other transcript k) (Trace.prefix tr i)) → (∀ (i' : Nat), i' < i → ¬∃ (k : Bytes ), Trace.EventLogged (RatchetEvent.ReceiveUpdate me other transcript k) (Trace.prefix tr i')) → (labelBeforeEvent l me other transcript).canFlow (labelBeforeTimestamp l (i - 1)) tr

source

@[irreducible]

noncomputable def DY.Example.Ratchet.minimum.aux (p : Nat → Prop) (i1 i2 : Nat) :

Nat

Equations

DY.Example.Ratchet.minimum.aux p i1 i2 = if h : i1 ≥ i2 ∨ p i1 then i1 else DY.Example.Ratchet.minimum.aux p (i1 + 1) i2

Instances For

source

theorem DY.Example.Ratchet.minimum.aux.thm (p : Nat → Prop) (i1 i2 : Nat) :

(∀ (i : Nat), i < i1 → ¬p i) → p i2 → p (aux p i1 i2) ∧ ∀ (i : Nat), i < aux p i1 i2 → ¬p i

source

theorem DY.Example.Ratchet.minimum (p : Nat → Prop) (i : Nat) (h : p i) :

∃ (min : Nat ), p min ∧ ∀ (i' : Nat), i' < min → ¬p i'

source

theorem DY.Example.Ratchet.event_minimum_prefix [HasProofTrace] {EventT : Type} [ExecTraceTypes.Has (ProtocolEvent.ExecEntryT EventT)] (pred : EventT → Prop) (tr : ExecTrace) :

(∃ (ev : EventT), pred ev ∧ Trace.EventLogged ev tr) → ∃ (i : Nat ), ∃ (ev' : EventT), pred ev' ∧ Trace.EventLoggedAt ev' i tr ∧ Trace.EventLogged ev' (Trace.prefix tr (i + 1)) ∧ ∀ (i' : Nat) (ev'' : EventT), i' ≤ i → pred ev'' → ¬Trace.EventLogged ev'' (Trace.prefix tr i')

source

def DY.Example.Ratchet.ltkLabel [HasProofTrace] (p : Participant) :

Label

Equations

DY.Example.Ratchet.ltkLabel p = { isCorrupt := fun (tr : DY.ExecTrace) => ∃ (spk : DY.Bytes ), DY.LongTermKeys.LongTermKeyCompromised "Ratchet PKI" p spk tr, isCorruptLater := ⋯ }

Instances For

source

def DY.Example.Ratchet.keyLabelMyTurn [HasProofTrace] (me other : Participant) (transcript : Transcript) :

Label

Equations

One or more equations did not get rendered due to their size.
DY.Example.Ratchet.keyLabelMyTurn me other [] = DY.Label.pub
DY.Example.Ratchet.keyLabelMyTurn me other [head] = DY.Label.pub

Instances For

source

def DY.Example.Ratchet.keyLabelOtherTurn [HasProofTrace] (me other : Participant) (transcript : Transcript) :

Label

Equations

One or more equations did not get rendered due to their size.
DY.Example.Ratchet.keyLabelOtherTurn me other [] = DY.Label.pub
DY.Example.Ratchet.keyLabelOtherTurn me other [head] = DY.Label.pub

Instances For

source

theorem DY.Example.Ratchet.keyLabelMyTurn_shortTranscript [HasProofTrace] (me other : Participant) (transcript : Transcript) :

List.length transcript ≤ 1 → keyLabelMyTurn me other transcript = Label.pub

source

theorem DY.Example.Ratchet.keyLabelOtherTurn_shortTranscript [HasProofTrace] (me other : Participant) (transcript : Transcript) :

List.length transcript ≤ 1 → keyLabelOtherTurn me other transcript = Label.pub

source

theorem DY.Example.Ratchet.keyLabelMyTurn_eq [HasProofTrace] (me other : Participant) (transcript : Transcript) :

2 ≤ List.length transcript → keyLabelMyTurn me other transcript = ((stateLabel me transcript).join (stateLabel other transcript)).join ((keyLabelOtherTurn me other (List.tail transcript)).meet ((stateLabel me (List.tail transcript)).join ((stateLabel other transcript).join (labelBeforeEvent (ltkLabel other) me other transcript))))

source

theorem DY.Example.Ratchet.keyLabelOtherTurn_eq [HasProofTrace] (me other : Participant) (transcript : Transcript) :

2 ≤ List.length transcript → keyLabelOtherTurn me other transcript = ((stateLabel me transcript).join (stateLabel other transcript)).join ((keyLabelMyTurn me other (List.tail transcript)).meet ((stateLabel me transcript).join ((stateLabel other (List.tail transcript)).join (labelBeforeEvent (ltkLabel other) me other (List.tail transcript)))))

source

structure DY.Example.Ratchet.LongTermKeyUsage :

Type

principal : Participant

Instances For

source

@[instance_reducible]

instance DY.Example.Ratchet.instParseableSerializeableLongTermKeyUsage [HasProofTrace] :

Comparse.ParseableSerializeable LongTermKeyUsage

Equations

One or more equations did not get rendered due to their size.

source

def DY.Example.Ratchet.mkLongTermKeyUsage [HasProofTrace] (me : Participant) :

Usage

Equations

DY.Example.Ratchet.mkLongTermKeyUsage me = { type := "SigKey", tag := "Ratchet PKI", data := some (DY.Comparse.serialize { principal := me }) }

Instances For

source

theorem DY.Example.Ratchet.mkLongTermKeyUsage_inj [HasProofTrace] :

Function.Injective mkLongTermKeyUsage

source

@[instance_reducible]

instance DY.Example.Ratchet.RatchetSignPred [HasProofTrace] :

Signature.SignPred

Equations

One or more equations did not get rendered due to their size.

source

class DY.Example.Ratchet.HasBytesInvariants extends DY.Example.Ratchet.HasProofTrace :

Type 1

Instances

source

@[instance_reducible]

instance DY.Example.Ratchet.StateMyTurn.Invariant [HasBytesInvariants] :

PersistentLocalState.CompromisableLocalStateInv StateMyTurn

Equations

One or more equations did not get rendered due to their size.

source

theorem DY.Example.Ratchet.StateMyTurnInv_imp_Invariant [HasBytesInvariants] {tr : ProofTrace} (participant : Participant) (st : StateMyTurn) :

PersistentLocalState.LocalStateInv.invariant participant st tr → st.otherDhPk.Invariant tr ∧ st.k.Invariant tr

source

@[instance_reducible]

instance DY.Example.Ratchet.StateOtherTurn.Invariant [HasBytesInvariants] :

PersistentLocalState.CompromisableLocalStateInv StateOtherTurn

Equations

One or more equations did not get rendered due to their size.

source

theorem DY.Example.Ratchet.StateOtherTurnInv_imp_Invariant [HasBytesInvariants] {tr : ProofTrace} (participant : Participant) (st : StateOtherTurn) :

PersistentLocalState.LocalStateInv.invariant participant st tr → st.myDhSk.Invariant tr ∧ st.k.Invariant tr

source

@[instance_reducible]

instance DY.Example.Ratchet.instProofConfigMkLongTermKeyUsageLabel [HasBytesInvariants] :

LongTermKeys.ProofConfig "Ratchet PKI" mkLongTermKeyUsage (LongTermKeys.label "Ratchet PKI")

Equations

One or more equations did not get rendered due to their size.

source

@[instance_reducible]

instance DY.Example.Ratchet.RatchetEventInv [HasBytesInvariants] :

ProtocolEvent.EventInv RatchetEvent

Equations

One or more equations did not get rendered due to their size.

source

class DY.Example.Ratchet.HasTraceInvariant extends DY.Example.Ratchet.HasBytesInvariants :

Type 1

Instances

source

instance DY.Example.Ratchet.initialTranscriptHash.proof [HasTraceInvariant] :

HoareTriplePure initialTranscriptHash (fun (x : ProofTrace) => True) fun (res : Bytes) (tr : ProofTrace) => res.Publishable tr

source

instance DY.Example.Ratchet.computeTranscriptHash.proof [HasTraceInvariant] (previousTranscriptHash : Bytes) (elem : TranscriptElement) :

HoareTriplePure (computeTranscriptHash previousTranscriptHash elem) (fun (tr : ProofTrace) => previousTranscriptHash.Publishable tr ∧ elem.dhPk.Publishable tr) fun (res : Bytes) (tr : ProofTrace) => res.Publishable tr

source

instance DY.Example.Ratchet.firstKey.proof [HasTraceInvariant] :

HoareTriplePure firstKey (fun (x : ProofTrace) => True) fun (res : Bytes) (tr : ProofTrace) => res.Publishable tr

source

instance DY.Example.Ratchet.initiate.proof [HasTraceInvariant] (me other : Participant) (mySigKeyHandle : Nat) :

HoareTriple (initiate me other mySigKeyHandle) (fun (x : ProofTrace) => True) fun (x : Nat × Nat) (x_1 : ProofTrace) => True

source

instance DY.Example.Ratchet.processInitiate.proof [HasTraceInvariant] (me other : Participant) (otherVerifKeyHandle msgHandle : Nat) :

HoareTriple (processInitiate me other otherVerifKeyHandle msgHandle) (fun (x : ProofTrace) => True) fun (x : Nat) (x_1 : ProofTrace) => True

source

instance DY.Example.Ratchet.sendUpdate.proof [HasTraceInvariant] (me : Participant) (mySigKeyHandle stHandle : Nat) :

HoareTriple (sendUpdate me mySigKeyHandle stHandle) (fun (x : ProofTrace) => True) fun (x : Nat × Nat) (x_1 : ProofTrace) => True

source

theorem DY.Example.Ratchet.eventLogged_receiveUpdate_dhPk_label [HasTraceInvariant] (me recipient : Participant) (transcript : Transcript) (k : Bytes) (tr : ProofTrace) (h_transcript : 2 ≤ List.length transcript) :

Trace.Invariant tr → Trace.EventLogged (RatchetEvent.ReceiveUpdate me recipient transcript k) (Trace.erase tr) → ((stateLabel recipient transcript).join (labelBeforeEvent (ltkLabel recipient) me recipient transcript)).canFlow ((List.head transcript ⋯).dhPk.dhSkLabel tr) (Trace.erase tr)

source

theorem DY.Example.Ratchet.eventLogged_receiveUpdate_key_label [HasTraceInvariant] (me recipient : Participant) (transcript : Transcript) (k : Bytes) (tr : ProofTrace) :

2 ≤ List.length transcript → Trace.Invariant tr → Trace.EventLogged (RatchetEvent.ReceiveUpdate me recipient transcript k) (Trace.erase tr) → (keyLabelMyTurn me recipient transcript).canFlow (k.label tr) (Trace.erase tr)

source

instance DY.Example.Ratchet.processUpdate.proof [HasTraceInvariant] (me : Participant) (otherVerifKeyHandle stHandle msgHandle : Nat) :

HoareTriple (processUpdate me otherVerifKeyHandle stHandle msgHandle) (fun (x : ProofTrace) => True) fun (x : Nat) (x_1 : ProofTrace) => True

source

instance DY.Example.Ratchet.StateMyTurn.compromise.proof [HasTraceInvariant] (stHandle : Nat) :

HoareTriple (compromise stHandle) (fun (x : ProofTrace) => True) fun (x : Nat) (x_1 : ProofTrace) => True

source

instance DY.Example.Ratchet.StateOtherTurn.compromise.proof [HasTraceInvariant] (stHandle : Nat) :

HoareTriple (compromise stHandle) (fun (x : ProofTrace) => True) fun (x : Nat) (x_1 : ProofTrace) => True

source

instance DY.Example.Ratchet.instReachableImpliesInvariantReachability [HasTraceInvariant] :

ReachableImpliesInvariant initiate.reachability

source

instance DY.Example.Ratchet.instReachableImpliesInvariantReachability_1 [HasTraceInvariant] :

ReachableImpliesInvariant processInitiate.reachability

source

instance DY.Example.Ratchet.instReachableImpliesInvariantReachability_2 [HasTraceInvariant] :

ReachableImpliesInvariant sendUpdate.reachability

source

instance DY.Example.Ratchet.instReachableImpliesInvariantReachability_3 [HasTraceInvariant] :

ReachableImpliesInvariant processUpdate.reachability

source

instance DY.Example.Ratchet.instReachableImpliesInvariantReachability_4 [HasTraceInvariant] :

ReachableImpliesInvariant StateMyTurn.compromise.reachability

source

instance DY.Example.Ratchet.instReachableImpliesInvariantReachability_5 [HasTraceInvariant] :

ReachableImpliesInvariant StateOtherTurn.compromise.reachability