(herald "Blanchet's Simple Example Protocol"
  (comment "There is a flaw in this protocol by design"))
(comment "CPSA 3.4.0")
(comment "All input read from blanchet.scm")

Trees: 0 4 6 11 14 18 23 25.

Tree 0.

2 3 1 0 
(defprotocol blanchet basic
  (defrole init
    (vars (a b akey) (s skey) (d data))
    (trace (send (enc (enc s (invk a)) b)) (recv (enc d s)))
    (uniq-orig s))
  (defrole resp
    (vars (a b akey) (s skey) (d data))
    (trace (recv (enc (enc s (invk a)) b)) (send (enc d s)))
    (uniq-orig d))
  (comment "Blanchet's protocol"))

Item 0, Children: 1 2.

(enc d s) (enc (enc s (invk a)) b) ((d d) (s s) (a a) (b b)) init blanchet 0 
(defskeleton blanchet
  (vars (d data) (s skey) (a b akey))
  (defstrand init 2 (d d) (s s) (a a) (b b))
  (non-orig (invk b))
  (uniq-orig s)
  (comment "Analyze from the initiator's perspective")
  (label 0)
  (unrealized (0 1))
  (origs (s (0 0)))
  (comment "2 in cohort - 2 not yet seen"))

Item 1, Parent: 0, Child: 3.

(enc d s) (enc (enc s (invk a-0)) b-0) (enc d s) (enc (enc s (invk a)) b) ((d d) (s s) (a a-0) (b b-0)) resp ((d d) (s s) (a a) (b b)) init blanchet 1 
(defskeleton blanchet
  (vars (d data) (s skey) (a b a-0 b-0 akey))
  (defstrand init 2 (d d) (s s) (a a) (b b))
  (defstrand resp 2 (d d) (s s) (a a-0) (b b-0))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (invk b))
  (uniq-orig d s)
  (operation encryption-test (added-strand resp 2) (enc d s) (0 1))
  (label 1)
  (parent 0)
  (unrealized (1 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 2, Parent: 0.

s s (enc d s) (enc (enc s (invk a)) b) ((d d) (s s) (a a) (b b)) init blanchet 2 
(defskeleton blanchet
  (vars (d data) (s skey) (a b akey))
  (defstrand init 2 (d d) (s s) (a a) (b b))
  (deflistener s)
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (invk b))
  (uniq-orig s)
  (operation encryption-test (added-listener s) (enc d s) (0 1))
  (label 2)
  (parent 0)
  (unrealized (1 0))
  (comment "empty cohort"))

Item 3, Parent: 1.

(enc d s) (enc (enc s (invk a)) b) (enc d s) (enc (enc s (invk a)) b) ((d d) (s s) (a a) (b b)) resp ((d d) (s s) (a a) (b b)) init blanchet 3 (realized)
(defskeleton blanchet
  (vars (d data) (s skey) (a b akey))
  (defstrand init 2 (d d) (s s) (a a) (b b))
  (defstrand resp 2 (d d) (s s) (a a) (b b))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (invk b))
  (uniq-orig d s)
  (operation nonce-test (contracted (a-0 a) (b-0 b)) s (1 0)
    (enc (enc s (invk a)) b))
  (label 3)
  (parent 1)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (b b) (s s) (d d))))
  (origs (d (1 1)) (s (0 0))))

Tree 4.

5 4 
(defprotocol blanchet basic
  (defrole init
    (vars (a b akey) (s skey) (d data))
    (trace (send (enc (enc s (invk a)) b)) (recv (enc d s)))
    (uniq-orig s))
  (defrole resp
    (vars (a b akey) (s skey) (d data))
    (trace (recv (enc (enc s (invk a)) b)) (send (enc d s)))
    (uniq-orig d))
  (comment "Blanchet's protocol"))

Item 4, Child: 5.

(enc d s) (enc (enc s (invk a)) b) ((d d) (s s) (a a) (b b)) resp blanchet 4 
(defskeleton blanchet
  (vars (d data) (s skey) (a b akey))
  (defstrand resp 2 (d d) (s s) (a a) (b b))
  (non-orig (invk a) (invk b))
  (uniq-orig d)
  (comment "Analyze from the responder's perspective")
  (label 4)
  (unrealized (0 0))
  (origs (d (0 1)))
  (comment "1 in cohort - 1 not yet seen"))

Item 5, Parent: 4.

(enc (enc s (invk a)) b-0) (enc d s) (enc (enc s (invk a)) b) ((s s) (a a) (b b-0)) init ((d d) (s s) (a a) (b b)) resp blanchet 5 (realized)
(defskeleton blanchet
  (vars (d data) (s skey) (a b b-0 akey))
  (defstrand resp 2 (d d) (s s) (a a) (b b))
  (defstrand init 1 (s s) (a a) (b b-0))
  (precedes ((1 0) (0 0)))
  (non-orig (invk a) (invk b))
  (uniq-orig d s)
  (operation encryption-test (added-strand init 1) (enc s (invk a))
    (0 0))
  (label 5)
  (parent 4)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (b b) (s s) (d d))))
  (origs (s (1 0)) (d (0 1))))

Tree 6.

8 10 9 7 6 
(defprotocol blanchet basic
  (defrole init
    (vars (a b akey) (s skey) (d data))
    (trace (send (enc (enc s (invk a)) b)) (recv (enc d s)))
    (uniq-orig s))
  (defrole resp
    (vars (a b akey) (s skey) (d data))
    (trace (recv (enc (enc s (invk a)) b)) (send (enc d s)))
    (uniq-orig d))
  (comment "Blanchet's protocol"))

Item 6, Children: 7 8.

d d (enc d s) (enc (enc s (invk a)) b) ((d d) (s s) (a a) (b b)) init blanchet 6 
(defskeleton blanchet
  (vars (d data) (s skey) (a b akey))
  (defstrand init 2 (d d) (s s) (a a) (b b))
  (deflistener d)
  (non-orig (invk b))
  (uniq-orig s)
  (comment "From the initiator's perspective, is the secret leaked?")
  (label 6)
  (unrealized (0 1))
  (origs (s (0 0)))
  (comment "2 in cohort - 2 not yet seen"))

Item 7, Parent: 6, Child: 9.

(enc d s) (enc (enc s (invk a-0)) b-0) d d (enc d s) (enc (enc s (invk a)) b) ((d d) (s s) (a a-0) (b b-0)) resp ((d d) (s s) (a a) (b b)) init blanchet 7 
(defskeleton blanchet
  (vars (d data) (s skey) (a b a-0 b-0 akey))
  (defstrand init 2 (d d) (s s) (a a) (b b))
  (deflistener d)
  (defstrand resp 2 (d d) (s s) (a a-0) (b b-0))
  (precedes ((0 0) (2 0)) ((2 1) (0 1)) ((2 1) (1 0)))
  (non-orig (invk b))
  (uniq-orig d s)
  (operation encryption-test (added-strand resp 2) (enc d s) (0 1))
  (label 7)
  (parent 6)
  (unrealized (1 0) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 8, Parent: 6.

s s d d (enc d s) (enc (enc s (invk a)) b) ((d d) (s s) (a a) (b b)) init blanchet 8 
(defskeleton blanchet
  (vars (d data) (s skey) (a b akey))
  (defstrand init 2 (d d) (s s) (a a) (b b))
  (deflistener d)
  (deflistener s)
  (precedes ((0 0) (2 0)) ((2 1) (0 1)))
  (non-orig (invk b))
  (uniq-orig s)
  (operation encryption-test (added-listener s) (enc d s) (0 1))
  (label 8)
  (parent 6)
  (unrealized (2 0))
  (comment "empty cohort"))

Item 9, Parent: 7, Child: 10.

(enc d s) (enc (enc s (invk a)) b) d d (enc d s) (enc (enc s (invk a)) b) ((d d) (s s) (a a) (b b)) resp ((d d) (s s) (a a) (b b)) init blanchet 9 
(defskeleton blanchet
  (vars (d data) (s skey) (a b akey))
  (defstrand init 2 (d d) (s s) (a a) (b b))
  (deflistener d)
  (defstrand resp 2 (d d) (s s) (a a) (b b))
  (precedes ((0 0) (2 0)) ((2 1) (0 1)) ((2 1) (1 0)))
  (non-orig (invk b))
  (uniq-orig d s)
  (operation nonce-test (contracted (a-0 a) (b-0 b)) s (2 0)
    (enc (enc s (invk a)) b))
  (label 9)
  (parent 7)
  (unrealized (1 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 10, Parent: 9.

s s (enc d s) (enc (enc s (invk a)) b) d d (enc d s) (enc (enc s (invk a)) b) ((d d) (s s) (a a) (b b)) resp ((d d) (s s) (a a) (b b)) init blanchet 10
(defskeleton blanchet
  (vars (d data) (s skey) (a b akey))
  (defstrand init 2 (d d) (s s) (a a) (b b))
  (deflistener d)
  (defstrand resp 2 (d d) (s s) (a a) (b b))
  (deflistener s)
  (precedes ((0 0) (2 0)) ((0 0) (3 0)) ((2 1) (0 1)) ((2 1) (1 0))
    ((3 1) (1 0)))
  (non-orig (invk b))
  (uniq-orig d s)
  (operation nonce-test (added-listener s) d (1 0) (enc d s))
  (label 10)
  (parent 9)
  (unrealized (3 0))
  (comment "empty cohort"))

Tree 11.

13 12 11 
(defprotocol blanchet basic
  (defrole init
    (vars (a b akey) (s skey) (d data))
    (trace (send (enc (enc s (invk a)) b)) (recv (enc d s)))
    (uniq-orig s))
  (defrole resp
    (vars (a b akey) (s skey) (d data))
    (trace (recv (enc (enc s (invk a)) b)) (send (enc d s)))
    (uniq-orig d))
  (comment "Blanchet's protocol"))

Item 11, Child: 12.

d d (enc d s) (enc (enc s (invk a)) b) ((d d) (s s) (a a) (b b)) resp blanchet 11 
(defskeleton blanchet
  (vars (d data) (s skey) (a b akey))
  (defstrand resp 2 (d d) (s s) (a a) (b b))
  (deflistener d)
  (non-orig (invk a) (invk b))
  (uniq-orig d)
  (comment "From the responders's perspective, is the secret leaked?")
  (label 11)
  (unrealized (0 0) (1 0))
  (preskeleton)
  (comment "Not a skeleton"))

Item 12, Parent: 11, Child: 13.

d d (enc d s) (enc (enc s (invk a)) b) ((d d) (s s) (a a) (b b)) resp blanchet 12 
(defskeleton blanchet
  (vars (d data) (s skey) (a b akey))
  (defstrand resp 2 (d d) (s s) (a a) (b b))
  (deflistener d)
  (precedes ((0 1) (1 0)))
  (non-orig (invk a) (invk b))
  (uniq-orig d)
  (comment "From the responders's perspective, is the secret leaked?")
  (label 12)
  (parent 11)
  (unrealized (0 0))
  (origs (d (0 1)))
  (comment "1 in cohort - 1 not yet seen"))

Item 13, Parent: 12.

(enc (enc s (invk a)) b-0) d d (enc d s) (enc (enc s (invk a)) b) ((s s) (a a) (b b-0)) init ((d d) (s s) (a a) (b b)) resp blanchet 13 (realized) 
(defskeleton blanchet
  (vars (d data) (s skey) (a b b-0 akey))
  (defstrand resp 2 (d d) (s s) (a a) (b b))
  (deflistener d)
  (defstrand init 1 (s s) (a a) (b b-0))
  (precedes ((0 1) (1 0)) ((2 0) (0 0)))
  (non-orig (invk a) (invk b))
  (uniq-orig d s)
  (operation encryption-test (added-strand init 1) (enc s (invk a))
    (0 0))
  (label 13)
  (parent 12)
  (unrealized)
  (shape)
  (maps ((0 1) ((a a) (b b) (s s) (d d))))
  (origs (s (2 0)) (d (0 1))))

Tree 14.

16 17 15 14 
(defprotocol blanchet-corrected basic
  (defrole init
    (vars (a b akey) (s skey) (d data))
    (trace (send (enc (enc s b (invk a)) b)) (recv (enc d s)))
    (uniq-orig s))
  (defrole resp
    (vars (a b akey) (s skey) (d data))
    (trace (recv (enc (enc s b (invk a)) b)) (send (enc d s)))
    (uniq-orig d))
  (comment "Corrected Blanchet's protocol"))

Item 14, Children: 15 16.

(enc d s) (enc (enc s b (invk a)) b) ((d d) (s s) (a a) (b b)) init blanchet-corrected 14
(defskeleton blanchet-corrected
  (vars (d data) (s skey) (a b akey))
  (defstrand init 2 (d d) (s s) (a a) (b b))
  (non-orig (invk b))
  (uniq-orig s)
  (comment "Analyze from the initiator's perspective")
  (label 14)
  (unrealized (0 1))
  (origs (s (0 0)))
  (comment "2 in cohort - 2 not yet seen"))

Item 15, Parent: 14, Child: 17.

(enc d s) (enc (enc s b-0 (invk a-0)) b-0) (enc d s) (enc (enc s b (invk a)) b) ((d d) (s s) (a a-0) (b b-0)) resp ((d d) (s s) (a a) (b b)) init blanchet-corrected 15
(defskeleton blanchet-corrected
  (vars (d data) (s skey) (a b a-0 b-0 akey))
  (defstrand init 2 (d d) (s s) (a a) (b b))
  (defstrand resp 2 (d d) (s s) (a a-0) (b b-0))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (invk b))
  (uniq-orig d s)
  (operation encryption-test (added-strand resp 2) (enc d s) (0 1))
  (label 15)
  (parent 14)
  (unrealized (1 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 16, Parent: 14.

s s (enc d s) (enc (enc s b (invk a)) b) ((d d) (s s) (a a) (b b)) init blanchet-corrected 16
(defskeleton blanchet-corrected
  (vars (d data) (s skey) (a b akey))
  (defstrand init 2 (d d) (s s) (a a) (b b))
  (deflistener s)
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (invk b))
  (uniq-orig s)
  (operation encryption-test (added-listener s) (enc d s) (0 1))
  (label 16)
  (parent 14)
  (unrealized (1 0))
  (comment "empty cohort"))

Item 17, Parent: 15.

(enc d s) (enc (enc s b (invk a)) b) (enc d s) (enc (enc s b (invk a)) b) ((d d) (s s) (a a) (b b)) resp ((d d) (s s) (a a) (b b)) init blanchet-corrected 17 (realized) 
(defskeleton blanchet-corrected
  (vars (d data) (s skey) (a b akey))
  (defstrand init 2 (d d) (s s) (a a) (b b))
  (defstrand resp 2 (d d) (s s) (a a) (b b))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (invk b))
  (uniq-orig d s)
  (operation nonce-test (contracted (a-0 a) (b-0 b)) s (1 0)
    (enc (enc s b (invk a)) b))
  (label 17)
  (parent 15)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (b b) (s s) (d d))))
  (origs (d (1 1)) (s (0 0))))

Tree 18.

20 22 21 19 18 
(defprotocol blanchet-corrected basic
  (defrole init
    (vars (a b akey) (s skey) (d data))
    (trace (send (enc (enc s b (invk a)) b)) (recv (enc d s)))
    (uniq-orig s))
  (defrole resp
    (vars (a b akey) (s skey) (d data))
    (trace (recv (enc (enc s b (invk a)) b)) (send (enc d s)))
    (uniq-orig d))
  (comment "Corrected Blanchet's protocol"))

Item 18, Children: 19 20.

d d (enc d s) (enc (enc s b (invk a)) b) ((d d) (s s) (a a) (b b)) init blanchet-corrected 18
(defskeleton blanchet-corrected
  (vars (d data) (s skey) (a b akey))
  (defstrand init 2 (d d) (s s) (a a) (b b))
  (deflistener d)
  (non-orig (invk b))
  (uniq-orig s)
  (comment "From the initiator's perspective, is the secret leaked?")
  (label 18)
  (unrealized (0 1))
  (origs (s (0 0)))
  (comment "2 in cohort - 2 not yet seen"))

Item 19, Parent: 18, Child: 21.

(enc d s) (enc (enc s b-0 (invk a-0)) b-0) d d (enc d s) (enc (enc s b (invk a)) b) ((d d) (s s) (a a-0) (b b-0)) resp ((d d) (s s) (a a) (b b)) init blanchet-corrected 19
(defskeleton blanchet-corrected
  (vars (d data) (s skey) (a b a-0 b-0 akey))
  (defstrand init 2 (d d) (s s) (a a) (b b))
  (deflistener d)
  (defstrand resp 2 (d d) (s s) (a a-0) (b b-0))
  (precedes ((0 0) (2 0)) ((2 1) (0 1)) ((2 1) (1 0)))
  (non-orig (invk b))
  (uniq-orig d s)
  (operation encryption-test (added-strand resp 2) (enc d s) (0 1))
  (label 19)
  (parent 18)
  (unrealized (1 0) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 20, Parent: 18.

s s d d (enc d s) (enc (enc s b (invk a)) b) ((d d) (s s) (a a) (b b)) init blanchet-corrected 20
(defskeleton blanchet-corrected
  (vars (d data) (s skey) (a b akey))
  (defstrand init 2 (d d) (s s) (a a) (b b))
  (deflistener d)
  (deflistener s)
  (precedes ((0 0) (2 0)) ((2 1) (0 1)))
  (non-orig (invk b))
  (uniq-orig s)
  (operation encryption-test (added-listener s) (enc d s) (0 1))
  (label 20)
  (parent 18)
  (unrealized (2 0))
  (comment "empty cohort"))

Item 21, Parent: 19, Child: 22.

(enc d s) (enc (enc s b (invk a)) b) d d (enc d s) (enc (enc s b (invk a)) b) ((d d) (s s) (a a) (b b)) resp ((d d) (s s) (a a) (b b)) init blanchet-corrected 21
(defskeleton blanchet-corrected
  (vars (d data) (s skey) (a b akey))
  (defstrand init 2 (d d) (s s) (a a) (b b))
  (deflistener d)
  (defstrand resp 2 (d d) (s s) (a a) (b b))
  (precedes ((0 0) (2 0)) ((2 1) (0 1)) ((2 1) (1 0)))
  (non-orig (invk b))
  (uniq-orig d s)
  (operation nonce-test (contracted (a-0 a) (b-0 b)) s (2 0)
    (enc (enc s b (invk a)) b))
  (label 21)
  (parent 19)
  (unrealized (1 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 22, Parent: 21.

s s (enc d s) (enc (enc s b (invk a)) b) d d (enc d s) (enc (enc s b (invk a)) b) ((d d) (s s) (a a) (b b)) resp ((d d) (s s) (a a) (b b)) init blanchet-corrected 22
(defskeleton blanchet-corrected
  (vars (d data) (s skey) (a b akey))
  (defstrand init 2 (d d) (s s) (a a) (b b))
  (deflistener d)
  (defstrand resp 2 (d d) (s s) (a a) (b b))
  (deflistener s)
  (precedes ((0 0) (2 0)) ((0 0) (3 0)) ((2 1) (0 1)) ((2 1) (1 0))
    ((3 1) (1 0)))
  (non-orig (invk b))
  (uniq-orig d s)
  (operation nonce-test (added-listener s) d (1 0) (enc d s))
  (label 22)
  (parent 21)
  (unrealized (3 0))
  (comment "empty cohort"))

Tree 23.

24 23 
(defprotocol blanchet-corrected basic
  (defrole init
    (vars (a b akey) (s skey) (d data))
    (trace (send (enc (enc s b (invk a)) b)) (recv (enc d s)))
    (uniq-orig s))
  (defrole resp
    (vars (a b akey) (s skey) (d data))
    (trace (recv (enc (enc s b (invk a)) b)) (send (enc d s)))
    (uniq-orig d))
  (comment "Corrected Blanchet's protocol"))

Item 23, Child: 24.

(enc d s) (enc (enc s b (invk a)) b) ((d d) (s s) (a a) (b b)) resp blanchet-corrected 23
(defskeleton blanchet-corrected
  (vars (d data) (s skey) (a b akey))
  (defstrand resp 2 (d d) (s s) (a a) (b b))
  (non-orig (invk a) (invk b))
  (uniq-orig d)
  (comment "Analyze from the responder's perspective")
  (label 23)
  (unrealized (0 0))
  (origs (d (0 1)))
  (comment "1 in cohort - 1 not yet seen"))

Item 24, Parent: 23.

(enc (enc s b (invk a)) b) (enc d s) (enc (enc s b (invk a)) b) ((s s) (a a) (b b)) init ((d d) (s s) (a a) (b b)) resp blanchet-corrected 24 (realized) 
(defskeleton blanchet-corrected
  (vars (d data) (s skey) (a b akey))
  (defstrand resp 2 (d d) (s s) (a a) (b b))
  (defstrand init 1 (s s) (a a) (b b))
  (precedes ((1 0) (0 0)))
  (non-orig (invk a) (invk b))
  (uniq-orig d s)
  (operation encryption-test (added-strand init 1) (enc s b (invk a))
    (0 0))
  (label 24)
  (parent 23)
  (unrealized)
  (shape)
  (maps ((0) ((a a) (b b) (s s) (d d))))
  (origs (s (1 0)) (d (0 1))))

Tree 25.

28 27 26 25 
(defprotocol blanchet-corrected basic
  (defrole init
    (vars (a b akey) (s skey) (d data))
    (trace (send (enc (enc s b (invk a)) b)) (recv (enc d s)))
    (uniq-orig s))
  (defrole resp
    (vars (a b akey) (s skey) (d data))
    (trace (recv (enc (enc s b (invk a)) b)) (send (enc d s)))
    (uniq-orig d))
  (comment "Corrected Blanchet's protocol"))

Item 25, Child: 26.

d d (enc d s) (enc (enc s b (invk a)) b) ((d d) (s s) (a a) (b b)) resp blanchet-corrected 25
(defskeleton blanchet-corrected
  (vars (d data) (s skey) (a b akey))
  (defstrand resp 2 (d d) (s s) (a a) (b b))
  (deflistener d)
  (non-orig (invk a) (invk b))
  (uniq-orig d)
  (comment "From the responders's perspective, is the secret leaked?")
  (label 25)
  (unrealized (0 0) (1 0))
  (preskeleton)
  (comment "Not a skeleton"))

Item 26, Parent: 25, Child: 27.

d d (enc d s) (enc (enc s b (invk a)) b) ((d d) (s s) (a a) (b b)) resp blanchet-corrected 26
(defskeleton blanchet-corrected
  (vars (d data) (s skey) (a b akey))
  (defstrand resp 2 (d d) (s s) (a a) (b b))
  (deflistener d)
  (precedes ((0 1) (1 0)))
  (non-orig (invk a) (invk b))
  (uniq-orig d)
  (comment "From the responders's perspective, is the secret leaked?")
  (label 26)
  (parent 25)
  (unrealized (0 0))
  (origs (d (0 1)))
  (comment "1 in cohort - 1 not yet seen"))

Item 27, Parent: 26, Child: 28.

(enc (enc s b (invk a)) b) d d (enc d s) (enc (enc s b (invk a)) b) ((s s) (a a) (b b)) init ((d d) (s s) (a a) (b b)) resp blanchet-corrected 27
(defskeleton blanchet-corrected
  (vars (d data) (s skey) (a b akey))
  (defstrand resp 2 (d d) (s s) (a a) (b b))
  (deflistener d)
  (defstrand init 1 (s s) (a a) (b b))
  (precedes ((0 1) (1 0)) ((2 0) (0 0)))
  (non-orig (invk a) (invk b))
  (uniq-orig d s)
  (operation encryption-test (added-strand init 1) (enc s b (invk a))
    (0 0))
  (label 27)
  (parent 26)
  (unrealized (1 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 28, Parent: 27.

s s (enc (enc s b (invk a)) b) d d (enc d s) (enc (enc s b (invk a)) b) ((s s) (a a) (b b)) init ((d d) (s s) (a a) (b b)) resp blanchet-corrected 28
(defskeleton blanchet-corrected
  (vars (d data) (s skey) (a b akey))
  (defstrand resp 2 (d d) (s s) (a a) (b b))
  (deflistener d)
  (defstrand init 1 (s s) (a a) (b b))
  (deflistener s)
  (precedes ((0 1) (1 0)) ((2 0) (0 0)) ((2 0) (3 0)) ((3 1) (1 0)))
  (non-orig (invk a) (invk b))
  (uniq-orig d s)
  (operation nonce-test (added-listener s) d (1 0) (enc d s))
  (label 28)
  (parent 27)
  (unrealized (3 0))
  (comment "empty cohort"))