(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")

Trees: 0 2.

Tree 0.

1 0 
(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)))))

Item 0, Child: 1.

(enc cert (enc nb (privk a)) k) (enc nb k) (enc k (pubk b)) ((cert cert) (nb nb) (client a) (server b) (k k)) resp an_ssl 0 
(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"))

Item 1, Parent: 0.

(enc cert-0 (enc nb (privk a)) k-0) (enc nb k-0) (enc k-0 (pubk server)) (enc cert (enc nb (privk a)) k) (enc nb k) (enc k (pubk b)) ((cert cert-0) (nb nb) (client a) (server server) (k k-0)) init ((cert cert) (nb nb) (client a) (server b) (k k)) resp an_ssl 1 (realized)
(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))))

Tree 2.

4 2 
(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)))))

Item 2, Child: 4.

(enc cert (enc a b k nb (privk a)) k) (enc nb k) (enc k (pubk b)) ((cert cert) (nb nb) (client a) (server b) (k k)) resp an_ssl_revised 2
(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"))

Item 4, Parent: 2.

(enc cert (enc a b k nb (privk a)) k) (enc nb k) (enc k (pubk b)) (enc cert (enc a b k nb (privk a)) k) (enc nb k) (enc k (pubk b)) ((cert cert) (nb nb) (client a) (server b) (k k)) init ((cert cert) (nb nb) (client a) (server b) (k k)) resp an_ssl_revised 4 (realized) 
(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))))