cpsa-3.6.8: tst/target.scm

;;; Target terms experiment
;

(defprotocol target-simple basic
  (defrole comb (vars (k1 k2 skey) (n1 n2 text))
    (trace
     (send  (enc "oo" (enc "bar" n1 k1) (enc "baz" n2 k1) k2))
     (recv n1)
    )
    (non-orig k1 k2)
    (uniq-orig n1 n2)
    )
  (defrole trans1 (vars (n text) (k1 k2 skey) (m mesg))
  (trace
   (recv (enc "oo" (enc "bar" n k1) m k2))
   (send m))
   (non-orig k1 k2)
  )
  (defrole trans2 (vars (n text) (k skey))
    (trace
     (recv (enc "baz" n k))
     (send n)
     )
    (non-orig k)
  )
)

(defskeleton target-simple
  (vars )
  (defstrand comb 2 )
)

; The aim of this experiment was to verify a suspected incompleteness
; in CPSA.  This protocol is designed so that the initiator point of
; view has a single shape.  The protocol deals with encrypted pieces
; identified with a tag, either "foo", "bar", or "baz".  When a nonce
; is generated by the init role, it is encrypted with "foo."  The
; combiner role (comb) takes two "foo" pieces associated with nonces
; n1 and n2, and combines them to make a pair where n1 is placed in a
; "bar" piece and n2 is placed in a "baz" piece and these two are
; encrypted under another key.  There are two transforming roles.  One
; takes an encryption with two pieces in it where the first is a "bar"
; piece and removes the second piece from the encryption.  The other
; decrypts the nonce out of a "baz" piece.

; The shape expected involves a single init role that generates a
; "foo" piece with a nonce n.  That message supplied to the combiner
; role twice, which produces an "oo" encryption of an n "bar" piece
; and an n "baz" piece.  A trans1 instance extracts the "baz" piece,
; and a trans2 instance extracts n from the baz piece and returns it
; to init.

(defprotocol target basic
  (defrole comb (vars (k1 k2 skey) (n1 n2 text))
    (trace
     (recv (enc "foo" n1 k1))
     (recv (enc "foo" n2 k1))
     (send  (enc "oo" (enc "bar" n1 k1) (enc "baz" n2 k1) k2))
    )
    (non-orig k1 k2)
    (neq (n1 n2))
    )
  (defrole init (vars (k skey) (n text))
    (trace
     (send (enc "foo" n k))
     (recv n))
    (uniq-orig n)
    (non-orig k)
  )
  (defrole trans1 (vars (n text) (k1 k2 skey) (m mesg))
  (trace
   (recv (enc "oo" (enc "bar" n k1) m k2))
   (send m))
   (non-orig k1 k2)
  )
  (defrole trans2 (vars (n text) (k skey))
    (trace
     (recv (enc "baz" n k))
     (send n)
     )
    (non-orig k)
  )
)

;(defskeleton target
;  (vars )
;  (defstrand init 2 )
;)