---

Step * of Lemma CR-protocol-legal

∀s:SES
  Legal([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
{ ProveProtocolLegal }

---

Latex:

---

Latex:
\mforall{}s:SES
    Legal([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:
ProveProtocolLegal

---

Home Index