---

Step * of Lemma CR-protocol-fresh

∀s:SES
  (ActionsDisjoint
  ⇒ FreshSignatures([CR-initiator1{i:l}(s);
                      CR-initiator2{i:l}(s);
                      CR-initiator3;
                      CR-responder1{i:l}(s);
                      CR-responder2{i:l}(s);
                      CR-responder3]))
BY
{ (Auto THEN ProveProtocolFresh⋅) }

---

Latex:

---

Latex:
\mforall{}s:SES
    (ActionsDisjoint
    {}\mRightarrow{}  FreshSignatures([CR-initiator1\{i:l\}(s);
                                            CR-initiator2\{i:l\}(s);
                                            CR-initiator3;
                                            CR-responder1\{i:l\}(s);
                                            CR-responder2\{i:l\}(s);
                                            CR-responder3]))


By

---

Latex:
(Auto  THEN  ProveProtocolFresh\mcdot{})

---

Home Index