def DY.Example.Ratchet.honestAttacker : Traceful Unit

Equations

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

theorem DY.Example.Ratchet.honestAttacker_properties : have tr := (honestAttacker.run Trace.nil).snd.val; Trace.Reachable reachability tr ∧ ∃ (t1 : Nat), ∃ (t2 : Nat), ∃ (transcript : Transcript), ∃ (k : Bytes), List.length transcript = 21 ∧ t1 < t2 ∧ Trace.EventLoggedAt (RatchetEvent.SendUpdate "Alice" "Bob" transcript k) t1 tr ∧ Trace.EventLoggedAt (RatchetEvent.ReceiveUpdate "Bob" "Alice" transcript k) t2 tr

def DY.Example.Ratchet.compromiseStateMyTurnAttacker : Traceful Unit

Equations

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

theorem DY.Example.Ratchet.compromiseStateMyTurnAttacker_properties : have tr := (compromiseStateMyTurnAttacker.run Trace.nil).snd.val; Trace.Reachable reachability tr ∧ ∃ (t : Nat), ∃ (transcript : Transcript), ∃ (k : Bytes), List.length transcript = 21 ∧ Trace.EventLoggedAt (RatchetEvent.ReceiveUpdate "Bob" "Alice" transcript k) t tr ∧ k.AttackerKnows tr

def DY.Example.Ratchet.compromiseStateOtherTurnAttacker : Traceful Unit

Equations

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

theorem DY.Example.Ratchet.compromiseStateOtherTurnAttacker_properties : have tr := (compromiseStateOtherTurnAttacker.run Trace.nil).snd.val; Trace.Reachable reachability tr ∧ ∃ (t : Nat), ∃ (transcript : Transcript), ∃ (k : Bytes), List.length transcript = 21 ∧ Trace.EventLoggedAt (RatchetEvent.ReceiveUpdate "Bob" "Alice" transcript k) t tr ∧ k.AttackerKnows tr

def DY.Example.Ratchet.compromiseSigKeyAttacker : Traceful Unit

Equations

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

theorem DY.Example.Ratchet.compromiseSigKeyAttacker_properties : have tr := (compromiseSigKeyAttacker.run Trace.nil).snd.val; Trace.Reachable reachability tr ∧ ∃ (t : Nat), ∃ (transcript : Transcript), ∃ (k : Bytes), List.length transcript = 21 ∧ Trace.EventLoggedAt (RatchetEvent.SendUpdate "Alice" "Bob" transcript k) t tr ∧ k.AttackerKnows tr