---

Step * of Lemma NSL-protocol-legal

∀s:SES
  Legal([NSL-initiator1{i:l}(s);
         NSL-initiator2{i:l}(s);
         NSL-initiator3;
         NSL-responder0{i:l}(s);
         NSL-responder1{i:l}(s);
         NSL-responder2{i:l}(s);
         NSL-responder3])
BY
{ ProveProtocolLegal }

---

Latex:

---

Latex:
\mforall{}s:SES
    Legal([NSL-initiator1\{i:l\}(s);
                  NSL-initiator2\{i:l\}(s);
                  NSL-initiator3;
                  NSL-responder0\{i:l\}(s);
                  NSL-responder1\{i:l\}(s);
                  NSL-responder2\{i:l\}(s);
                  NSL-responder3])


By

---

Latex:
ProveProtocolLegal

---

Home Index