(herald "Old SSL version discussed by Abadi-Needham.")

(comment "CPSA 2.2.11")
(comment "All input read from an_ssl.scm")

(defprotocol an_ssl basic
  (defrole init
    (vars (client server name) (k skey) (cert nb text))
    (trace (send (enc k (pubk server))) (recv (enc nb k))
      (send (enc cert (enc nb (privk client)) k))))
  (defrole resp
    (vars (client server name) (k skey) (cert nb text))
    (trace (recv (enc k (pubk server))) (send (enc nb k))
      (recv (enc cert (enc nb (privk client)) k)))))

(defskeleton an_ssl
  (vars (nb cert text) (a b name) (k skey))
  (defstrand resp 3 (cert cert) (nb nb) (client a) (server b) (k k))
  (non-orig (privk a) (privk b))
  (uniq-orig nb k)
  (traces
    ((recv (enc k (pubk b))) (send (enc nb k))
      (recv (enc cert (enc nb (privk a)) k))))
  (label 0)
  (unrealized (0 2))
  (origs (nb (0 1)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton an_ssl
  (vars (nb cert cert-0 text) (a b server name) (k k-0 skey))
  (defstrand resp 3 (cert cert) (nb nb) (client a) (server b) (k k))
  (defstrand init 3 (cert cert-0) (nb nb) (client a) (server server)
    (k k-0))
  (precedes ((0 1) (1 1)) ((1 2) (0 2)))
  (non-orig (privk a) (privk b))
  (uniq-orig nb k)
  (operation encryption-test (added-strand init 3) (enc nb (privk a))
    (0 2))
  (traces
    ((recv (enc k (pubk b))) (send (enc nb k))
      (recv (enc cert (enc nb (privk a)) k)))
    ((send (enc k-0 (pubk server))) (recv (enc nb k-0))
      (send (enc cert-0 (enc nb (privk a)) k-0))))
  (label 1)
  (parent 0)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (b b) (k k) (nb nb) (cert cert))))
  (origs (nb (0 1))))

(comment "Nothing left to do")

(defprotocol an_ssl_revised basic
  (defrole init
    (vars (client server name) (k skey) (cert nb text))
    (trace (send (enc k (pubk server))) (recv (enc nb k))
      (send (enc cert (enc client server k nb (privk client)) k))))
  (defrole resp
    (vars (client server name) (k skey) (cert nb text))
    (trace (recv (enc k (pubk server))) (send (enc nb k))
      (recv (enc cert (enc client server k nb (privk client)) k)))))

(defskeleton an_ssl_revised
  (vars (nb cert text) (a b name) (k skey))
  (defstrand resp 3 (cert cert) (nb nb) (client a) (server b) (k k))
  (non-orig (privk a) (privk b))
  (uniq-orig nb k)
  (traces
    ((recv (enc k (pubk b))) (send (enc nb k))
      (recv (enc cert (enc a b k nb (privk a)) k))))
  (label 2)
  (unrealized (0 2))
  (origs (nb (0 1)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton an_ssl_revised
  (vars (nb cert cert-0 text) (a b name) (k skey))
  (defstrand resp 3 (cert cert) (nb nb) (client a) (server b) (k k))
  (defstrand init 3 (cert cert-0) (nb nb) (client a) (server b) (k k))
  (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2)))
  (non-orig (privk a) (privk b))
  (uniq-orig nb k)
  (operation encryption-test (added-strand init 3)
    (enc a b k nb (privk a)) (0 2))
  (traces
    ((recv (enc k (pubk b))) (send (enc nb k))
      (recv (enc cert (enc a b k nb (privk a)) k)))
    ((send (enc k (pubk b))) (recv (enc nb k))
      (send (enc cert-0 (enc a b k nb (privk a)) k))))
  (label 3)
  (parent 2)
  (unrealized (0 2))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton an_ssl_revised
  (vars (nb cert text) (a b name) (k skey))
  (defstrand resp 3 (cert cert) (nb nb) (client a) (server b) (k k))
  (defstrand init 3 (cert cert) (nb nb) (client a) (server b) (k k))
  (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2)))
  (non-orig (privk a) (privk b))
  (uniq-orig nb k)
  (operation encryption-test (displaced 2 1 init 3)
    (enc cert-0 (enc a b k nb (privk a)) k) (0 2))
  (traces
    ((recv (enc k (pubk b))) (send (enc nb k))
      (recv (enc cert (enc a b k nb (privk a)) k)))
    ((send (enc k (pubk b))) (recv (enc nb k))
      (send (enc cert (enc a b k nb (privk a)) k))))
  (label 4)
  (parent 3)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (b b) (k k) (nb nb) (cert cert))))
  (origs (k (1 0)) (nb (0 1))))

(defskeleton an_ssl_revised
  (vars (nb cert cert-0 text) (a b name) (k skey))
  (defstrand resp 3 (cert cert) (nb nb) (client a) (server b) (k k))
  (defstrand init 3 (cert cert-0) (nb nb) (client a) (server b) (k k))
  (deflistener k)
  (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 0) (2 0)) ((1 2) (0 2))
    ((2 1) (0 2)))
  (non-orig (privk a) (privk b))
  (uniq-orig nb k)
  (operation encryption-test (added-listener k)
    (enc cert (enc a b k nb (privk a)) k) (0 2))
  (traces
    ((recv (enc k (pubk b))) (send (enc nb k))
      (recv (enc cert (enc a b k nb (privk a)) k)))
    ((send (enc k (pubk b))) (recv (enc nb k))
      (send (enc cert-0 (enc a b k nb (privk a)) k)))
    ((recv k) (send k)))
  (label 5)
  (parent 3)
  (unrealized (2 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton an_ssl_revised
  (vars (nb cert cert-0 text) (a b name) (k skey))
  (defstrand resp 3 (cert cert) (nb nb) (client a) (server b) (k k))
  (defstrand init 3 (cert cert-0) (nb nb) (client a) (server b) (k k))
  (deflistener k)
  (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (2 0)) ((2 1) (0 2)))
  (non-orig (privk a) (privk b))
  (uniq-orig nb k)
  (operation nonce-test (displaced 3 1 init 3) k (2 0) (enc k (pubk b)))
  (traces
    ((recv (enc k (pubk b))) (send (enc nb k))
      (recv (enc cert (enc a b k nb (privk a)) k)))
    ((send (enc k (pubk b))) (recv (enc nb k))
      (send (enc cert-0 (enc a b k nb (privk a)) k)))
    ((recv k) (send k)))
  (label 6)
  (parent 5)
  (unrealized (2 0))
  (comment "empty cohort"))

(comment "Nothing left to do")