cpsa 3.6.6 → 3.6.7
raw patch · 8 files changed
+608/−68 lines, 8 files
Files
- ChangeLog +16/−0
- Makefile +5/−18
- README.txt +4/−2
- cpsa.cabal +44/−48
- doc/examples/Makefile +11/−0
- doc/examples/bltk_test.scm +74/−0
- doc/examples/rules.scm +65/−0
- doc/examples/rules.xhtml +389/−0
ChangeLog view
@@ -1,3 +1,19 @@+2021-04-27 John D. Ramsdell <ramsdell@mitre.org>++ * cpsa.cabal (Version): Tagged as 3.6.7++2021-04-27 Joshua D. Guttman <guttman@mitre.org>++ * cpsa.cabal: clarified package description (deorigination)++2021-04-14 John D. Ramsdell <ramsdell@mitre.org>++ * Makefile: Vastly simplified.++2020-10-27 John D. Ramsdell <ramsdell@mitre.org>++ * cpsa.cabal (Data-Files): Added missing examples to Data-files.+ 2020-05-21 John D. Ramsdell <ramsdell@mitre.org> * cpsa.cabal (Version): Tagged as 3.6.6
Makefile view
@@ -1,28 +1,15 @@ # Haskell/Cabal Makefile # Requires GNU Make-# The all target creates a default configuration if need be. -PACKAGE := $(wildcard *.cabal)-CONFIG = configured+TOOL = cabal -all: $(CONFIG)- cabal build+all:+ $(TOOL) build Makefile: @echo make $@ -$(PACKAGE):- @echo make $@--$(CONFIG): $(PACKAGE)- cabal configure- touch $(CONFIG)--clean:- -rm $(CONFIG)- cabal clean- %: force- cabal $@+ $(TOOL) $@ -.PHONY: all clean force+.PHONY: all force
README.txt view
@@ -8,9 +8,11 @@ CPSA attempts to enumerate all essentially different executions possible for a cryptographic protocol. We call them the shapes of the-protocol. Naturally occurring protocols have only finitely many,+protocol. Many naturally occurring protocols have only finitely many, indeed very few shapes. Authentication and secrecy properties are-easy to determine from them, as are attacks and anomalies.+easy to determine from them, as are attacks and anomalies, and an+auxiliary tool reads off strongest authentication and secrecy goals+from the shapes. For each input problem, the CPSA program is given some initial behavior, and it discovers what shapes are compatible with it.
cpsa.cabal view
@@ -1,5 +1,5 @@ Name: cpsa-Version: 3.6.6+Version: 3.6.7 Maintainer: mliskov@mitre.org Cabal-Version: >= 1.10 License: BSD3@@ -7,39 +7,34 @@ Synopsis: Symbolic cryptographic protocol analyzer Description: The Cryptographic Protocol Shapes Analyzer (CPSA) attempts to- enumerate all essentially different executions possibe for a+ enumerate all essentially different executions possible for a cryptographic protocol. We call them the shapes of the protocol.- Naturally occurring protocols have only finitely many, indeed very- few shapes. Authentication and secrecy properties are easy to- determine from them, as are attacks and anomalies.+ Many naturally occurring protocols have only finitely many, indeed+ very few shapes. Authentication and secrecy properties are easy to+ determine from them, as are attacks and anomalies, and an auxiliary+ tool reads off strongest authentication and secrecy goals from the+ shapes. . For each input problem, the CPSA program is given some initial behavior, and it discovers what shapes are compatible with it. Normally, the initial behavior is from the point of view of one participant. The analysis reveals what the other participants must- have done, given the participant's view. The search is based on a- high-level algorithm that was claimed to be complete, i.e. every- shape can in fact be found in a finite number of steps. Further- theoretical work showed classes of executions that are not found by- the algorithm, however it also showed that every omitted execution- requires an unnatural interpretation of a protocol's roles. Hence- the algorithm is complete relative to natural role semantics.- .- The package contains a set of programs used to perform and display- the analysis. A standards complient browser, such as Firefox,- Safari, or Chrome, is required to display the results. Program- documentation is in the doc directory in the source distribution,- and installed in the package's data directory. You can locate the- package's data directory by typing "cpsa --help" to a command- prompt. New users should start learning to use the tool from the- manual, found at "cpsamanual.pdf" in the data directory. Examples- referenced in the manual can be found in the data directory as well.- It is suggested that users make an examples directory and copy- "*.scm *.xhtml" to their local examples directory, both so that- they may be modified and for ease of access.+ have done, given the participant's view. The search is complete,+ i.e. we proved every shape can be found in a finite number of steps,+ relative to a procedural semantics of protocol roles. This version+ of CPSA has the ability to analyze Diffie-Hellman protocols. .- Serious Windows users should install MSYS so as to allow the use of- make and script execution.+ The package contains a set of programs used to perform the analysis+ and display it in a browser. Program documentation is in the doc+ directory in the source distribution, and installed in the package's+ data directory. You can locate the package's data directory by+ typing "cpsa --help" to a command prompt. New users should start+ learning to use the tool from the manual, found at "cpsamanual.pdf"+ in the data directory. Examples referenced in the manual can be+ found in the data directory as well. It is suggested that users+ make an examples directory and copy "*.scm *.xhtml" to their local+ examples directory, both so that they may be modified and for ease+ of access. . The theory and algorithm used by CPSA was developed with the help of Joshua D. Guttman, John D. Ramsdell, Jon C. Herzog, Shaddin@@ -49,30 +44,31 @@ Category: Cryptography Build-Type: Simple Data-Files:- Make.hs cpsa.mk cpsamanual.pdf examples/blanchet.scm- examples/blanchet.xhtml examples/bltk_or.scm examples/bltk_or.xhtml- examples/envelope.scm examples/envelope.xhtml examples/ffgg.scm- examples/ffgg.xhtml examples/fnof_test.scm examples/fnof_test.xhtml- examples/fnof_yahalom.scm examples/fnof_yahalom.xhtml- examples/goals.scm examples/goals.xhtml examples/kerb.scm+ Make.hs cpsa.mk cpsamanual.pdf init/Makefile init/template.lisp+ examples/IKE_variants.tar.gz examples/IKE_variants_nobase.tar.gz+ examples/Makefile examples/blanchet.scm examples/blanchet.xhtml+ examples/bltk_or.scm examples/bltk_or.xhtml examples/bltk_test.scm+ examples/dh_mim.scm examples/dh_mim.xhtml examples/envelope.scm+ examples/envelope.xhtml examples/eq_test.scm examples/eq_test.xhtml+ examples/ffgg.scm examples/ffgg.xhtml+ examples/fluffy_draft03_fixing_gske.scm+ examples/fluffy_draft03_gske.scm+ examples/fluffy_draft03_improving_pske.scm+ examples/fluffy_draft03_pske.scm examples/fnof_test.scm+ examples/fnof_test.xhtml examples/fnof_yahalom.scm+ examples/fnof_yahalom.xhtml examples/goals.scm examples/goals.xhtml+ examples/iadh_um.scm examples/iadh_um.xhtml examples/kerb.scm examples/kerb.xhtml examples/lt_test.scm examples/lt_test.xhtml examples/neq_test.scm examples/neq_test.xhtml examples/ns.scm examples/ns.xhtml examples/or.scm examples/or.xhtml examples/pkinit.scm examples/pkinit.xhtml examples/plaindh.scm examples/plaindh.xhtml examples/priority_test.scm- examples/priority_test.xhtml examples/station.scm- examples/station.xhtml examples/subsort_test.scm examples/woolam.scm- examples/yahalom.scm examples/yahalom.xhtml- examples/IKE_variants.tar.gz examples/IKE_variants_nobase.tar.gz- examples/iadh_um.scm examples/iadh_um.xhtml- examples/subsort_test.xhtml examples/woolam.xhtml- examples/dh_mim.scm examples/dh_mim.xhtml- examples/fluffy_draft03_fixing_gske.scm- examples/fluffy_draft03_gske.scm- examples/fluffy_draft03_improving_pske.scm- examples/fluffy_draft03_pske.scm examples/eq_test.scm- init/Makefile init/template.lisp- examples/eq_test.xhtml+ examples/priority_test.xhtml examples/rules.scm examples/rules.xhtml+ examples/station.scm examples/station.xhtml+ examples/subsort_test.scm examples/subsort_test.xhtml+ examples/woolam.scm examples/woolam.xhtml examples/yahalom.scm+ examples/yahalom.xhtml+ Data-Dir: doc Extra-Source-Files: Makefile ChangeLog README.txt NEWS mkghci cpsatst setup.bat@@ -118,7 +114,7 @@ tst/role_uniq.scm tst/role_uniq.tst tst/rule-order.scm tst/rule-order.tst tst/trust-anchor.scm tst/trust-anchor.tst tst/blanchet_doorsep.prot tst/blanchet_doorsep.tst- + Source-Repository head Type: git Location: git://github.com/mitre/cpsa.git@@ -178,7 +174,7 @@ CPSA.Lib.Printer CPSA.Lib.Entry CPSA.Lib.Algebra CPSA.Annotations.Formulas CPSA.Annotations.Annotations CPSA.Basic.Algebra CPSA.DiffieHellman.Algebra- + Executable cpsadiff Main-Is: CPSA/Diff/Main.hs Default-Language: Haskell2010
+ doc/examples/Makefile view
@@ -0,0 +1,11 @@+CPSAFLAGS = +RTS -N3 -M512m -RTS++SRCS := $(wildcard *.scm) $(wildcard *.lsp)++include ../cpsa.mk++all: $(SRCS:%.scm=%_shapes.xhtml) $(SRCS:%.scm=%.xhtml) \+ $(SRCS:%.lsp=%_shapes.xhtml) $(SRCS:%.lsp=%.xhtml)++clean:+ -rm *.txt *.xhtml
+ doc/examples/bltk_test.scm view
@@ -0,0 +1,74 @@+(herald "bltk Test File"+ (algebra diffie-hellman)+ (bound 12))++(defprotocol test diffie-hellman+ (defrole r+ (vars (a b name) (n text))+ (trace + (send (enc n (bltk a b)))+ (recv (enc n (bltk b a))))+ (uniq-orig n)))++;; This POV is realized. That demonstrates that (bltk a b) = (bltk b a)+(defskeleton test+ (vars (a b name))+ (defstrand r 2 (a a) (b b))+ (non-orig (bltk a b) (bltk b a)))++;; These next two skeletons show that it is sufficient to declare+;; either (bltk a b) or (bltk b a) to be non.+(defskeleton test+ (vars (a b name) (n text))+ (defstrand r 2 (a a) (b b) (n n))+ (deflistener n)+ (non-orig (bltk a b)))++(defskeleton test+ (vars (a b name) (n text))+ (defstrand r 2 (a a) (b b) (n n))+ (deflistener n)+ (non-orig (bltk b a)))++;; This is the same protocol as above with bltk replaced with ltk+(defprotocol test2 diffie-hellman+ (defrole r+ (vars (a b name) (n text))+ (trace + (send (enc n (ltk a b)))+ (recv (enc n (ltk b a))))+ (uniq-orig n)))++;; The only way to realize this skeleton is to learn that a = b. This+;; is in contrast to the first skeleton above. +(defskeleton test2+ (vars (a b name))+ (defstrand r 2 (a a) (b b))+ (non-orig (ltk a b)))+++;; This protocol demonstrates that the position of the names a and b+;; in (bltk a b) are not enough to determine which principal is+;; inhabiting the role. The first send of each role commits to the+;; identity of itself and its peer. +(defprotocol test3 diffie-hellman+ (defrole recvr+ (vars (a b name) (n text))+ (trace+ (send (cat "i am" a "you are" b))+ (recv (enc n (bltk a b)))))+ (defrole sender+ (vars (a b name) (n text))+ (trace+ (send (cat "i am" b "you are" a))+ (send (enc n (bltk a b))))+ (uniq-orig n)))++;; Since (bltk a b) = (bltk b a) the recvr role may receive the+;; encryption from its inteded peer or from itself. That is, both a+;; and b use the same key when inhabiting the sender role.+(defskeleton test3+ (vars (a b name))+ (defstrand recvr 2 (a a) (b b))+ (non-orig (bltk a b)))+
+ doc/examples/rules.scm view
@@ -0,0 +1,65 @@+(herald "Rules and Facts")++(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"))++;;; With no inequality fact,+;;; a shape should be found where n1 = n2.+(defskeleton neq-test+ (vars)+ (defstrand init 2)+ (comment "This skeleton should have a shape"))++;;; With an inequality fact,+;;; no shape should exist.+(defskeleton neq-test+ (vars (n1 n2 text))+ (defstrand init 2 (n1 n1) (n2 n2))+ (facts (neq n1 n2)) ; assert n1 != n2+ (comment "This skeleton should have no shapes"))++;;;++(herald doorsep (comment "Door Simple Example Protocol"))++(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 (p akey))+ (defstrand door 3 (p p))+ (non-orig (invk p))+ (comment "Analyze from the doors's perspective"))
+ doc/examples/rules.xhtml view
@@ -0,0 +1,389 @@+<?xml version="1.0"?>+<!-- CPSA 3.6.2 -->+<html xmlns="http://www.w3.org/1999/xhtml">+<head>+ <title>Rules and Facts</title>+ <meta http-equiv="content-type" content="application/xhtml+xml; charset=UTF-8" />+ <style>+ svg.diagram { border-width: 1px; border-style: solid }+ </style>+</head>+<body>++<pre>(herald "Rules and Facts")+(comment "CPSA 3.6.2")+(comment "All input read from rules.scm")</pre>++<p id="top">Trees: <a href="#t0">0</a> <a href="#t2">2</a> <a href="#t3">3</a>.</p>++<p id="t0">Tree <a href="#top">0</a>.</p>++<div>+ <svg+ class='diagram' width='129.840pt' height='79.920pt'+ xmlns='http://www.w3.org/2000/svg' version='1.1'+ viewBox='0 0 129.840 79.920' font-size='12.000'>+ <text+ x='89.880' y='26.040'+ style='font-weight: bold; text-anchor: middle; fill: blue;'+ onclick='window.open("#k1", "_self")'>1</text>+ <line+ x1='39.960' y1='39.960' x2='89.880' y2='39.960'+ style='stroke-width: 0.960; stroke: gray;'/>+ <text+ x='39.960' y='26.040' style='text-anchor: middle; fill: black;'+ onclick='window.open("#k0", "_self")'>0</text>+ </svg></div>++<pre>(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"))</pre>++<p id="k0">Item <a href="#t0">0</a>, Child: <a href="#k1">1</a>.</p>++<div>+ <svg+ class='diagram' width='79.920pt' height='229.920pt'+ xmlns='http://www.w3.org/2000/svg' version='1.1'+ viewBox='0 0 79.920 229.920' font-size='12.000'>+ <defs>+ <marker+ id='arrow' orient='auto' markerWidth='5' markerHeight='10' refX='5'+ refY='5'>+ <path+ d='M 0 0 5 5 0 10'+ style='stroke-width: 2; fill: none; stroke: black;'/></marker>+ </defs>+ <line+ x1='39.960' y1='114.960' x2='39.960' y2='189.960'+ style='stroke-width: 0.960; stroke: gray;'/>+ <g><title>n2</title>+ <circle style='fill: red;' cx='39.960' cy='189.960' r='6.000'/></g>+ <g><title>(cat n1 (enc n1 n2 k))</title>+ <circle cx='39.960' cy='114.960' r='6.000'/></g>+ <g><title>((n1 n1) (n2 n2) (k k))</title>+ <text x='39.960' y='77.460' style='text-anchor: middle;'>init</text>+ </g>+ <text+ x='39.960' y='39.960' style='text-anchor: middle;'>neq-test 0</text>+ </svg></div>++<pre>(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"))</pre>++<p id="k1">Item <a href="#t0">1</a>, Parent: <a href="#k0">0</a>.</p>++<div>+ <svg+ class='diagram' width='79.920pt' height='229.920pt'+ xmlns='http://www.w3.org/2000/svg' version='1.1'+ viewBox='0 0 79.920 229.920' font-size='12.000'>+ <defs>+ <marker+ id='arrow' orient='auto' markerWidth='5' markerHeight='10' refX='5'+ refY='5'>+ <path+ d='M 0 0 5 5 0 10'+ style='stroke-width: 2; fill: none; stroke: black;'/></marker>+ </defs>+ <line+ x1='39.960' y1='114.960' x2='39.960' y2='189.960'+ style='stroke-width: 0.960; stroke: gray;'/>+ <g><title>n1</title>+ <circle style='fill: blue;' cx='39.960' cy='189.960' r='6.000'/></g>+ <g><title>(cat n1 (enc n1 n1 k))</title>+ <circle cx='39.960' cy='114.960' r='6.000'/></g>+ <g><title>((n1 n1) (n2 n1) (k k))</title>+ <text x='39.960' y='77.460' style='text-anchor: middle;'>init</text>+ </g>+ <text+ x='39.960' y='39.960'+ style='text-anchor: middle;'>neq-test 1 (realized)</text></svg></div>++<pre>(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))))</pre>++<p id="t2">Tree <a href="#top">2</a>.</p>++<div>+ <svg+ class='diagram' width='79.920pt' height='79.920pt'+ xmlns='http://www.w3.org/2000/svg' version='1.1'+ viewBox='0 0 79.920 79.920' font-size='12.000'>+ <text+ x='39.960' y='26.040' style='text-anchor: middle; fill: red;'+ onclick='window.open("#k2", "_self")'>2</text>+ </svg></div>++<pre>(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"))</pre>++<p id="k2">Item <a href="#t2">2</a>.</p>++<div>+ <svg+ class='diagram' width='79.920pt' height='229.920pt'+ xmlns='http://www.w3.org/2000/svg' version='1.1'+ viewBox='0 0 79.920 229.920' font-size='12.000'>+ <defs>+ <marker+ id='arrow' orient='auto' markerWidth='5' markerHeight='10' refX='5'+ refY='5'>+ <path+ d='M 0 0 5 5 0 10'+ style='stroke-width: 2; fill: none; stroke: black;'/></marker>+ </defs>+ <line+ x1='39.960' y1='114.960' x2='39.960' y2='189.960'+ style='stroke-width: 0.960; stroke: gray;'/>+ <g><title>n2</title>+ <circle style='fill: red;' cx='39.960' cy='189.960' r='6.000'/></g>+ <g><title>(cat n1 (enc n1 n2 k))</title>+ <circle cx='39.960' cy='114.960' r='6.000'/></g>+ <g><title>((n1 n1) (n2 n2) (k k))</title>+ <text x='39.960' y='77.460' style='text-anchor: middle;'>init</text>+ </g>+ <text+ x='39.960' y='39.960' style='text-anchor: middle;'>neq-test 2</text>+ </svg></div>++<pre>(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"))</pre>++<p id="t3">Tree <a href="#top">3</a>.</p>++<div>+ <svg+ class='diagram' width='179.760pt' height='79.920pt'+ xmlns='http://www.w3.org/2000/svg' version='1.1'+ viewBox='0 0 179.760 79.920' font-size='12.000'>+ <text+ x='139.800' y='26.040'+ style='font-weight: bold; text-anchor: middle; fill: blue;'+ onclick='window.open("#k5", "_self")'>5</text>+ <line+ x1='89.880' y1='39.960' x2='139.800' y2='39.960'+ style='stroke-width: 0.960; stroke: gray;'/>+ <text+ x='89.880' y='26.040' style='text-anchor: middle; fill: black;'+ onclick='window.open("#k4", "_self")'>4</text>+ <line+ x1='39.960' y1='39.960' x2='89.880' y2='39.960'+ style='stroke-width: 0.960; stroke: gray;'/>+ <text+ x='39.960' y='26.040' style='text-anchor: middle; fill: black;'+ onclick='window.open("#k3", "_self")'>3</text>+ </svg></div>++<pre>(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"))</pre>++<p id="k3">Item <a href="#t3">3</a>, Child: <a href="#k4">4</a>.</p>++<div>+ <svg+ class='diagram' width='79.920pt' height='304.920pt'+ xmlns='http://www.w3.org/2000/svg' version='1.1'+ viewBox='0 0 79.920 304.920' font-size='12.000'>+ <defs>+ <marker+ id='arrow' orient='auto' markerWidth='5' markerHeight='10' refX='5'+ refY='5'>+ <path+ d='M 0 0 5 5 0 10'+ style='stroke-width: 2; fill: none; stroke: black;'/></marker>+ </defs>+ <line+ x1='39.960' y1='114.960' x2='39.960' y2='264.960'+ style='stroke-width: 0.960; stroke: gray;'/>+ <g><title>t</title>+ <circle style='fill: blue;' cx='39.960' cy='264.960' r='6.000'/></g>+ <g><title>(enc t k)</title>+ <circle cx='39.960' cy='189.960' r='6.000'/></g>+ <g><title>(enc (enc k (invk p)) d)</title>+ <circle style='fill: red;' cx='39.960' cy='114.960' r='6.000'/></g>+ <g><title>((t t) (k k) (d d) (p p))</title>+ <text x='39.960' y='77.460' style='text-anchor: middle;'>door</text>+ </g>+ <text+ x='39.960' y='39.960' style='text-anchor: middle;'>doorsep 3</text>+ </svg></div>++<pre>(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"))</pre>++<p id="k4">Item <a href="#t3">4</a>, Parent: <a href="#k3">3</a>, Child: <a href="#k5">5</a>.</p>++<div>+ <svg+ class='diagram' width='179.880pt' height='304.920pt'+ xmlns='http://www.w3.org/2000/svg' version='1.1'+ viewBox='0 0 179.880 304.920' font-size='12.000'>+ <defs>+ <marker+ id='arrow' orient='auto' markerWidth='5' markerHeight='10' refX='5'+ refY='5'>+ <path+ d='M 0 0 5 5 0 10'+ style='stroke-width: 2; fill: none; stroke: black;'/></marker>+ </defs>+ <line+ x1='139.920' y1='114.960' x2='139.920' y2='114.960'+ style='stroke-width: 0.960; stroke: gray;'/>+ <line+ x1='39.960' y1='114.960' x2='39.960' y2='264.960'+ style='stroke-width: 0.960; stroke: gray;'/>+ <path+ d='M 139.920 114.960 Q 92.940 114.960 45.960 114.960'+ style='stroke-dasharray: 6.000,2.400; stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>+ <g><title>(enc (enc k (invk p)) d-0)</title>+ <circle cx='139.920' cy='114.960' r='6.000'/></g>+ <g><title>t</title>+ <circle style='fill: blue;' cx='39.960' cy='264.960' r='6.000'/></g>+ <g><title>(enc t k)</title>+ <circle cx='39.960' cy='189.960' r='6.000'/></g>+ <g><title>(enc (enc k (invk p)) d)</title>+ <circle style='fill: red;' cx='39.960' cy='114.960' r='6.000'/></g>+ <g><title>((k k) (d d-0) (p p))</title>+ <text+ x='139.920' y='77.460' style='text-anchor: middle;'>person</text>+ </g>+ <g><title>((t t) (k k) (d d) (p p))</title>+ <text x='39.960' y='77.460' style='text-anchor: middle;'>door</text>+ </g>+ <text+ x='89.940' y='39.960' style='text-anchor: middle;'>doorsep 4</text>+ </svg></div>++<pre>(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"))</pre>++<p id="k5">Item <a href="#t3">5</a>, Parent: <a href="#k4">4</a>.</p>++<div>+ <svg+ class='diagram' width='179.880pt' height='304.920pt'+ xmlns='http://www.w3.org/2000/svg' version='1.1'+ viewBox='0 0 179.880 304.920' font-size='12.000'>+ <defs>+ <marker+ id='arrow' orient='auto' markerWidth='5' markerHeight='10' refX='5'+ refY='5'>+ <path+ d='M 0 0 5 5 0 10'+ style='stroke-width: 2; fill: none; stroke: black;'/></marker>+ </defs>+ <line+ x1='139.920' y1='114.960' x2='139.920' y2='114.960'+ style='stroke-width: 0.960; stroke: gray;'/>+ <line+ x1='39.960' y1='114.960' x2='39.960' y2='264.960'+ style='stroke-width: 0.960; stroke: gray;'/>+ <path+ d='M 139.920 114.960 Q 92.940 114.960 45.960 114.960'+ style='stroke-width: 0.960; stroke: black; marker-end: url(#arrow); fill: none;'/>+ <g><title>(enc (enc k (invk p)) d)</title>+ <circle cx='139.920' cy='114.960' r='6.000'/></g>+ <g><title>t</title>+ <circle style='fill: blue;' cx='39.960' cy='264.960' r='6.000'/></g>+ <g><title>(enc t k)</title>+ <circle cx='39.960' cy='189.960' r='6.000'/></g>+ <g><title>(enc (enc k (invk p)) d)</title>+ <circle style='fill: blue;' cx='39.960' cy='114.960' r='6.000'/></g>+ <g><title>((k k) (d d) (p p))</title>+ <text+ x='139.920' y='77.460' style='text-anchor: middle;'>person</text>+ </g>+ <g><title>((t t) (k k) (d d) (p p))</title>+ <text x='39.960' y='77.460' style='text-anchor: middle;'>door</text>+ </g>+ <text+ x='89.940' y='39.960'+ style='text-anchor: middle;'>doorsep 5 (realized)</text></svg></div>++<pre>(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))</pre>++</body>+</html>