(herald "Rules and Facts") (comment "CPSA 3.6.2") (comment "All input read from rules.scm")
Tree 0.
(defprotocol neq-test basic (defrole init (vars (n1 n2 text) (k skey)) (trace (send (cat n1 (enc n1 n2 k))) (recv n2)) (non-orig k) (uniq-orig n1 n2)) (defrule neq (forall ((a mesg)) (implies (fact neq a a) (false)))) (comment "Impose an nequality constraint using facts and rules"))
(defskeleton neq-test (vars (n1 n2 text) (k skey)) (defstrand init 2 (n1 n1) (n2 n2) (k k)) (non-orig k) (uniq-orig n1 n2) (comment "This skeleton should have a shape") (label 0) (unrealized (0 1)) (origs (n1 (0 0)) (n2 (0 0))) (comment "1 in cohort - 1 not yet seen"))
(defskeleton neq-test (vars (n1 text) (k skey)) (defstrand init 2 (n1 n1) (n2 n1) (k k)) (non-orig k) (uniq-orig n1) (operation nonce-test (displaced 1 0 init 1) n2 (0 1) (enc n1 n2 k)) (label 1) (parent 0) (unrealized) (shape) (maps ((0) ((n1 n1) (n2 n1) (k k)))) (origs (n1 (0 0))))
Tree 2.
(defprotocol neq-test basic (defrole init (vars (n1 n2 text) (k skey)) (trace (send (cat n1 (enc n1 n2 k))) (recv n2)) (non-orig k) (uniq-orig n1 n2)) (defrule neq (forall ((a mesg)) (implies (fact neq a a) (false)))) (comment "Impose an nequality constraint using facts and rules"))
Item 2.
(defskeleton neq-test (vars (n1 n2 text) (k skey)) (defstrand init 2 (n1 n1) (n2 n2) (k k)) (non-orig k) (uniq-orig n1 n2) (facts (neq n1 n2)) (comment "This skeleton should have no shapes") (label 2) (unrealized (0 1)) (origs (n1 (0 0)) (n2 (0 0))) (comment "empty cohort"))
Tree 3.
(defprotocol doorsep basic (defrole person (vars (d p akey) (k skey) (t text)) (trace (send (enc (enc k (invk p)) d)) (recv (enc t k)) (send t))) (defrole door (vars (d p akey) (k skey) (t text)) (trace (recv (enc (enc k (invk p)) d)) (send (enc t k)) (recv t))) (defrule trust (forall ((z strd) (p d akey)) (implies (and (p "person" z 1) (p "person" "p" z p) (p "person" "d" z d) (non (invk p))) (non (invk d)))) (comment "The trust rule")) (comment "Door Simple Example Protocol"))
(defskeleton doorsep (vars (t text) (k skey) (p d akey)) (defstrand door 3 (t t) (k k) (d d) (p p)) (non-orig (invk p)) (comment "Analyze from the doors's perspective") (label 3) (unrealized (0 0)) (origs) (comment "1 in cohort - 1 not yet seen"))
(defskeleton doorsep (vars (t text) (k skey) (p d d-0 akey)) (defstrand door 3 (t t) (k k) (d d) (p p)) (defstrand person 1 (k k) (d d-0) (p p)) (precedes ((1 0) (0 0))) (non-orig (invk p) (invk d-0)) (rule trust) (operation encryption-test (added-strand person 1) (enc k (invk p)) (0 0)) (label 4) (parent 3) (unrealized (0 0)) (comment "1 in cohort - 1 not yet seen"))
(defskeleton doorsep (vars (t text) (k skey) (p d akey)) (defstrand door 3 (t t) (k k) (d d) (p p)) (defstrand person 1 (k k) (d d) (p p)) (precedes ((1 0) (0 0))) (non-orig (invk p) (invk d)) (operation encryption-test (contracted (d-0 d)) (enc k (invk p)) (0 0) (enc (enc k (invk p)) d)) (label 5) (parent 4) (unrealized) (shape) (maps ((0) ((p p) (d d) (k k) (t t)))) (origs))