(comment "CPSA 2.1.0")
(comment "All input read")

(defprotocol kelly1 basic
  (defrole client
    (vars (C A S name) (Ns request Check policy response text))
    (trace (send (cat C S request))
      (recv (cat S C (enc response Ns (privk S))))
      (send (cat C A Check (pubk S)))
      (recv (cat A C (enc policy (pubk S) Ns (privk A))))))
  (defrole appraiser
    (vars (C A S name) (N Ns hello Quote measurements Check policy text)
      (AIK name))
    (trace (recv (cat S A hello)) (send (cat A S N))
      (recv
        (cat S A (enc Quote measurements N Ns (pubk S) (privk AIK))
          (pubk S))) (recv (cat C A Check (pubk S)))
      (send (cat A C (enc policy (pubk S) Ns (privk A)))))
    (non-orig (privk A) (privk AIK))
    (uniq-orig N))
  (defrole server
    (vars (C A S name)
      (N Ns hello Quote measurements request response text) (AIK name))
    (trace (send (cat S A hello)) (recv (cat A S N))
      (send
        (cat S A (enc Quote measurements N Ns (pubk S) (privk AIK))
          (pubk S))) (recv (cat C S request))
      (send (cat S C (enc response Ns (privk S)))))
    (non-orig (privk S) (privk AIK))
    (uniq-orig Ns)))

(defskeleton kelly1
  (vars (Ns request Check policy response text) (A C S name))
  (defstrand client 4 (Ns Ns) (request request) (Check Check)
    (policy policy) (response response) (C C) (A A) (S S))
  (non-orig (privk A))
  (traces
    ((send (cat C S request))
      (recv (cat S C (enc response Ns (privk S))))
      (send (cat C A Check (pubk S)))
      (recv (cat A C (enc policy (pubk S) Ns (privk A))))))
  (label 0)
  (unrealized (0 3))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton kelly1
  (vars
    (Ns request Check policy response N hello Quote measurements Check-0
      text) (A C S C-0 AIK name))
  (defstrand client 4 (Ns Ns) (request request) (Check Check)
    (policy policy) (response response) (C C) (A A) (S S))
  (defstrand appraiser 5 (N N) (Ns Ns) (hello hello) (Quote Quote)
    (measurements measurements) (Check Check-0) (policy policy) (C C-0)
    (A A) (S S) (AIK AIK))
  (precedes ((1 4) (0 3)))
  (non-orig (privk A) (privk AIK))
  (uniq-orig N)
  (operation encryption-test (added-strand appraiser 5)
    (enc policy (pubk S) Ns (privk A)) (0 3))
  (traces
    ((send (cat C S request))
      (recv (cat S C (enc response Ns (privk S))))
      (send (cat C A Check (pubk S)))
      (recv (cat A C (enc policy (pubk S) Ns (privk A)))))
    ((recv (cat S A hello)) (send (cat A S N))
      (recv
        (cat S A (enc Quote measurements N Ns (pubk S) (privk AIK))
          (pubk S))) (recv (cat C-0 A Check-0 (pubk S)))
      (send (cat A C-0 (enc policy (pubk S) Ns (privk A))))))
  (label 1)
  (parent 0)
  (unrealized (1 2))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton kelly1
  (vars
    (Ns request Check policy response N hello Quote measurements Check-0
      hello-0 text) (A C S C-0 AIK A-0 name))
  (defstrand client 4 (Ns Ns) (request request) (Check Check)
    (policy policy) (response response) (C C) (A A) (S S))
  (defstrand appraiser 5 (N N) (Ns Ns) (hello hello) (Quote Quote)
    (measurements measurements) (Check Check-0) (policy policy) (C C-0)
    (A A) (S S) (AIK AIK))
  (defstrand server 3 (N N) (Ns Ns) (hello hello-0) (Quote Quote)
    (measurements measurements) (A A-0) (S S) (AIK AIK))
  (precedes ((1 1) (2 1)) ((1 4) (0 3)) ((2 2) (0 1)) ((2 2) (1 2)))
  (non-orig (privk A) (privk S) (privk AIK))
  (uniq-orig Ns N)
  (operation encryption-test (added-strand server 3)
    (enc Quote measurements N Ns (pubk S) (privk AIK)) (1 2))
  (traces
    ((send (cat C S request))
      (recv (cat S C (enc response Ns (privk S))))
      (send (cat C A Check (pubk S)))
      (recv (cat A C (enc policy (pubk S) Ns (privk A)))))
    ((recv (cat S A hello)) (send (cat A S N))
      (recv
        (cat S A (enc Quote measurements N Ns (pubk S) (privk AIK))
          (pubk S))) (recv (cat C-0 A Check-0 (pubk S)))
      (send (cat A C-0 (enc policy (pubk S) Ns (privk A)))))
    ((send (cat S A-0 hello-0)) (recv (cat A-0 S N))
      (send
        (cat S A-0 (enc Quote measurements N Ns (pubk S) (privk AIK))
          (pubk S)))))
  (label 2)
  (parent 1)
  (unrealized (0 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton kelly1
  (vars
    (Ns request Check policy response hello Check-0 N hello-0 Quote
      measurements request-0 text) (A C S C-0 C-1 A-0 AIK name))
  (defstrand client 4 (Ns Ns) (request request) (Check Check)
    (policy policy) (response response) (C C) (A A) (S S))
  (defstrand appraiser 5 (N N) (Ns Ns) (hello hello) (Quote Quote)
    (measurements measurements) (Check Check-0) (policy policy) (C C-0)
    (A A) (S S) (AIK AIK))
  (defstrand server 5 (N N) (Ns Ns) (hello hello-0) (Quote Quote)
    (measurements measurements) (request request-0) (response response)
    (C C-1) (A A-0) (S S) (AIK AIK))
  (precedes ((1 1) (2 1)) ((1 4) (0 3)) ((2 2) (1 2)) ((2 4) (0 1)))
  (non-orig (privk A) (privk S) (privk AIK))
  (uniq-orig Ns N)
  (operation encryption-test (added-strand server 5)
    (enc response Ns (privk S)) (0 1))
  (traces
    ((send (cat C S request))
      (recv (cat S C (enc response Ns (privk S))))
      (send (cat C A Check (pubk S)))
      (recv (cat A C (enc policy (pubk S) Ns (privk A)))))
    ((recv (cat S A hello)) (send (cat A S N))
      (recv
        (cat S A (enc Quote measurements N Ns (pubk S) (privk AIK))
          (pubk S))) (recv (cat C-0 A Check-0 (pubk S)))
      (send (cat A C-0 (enc policy (pubk S) Ns (privk A)))))
    ((send (cat S A-0 hello-0)) (recv (cat A-0 S N))
      (send
        (cat S A-0 (enc Quote measurements N Ns (pubk S) (privk AIK))
          (pubk S))) (recv (cat C-1 S request-0))
      (send (cat S C-1 (enc response Ns (privk S))))))
  (label 3)
  (parent 2)
  (unrealized)
  (shape))

(comment "Nothing left to do")