theorem DY.Example.Ratchet.authentication (me recipient : Participant) (transcript : Transcript) (k : Bytes) (time : Nat) (tr : ExecTrace) : Trace.Reachable reachability tr → Trace.EventLoggedAt (RatchetEvent.ReceiveUpdate me recipient transcript k) time tr → have trBefore := Trace.prefix tr time; Trace.EventLogged (RatchetEvent.SendUpdate recipient me transcript k) trBefore ∨ ∃ (spk : Bytes), LongTermKeys.LongTermKeyCompromised "Ratchet PKI" recipient spk trBefore

@[irreducible]

def DY.Example.Ratchet.ReceiveUpdateKeyCompromiseScenario (me recipient : Participant) (transcript : Transcript) (tr : ExecTrace) : Prop

Equations

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

@[irreducible]

def DY.Example.Ratchet.SendUpdateKeyCompromiseScenario (me recipient : Participant) (transcript : Transcript) (tr : ExecTrace) : Prop

Equations

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

theorem DY.Example.Ratchet.secrecy_receiveUpdate_recursive (me recipient : Participant) (transcript : Transcript) (k : Bytes) (tr : ExecTrace) : Trace.Reachable reachability tr → k.AttackerKnows tr → Trace.EventLogged (RatchetEvent.ReceiveUpdate me recipient transcript k) tr → ReceiveUpdateKeyCompromiseScenario me recipient transcript tr

theorem DY.Example.Ratchet.secrecy_sendUpdate_recursive (me recipient : Participant) (transcript : Transcript) (k : Bytes) (tr : ExecTrace) : Trace.Reachable reachability tr → k.AttackerKnows tr → Trace.EventLogged (RatchetEvent.SendUpdate me recipient transcript k) tr → SendUpdateKeyCompromiseScenario me recipient transcript tr

theorem DY.Example.Ratchet.secrecy_receiveUpdate_unfolded (me recipient : Participant) (transcript : Transcript) (k : Bytes) (tr : ExecTrace) : Trace.Reachable reachability tr → k.AttackerKnows tr → Trace.EventLogged (RatchetEvent.ReceiveUpdate me recipient transcript k) tr → (List.length transcript ≤ 1 ∨ StateCompromised me transcript tr ∨ StateCompromised me (List.tail transcript) tr ∨ StateCompromised recipient transcript tr) ∨ ∃ (previousTranscript : List TranscriptElement), ∃ (i : Nat), ∃ (k : Bytes), previousTranscript <:+ transcript ∧ Trace.EventLoggedAt (RatchetEvent.ReceiveUpdate me recipient previousTranscript k) i tr ∧ (∃ (spk : Bytes), LongTermKeys.LongTermKeyCompromised "Ratchet PKI" recipient spk (Trace.prefix tr i)) ∧ (previousTranscript.length ≤ 2 ∨ StateCompromised me previousTranscript tr ∨ StateCompromised me previousTranscript.tail tr ∨ StateCompromised recipient previousTranscript.tail tr ∨ StateCompromised recipient previousTranscript.tail.tail tr)

theorem DY.Example.Ratchet.secrecy_sendUpdate_unfolded (me recipient : Participant) (transcript : Transcript) (k : Bytes) (tr : ExecTrace) : Trace.Reachable reachability tr → k.AttackerKnows tr → Trace.EventLogged (RatchetEvent.SendUpdate me recipient transcript k) tr → (List.length transcript ≤ 1 ∨ StateCompromised me transcript tr ∨ StateCompromised recipient transcript tr ∨ StateCompromised recipient (List.tail transcript) tr) ∨ ∃ (previousTranscript : List TranscriptElement), ∃ (i : Nat), ∃ (k : Bytes), previousTranscript <:+ transcript ∧ Trace.EventLoggedAt (RatchetEvent.ReceiveUpdate me recipient previousTranscript k) i tr ∧ (∃ (spk : Bytes), LongTermKeys.LongTermKeyCompromised "Ratchet PKI" recipient spk (Trace.prefix tr i)) ∧ (previousTranscript.length ≤ 2 ∨ StateCompromised me previousTranscript tr ∨ StateCompromised me previousTranscript.tail tr ∨ StateCompromised recipient previousTranscript.tail tr ∨ StateCompromised recipient previousTranscript.tail.tail tr)