(comment "CPSA 2.2.11")
(comment "Extracted shapes")
(herald "Simplest approx to TLS:  Send pms encrypted.")
(comment "CPSA 2.2.11")
(comment "All input read from tls0.scm")

Trees: 0 1.

Tree 0.

0 
(defprotocol tls0 basic
  (defrole client
    (vars (pre_master_secret skey) (server_key akey))
    (trace (send (enc "client_version" pre_master_secret server_key))))
  (defrole server
    (vars (pre_master_secret skey) (server_key akey))
    (trace (recv (enc "client_version" pre_master_secret server_key)))))

Item 0.

pms pms (enc "client_version" pms k) ((pre_master_secret pms) (server_key k)) server tls0 0 (realized)
(defskeleton tls0
  (vars (pms skey) (k akey))
  (defstrand server 1 (pre_master_secret pms) (server_key k))
  (deflistener pms)
  (non-orig (invk k))
  (uniq-orig pms)
  (comment
    "Neither confidentiality nor authentication guarantees to server")
  (traces ((recv (enc "client_version" pms k))) ((recv pms) (send pms)))
  (label 0)
  (unrealized)
  (shape)
  (maps ((0 1) ((pms pms) (k k))))
  (origs))

Tree 1.

1 
(defprotocol tls0 basic
  (defrole client
    (vars (pre_master_secret skey) (server_key akey))
    (trace (send (enc "client_version" pre_master_secret server_key))))
  (defrole server
    (vars (pre_master_secret skey) (server_key akey))
    (trace (recv (enc "client_version" pre_master_secret server_key)))))

Item 1.

pms pms (enc "client_version" pms k) ((pre_master_secret pms) (server_key k)) client tls0 1 
(defskeleton tls0
  (vars (pms skey) (k akey))
  (defstrand client 1 (pre_master_secret pms) (server_key k))
  (deflistener pms)
  (non-orig (invk k))
  (uniq-orig pms)
  (comment
    "No authentication guarantees to client, but confidentiality.")
  (traces ((send (enc "client_version" pms k))) ((recv pms) (send pms)))
  (label 1)
  (unrealized (1 0))
  (preskeleton)
  (comment "Not a skeleton"))