---

Step * of Lemma CRX-authentication-theorem

∀sth:SecurityTheory
  (CRX-protocol{i:l}(sth-es(sth)) |= CR-initiator4{i:l}(sth-es(sth)) authenticates 2 messages 
  ∧ CRX-protocol{i:l}(sth-es(sth)) |= CR-responder6{i:l}(sth-es(sth)) authenticates 3 messages )
BY
{ ProveAuthentication }

---

Latex:

---

Latex:
\mforall{}sth:SecurityTheory
    (CRX-protocol\{i:l\}(sth-es(sth))  |=  CR-initiator4\{i:l\}(sth-es(sth))  authenticates  2  messages 
    \mwedge{}  CRX-protocol\{i:l\}(sth-es(sth))  |=  CR-responder6\{i:l\}(sth-es(sth))  authenticates  3  messages  )


By

---

Latex:
ProveAuthentication

---

Home Index