(comment "CPSA 2.2.11")
(comment "Extracted shapes")

(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 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 2)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (b b) (k k) (nb nb) (cert cert))))
  (origs (k (1 0)) (nb (0 1))))

(comment "Nothing left to do")