diff --git a/ChangeLog b/ChangeLog --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,47 @@ +2011-05-18 John D. Ramsdell + + * cpsa.cabal (Version): Tagged as version 2.2.4. + +2011-05-16 John D. Ramsdell + + * src/prover9.pl: Added a translator from cpsalogic output to + prover9 syntax. + +2011-05-13 John D. Ramsdell + + * src/CPSA/Lib/Reduction.hs (parMap): The option to compile CPSA + without using the parallel runtime has been removed. The parallel + library comes with Haskell Platform, so it is always available + these days. + + * cpsa.cabal (Executable cpsa): Added the GHC option -rtsopts when + the compiler is version 7.0.0 or greater. In 7.0.0, needed + runtime option have been disabled for security reasons by default. + +2011-05-12 John D. Ramsdell + + * src/CPSA/Logic/Logic.hs (precForm): Shortened the predicate's + name from precedes to prec. + + * src/CPSA/Logic/Logic.hs (origForm): Added the orig predicate + which asserts the node of origination for each uniquely originating + atom. + + * src/CPSA/Lib/Reduction.hs (origs): Added nodes of origination + of uniquely originating atoms for POV and shapes for cpsalogic. + + * src/CPSA/Lib/Reduction.hs (commentPreskel): Rewrote this + function so as to make its much more understandable. + +2011-05-09 John D. Ramsdell + + * doc/cpsaspec.tex: Added the orig predicate to shape analysis + sentences so that eliminate a counterexample to Conjecture B.1. + The addition of this predicate in necessary because with out it, + there is no way to ensure that skeletons that model a description + of a skeleton preserve nodes of origination of uniquely + originating atoms. + 2011-05-04 John D. Ramsdell * cpsa.cabal (Version): Tagged as version 2.2.3. diff --git a/NEWS b/NEWS --- a/NEWS +++ b/NEWS @@ -1,5 +1,20 @@ CPSA NEWS -- history of user-visible changes. +* Changes in version 2.2.4 + +** GHC link time option added + For GHC version 7.0.0 or greater, some runtime options used by CPSA + were turned off by default due to security concerns irrelevant to + CPSA. The runtime options are now enabled. + +** Shape Analysis Sentences + The orig predicate was added to a description of a skeleton. + Without it, the important property of a shape analysis sentence + described in Theorem B.1 of The CPSA Specification does not hold. + + Also, the Prolog program src/prover9.pl was added. It translates + cpsalogic output into prover9 syntax. + * Changes in version 2.2.3 ** New program added diff --git a/README b/README --- a/README +++ b/README @@ -65,14 +65,10 @@ PARALLELISM -By default, CPSA is built so it can make use of multiple processors. -To make use of more than one processor, start CPSA with a runtime flag -that specifies the number of processors to be used, such as "+RTS -N4 +CPSA is built so it can make use of multiple processors. To make use +of more than one processor, start CPSA with a runtime flag that +specifies the number of processors to be used, such as "+RTS -N4 -RTS". The GHC documentation describes the -N option in detail. - -If the Control.Parallel library is not installed, configure CPSA using: - -$ runghc Setup.hs configure -f-par DOCUMENTATION diff --git a/cpsa.cabal b/cpsa.cabal --- a/cpsa.cabal +++ b/cpsa.cabal @@ -1,5 +1,5 @@ Name: cpsa -Version: 2.2.3 +Version: 2.2.4 Maintainer: ramsdell@mitre.org Cabal-Version: >= 1.6 License: BSD3 @@ -53,42 +53,41 @@ doc/cpsaoverview.tex doc/cpsadiagrams.mp doc/strands.mp doc/cmstrands.mp doc/carriers.mp doc/termtree.mp doc/cpsa.bib doc/SDAG.lhs doc/cpsatheory.pdf doc/cpsaspec.pdf doc/cpsadesign.pdf - src/index.html src/cpsacgi src/cpsacgi.py src/cpsa2svg - src/cpsa.el src/httpd_allow_execmem.te src/cpsaops.scm src/preskel - src/cpsa.pl src/pp.pl src/sexpr.pl src/zoom.js src/js2hs src/ghcmemlimit - build.xml src/cpsaextras/Main.scala src/cpsaextras/Pretty.scala - src/cpsaextras/Printer.scala src/cpsaextras/SExpr.scala - tst/README tst/Makefile - tst/Make.hs tst/checktst tst/cpsagraphall tst/cpsashapesall - tst/blanchet.scm tst/blanchet.tst tst/completeness-test.scm - tst/completeness-test.tst tst/crushing.tst tst/crushing.tst - tst/dass.lisp tst/dass-mod.lisp tst/dass_simple.scm - tst/dass_simple.tst tst/denning-sacco.scm tst/denning-sacco.tst - tst/deorig_contract.scm tst/deorig_contract.tst tst/dhke.scm - tst/dhke.tst tst/deorig_simple.scm tst/deorig_simple.tst - tst/ds-short.lisp tst/dy.lsp tst/dy.tst tst/encsig.scm - tst/encsig.tst tst/epmo_acctnum.scm tst/epmo_acctnum.tst - tst/epmo.scm tst/epmo.tst tst/ffgg.scm tst/ffgg.tst - tst/fragile_pruning.scm tst/fragile_pruning.tst tst/isoreject.scm - tst/isoreject.tst tst/kelly1.scm tst/kelly1.tst tst/kelly64.lisp - tst/kerb5.lisp tst/kerberos.scm tst/kerberos.tst - tst/missing_contraction.scm tst/missing_contraction.tst - tst/neuman-stubblebine-alt.lisp tst/neuman-stubblebine-reauth.lisp - tst/neuman-stubblebine-reauth.lsp tst/neuman-stubblebine-reauth.tst - tst/neuman-stubblebine.scm tst/neuman-stubblebine.tst - tst/no_contraction.scm tst/no_contraction.tst tst/nonaug-prune.scm - tst/nonaug-prune.tst tst/non_transforming.scm - tst/non_transforming.tst tst/nsl3.scm tst/nsl3.tst tst/nsl4cm1.lsp - tst/nsl4cm1.tst tst/nsl4.lisp tst/nsl4resp2.lisp tst/nsl5i.lisp - tst/nsl5.lisp tst/nslsk.scm tst/nslsk.tst tst/ns.scm tst/ns.tst - tst/or.scm tst/or.tst tst/pca.scm tst/pca.tst tst/pruning1.scm - tst/pruning1.tst tst/sigenc.scm tst/sigenc.tst - tst/sorted_epmo_acctnum.scm tst/sorted_epmo_acctnum.tst - tst/targetterms2.scm tst/targetterms2.tst tst/targetterms6.scm - tst/targetterms6.tst tst/targetterms8.scm - tst/targetterms8.tst tst/tnsl5.lisp tst/uncarried_keys.scm - tst/uncarried_keys.tst tst/uo.scm tst/uo.tst tst/updatetst - tst/weird.scm tst/weird.tst tst/wide-mouth-frog.lsp + src/index.html src/cpsacgi src/cpsacgi.py src/cpsa2svg src/cpsa.el + src/httpd_allow_execmem.te src/cpsaops.scm src/preskel src/cpsa.pl + src/pp.pl src/sexpr.pl src/prover9.pl src/zoom.js src/js2hs + src/ghcmemlimit build.xml src/cpsaextras/Main.scala + src/cpsaextras/Pretty.scala src/cpsaextras/Printer.scala + src/cpsaextras/SExpr.scala tst/README tst/Makefile tst/Make.hs + tst/checktst tst/cpsagraphall tst/cpsashapesall tst/blanchet.scm + tst/blanchet.tst tst/completeness-test.scm tst/completeness-test.tst + tst/crushing.tst tst/crushing.tst tst/dass.lisp tst/dass-mod.lisp + tst/dass_simple.scm tst/dass_simple.tst tst/denning-sacco.scm + tst/denning-sacco.tst tst/deorig_contract.scm + tst/deorig_contract.tst tst/dhke.scm tst/dhke.tst + tst/deorig_simple.scm tst/deorig_simple.tst tst/ds-short.lisp + tst/dy.lsp tst/dy.tst tst/encsig.scm tst/encsig.tst + tst/epmo_acctnum.scm tst/epmo_acctnum.tst tst/epmo.scm tst/epmo.tst + tst/ffgg.scm tst/ffgg.tst tst/fragile_pruning.scm + tst/fragile_pruning.tst tst/isoreject.scm tst/isoreject.tst + tst/kelly1.scm tst/kelly1.tst tst/kelly64.lisp tst/kerb5.lisp + tst/kerberos.scm tst/kerberos.tst tst/missing_contraction.scm + tst/missing_contraction.tst tst/neuman-stubblebine-alt.lisp + tst/neuman-stubblebine-reauth.lisp tst/neuman-stubblebine-reauth.lsp + tst/neuman-stubblebine-reauth.tst tst/neuman-stubblebine.scm + tst/neuman-stubblebine.tst tst/no_contraction.scm + tst/no_contraction.tst tst/nonaug-prune.scm tst/nonaug-prune.tst + tst/non_transforming.scm tst/non_transforming.tst tst/nsl3.scm + tst/nsl3.tst tst/nsl4cm1.lsp tst/nsl4cm1.tst tst/nsl4.lisp + tst/nsl4resp2.lisp tst/nsl5i.lisp tst/nsl5.lisp tst/nslsk.scm + tst/nslsk.tst tst/ns.scm tst/ns.tst tst/or.scm tst/or.tst + tst/pca.scm tst/pca.tst tst/pruning1.scm tst/pruning1.tst + tst/sigenc.scm tst/sigenc.tst tst/sorted_epmo_acctnum.scm + tst/sorted_epmo_acctnum.tst tst/targetterms2.scm + tst/targetterms2.tst tst/targetterms6.scm tst/targetterms6.tst + tst/targetterms8.scm tst/targetterms8.tst tst/tnsl5.lisp + tst/uncarried_keys.scm tst/uncarried_keys.tst tst/uo.scm tst/uo.tst + tst/updatetst tst/weird.scm tst/weird.tst tst/wide-mouth-frog.lsp tst/wide-mouth-frog.tst tst/wonthull2.scm tst/wonthull2.tst tst/wonthull3.scm tst/wonthull3.tst tst/wonthull.scm tst/wonthull.tst tst/woolam.scm tst/woolam.tst tst/yahalom-6.3.6.scm @@ -98,21 +97,15 @@ tst/epmo-key-hash.scm tst/epmo-key-hash.tst tst/wang.lisp tst/pkinit.scm tst/pkinit.tst --- Disable with -f-par option during configuration. - -Flag Par - Description: Enable use of the parallel construct par - Default: True - -- Algebra implementations must import CPSA.Lib.CPSA. -- Tools may additionally import CPSA.Lib.Entry. -- No other modules in CPSA.Lib should be imported by applications. Executable cpsa Main-Is: CPSA/Lib/Main.hs - Build-Depends: base >= 3 && < 5, containers + Build-Depends: base >= 3 && < 5, containers, parallel GHC-Options: - -Wall -fno-warn-name-shadowing -fwarn-unused-imports + -Wall -fno-warn-name-shadowing -fwarn-unused-imports -threaded Hs-Source-Dirs: src Other-Modules: Paths_cpsa CPSA.Lib.Vector CPSA.Lib.Utilities CPSA.Lib.Pretty @@ -121,10 +114,8 @@ CPSA.Lib.Displayer CPSA.Lib.Cohort CPSA.Lib.Expand CPSA.Lib.CPSA CPSA.Lib.Reduction CPSA.Basic.Algebra CPSA.DiffieHellman.Algebra CPSA.DiffieHellman.IntLinEq CPSA.SimpleDiffieHellman.Algebra - if flag(par) - Cpp-Options: -DHAVE_PAR - GHC-Options: -threaded - Build-Depends: parallel + if impl(ghc >= 7.0.0) + GHC-Options: -rtsopts Executable cpsagraph Main-Is: CPSA/Graph/Main.hs diff --git a/doc/Make.hs b/doc/Make.hs --- a/doc/Make.hs +++ b/doc/Make.hs @@ -1,6 +1,6 @@ -- A simple, CPSA specific make system -module Make (cpsa, shapes, annos, cleanse, get, set, +module Make (cpsa, shapes, logic, annos, params, cleanse, get, set, build, clean, roots) where {- Place a copy of this source file in the directory used to store @@ -27,12 +27,21 @@ If successful, the shapes are in the file prob_shapes.xhtml. +*Make> logic "prob" + +If successful, the shape analysis sentences are in the file +prob_logic.text. + When the protocol is annotated with rely-guarantee formulas, type: *Make> annos "prob" If successful, the annotated shapes are in the file prob_annotations.xhtml. +*Make> params "prob" + +If successful, roles with parameter descriptions are in prob_parameters.txt. + To remove the files generated from source files, type: *Make> cleanse "prob" @@ -168,6 +177,20 @@ inputExt = cpsaExt, outputExt = shapesRoot ++ cpsaExt } +-- Logic Rule + +logic :: FilePath -> IO () +logic root = + do + cpsaAll root -- Run CPSA if need be + make logicRule root + +logicRule :: Rule +logicRule = + Rule { prog = "cpsalogic", + inputExt = cpsaExt, + outputExt = logicExt } + -- Annotations Rule annos :: FilePath -> IO () @@ -205,6 +228,7 @@ rm $ root ++ graphExt rm $ root ++ shapesRoot ++ cpsaExt rm $ root ++ shapesRoot ++ graphExt + rm $ root ++ logicExt rm $ root ++ annosRoot ++ cpsaExt rm $ root ++ annosRoot ++ graphExt rm $ root ++ paramsRoot ++ cpsaExt @@ -223,6 +247,9 @@ shapesRoot :: String shapesRoot = "_shapes" + +logicExt :: String +logicExt = "_logic.text" annosRoot :: String annosRoot = "_annotations" diff --git a/doc/cpsa.bib b/doc/cpsa.bib --- a/doc/cpsa.bib +++ b/doc/cpsa.bib @@ -259,15 +259,22 @@ editor = {Veronique Cortier and Steve Kremer}, series = {Cryptology and Information Security Series}} -@Article{CokerEtAl11, - author = {George Coker and Joshua Guttman and Peter Loscocco - and Amy Herzog and Jonathan Millen and Brian - O'Hanlon and John Ramsdell and Ariel Segall and - Justin Sheehy and Brian Sniffen}, - title = {Principles of Remote Attestation}, - journal = {International Journal of Information Security}, - year = 2011, - note = {Forthcoming}} +@article{CokerEtAl11, + author = {George Coker and Joshua Guttman and Peter Loscocco and + Amy Herzog and Jonathan Millen and Brian O'Hanlon + and John Ramsdell and Ariel Segall and Justin Sheehy + and Brian Sniffen}, + affiliation = {National Security Agency and The MITRE Corporation}, + title = {Principles of remote attestation}, + journal = {International Journal of Information Security}, + publisher = {Springer Berlin / Heidelberg}, + issn = {1615-5262}, + keyword = {Computer Science}, + pages = {1--19}, + url = {http://dx.doi.org/10.1007/s10207-011-0124-7}, + note = {10.1007/s10207-011-0124-7}, + year = {2011} +} @InProceedings{Guttman09, author = {Joshua D. Guttman}, diff --git a/doc/cpsadesign.pdf b/doc/cpsadesign.pdf Binary files a/doc/cpsadesign.pdf and b/doc/cpsadesign.pdf differ diff --git a/doc/cpsaoverview.pdf b/doc/cpsaoverview.pdf Binary files a/doc/cpsaoverview.pdf and b/doc/cpsaoverview.pdf differ diff --git a/doc/cpsaprimer.pdf b/doc/cpsaprimer.pdf Binary files a/doc/cpsaprimer.pdf and b/doc/cpsaprimer.pdf differ diff --git a/doc/cpsaprimer.tex b/doc/cpsaprimer.tex --- a/doc/cpsaprimer.tex +++ b/doc/cpsaprimer.tex @@ -1181,7 +1181,7 @@ The \texttt{cpsalogic} program extracts a formula in the language of order-sorted first-order logic for each problem and its shapes from a {\cpsa} run. The formula is called a shape analysis sentence. The -formula is modeled by all realized skeletons when {\cpsa} finds all +formula is satisfied in all realized skeletons when {\cpsa} finds all the shapes for the problem. The details of formula extraction are presented in Appendix~B of The {\cpsa} Specification~\cite{cpsaspec09}. diff --git a/doc/cpsaspec.pdf b/doc/cpsaspec.pdf Binary files a/doc/cpsaspec.pdf and b/doc/cpsaspec.pdf differ diff --git a/doc/cpsaspec.tex b/doc/cpsaspec.tex --- a/doc/cpsaspec.tex +++ b/doc/cpsaspec.tex @@ -150,14 +150,18 @@ \section{Notation}\label{sec:notation} A finite sequence\index{sequence} is a function from an initial -segment of the whole numbers. The length of a sequence~$f$ is~$|f|$, -and sequence~$f=\seq{f(1),\ldots,f(n)}$ for $n=|f|$. Alternatively, +segment of the whole numbers. The length of a sequence~$X$ is~$|X|$, +and sequence~$X=\seq{X(1),\ldots,X(n)}$ for $n=|X|$. Alternatively, $\seq{x_1,x_2,\ldots,x_n} =x_1\cons x_2\cons\ldots\cons x_n\cons\seq{}$. If~$S$ is a set, then~$S^\ast$ is the set of finite sequences of~$S$, and~$S^+$ is the non-empty finite sequences of~$S$. -The concatenation of sequences~$f_0$ and~$f_1$ is~$f_0\append f_1$. -The prefix of sequence~$f$ of length~$n$ is~$\prefix{f}{n}$. +The concatenation of sequences~$X_0$ and~$X_1$ is~$X_0\append X_1$. +The prefix of sequence~$X$ of length~$n$ is~$\prefix{X}{n}$. +Generally, when discussing terms, a lowercase Latin letter is used to +denote a term, and an uppercase Latin letter is used to denote a set +of terms or a sequence of terms. + \chapter{Order-Sorted Message Algebras}\label{chp:order-sorted mesg algs} {\cpsa} models a message by an equivalence class of terms over a @@ -378,6 +382,7 @@ $\Theta_X$, and its trace is $\Theta_X(s)$. In a strand space, the elements of the generator set~$X$ denote atomic message elements, such as keys, and not composite messages, such as encryptions and pairs. +\enlargethispage{3ex} Therefore, the sort of every variable in~$X$ is a base sort. Message events occur at nodes in a strand space. For each strand~$s$, @@ -404,9 +409,11 @@ Each acyclic graph has a transitive asymmetric relation~$\prec$ on its vertices. The relation specifies the causal ordering of nodes in a -bundle. Relation~$R$ on set~$S$ is \emph{asymmetric} iff -$x\mathbin{R}y$ implies not $y\mathbin{R}x$ for all distinct $x,y \in -S$. +bundle. Relation~$R$ on set~$S$ is +\index{asymmetric relation}\emph{asymmetric} iff $x\mathbin{R}y$ implies not +$y\mathbin{R}x$ for all distinct $x,y \in S$. An asymmetric +transitive binary relation is also called a \index{strict partial + order}\index{partial order!strict}strict partial order. An atom \index{uniquely originates}\emph{uniquely originates} in a bundle if it originates in the trace of exactly one strand. An atom @@ -476,7 +483,7 @@ a message, because every key it uses must be carried in a message. Consider a uniquely originating atom that originates on a regular strand. The penetrator cannot make the atom using a create role, -because the atom would originate at more than one node. Therefore, +because the atom would originate in more than one trace. Therefore, the penetrator can use a uniquely originating atom to encrypt or decrypt a message only if it is transmitted by a regular strand unprotected by encryption. @@ -506,7 +513,7 @@ is the transitive asymmetric relation associated with the bundle without penetrator nodes, $N$ is the set of non-originating atoms with variables that occur in $\Theta'_X$, and $U$ is the set of atoms that -uniquely originate and are carried by some regular node. +uniquely originate and are carried by some regular event. A protoskeleton $\skel_X(\rl,P,\Theta_X,\prec,N,U)$ is a \index{preskeleton}\emph{preskeleton} if the following properties hold. @@ -515,9 +522,9 @@ satisfy the conditions for being a part of a run of protocol~$P$. \item Relation $\prec$ is transitive, asymmetric, and includes the strand succession relation $(\Rightarrow)$. -\item Each atom in $N$ is carried at no node, and each variable - in the atom occurs at some node. -\item Each atom in $U$ is carried at some node. +\item Each atom in $N$ is carried by no event, and each variable + in the atom occurs in some event. +\item Each atom in $U$ is carried by some event. \item $N$ includes the non-originating atoms inherited from roles via the role map. \item $U$ includes the uniquely originating atoms inherited from roles via @@ -538,8 +545,9 @@ $k_1=\skel_Y(rl_1,P,\Theta_1,\prec_1,N_1,U_1)$ be preskeletons. There is a \index{preskeleton homomorphism}\index{homomorphism!preskeleton}\emph{preskeleton - homomorphism} from~$k_0$ to~$k_1$ if~$\phi$ and~$\sigma$ are maps -with the following properties: + homomorphism}\label{def:preskeleton homomorphism} from~$k_0$ +to~$k_1$ if~$\phi$ and~$\sigma$ are maps with the following +properties: \begin{enumerate} \item $\phi$ maps strands of~$k_0$ into those of~$k_1$, and nodes as $\phi((s,p))=(\phi(s),p)$, that is $\phi$ is in @@ -578,9 +586,8 @@ to make penetrator derived messages visible in skeletons. We say skeleton~$k$ \emph{realizes modulo listeners} bundle $\Upsilon(\Theta,\to) $ if~$k$ realizes $\Upsilon(\Theta',\to')$ and -\hbox{$\Upsilon(\Theta,\to)$} is the result of removing full length -listener strands, and adjusting the communication ordering $\to$ -appropriately. +\hbox{$\Upsilon(\Theta,\to)$} is the result of removing listener +strands, and adjusting the communication ordering $\to$ appropriately. The set of bundles denoted by preskeleton~$k$, $\sembrack{k}$, is: $$\sembrack{k_0} = \{\Upsilon\mid @@ -591,11 +598,6 @@ that $\sembrack{k_0}=\bigcup_{k_1\in K}\sembrack{k_1}$. \label{def:preskeleton denotation} -Let~$\longrightarrow$ be an irreflexive reduction relation on -preskeletons. The relation~$\longrightarrow$ is \emph{semantics - preserving} if $\sembrack{k_0}=\bigcup_{k_1\in\{k_1\mid - k_0\longrightarrow k_1\}}\sembrack{k_1}$. - \section{Blanchet's Simple Example Protocol}\label{sec:blanchet's simple example protocol} @@ -613,24 +615,24 @@ This {\cpsa} description of the protocol has an initiator and a responder role. $$\begin{array}{r@{{}={}}l} -\init(a,b\colon A,s\colon S, d\colon T)& +\init(a,b\colon A,s\colon S, d\colon D)& \role(\seq{\outbnd\enc{\enc{s}{a^{-1}}}{b},\inbnd\enc{d}{s}}, \emptyset,\emptyset)\\ -\resp(a,b\colon A,s\colon S, d\colon T)& +\resp(a,b\colon A,s\colon S, d\colon D)& \role(\seq{\inbnd\enc{\enc{s}{a^{-1}}}{b},\outbnd\enc{d}{s}}, \emptyset,\emptyset) \end{array}$$ where we use~$A$ for sort \dom{akey}, $S$ for sort \dom{skey}, and -$T$ for sort \dom{text} to save space. The algebra for the initiator +$D$ for sort \dom{data} to save space. The algebra for the initiator role is generated from $X$, where $X_A=\{a,b\}$, $X_S=\{s\}$, -$X_T=\{d\}$, $X_{\dom{data}}=\emptyset$, $X_{\dom{name}}=\emptyset$, +$X_D=\{d\}$, $X_{\dom{text}}=\emptyset$, $X_{\dom{name}}=\emptyset$, and $X_\top=\emptyset$. An interesting point of view for analysis is to see if the authentication goals of the initiator are met. To do so, we assume there was full length run of an initiator strand, and let {\cpsa} determine what else must have happened. Let variable set $Y=a,b\colon -A,s\colon S, d\colon T$. The point-of-view skeleton is: +A,s\colon S, d\colon D$. The point-of-view skeleton is: $$\begin{array}{r@{}ll} \skel_Y( &\seq{\init(a_0,b_0,s_0,d_0)}, @@ -715,7 +717,7 @@ The shape generated by {\cpsa} follows. An early indication of a problem is the variable set for the shape has three asymmetric keys. -Let variable set $Z=a,b,b'\colon A,s\colon S, d\colon T$. The shape +Let variable set $Z=a,b,b'\colon A,s\colon S, d\colon D$. The shape is: $$\begin{array}{r@{}ll} \skel_Z( @@ -777,7 +779,7 @@ The {\cpsa} description of the protocol also has an initiator and a responder role. $$\begin{array}{r@{{}={}}l} -\init(a,b\colon A, m\colon T)& +\init(a,b\colon A, m\colon D)& \role(\seq{\outbnd\enc{\enc{m}{b},a}{b},\inbnd\enc{\enc{m}{a},b}{a}}, \emptyset,\emptyset)\\ \resp(a,b\colon A, m\colon\top)& @@ -787,7 +789,7 @@ An interesting point of view for analysis is to see if~$m$ is kept secret after the initiator sends its message. Let variable set -$Z=a,b\colon A, m\colon T$. The initial scenario preskeleton is: +$Z=a,b\colon A, m\colon D$. The initial scenario preskeleton is: $$\begin{array}{r@{}ll} \skel_Z( &\seq{\init(a_0,b_0,m_0),\lsn(x)}, @@ -2047,11 +2049,11 @@ structure preserving maps~$\delta_i$, and the shape~$k_i$ is described by~$\Phi_i$. -Models of a shape sentence are skeletons. If {\cpsa} finds all of the -shapes and the homomorphisms associated with a point-of-view skeleton, -the analysis' shape sentence is modeled by all realized skeletons. -Shape sentences are closely related to security -goals~\cite{guttman09}, and motivated by that work. +An interpretation of a shape sentence is a skeleton. If {\cpsa} finds +all of the shapes and the homomorphisms associated with a +point-of-view skeleton, the analysis' shape sentence is satisfied in +all realized skeletons. Shape sentences are closely related to +security goals~\cite{guttman09}, and motivated by that work. \section{Shape Formulas} @@ -2065,13 +2067,14 @@ independent predicates. For each role $r=\role_Y(C,N,U)$ in protocol~$P$, there are protocol specific binary predicates $P[r,h,x]\colon\dom{nat}\times S$ for every $1\leq h\leq|C|$ -and~$x\colon S$ that occurs in~$C|_h$. The protocol independent unary -predicates are $\cn{non}\colon\dom{mesg}$ and -$\cn{uniq}\colon\dom{mesg}$. The protocol independent predicate of -arity four is $\cn{precedes}\colon -\dom{nat}\times\dom{nat}\times\dom{nat}\times\dom{nat}$. The -predicate \cn{false} has arity zero and, of course, equality is -binary. +and~$x\colon S$ that occurs in~$C|_h$. The protocol independent +predicate of arity four is $\cn{prec}\colon +\dom{nat}\times\dom{nat}\times\dom{nat}\times\dom{nat}$. The protocol +independent unary predicates are $\cn{non}\colon B$ and +$\cn{uniq}\colon B$ for each base sort~$B$, and the protocol +independent ternary predicates are $\cn{orig}\colon +B\times\dom{nat}\times\dom{nat}$. The predicate \cn{false} has arity +zero and, of course, equality is binary. We define~$\form(k)=(Y,\Phi)$, where~$\Phi$ is $k$'s skeleton formula, and~$Y$ is the formula's variable set. Let @@ -2088,14 +2091,16 @@ homomorphism described near the end of Chapter~\ref{chp:strand spaces and bundles}. \item For each $(s,i)\prec(s',i')$, assert - $\cn{precedes}(z_s,i,z_{s'},i')$. + $\cn{prec}(z_s,i,z_{s'},i')$. \item For each $t\in N$, assert $\cn{non}(t)$. \item For each $t\in U$, assert $\cn{uniq}(t)$. +\item For each $t\in U$ and $(s,i)\in\orig_k(t)$, assert + $\cn{orig}(t,z_s, i)$. \end{itemize} In the code that extracts a shape analysis sentence, the -$\cn{procedes}$ predicate is not asserted for strand succession, and -only for communication when the it is in the transitive reduction of +$\cn{prec}$ predicate is not asserted for strand succession, and +only for communication when it is in the transitive reduction of the~$\prec$ relation. The missing relations must be asserted as axioms for proper handling of a shape sentence. @@ -2112,16 +2117,16 @@ \begin{figure} $$\begin{array}{l} -\all{a_0,b_0\colon A, s_0\colon S, d_0\colon T, z_0\colon N}\\ +\all{a_0,b_0\colon A, s_0\colon S, d_0\colon D, z_0\colon N}\\ \quad\init_{2,a}(z_0,a_0)\wedge \init_{2,b}(z_0,b_0)\wedge \init_{2,s}(z_0,s_0)\wedge \init_{2,d}(z_0,d_0)\wedge{}\\ \quad\cn{non}(a_0^{-1})\wedge \cn{non}(b_0^{-1})\wedge -\cn{uniq}(s_0)\\ +\cn{uniq}(s_0)\wedge\cn{orig}(s_0,z_0,1)\\ \quad\rightarrow\\ -\quad\some{a_1,b_1\colon A, s_1\colon S, d_1\colon T, z_1,z_2\colon +\quad\some{a_1,b_1\colon A, s_1\colon S, d_1\colon D, z_1,z_2\colon N}\\ \qquad z_0=z_1\wedge a_0=a_1\wedge b_0=b_1\wedge s_0=s_1\wedge d_0=d_1\wedge{}\\ \qquad\init_{2,a}(z_1,a_1)\wedge @@ -2132,11 +2137,11 @@ \resp_{2,b}(z_1,b_1)\wedge \resp_{2,s}(z_1,s_1)\wedge \resp_{2,d}(z_1,d_1)\wedge{}\\ -\qquad\cn{precedes}(z_1,1,z_2,1)\wedge -\cn{precedes}(z_2,2,z_1,2)\wedge{}\\ +\qquad\cn{prec}(z_1,1,z_2,1)\wedge +\cn{prec}(z_2,2,z_1,2)\wedge{}\\ \qquad\cn{non}(a_1^{-1})\wedge \cn{non}(b_1^{-1})\wedge -\cn{uniq}(s_1) +\cn{uniq}(s_1)\wedge\cn{orig}(s_1,z_1,1) \end{array}$$ \caption{A Shape Analysis Sentence for Blanchet's Protocol}\label{fig:blanchet's shape analysis sentence} @@ -2159,12 +2164,13 @@ strand progress predicate $P[r,h,x](z,t)$ is written $r_{h,x}(z,t)$ with the protocol left implicit. -\section{Models of Shape Formulas} +\section{Semantics of Shape Formulas} -The universe for a model of a shape formula is -$\alg{D}=\nat\cup\alga_X$. When skeleton~$k$ and variable assignment -$\alpha:Z\to \alg{D}$ model formula~$\Psi$, we write -$k,\alpha\models\Psi$. +Once again, let $k=\skel_X(\rl,P,\Theta,\prec,N,U)$. The universe of +discourse is $\alg{D}=\nat\cup\alga_X$. When formula~$\Psi$ is +satisfied in skeleton~$k$ with variable assignment $\alpha\colon Y\to +\alg{D}$, we write $k,\alpha\models\Psi$. When sentence~$\Sigma$ is +satisfied in skeleton~$k$, we write $k\models\Sigma$. For each protocol specific predicate $P[r,h,x]$, $k,\alpha\models P[r,h,x](y,z)$ iff $\alpha(y)\in\nat$, $\alpha(z)\in\alga$, and with @@ -2177,53 +2183,93 @@ $\comp{\sigma}{C|_\ell}=\Theta(s)$, and $\ell=|\Theta(s)|$. \end{enumerate} -In a model, $\rl(s)$ need not be~$r$. The events that make up a -strand's trace is all that matters. The protocol specific predicate -$P[r,h,x]$ is called a \index{strand progress predicate}\emph{strand - progress predicate}, because it asserts a strand is associated with -an instance of role~$r$ of height at least~$h$. +In an interpretation, $\rl(s)$ need not be~$r$. The events that make +up a strand's trace is all that matters. The protocol specific +predicate $P[r,h,x]$ is called a \index{strand progress + predicate}\emph{strand progress predicate}, because it asserts a +strand is associated with an instance of role~$r$ of height at +least~$h$. -Modeling the protocol independent predicates is straightforward. +The interpretation of the protocol independent predicates is +straightforward. \begin{itemize} +\item $k,\alpha\models\cn{prec}(w,x,y,z)$ iff +$(\alpha(w),\alpha(x))\prec(\alpha(y),\alpha(z))$. \item $k,\alpha\models\cn{non}(y)$ iff $\alpha(y)\in N$. \item $k,\alpha\models\cn{uniq}(y)$ iff $\alpha(y)\in U$. +\item $k,\alpha\models\cn{orig}(x,y,z)$ iff $\alpha(x)\in U$ and + $(\alpha(y),\alpha(z))\in\orig_k(\alpha(x))$. \item $k,\alpha\models y=z$ iff $\alpha(y)=\alpha(z)$. -\item $k,\alpha\models\cn{precedes}(w,x,y,z)$ iff -$(\alpha(w),\alpha(x))\prec(\alpha(y),\alpha(z))$. \item $k,\alpha\not\models\cn{false}$. \end{itemize} -\begin{conj} -Let $\form(k)=(X,\Psi)$ and $\Phi=\some{X}\Psi$. -Skeleton~$k'$ models~$\Phi$ if there is a homomorphism from~$k$ to -$k'$, i.e.\ $k'\models\Phi$ iff $\some{\delta}k\homomorphism{\delta}k'$. -\end{conj} +\begin{thm}\label{thm:skeleton models} +Let $\form(k)=(X,\Psi)$ and $\Phi=\some{X}\Psi$. Formula~$\Phi$ is +satisfied in~$k'$ iff there is a homomorphism from~$k$ to +$k'$, i.e.\ $k'\models\Phi$ iff +$\some{\delta}k\homomorphism{\delta}k'$. +\end{thm} -This conjecture is essentially a restatement of the first of the two -main results from~\cite{guttman09}. +This theorem corrects the first of the two main results +from~\cite{guttman09}, as that paper omits the \cn{orig} predicate. +\begin{proof} +For the forward direction, assume~$\alpha$ is a variable assignment +for the variables in~$X$ such that $k',\alpha\models\Psi$, and let~$Z$ +be the sequence of strand variables constructed while +generating~$\Psi$ from~$k$. Then the pair of maps +$\delta=(\comp{\alpha}{Z},\alpha)$ demonstrate a homomorphism from~$k$ +to~$k'$, i.e.\ each item in the definition of a preskeleton +homomorphism on Page~\pageref{def:preskeleton homomorphism} is +satisfied. + +For the reverse direction, assume maps $\delta=(\phi,\sigma)$ are such +that $k\homomorphism{\delta}k'$. Then the desired variable assigment is +$$\alpha(x)=\left\{ +\begin{array}{ll} +\phi(Z^{-1}(x))&x\in\sran(Z)\\ +\sigma(x)&x\in\sdom(\sigma). +\end{array}\right.$$ +\end{proof} + The set of bundles denoted by preskeleton~$k$, $\sembrack{k}$ is defined on Page~\pageref{def:preskeleton denotation}. -\begin{conj} +\begin{thm}\label{thm:sentence implies} Let $k\homomorphism{\delta_i}k_i$ be a complete set of homomorphisms for shapes $k_i\in K$, and assume $\sembrack{k}=\bigcup_{k'\in K}\sembrack{k'}$. Then the shape analysis -sentence~$\Sigma=\sent(k\homomorphism{\delta_i}k_i)$ is modeled by all -realized skeletons~$k$, i.e.\ $k\models\Sigma$. -\end{conj} +sentence~$\Sigma=\sent(k\homomorphism{\delta_i}k_i)$ is satisfied in +all realized skeletons~$k$, i.e.\ $k\models\Sigma$. +\end{thm} -A shape analysis sentence can be translated into the language of -ordinary first-order logic and used with an automated first-order -theorem prover. If security goal~$\Phi$ can be derived from shape -analysis sentence~$\Sigma$, then $\Phi$ is modeled by all realized -skeletons. +\begin{proof} +Shapes are maximal among realized skeletons, so there is no realized +skeleton in the image of~$k$ that is not in the image of one of the +shapes. Therefore, by Theorem~\ref{thm:skeleton models}, the negation +of the hypothesis of the implication is satisfied in all realized +skeletons that are not in the image of~$k$, and the disjunction is +satisfied in the remaining realized skeletons. +\end{proof} -\begin{conj} -Suppose $\Phi$ is a security goal and $\Sigma$ is a shape analysis -sentence modeled by all realized skeletons. Then $\Sigma\vdash\Phi$ -iff $\Phi$ is modeled by all realized skeletons. -\end{conj} +The security goals of a protocol can be formalized using the same +language used to specify shape analysis sentences. A security goal +can express an authentication goal or a secrecy goal. + +Security goals and shape analysis sentences can be translated into the +language of ordinary first-order logic and used with an automated +first-order theorem prover. If a theorem prover deduces security +goal~$\Phi$ from shape analysis sentence~$\Sigma$, then $\Phi$ is +satisfied in all realized skeletons. + +Security goals can be used to ensure essential properties of a +protocol are preserved in the face of changes to the protocol. +Suppose an initial version of a protocol is specified, and shape +analysis sentences for it are produced. The sentences can be edited +to produce a formalization of security goals that should be preserved +during any revision to the protocol. After a revision, one can +generate revised shape analysis sentences, and use them to make sure +each security goal is still deducible. \bibliography{cpsa} \bibliographystyle{plain} diff --git a/doc/cpsatheory.pdf b/doc/cpsatheory.pdf Binary files a/doc/cpsatheory.pdf and b/doc/cpsatheory.pdf differ diff --git a/doc/cpsauser.html b/doc/cpsauser.html --- a/doc/cpsauser.html +++ b/doc/cpsauser.html @@ -442,8 +442,8 @@

The cpsalogic program extracts a formula in the language of order-sorted first-order logic for each problem and its shapes from a CPSA run. The formula is called a shape analysis - sentence. The formula is modeled by all realized skeletons when CPSA - finds all the shapes for the problem.

+ sentence. The formula is satisfied in all realized skeletons when + CPSA finds all the shapes for the problem.

Usage

diff --git a/doc/macros.tex b/doc/macros.tex --- a/doc/macros.tex +++ b/doc/macros.tex @@ -1,5 +1,5 @@ \newcommand{\cpsa}{\textsc{cpsa}} -\newcommand{\version}{2.2.3} +\newcommand{\version}{2.2.4} \newcommand{\cpsacopying}{\begingroup \renewcommand{\thefootnote}{}\footnotetext{{\copyright} 2010 The MITRE Corporation. Permission to copy without fee all or part of diff --git a/src/CPSA/Lib/Reduction.hs b/src/CPSA/Lib/Reduction.hs --- a/src/CPSA/Lib/Reduction.hs +++ b/src/CPSA/Lib/Reduction.hs @@ -6,17 +6,13 @@ -- modify it under the terms of the BSD License as published by the -- University of California. -{-# LANGUAGE CPP #-} - -- Provides the top-level search loop, which implements term reduction -- on skeletos. module CPSA.Lib.Reduction (solve) where import System.IO -#if defined HAVE_PAR import Control.Parallel -#endif import qualified Data.List as L import CPSA.Lib.Utilities import CPSA.Lib.SExpr @@ -84,8 +80,6 @@ data Algebra t p g s e c => Reduct t p g s e c = Reduct !(LPreskel t p g s e c) !Int !Bool ![Preskel t p g s e c] ![Int] -#if defined HAVE_PAR - parMap :: (a -> b) -> [a] -> [b] parMap _ [] = [] parMap f (x:xs) = @@ -94,12 +88,12 @@ y = f x ys = parMap f xs -#else +{-- Turn off parallism with this: parMap :: (a -> b) -> [a] -> [b] parMap = map -#endif +-} -- Entry point for analysis solve :: Algebra t p g s e c => Options -> Handle -> @@ -299,28 +293,67 @@ commentPreskel :: Algebra t p g s e c => LPreskel t p g s e c -> [Int] -> [Node] -> Bool -> String -> SExpr () commentPreskel lk seen unrealized shape msg = - displayPreskel k l + displayPreskel k $ + addKeyValues "label" [N () (label lk)] $ + maybeAddVKeyValues "parent" (\p -> [N () (label p)]) (parent lk) $ + condAddKeyValues "seen" (not $ null seen) + (map (N ()) (L.sort (L.nub seen))) $ + addKeyValues "unrealized" (map displayNode $ L.sort unrealized) $ + condAddKeyValues "shape" shape [] $ + -- Structure preserving maps + -- Added for cpsalogic program + condAddKeyValues "maps" shape (maps k) $ + -- Nodes of origination + -- Added for cpsalogic program + condAddKeyValues "origs" (starter k || shape) (origs k) $ + -- Messages + case msg of + "" -> [] + -- Preskeleton key added for cpsalogic program + "Not a skeleton" -> addKeyValues "preskeleton" [] [comment msg] + _ -> [comment msg] where k = content lk - l = L () [S () "label", N () (label lk)] : p - p = maybe s (\p -> L () [S () "parent", N () (label p)] : s) (parent lk) - s | null seen = r - | otherwise = L () (S () "seen" : kids) : r - kids = map (N ()) (L.sort (L.nub seen)) - r = L () (S () "unrealized" : nodes) : notes - nodes = map displayNode (L.sort unrealized) - notes = if shape then L () [S () "shape"] : spm : msgs else msgs - -- Structure preserving map (homomorphism) - spm = L () (S () "maps" : map (amap $ strandMap k) (envMaps k)) + starter k = -- True for the POV skeleton and + case pov k of -- just a few others + Nothing -> False + Just k' -> nstrands k == nstrands k' + +addKeyValues :: String -> [SExpr ()] -> [SExpr ()] -> [SExpr ()] +addKeyValues key values rest = + L () (S () key : values) : rest + +condAddKeyValues :: String -> Bool -> [SExpr ()] -> [SExpr ()] -> [SExpr ()] +condAddKeyValues _ False _ rest = + rest +condAddKeyValues key True values rest = + addKeyValues key values rest + +maybeAddVKeyValues :: String -> (a -> [SExpr ()]) -> Maybe a -> + [SExpr ()] -> [SExpr ()] +maybeAddVKeyValues _ _ Nothing rest = + rest +maybeAddVKeyValues key f (Just x) rest = + addKeyValues key (f x) rest + +-- Prints structure preserving maps (homomorphisms) +maps :: Algebra t p g s e c => Preskel t p g s e c -> [SExpr ()] +maps k = + map (amap $ strandMap k) (envMaps k) + where amap strands env = L () [L () strands, L () env] strandMap k = map (N ()) (prob k) envMaps k = - case (pov k) of + case pov k of Nothing -> [] Just k' -> map (displayEnv (ctx k') (ctx k)) (homomorphism k' k (prob k)) ctx k = addToContext emptyContext (kvars k) - msgs = case msg of - "" -> [] - "Not a skeleton" -> L () [S () "preskeleton"] : [comment msg] - _ -> [comment msg] + +-- Prints the nodes of origination for each uniquely originating atom +origs :: Algebra t p g s e c => Preskel t p g s e c -> [SExpr ()] +origs k = + [ L () [displayTerm ctx t, displayNode n] + | (t, ns) <- korig k, n <- ns ] + where + ctx = addToContext emptyContext (kvars k) diff --git a/src/CPSA/Lib/Strand.hs b/src/CPSA/Lib/Strand.hs --- a/src/CPSA/Lib/Strand.hs +++ b/src/CPSA/Lib/Strand.hs @@ -9,7 +9,7 @@ module CPSA.Lib.Strand (Instance, mkInstance, bldInstance, mkListener, role, env, trace, height, listenerTerm, Sid, Node, mkPreskel, firstSkeleton, Pair, Preskel, gen, protocol, insts, orderings, - pov, knon, kunique, kcomment, nstrands, kvars, kterms, uniqOrig, + pov, knon, kunique, korig, kcomment, nstrands, kvars, kterms, uniqOrig, preskelWellFormed, verbosePreskelWellFormed, Strand, GraphStrand, inst, nodes, Vertex, GraphNode, preds, event, graphNode, strands, vertex, Gist, gist, contract, augment, inheritRnon, diff --git a/src/CPSA/Logic/Logic.hs b/src/CPSA/Logic/Logic.hs --- a/src/CPSA/Logic/Logic.hs +++ b/src/CPSA/Logic/Logic.hs @@ -105,8 +105,15 @@ loadRoles :: (Algebra t p g s e c, Monad m) => g -> [SExpr Pos] -> m (g, [Role t p g s e c]) loadRoles origin xs = - mapAccumLM loadRole origin xs + mapAccumLM loadRole origin $ stripComments xs +stripComments :: [SExpr Pos] -> [SExpr Pos] +stripComments xs = + filter pred xs + where + pred (L _ (S _ sym : _)) = sym == "defrole" + pred _ = True -- Catch bad entries + -- A monad version of map accumulation from the left mapAccumLM :: Monad m => (a -> b -> m (a, c)) -> a -> [b] -> m (a, [c]) mapAccumLM _ z [] = @@ -189,6 +196,7 @@ orderings :: [Pair], nons :: [t], uniqs :: [t], + origs :: [(t, Node)], isSkeleton :: Bool, isShape :: !Bool, -- Always looked at, so make it strict homomorphisms :: [SExpr Pos], -- Loaded later @@ -205,6 +213,7 @@ orderings <- loadOrderings heights (assoc precedesKey xs) nons <- loadBaseTerms kvars (assoc nonOrigKey xs) uniqs <- loadBaseTerms kvars (assoc uniqOrigKey xs) + origs <- loadOrigs kvars heights (assoc origsKey xs) let kctx = addToContext ctx (kvars ++ strands) return (Preskel { protocol = prot, kgen = gen'', @@ -213,6 +222,7 @@ orderings = orderings, nons = nons, uniqs = uniqs, + origs = origs, isSkeleton = not $ hasKey preskeletonKey xs, isShape = hasKey shapeKey xs, homomorphisms = assoc mapsKey xs, @@ -337,6 +347,25 @@ True -> return t False -> fail (shows (annotation x) "Expecting an atom") +loadOrigs :: (Algebra t p g s e c, Monad m) => [t] -> Strands -> + [SExpr Pos] -> m [(t, Node)] +loadOrigs _ _ [] = return [] +loadOrigs vars heights (x : xs) = + do + o <- loadOrig vars heights x + os <- loadOrigs vars heights xs + return (adjoin o os) + +loadOrig :: (Algebra t p g s e c, Monad m) => [t] -> Strands -> + SExpr Pos -> m (t, Node) +loadOrig vars heights (L _ [x, y]) = + do + t <- loadTerm vars x + n <- loadNode heights y + return (t, n) +loadOrig _ _ x = + fail (shows (annotation x) "Malformed origination") + -- Homomorphisms -- The maps entry in a preskeleton contains a list of homomorphisms. @@ -411,6 +440,10 @@ uniqOrigKey :: String uniqOrigKey = "uniq-orig" +-- The key used to extract the nodes of origination +origsKey :: String +origsKey = "origs" + -- Formula printing displayFormula :: (Algebra t p g s e c, Monad m) => @@ -442,9 +475,10 @@ let strands = displayVars (kctx k) (map strand $ insts k) return (vars ++ listMap nat strands, map (strandForm k) (insts k) ++ - map (precedesForm k) (orderings k) ++ + map (precForm k) (orderings k) ++ map (unary "non" $ kctx k) (nons k) ++ - map (unary "uniq" $ kctx k) (uniqs k)) + map (unary "uniq" $ kctx k) (uniqs k) ++ + map (origForm k) (origs k)) listMap :: ([SExpr ()] -> [SExpr ()]) -> [SExpr ()] -> [SExpr ()] listMap _ [] = [] @@ -477,9 +511,9 @@ quote x = x -- Creates the atomic formula used to describe a node ordering relation -precedesForm :: Algebra t p g s e c => Preskel t p g s e c -> Pair -> SExpr () -precedesForm k ((s, i), (s', i')) = - L () [S () "precedes", +precForm :: Algebra t p g s e c => Preskel t p g s e c -> Pair -> SExpr () +precForm k ((s, i), (s', i')) = + L () [S () "prec", displayTerm (kctx k) t, N () i, displayTerm (kctx k) t', @@ -487,6 +521,16 @@ where t = strand $ insts k !! s t' = strand $ insts k !! s' + +origForm :: Algebra t p g s e c => Preskel t p g s e c -> + (t, Node) -> SExpr () +origForm k (t, (s, i)) = + L () [S () "orig", + displayTerm (kctx k) t, + displayTerm (kctx k) z, + N () i] + where + z = strand $ insts k !! s -- Creates a formula associated with a shape. It is a disjunction of -- existentially quantified formulas that describe the homomorphism diff --git a/src/prover9.pl b/src/prover9.pl new file mode 100644 --- /dev/null +++ b/src/prover9.pl @@ -0,0 +1,295 @@ +% -*- mode: prolog -*- + +%% CPSA tools in Prolog + +%% Translates the output of the cpsalogic program into the syntax of +%% Prover9. + +%% Known to work in SWI-Prolog, but not with GNU Prolog. + +%% Copyright (c) 2011 The MITRE Corporation +%% +%% This program is free software: you can redistribute it and/or +%% modify it under the terms of the BSD License as published by the +%% University of California. + +:- module(prover9, [prover9/2]). + +:- use_module(pp). +:- use_module(sexpr). + +%% prover9(+In, +Out) Translates cpsalogic program output in file In, +%% into the syntax of Prover9 and places it in file Out. +prover9(In, Out) :- + sexpr:read_sexpr_list(In, Forms), + open(Out, write, Stream), + top_forms_pp(Stream, Forms), + close(Stream). + +%% Ignore all forms except the ones that start with forall. +top_forms_pp(_, []). +top_forms_pp(Out, [[forall|Rest]|Forms]) :- + !, + form_to_pretty([forall|Rest], Pretty), + pp:pr(Out, 72, Pretty), + put_char(Out, '.'), + nl(Out), + nl(Out), + top_forms_pp(Out, Forms). +top_forms_pp(Out, [_|Forms]) :- + top_forms_pp(Out, Forms). + +%% Formula classification + +form_to_pretty([equal|Terms], Pretty) :- + !, + equal(Terms, Pretty). +form_to_pretty([implies|Forms], Pretty) :- + !, + implication(Forms, Pretty). +form_to_pretty([and|Forms], Pretty) :- + !, + junction(and, Forms, Pretty). +form_to_pretty([or| Forms], Pretty) :- + !, + junction(or, Forms, Pretty). +form_to_pretty([forall|Rest], Pretty) :- + !, + quantifier(forall, Rest, Pretty). +form_to_pretty([exists|Rest], Pretty) :- + !, + quantifier(exists, Rest, Pretty). +form_to_pretty(Forms, Pretty) :- + atomic_form(Forms, Pretty). + +%% In general, breaks are before binary operators. + +%% Equality + +equal([L, R], Pretty) :- + term_to_pretty(L, Left), + pp:brk(1, Brk), + pp:atm('= ', Op), + term_to_pretty(R, Right), + pp:blo(0, [Left, Brk, Op, Right], Pretty). + +%% Implication + +implication([H, C], Pretty) :- + form_to_pretty(H, Hypoth), + pp:brk(1, Brk), + pp:atm('-> ', Op), + form_to_pretty(C, Concl), + pp:blo(0, [Hypoth, Brk, Op, Concl], Pretty). + +%% Conjunction and disjunction + +junction(and, [], Pretty) :- + pp:atm('$T', Pretty). +junction(or, [], Pretty) :- + pp:atm('$F', Pretty). +junction(_, [Form], Pretty) :- + !, + form_to_pretty(Form, Pretty). +junction(Kind, [Form|Forms], Pretty) :- + form_to_pretty(Form, First), + junction_op(Kind, Op), + junction_rest(Op, Forms, Pretties), + pp:blo(0, [First|Pretties], Pretty). + +junction_op(and, Pretty) :- + pp:atm('&', Pretty). +junction_op(or, Pretty) :- + pp:atm('|', Pretty). + +junction_rest(_, [], []). +junction_rest(Op, [Form|Forms], [Brk, Op, Sp, Next|Pretties]) :- + pp:brk(1, Brk), + pp:atm(' ', Sp), + form_to_pretty(Form, Next), + junction_rest(Op, Forms, Pretties). + +%% Quantifiers forall and exists + +%% This code simply drops the sort declarations. + +quantifier(_, [[], Body], Pretty) :- + !, + form_to_pretty(Body, Pretty). +quantifier(Kind, [Decls, Body], Pretty) :- + quantifier_op(Kind, Op), + decls(Decls, Vars), + quantifier_rest(Op, Vars, Body, Pretties), + pp:blo(2, Pretties, Pretty). + +quantifier_op(forall, Pretty) :- + pp:atm(all, Pretty). +quantifier_op(exists, Pretty) :- + pp:atm(exists, Pretty). + +%% Collect vars in declarations. + +decls(Decls, Vars) :- + decls(Decls, Vars, []). + +decls([], Vars, Vars). +decls([Decl|Decls], Vars, End) :- + decl(Decl, Vars, Middle), + decls(Decls, Middle, End). + +decl([_], Vars, Vars). +decl([Var|Decl], [Var|Vars], End) :- + atom(Var), + decl(Decl, Vars, End). + +quantifier_rest(_, [], Body, [Left, Brk, Pretty, Right]) :- + pp:atm('(', Left), + pp:brk(0, Brk), + form_to_pretty(Body, Pretty), + pp:atm(')', Right). +quantifier_rest(Op, [Var|Vars], Body, [Op, Sp, V, Brk|Pretties]) :- + pp:atm(' ', Sp), + term_to_pretty(Var, V), + pp:brk(1, Brk), + quantifier_rest(Op, Vars, Body, Pretties). + +% Atomic formulas + +atomic_form([Pred], Pretty) :- + atom(Pred), + pp:atm(Pred, Pretty). +atomic_form([Pred, Term|Terms], Pretty) :- + atom(Pred), + pp:atm(Pred, P), + pp:atm('(', Left), + term_to_pretty(Term, T), + terms_to_pretty(Terms, Ts), + pp:blo(2, [P, Left, T|Ts], Pretty). + +terms_to_pretty([], [Right]) :- + pp:atm(')', Right). +terms_to_pretty([Term|Terms], [Comma, Brk, T|Pretties]) :- + pp:atm(',', Comma), + pp:brk(1, Brk), + term_to_pretty(Term, T), + terms_to_pretty(Terms, Pretties). + +term_to_pretty(Term, Pretty) :- + load_term(Term, Internal), + term_pp(Internal, Pretty). + +%% Load a term using CPSA's parsing rules for terms. Also, convert +%% variables into uppercase atoms, and constants into lowercase atoms. + +load_term(Term, Internal) :- + atom(Term), + upcase_symbol(Term, Internal). +load_term(Term, Internal) :- + string(Term), + string_to_atom(Term, Atom), + downcase_symbol(Atom, Internal). +load_term(Term, Term) :- + integer(Term), + Term >= 0. +load_term([privk|Terms], Internals) :- + !, + load_term([invk, [pubk|Terms]], Internals). +load_term([cat,Term], Internals) :- + !, + load_term(Term, Internals). +load_term([cat,Term|Terms], [cat, X, Y]) :- + !, + load_term(Term, X), + load_term([cat|Terms], Y). +load_term([enc|Terms], Internal) :- + !, + load_enc(Terms, Internal). +load_term([Term|Terms], [Term|Internals]) :- + atom(Term), + load_terms(Terms, Internals). + +upcase_symbol(Atom, Symbol) :- + atom_chars(Atom, Chars), + upcase_parts(Chars, Parts), + atom_chars(Symbol, Parts). + +upcase_parts([First|Rest], [Lead|Tail]) :- + upcase_atom(First, Lead), + symbol_parts(Rest, Tail). + +downcase_symbol(Atom, Symbol) :- + atom_chars(Atom, Chars), + downcase_parts(Chars, Parts), + atom_chars(Symbol, Parts). + +%% The null constant is used for the name of the listener role. + +downcase_parts([], ['"', '"']). +downcase_parts([First|Rest], [Lead|Tail]) :- + downcase_atom(First, Lead), + symbol_parts(Rest, Tail). + +symbol_parts([], []). +symbol_parts(['-'|Rest], ['_'|Tail]) :- + !, + symbol_parts(Rest, Tail). +symbol_parts([First|Rest], [First|Tail]) :- + symbol_parts(Rest, Tail). + +load_enc(Terms, [enc, X, Y]) :- + split(Terms, As, B), + load_term([cat|As], X), + load_term(B, Y). + +split([X], [], X). +split([X, Y|Z], [X|A], B) :- + split([Y|Z], A, B). + +load_terms([], []). +load_terms([T|Ts], [I|Is]) :- + load_term(T, I), + load_terms(Ts, Is). + +%% Pretty print a term. + +term_pp(Term, Pretty) :- + atom(Term), + pp:atm(Term, Pretty). +term_pp([Term], Pretty) :- + atom(Term), + pp:atm(Term, Pretty). +term_pp([Pred, Term|Terms], Pretty) :- + atom(Pred), + pp:atm(Pred, P), + pp:atm('(', Left), + term_pp(Term, Arg), + args_pp(Terms, Pretties), + blo(2, [P, Left, Arg|Pretties], Pretty). +%% Natural numbers are turned into lists of nulls. +%% The number is the length of the list. +term_pp(0, Pretty) :- + pp:atm('[]', Pretty). +term_pp(Term, Pretty) :- + integer(Term), + succ(Num, Term), + pp:atm('[[]', First), + nat_pp(Num, Pretties), + blo(1, [First|Pretties], Pretty). + +args_pp([], [Pretty]) :- + pp:atm(')', Pretty). +args_pp([Term|Terms], [Comma, Brk, Pretty|Pretties]) :- + pp:atm(',', Comma), + pp:brk(1, Brk), + term_pp(Term, Pretty), + args_pp(Terms, Pretties). + +nat_pp(0, [Right]) :- + !, + pp:atm(']', Right). +nat_pp(Num, [Comma, Brk, Nil|Pretties]) :- + succ(Num1, Num), + pp:atm(',', Comma), + pp:brk(1, Brk), + pp:atm('[]', Nil), + nat_pp(Num1, Pretties). diff --git a/tst/blanchet.tst b/tst/blanchet.tst --- a/tst/blanchet.tst +++ b/tst/blanchet.tst @@ -1,7 +1,7 @@ (herald "Blanchet's Simple Example Protocol" (comment "There is a flaw in this protocol by design")) -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol blanchet basic @@ -20,6 +20,7 @@ (traces ((send (enc (enc s (privk a)) (pubk b))) (recv (enc d s)))) (label 0) (unrealized (0 1)) + (origs (s (0 0))) (comment "2 in cohort - 2 not yet seen")) (defskeleton blanchet @@ -67,7 +68,8 @@ (parent 1) (unrealized) (shape) - (maps ((0) ((a a) (b b) (s s) (d d))))) + (maps ((0) ((a a) (b b) (s s) (d d)))) + (origs (s (0 0)))) (comment "Nothing left to do") @@ -89,6 +91,7 @@ ((recv d) (send d))) (label 4) (unrealized (0 1)) + (origs (s (0 0))) (comment "2 in cohort - 2 not yet seen")) (defskeleton blanchet @@ -180,6 +183,7 @@ (traces ((recv (enc (enc s (privk a)) (pubk b))) (send (enc d s)))) (label 9) (unrealized (0 0)) + (origs) (comment "1 in cohort - 1 not yet seen")) (defskeleton blanchet @@ -197,7 +201,8 @@ (parent 9) (unrealized) (shape) - (maps ((0) ((a a) (b b) (s s) (d d))))) + (maps ((0) ((a a) (b b) (s s) (d d)))) + (origs (s (1 0)))) (comment "Nothing left to do") @@ -234,6 +239,7 @@ (label 12) (parent 11) (unrealized (0 0)) + (origs (d (0 1))) (comment "1 in cohort - 1 not yet seen")) (defskeleton blanchet @@ -252,7 +258,8 @@ (parent 12) (unrealized) (shape) - (maps ((0 1) ((a a) (b b) (s s) (d d))))) + (maps ((0 1) ((a a) (b b) (s s) (d d)))) + (origs (s (2 0)) (d (0 1)))) (comment "Nothing left to do") @@ -289,6 +296,7 @@ (label 15) (parent 14) (unrealized (0 0)) + (origs (d (0 1))) (comment "1 in cohort - 1 not yet seen")) (defskeleton blanchet @@ -307,7 +315,8 @@ (parent 15) (unrealized) (shape) - (maps ((0 1) ((a a) (b b) (s s) (d d))))) + (maps ((0 1) ((a a) (b b) (s s) (d d)))) + (origs (s (2 0)) (d (0 1)))) (comment "Nothing left to do") @@ -329,6 +338,7 @@ ((recv d) (send d))) (label 17) (unrealized (0 1)) + (origs (s (0 0))) (comment "2 in cohort - 2 not yet seen")) (defskeleton blanchet diff --git a/tst/completeness-test.tst b/tst/completeness-test.tst --- a/tst/completeness-test.tst +++ b/tst/completeness-test.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol completeness-test basic @@ -22,6 +22,7 @@ (send (enc "ok" s-0))) ((recv (enc "ok" s)))) (label 0) (unrealized (0 1) (1 0)) + (origs (n (0 0))) (comment "2 in cohort - 2 not yet seen")) (defskeleton completeness-test @@ -58,6 +59,7 @@ (label 2) (parent 0) (unrealized (0 1)) + (origs (n (0 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton completeness-test @@ -83,6 +85,7 @@ (unrealized) (shape) (maps ((0 1) ((b b) (n n) (s s) (a a) (s-0 s-0)))) + (origs (n (0 0))) (comment "1 in cohort - 0 not yet seen")) (defskeleton completeness-test @@ -103,7 +106,8 @@ (parent 2) (unrealized) (shape) - (maps ((0 1) ((b b) (n n) (s s) (a a) (s-0 s))))) + (maps ((0 1) ((b b) (n n) (s s) (a a) (s-0 s)))) + (origs (n (0 0)))) (comment "Nothing left to do") @@ -128,6 +132,7 @@ (send (enc "ok" s-0)))) (label 5) (unrealized (0 0) (1 1)) + (origs (n (1 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton completeness-test @@ -171,6 +176,7 @@ (unrealized) (shape) (maps ((0 1) ((b b) (n n) (s s) (a a) (s-0 s-0)))) + (origs (n (1 0))) (comment "1 in cohort - 0 not yet seen")) (defskeleton completeness-test @@ -191,7 +197,8 @@ (parent 6) (unrealized) (shape) - (maps ((0 1) ((b b) (n n) (s s) (a a) (s-0 s))))) + (maps ((0 1) ((b b) (n n) (s s) (a a) (s-0 s)))) + (origs (n (1 0)))) (comment "Nothing left to do") @@ -215,6 +222,7 @@ ((recv (enc "ok" s)))) (label 9) (unrealized (0 1) (1 0)) + (origs (n (0 0))) (comment "2 in cohort - 2 not yet seen")) (defskeleton completeness-test @@ -249,6 +257,7 @@ (label 11) (parent 9) (unrealized (1 1)) + (origs (n (1 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton completeness-test @@ -273,6 +282,7 @@ (unrealized) (shape) (maps ((0 1) ((b b) (n n) (s s) (a a)))) + (origs (n (0 0))) (comment "1 in cohort - 0 not yet seen")) (defskeleton completeness-test @@ -293,7 +303,8 @@ (parent 11) (unrealized) (shape) - (maps ((1 0) ((b b) (n n) (s s) (a a))))) + (maps ((1 0) ((b b) (n n) (s s) (a a)))) + (origs (n (1 0)))) (comment "Nothing left to do") @@ -317,6 +328,7 @@ ((send (enc a n (pubk b))) (recv (enc n (pubk a))))) (label 14) (unrealized (0 0) (1 1)) + (origs (n (1 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton completeness-test @@ -358,6 +370,7 @@ (unrealized) (shape) (maps ((0 1) ((b b) (n n) (s s) (a a)))) + (origs (n (1 0))) (comment "1 in cohort - 0 not yet seen")) (defskeleton completeness-test @@ -377,6 +390,7 @@ (parent 15) (unrealized) (shape) - (maps ((0 2) ((b b) (n n) (s s) (a a))))) + (maps ((0 2) ((b b) (n n) (s s) (a a)))) + (origs (n (2 0)))) (comment "Nothing left to do") diff --git a/tst/crushing.tst b/tst/crushing.tst --- a/tst/crushing.tst +++ b/tst/crushing.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol crushing basic @@ -31,6 +31,7 @@ (recv (enc n n1 n2 n3 n (invk k))))) (label 0) (unrealized (0 1) (0 2) (0 3) (0 5)) + (origs (n (0 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton crushing @@ -363,6 +364,7 @@ (parent 9) (unrealized) (shape) - (maps ((0) ((k k) (n n) (n1 n2) (n2 n2) (n3 n2))))) + (maps ((0) ((k k) (n n) (n1 n2) (n2 n2) (n3 n2)))) + (origs (n (0 0)) (n2 (1 1)))) (comment "Nothing left to do") diff --git a/tst/dass_simple.tst b/tst/dass_simple.tst --- a/tst/dass_simple.tst +++ b/tst/dass_simple.tst @@ -1,6 +1,6 @@ (herald "Distributed Authentication Security Service Protocol Variants") -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol dass-simple basic @@ -31,6 +31,7 @@ (enc (enc k (pubk b)) (invk kp)))) (recv (enc "resp" tb k)))) (label 0) (unrealized (0 1)) + (origs (k (0 0)) (kp (0 0))) (comment "2 in cohort - 2 not yet seen")) (defskeleton dass-simple @@ -138,7 +139,8 @@ (parent 3) (unrealized) (shape) - (maps ((0) ((a a) (b b) (k k) (kp kp) (ta ta) (tb tb))))) + (maps ((0) ((a a) (b b) (k k) (kp kp) (ta ta) (tb tb)))) + (origs (k (0 0)) (kp (0 0)))) (comment "Nothing left to do") @@ -171,6 +173,7 @@ (enc (enc k (pubk b)) (invk kp)))) (recv (enc "resp" tb k)))) (label 6) (unrealized (0 1)) + (origs (k (0 0)) (kp (0 0))) (comment "2 in cohort - 2 not yet seen")) (defskeleton dass+ @@ -334,6 +337,7 @@ (unrealized) (shape) (maps ((0) ((a a) (b b) (k k) (kp kp) (ta ta) (tb tb)))) + (origs (k (0 0)) (kp (0 0))) (comment "1 in cohort - 0 not yet seen")) (defskeleton dass+ @@ -356,6 +360,7 @@ (parent 12) (unrealized) (shape) - (maps ((0) ((a a) (b b) (k k) (kp kp) (ta ta) (tb tb))))) + (maps ((0) ((a a) (b b) (k k) (kp kp) (ta ta) (tb tb)))) + (origs (k (0 0)) (kp (0 0)))) (comment "Nothing left to do") diff --git a/tst/denning-sacco.tst b/tst/denning-sacco.tst --- a/tst/denning-sacco.tst +++ b/tst/denning-sacco.tst @@ -1,6 +1,6 @@ (herald "Denning-Sacco Protocol") -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol denning-sacco basic @@ -36,6 +36,7 @@ (enc a (pubk a) (privk ks)) (pubk b))))) (label 0) (unrealized (0 0)) + (origs) (comment "1 in cohort - 1 not yet seen")) (defskeleton denning-sacco @@ -182,6 +183,7 @@ (unrealized) (shape) (maps ((0) ((a a) (b b) (ks ks) (k k) (ta ta)))) + (origs (k (1 2))) (comment "1 in cohort - 0 not yet seen")) (defskeleton denning-sacco @@ -212,7 +214,8 @@ (parent 3) (unrealized) (shape) - (maps ((0) ((a b) (b b) (ks ks) (k k) (ta ta))))) + (maps ((0) ((a b) (b b) (ks ks) (k k) (ta ta)))) + (origs (k (1 2)))) (defskeleton denning-sacco (vars (ta text) (a b ks b-0 a-0 name) (k skey)) @@ -249,6 +252,7 @@ (unrealized) (shape) (maps ((0) ((a a) (b b) (ks ks) (k k) (ta ta)))) + (origs (k (1 2))) (comment "1 in cohort - 0 not yet seen")) (defskeleton denning-sacco @@ -280,7 +284,8 @@ (parent 3) (unrealized) (shape) - (maps ((0) ((a b-0) (b b) (ks ks) (k k) (ta ta))))) + (maps ((0) ((a b-0) (b b) (ks ks) (k k) (ta ta)))) + (origs (k (1 2)))) (defskeleton denning-sacco (vars (ta text) (a b ks a-0 b-0 name) (k skey)) @@ -317,6 +322,7 @@ (unrealized) (shape) (maps ((0) ((a a) (b b) (ks ks) (k k) (ta ta)))) + (origs (k (1 2))) (comment "1 in cohort - 0 not yet seen")) (defskeleton denning-sacco @@ -346,7 +352,8 @@ (parent 4) (unrealized) (shape) - (maps ((0) ((a a) (b b) (ks ks) (k k) (ta ta))))) + (maps ((0) ((a a) (b b) (ks ks) (k k) (ta ta)))) + (origs (k (1 2)))) (defskeleton denning-sacco (vars (ta text) (a b ks a-0 a-1 name) (k skey)) @@ -383,6 +390,7 @@ (unrealized) (shape) (maps ((0) ((a a) (b b) (ks ks) (k k) (ta ta)))) + (origs (k (1 2))) (comment "1 in cohort - 0 not yet seen")) (defskeleton denning-sacco @@ -412,6 +420,7 @@ (parent 4) (unrealized) (shape) - (maps ((0) ((a b) (b b) (ks ks) (k k) (ta ta))))) + (maps ((0) ((a b) (b b) (ks ks) (k k) (ta ta)))) + (origs (k (1 2)))) (comment "Nothing left to do") diff --git a/tst/deorig_contract.tst b/tst/deorig_contract.tst --- a/tst/deorig_contract.tst +++ b/tst/deorig_contract.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol deorig-contract basic @@ -19,6 +19,7 @@ (traces ((send (enc x1 k)) (send (enc x2 k)) (recv (enc x1 x2 k)))) (label 0) (unrealized (0 2)) + (origs (x2 (0 1)) (x1 (0 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton deorig-contract @@ -60,6 +61,7 @@ (label 2) (unrealized) (shape) - (maps ((0 1) ((k k) (x1 x1) (x2 x2))))) + (maps ((0 1) ((k k) (x1 x1) (x2 x2)))) + (origs (x2 (0 1)) (x1 (0 0)))) (comment "Nothing left to do") diff --git a/tst/deorig_simple.tst b/tst/deorig_simple.tst --- a/tst/deorig_simple.tst +++ b/tst/deorig_simple.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol deorig-simple basic @@ -19,6 +19,7 @@ (traces ((send (enc x2 k)) (recv x2))) (label 0) (unrealized (0 1)) + (origs (x2 (0 0))) (comment "empty cohort")) (comment "Nothing left to do") @@ -44,6 +45,7 @@ (label 1) (unrealized) (shape) - (maps ((0 1) ((k k) (x2 x2))))) + (maps ((0 1) ((k k) (x2 x2)))) + (origs (x2 (0 0)))) (comment "Nothing left to do") diff --git a/tst/dh_cert.tst b/tst/dh_cert.tst --- a/tst/dh_cert.tst +++ b/tst/dh_cert.tst @@ -1,6 +1,6 @@ (herald "Diffie-Hellman with Certificate" (algebra diffie-hellman)) -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol dh-cert diffie-hellman @@ -88,6 +88,7 @@ (enc "hash" (cat (exp gB x) (exp gy as-ltv))))))) (label 0) (unrealized (0 3)) + (origs (x (0 0)) (as-ltv (0 0))) (comment "2 in cohort - 2 not yet seen")) (defskeleton dh-cert @@ -475,6 +476,7 @@ (label 6) (parent 3) (unrealized) + (origs (as-ltv (0 0)) (x (0 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton dh-cert @@ -735,6 +737,7 @@ (label 11) (parent 6) (unrealized) + (origs (as-ltv (0 0)) (x (0 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton dh-cert @@ -1038,6 +1041,7 @@ (label 17) (parent 11) (unrealized) + (origs (as-ltv (0 0)) (x (0 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton dh-cert @@ -1159,7 +1163,8 @@ (maps ((0) ((ca ca) (a a) (b b) (as-ltv as-ltv) (bs-ltv bs-ltv-0) (x x) - (gB (exp (gen) bs-ltv)) (gy (exp (gen) y)))))) + (gB (exp (gen) bs-ltv)) (gy (exp (gen) y))))) + (origs (as-ltv (0 0)) (x (0 0)))) (defskeleton dh-cert (vars (ca a b name) (as-ltv bs-ltv expn)) @@ -1194,6 +1199,7 @@ (parent 18) (seen 22) (unrealized) + (origs (as-ltv (0 0))) (comment "1 in cohort - 0 not yet seen")) (defskeleton dh-cert @@ -1232,7 +1238,8 @@ (maps ((0) ((ca ca) (a a) (b b) (as-ltv as-ltv) (bs-ltv bs-ltv) (x x) - (gB (gen)) (gy (gen)))))) + (gB (gen)) (gy (gen))))) + (origs (as-ltv (0 0)) (x (0 0)))) (comment "Nothing left to do") @@ -1320,6 +1327,7 @@ (enc "hash" (cat (exp gx bs-ltv) (exp gA y))))))) (label 23) (unrealized (0 2)) + (origs (y (0 1)) (bs-ltv (0 1))) (comment "2 in cohort - 2 not yet seen")) (defskeleton dh-cert @@ -1475,6 +1483,7 @@ (label 26) (parent 24) (unrealized) + (origs (y (0 1)) (bs-ltv (0 1))) (comment "1 in cohort - 1 not yet seen")) (defskeleton dh-cert @@ -1558,6 +1567,7 @@ (label 28) (parent 26) (unrealized) + (origs (y (0 1)) (bs-ltv (0 1))) (comment "1 in cohort - 1 not yet seen")) (defskeleton dh-cert @@ -1727,6 +1737,7 @@ (label 32) (parent 28) (unrealized) + (origs (y (0 1)) (bs-ltv (0 1))) (comment "1 in cohort - 1 not yet seen")) (defskeleton dh-cert @@ -1945,7 +1956,8 @@ (maps ((0) ((ca ca) (a a) (b b) (bs-ltv bs-ltv) (as-ltv as-ltv-0) (y y) - (gA (exp (gen) as-ltv)) (gx (exp (gen) x)))))) + (gA (exp (gen) as-ltv)) (gx (exp (gen) x))))) + (origs (y (0 1)) (bs-ltv (0 1)))) (defskeleton dh-cert (vars (ca a b name) (bs-ltv as-ltv expn)) @@ -2062,6 +2074,7 @@ (parent 38) (seen 41) (unrealized) + (origs (bs-ltv (0 1))) (comment "1 in cohort - 0 not yet seen")) (defskeleton dh-cert @@ -2102,6 +2115,7 @@ (maps ((0) ((ca ca) (a a) (b b) (bs-ltv bs-ltv) (as-ltv as-ltv) (y y) - (gA (gen)) (gx (gen)))))) + (gA (gen)) (gx (gen))))) + (origs (bs-ltv (0 1)) (y (0 1)))) (comment "Nothing left to do") diff --git a/tst/dhke.tst b/tst/dhke.tst --- a/tst/dhke.tst +++ b/tst/dhke.tst @@ -1,6 +1,6 @@ (herald "Diffie-Hellman Key Exchange" (algebra diffie-hellman)) -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol dhke diffie-hellman @@ -34,6 +34,7 @@ (recv (enc "i" a b (exp (exp (gen) x) y))))) (label 0) (unrealized (0 0)) + (origs (y (0 1))) (comment "1 in cohort - 1 not yet seen")) (defskeleton dhke @@ -82,7 +83,8 @@ (parent 1) (unrealized) (shape) - (maps ((0) ((a a) (b b) (x x) (y y))))) + (maps ((0) ((a a) (b b) (x x) (y y)))) + (origs (x (1 0)) (y (0 1)))) (defskeleton dhke (vars (a b name) (x y expn)) @@ -164,6 +166,7 @@ (enc a b (exp (exp (gen) x) y)))))) (label 5) (unrealized (0 1)) + (origs (x (0 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton dhke @@ -212,7 +215,8 @@ (parent 6) (unrealized) (shape) - (maps ((0) ((a a) (b b) (x x) (y y))))) + (maps ((0) ((a a) (b b) (x x) (y y)))) + (origs (y (1 1)) (x (0 0)))) (defskeleton dhke (vars (a b a-0 name) (x y x-0 expn)) @@ -308,7 +312,8 @@ (parent 10) (unrealized) (shape) - (maps ((0 1) ((n n) (x x) (y y))))) + (maps ((0 1) ((n n) (x x) (y y)))) + (origs (x (0 0)) (n (0 2)))) (comment "Nothing left to do") @@ -337,6 +342,7 @@ (recv (enc "i" a b (exp h y))))) (label 12) (unrealized (0 0) (0 2)) + (origs (y (0 1))) (comment "1 in cohort - 1 not yet seen")) (defskeleton dhke-with-base-vars @@ -385,7 +391,8 @@ (parent 13) (unrealized) (shape) - (maps ((0) ((a a) (b b) (h (exp (gen) x)) (y y))))) + (maps ((0) ((a a) (b b) (h (exp (gen) x)) (y y)))) + (origs (x (1 0)) (y (0 1)))) (defskeleton dhke-with-base-vars (vars (a b name) (y x expn)) @@ -461,6 +468,7 @@ (recv (cat (enc g (privk b)) (enc a b (exp g x)))))) (label 17) (unrealized (0 1)) + (origs (x (0 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton dhke-with-base-vars @@ -507,7 +515,8 @@ (parent 18) (unrealized) (shape) - (maps ((0) ((a a) (b b) (g (exp (gen) y)) (x x))))) + (maps ((0) ((a a) (b b) (g (exp (gen) y)) (x x)))) + (origs (y (1 1)) (x (0 0)))) (defskeleton dhke-with-base-vars (vars (a b a-0 name) (h base) (x y expn)) @@ -595,6 +604,7 @@ (parent 22) (seen 24) (unrealized (1 2)) + (origs (y (1 1)) (x (0 0)) (n (0 2))) (comment "3 in cohort - 2 not yet seen")) (defskeleton dh-mim-with-base-vars @@ -615,7 +625,8 @@ (unrealized) (shape) (maps - ((0 1) ((n n) (x x) (hy (exp (gen) y)) (y y) (hx (exp (gen) x)))))) + ((0 1) ((n n) (x x) (hy (exp (gen) y)) (y y) (hx (exp (gen) x))))) + (origs (n (0 2)) (x (0 0)) (y (1 1)))) (defskeleton dh-mim-with-base-vars (vars (n text) (hy hx base) (x y expn)) @@ -760,7 +771,8 @@ (parent 31) (unrealized) (shape) - (maps ((0 1) ((n n) (x x) (hy (gen)) (y y) (hx (gen)))))) + (maps ((0 1) ((n n) (x x) (hy (gen)) (y y) (hx (gen))))) + (origs (x (0 0)) (y (1 1)) (n (0 2)))) (comment "Nothing left to do") @@ -799,6 +811,7 @@ (label 34) (parent 33) (unrealized (1 0)) + (origs (x (0 0)) (n (0 2))) (comment "1 in cohort - 1 not yet seen")) (defskeleton dh-mim-with-base-vars @@ -865,6 +878,7 @@ (parent 36) (unrealized) (shape) - (maps ((0 1) ((n n) (x x) (hy (gen)))))) + (maps ((0 1) ((n n) (x x) (hy (gen))))) + (origs (x (0 0)) (n (0 2)))) (comment "Nothing left to do") diff --git a/tst/dy.tst b/tst/dy.tst --- a/tst/dy.tst +++ b/tst/dy.tst @@ -1,6 +1,6 @@ (herald "Example 1.3 from 1983 Dolev-Yao Paper") -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol dy basic @@ -23,6 +23,7 @@ (recv (enc (enc m (pubk a)) b (pubk a))))) (label 0) (unrealized (0 1)) + (origs (m (0 0))) (comment "3 in cohort - 3 not yet seen")) (defskeleton dy @@ -39,7 +40,8 @@ (parent 0) (unrealized) (shape) - (maps ((0) ((a b) (b b) (m m))))) + (maps ((0) ((a b) (b b) (m m)))) + (origs (m (0 0)))) (defskeleton dy (vars (m text) (a b name)) @@ -59,7 +61,8 @@ (parent 0) (unrealized) (shape) - (maps ((0) ((a a) (b b) (m m))))) + (maps ((0) ((a a) (b b) (m m)))) + (origs (m (0 0)))) (defskeleton dy (vars (m text) (a b a-0 name)) @@ -194,7 +197,8 @@ (parent 5) (unrealized) (shape) - (maps ((0) ((a a) (b b) (m m))))) + (maps ((0) ((a a) (b b) (m m)))) + (origs (m (0 0)))) (defskeleton dy (vars (m text) (a b a-0 name)) diff --git a/tst/encsig.tst b/tst/encsig.tst --- a/tst/encsig.tst +++ b/tst/encsig.tst @@ -1,7 +1,7 @@ (herald "Encrypted Signed Message Example" (comment "Shows examples of key usage of asymmetric keys")) -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol mult-keys-enc-sig basic @@ -27,6 +27,7 @@ (send (enc (enc n2 (pubk "enc" b)) (privk "sig" a))))) (label 0) (unrealized (0 1)) + (origs (n1 (0 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton mult-keys-enc-sig @@ -48,7 +49,8 @@ (parent 0) (unrealized) (shape) - (maps ((0) ((a a) (b b) (n1 n1) (n2 n2))))) + (maps ((0) ((a a) (b b) (n1 n1) (n2 n2)))) + (origs (n1 (0 0)))) (comment "Nothing left to do") @@ -75,6 +77,7 @@ (recv (enc (enc n2 (pubk "enc" b)) (privk "sig" a))))) (label 2) (unrealized (0 0) (0 2)) + (origs (n2 (0 1))) (comment "1 in cohort - 1 not yet seen")) (defskeleton mult-keys-enc-sig @@ -120,6 +123,7 @@ (unrealized) (shape) (maps ((0) ((a a) (b b) (n2 n2) (n1 n1)))) + (origs (n2 (0 1))) (comment "1 in cohort - 0 not yet seen")) (defskeleton mult-keys-enc-sig @@ -142,7 +146,8 @@ (parent 3) (unrealized) (shape) - (maps ((0) ((a a) (b b) (n2 n2) (n1 n1))))) + (maps ((0) ((a a) (b b) (n2 n2) (n1 n1)))) + (origs (n2 (0 1)))) (comment "Nothing left to do") @@ -169,6 +174,7 @@ (recv (enc (enc n2 (pubk "enc" b)) (privk "sig" a))))) (label 6) (unrealized (0 2)) + (origs (n2 (0 1))) (comment "1 in cohort - 1 not yet seen")) (defskeleton mult-keys-enc-sig @@ -191,7 +197,8 @@ (parent 6) (unrealized) (shape) - (maps ((0) ((a a) (b b) (n2 n2) (n1 n1))))) + (maps ((0) ((a a) (b b) (n2 n2) (n1 n1)))) + (origs (n2 (0 1)))) (comment "Nothing left to do") @@ -218,6 +225,7 @@ (recv (enc (enc n2 (pubk "enc" b)) (privk "sig" a))))) (label 8) (unrealized (0 0) (0 2)) + (origs (n2 (0 1))) (comment "1 in cohort - 1 not yet seen")) (defskeleton mult-keys-enc-sig @@ -282,7 +290,8 @@ (parent 9) (unrealized) (shape) - (maps ((0) ((a a) (b b) (n2 n2) (n1 n1))))) + (maps ((0) ((a a) (b b) (n2 n2) (n1 n1)))) + (origs (n2 (0 1)))) (defskeleton mult-keys-enc-sig (vars (n2 n1 text) (a b name)) @@ -308,6 +317,7 @@ (unrealized) (shape) (maps ((0) ((a a) (b b) (n2 n2) (n1 n1)))) + (origs (n2 (0 1))) (comment "1 in cohort - 0 not yet seen")) (defskeleton mult-keys-enc-sig @@ -338,6 +348,7 @@ (unrealized) (shape) (maps ((0) ((a a) (b b) (n2 n2) (n1 n1)))) + (origs (n2 (0 1))) (comment "2 in cohort - 1 not yet seen")) (defskeleton mult-keys-enc-sig diff --git a/tst/epmo-key-hash.tst b/tst/epmo-key-hash.tst --- a/tst/epmo-key-hash.tst +++ b/tst/epmo-key-hash.tst @@ -1,7 +1,7 @@ (herald "Electronic Purchase with Money Order Protocol with Key Hashing" (comment "Annotated with trust management formulas")) -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol epmo basic @@ -84,6 +84,7 @@ (cat (enc (enc "hash" (cat c nc nb nm price)) (privk b)) nb)))) (label 0) (unrealized (0 1) (0 3)) + (origs (nc (0 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton epmo @@ -207,7 +208,8 @@ (maps ((0) ((b b) (c c) (m m) (nb nb) (nc nc) (nm nm) (goods goods) - (price price))))) + (price price)))) + (origs (nc (0 0)) (nb (2 1)) (nm (1 1)))) (comment "Nothing left to do") @@ -288,6 +290,7 @@ (recv (enc (enc "hash" (cat b nb nm)) (privk m))))) (label 5) (unrealized (0 2)) + (origs (nb (0 1))) (comment "1 in cohort - 1 not yet seen")) (defskeleton epmo @@ -547,8 +550,8 @@ (parent 11) (unrealized) (shape) - (maps - ((0) ((b b) (c c) (m m) (nc nc) (nm nm) (nb nb) (price price))))) + (maps ((0) ((b b) (c c) (m m) (nc nc) (nm nm) (nb nb) (price price)))) + (origs (nc (2 0)) (nb (0 1)) (nm (1 1)))) (comment "Nothing left to do") @@ -629,6 +632,7 @@ (send (enc (enc "hash" (cat b nb nm)) (privk m))))) (label 13) (unrealized (0 2)) + (origs (nm (0 1))) (comment "1 in cohort - 1 not yet seen")) (defskeleton epmo @@ -726,6 +730,7 @@ (maps ((0) ((b b) (c c) (m m) (nb nb) (nc nc) (nm nm) (goods goods) - (price price))))) + (price price)))) + (origs (nc (2 0)) (nb (1 1)) (nm (0 1)))) (comment "Nothing left to do") diff --git a/tst/epmo.tst b/tst/epmo.tst --- a/tst/epmo.tst +++ b/tst/epmo.tst @@ -1,7 +1,7 @@ (herald "Electronic Purchase with Money Order Protocol" (comment "Annotated with trust management formulas")) -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol epmo basic @@ -84,6 +84,7 @@ (send (cat (enc (enc c nc nb nm price hash) (privk b)) nb)))) (label 0) (unrealized (0 1) (0 3)) + (origs (nc (0 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton epmo @@ -206,7 +207,8 @@ (maps ((0) ((b b) (c c) (m m) (hash hash) (nb nb) (nc nc) (nm nm) - (goods goods) (price price))))) + (goods goods) (price price)))) + (origs (nc (0 0)) (nb (2 1)) (nm (1 1)))) (comment "Nothing left to do") @@ -288,6 +290,7 @@ (recv (enc (enc b nb nm hash) (privk m))))) (label 5) (unrealized (0 2)) + (origs (nb (0 1))) (comment "1 in cohort - 1 not yet seen")) (defskeleton epmo @@ -456,7 +459,8 @@ (maps ((0) ((b b) (c c) (m m) (hash hash) (nc nc) (nm nm) (nb nb) - (price price))))) + (price price)))) + (origs (nc (2 0)) (nb (0 1)) (nm (1 1)))) (comment "Nothing left to do") @@ -537,6 +541,7 @@ (send (enc (enc b nb nm hash) (privk m))))) (label 11) (unrealized (0 2)) + (origs (nm (0 1))) (comment "1 in cohort - 1 not yet seen")) (defskeleton epmo @@ -632,6 +637,7 @@ (maps ((0) ((b b) (c c) (m m) (hash hash) (nb nb) (nc nc) (nm nm) - (goods goods) (price price))))) + (goods goods) (price price)))) + (origs (nc (2 0)) (nb (1 1)) (nm (0 1)))) (comment "Nothing left to do") diff --git a/tst/epmo_acctnum-key-hash.tst b/tst/epmo_acctnum-key-hash.tst --- a/tst/epmo_acctnum-key-hash.tst +++ b/tst/epmo_acctnum-key-hash.tst @@ -3,7 +3,7 @@ (displacement) (comment "This version includes account numbers in exchanges")) -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (comment "Displacement disabled") @@ -92,6 +92,7 @@ (send (enc (enc "hash" (cat b m nb nm)) (privk m))))) (label 0) (unrealized (0 2)) + (origs (nm (0 1))) (comment "1 in cohort - 1 not yet seen")) (defskeleton epmo_acctnum @@ -291,7 +292,8 @@ (maps ((0) ((b b) (m m) (c c) (nm nm) (nc nc) (nb nb) (goods goods) - (price price))))) + (price price)))) + (origs (nc (2 0)) (nm (0 1)) (nb (1 1)))) (defskeleton epmo_acctnum (vars (nm nc nb price acctnum goods nm-0 price-0 text) (m c b name)) @@ -459,6 +461,7 @@ (recv (enc (enc "hash" (cat b m nb nm)) (privk m))))) (label 9) (unrealized (0 2)) + (origs (nb (0 1))) (comment "1 in cohort - 1 not yet seen")) (defskeleton epmo_acctnum @@ -838,7 +841,8 @@ (maps ((0) ((b b) (m m) (c c) (nm nm) (nb nb) (nc nc) (acctnum acctnum) - (price price))))) + (price price)))) + (origs (nc (2 0)) (nm (1 1)) (nb (0 1)))) (defskeleton epmo_acctnum (vars (nm nb nc acctnum price acctnum-0 goods nm-0 price-0 text) diff --git a/tst/epmo_acctnum.tst b/tst/epmo_acctnum.tst --- a/tst/epmo_acctnum.tst +++ b/tst/epmo_acctnum.tst @@ -2,7 +2,7 @@ (displacement) (comment "This version includes account numbers in exchanges")) -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (comment "Displacement disabled") @@ -96,6 +96,7 @@ (send (enc (enc "hash" b m nb nm (pubk hash)) (privk m))))) (label 0) (unrealized (0 2)) + (origs (nm (0 1))) (comment "1 in cohort - 1 not yet seen")) (defskeleton epmo_acctnum @@ -387,7 +388,8 @@ (maps ((0) ((b b) (m m) (c c) (nm nm) (nc nc) (nb nb) (hash hash) - (goods goods) (price price))))) + (goods goods) (price price)))) + (origs (nc (2 0)) (nm (0 1)) (nb (1 1)))) (defskeleton epmo_acctnum (vars (nm nc nb price acctnum goods nm-0 price-0 text) @@ -836,6 +838,7 @@ (recv (enc (enc "hash" b m nb nm (pubk hash)) (privk m))))) (label 17) (unrealized (0 2)) + (origs (nb (0 1))) (comment "1 in cohort - 1 not yet seen")) (defskeleton epmo_acctnum @@ -1232,7 +1235,8 @@ (maps ((0) ((b b) (m m) (c c) (nm nm) (nb nb) (nc nc) (hash hash) - (acctnum acctnum) (price price))))) + (acctnum acctnum) (price price)))) + (origs (nc (2 0)) (nm (1 1)) (nb (0 1)))) (defskeleton epmo_acctnum (vars (nm nb nc acctnum price acctnum-0 goods nb-0 text) diff --git a/tst/ffgg.tst b/tst/ffgg.tst --- a/tst/ffgg.tst +++ b/tst/ffgg.tst @@ -1,7 +1,7 @@ (herald "The ffgg Protocol" (comment "From A Necessarily Parallel Attack by Jon K. Millen")) -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol ffgg basic @@ -44,6 +44,7 @@ (label 1) (parent 0) (unrealized (1 0)) + (origs (m (0 2))) (comment "1 in cohort - 1 not yet seen")) (defskeleton ffgg @@ -119,6 +120,7 @@ (parent 3) (unrealized) (shape) - (maps ((0 1) ((b b) (m m) (a a) (n1 n1) (n2 n2) (x x) (y y))))) + (maps ((0 1) ((b b) (m m) (a a) (n1 n1) (n2 n2) (x x) (y y)))) + (origs (n1 (2 1)) (n2-0 (2 1)) (n2 (3 1)) (n2-1 (3 1)) (m (0 2)))) (comment "Nothing left to do") diff --git a/tst/fragile_pruning.tst b/tst/fragile_pruning.tst --- a/tst/fragile_pruning.tst +++ b/tst/fragile_pruning.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol fragile_pruning basic @@ -28,6 +28,7 @@ (recv (enc n n1 n2 n3 n k)))) (label 0) (unrealized (0 1) (0 2) (0 3) (0 5)) + (origs (n (0 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton fragile_pruning @@ -147,6 +148,7 @@ (parent 5) (unrealized) (shape) - (maps ((0) ((k k) (n n) (n1 new) (n2 new) (n3 new))))) + (maps ((0) ((k k) (n n) (n1 new) (n2 new) (n3 new)))) + (origs (n (0 0)) (new (1 1)))) (comment "Nothing left to do") diff --git a/tst/isoreject.tst b/tst/isoreject.tst --- a/tst/isoreject.tst +++ b/tst/isoreject.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol isoreject basic @@ -22,6 +22,7 @@ (recv (enc nc nb b (privk a))))) (label 0) (unrealized (0 2)) + (origs (nb (0 1))) (comment "2 in cohort - 2 not yet seen")) (defskeleton isoreject @@ -61,7 +62,8 @@ (parent 0) (unrealized) (shape) - (maps ((0) ((a a) (b b) (na na) (nb nb) (nc nc))))) + (maps ((0) ((a a) (b b) (na na) (nb nb) (nc nc)))) + (origs (nc (1 1)) (nb (0 1)))) (defskeleton isoreject (vars (na nb nc text) (a b name)) @@ -81,7 +83,8 @@ (parent 1) (unrealized) (shape) - (maps ((0) ((a a) (b b) (na na) (nb nb) (nc nc))))) + (maps ((0) ((a a) (b b) (na na) (nb nb) (nc nc)))) + (origs (nb (0 1)))) (comment "Nothing left to do") @@ -105,6 +108,7 @@ (send (enc nc nb b (privk a))))) (label 4) (unrealized (0 1)) + (origs) (comment "2 in cohort - 2 not yet seen")) (defskeleton isoreject @@ -124,7 +128,8 @@ (parent 4) (unrealized) (shape) - (maps ((0) ((b b) (a a) (na na) (nb nb) (nc nc))))) + (maps ((0) ((b b) (a a) (na na) (nb nb) (nc nc)))) + (origs)) (defskeleton isoreject (vars (na nb nc text) (b a name)) @@ -143,6 +148,7 @@ (parent 4) (unrealized) (shape) - (maps ((0) ((b b) (a a) (na na) (nb nb) (nc nc))))) + (maps ((0) ((b b) (a a) (na na) (nb nb) (nc nc)))) + (origs (nb (1 1)))) (comment "Nothing left to do") diff --git a/tst/kelly1.tst b/tst/kelly1.tst --- a/tst/kelly1.tst +++ b/tst/kelly1.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol kelly1 basic @@ -41,6 +41,7 @@ (recv (cat A C (enc policy (pubk S) Ns (privk A)))))) (label 0) (unrealized (0 3)) + (origs) (comment "1 in cohort - 1 not yet seen")) (defskeleton kelly1 @@ -147,6 +148,7 @@ (maps ((0) ((A A) (C C) (S S) (Ns Ns) (request request) (Check Check) - (policy policy) (response response))))) + (policy policy) (response response)))) + (origs (Ns (2 2)) (N (1 1)))) (comment "Nothing left to do") diff --git a/tst/kerberos.tst b/tst/kerberos.tst --- a/tst/kerberos.tst +++ b/tst/kerberos.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol kerberos basic @@ -30,6 +30,7 @@ (recv (enc t-prime k)))) (label 0) (unrealized (0 1)) + (origs) (comment "2 in cohort - 2 not yet seen")) (defskeleton kerberos @@ -431,8 +432,8 @@ (parent 8) (unrealized) (shape) - (maps - ((0) ((a a) (b b) (ks ks) (t t) (t-prime t-prime) (l l) (k k))))) + (maps ((0) ((a a) (b b) (ks ks) (t t) (t-prime t-prime) (l l) (k k)))) + (origs (k (1 1)))) (defskeleton kerberos (vars (t t-prime l l-0 text) (a b ks b-0 ks-0 name) (k skey)) @@ -521,8 +522,8 @@ (parent 11) (unrealized) (shape) - (maps - ((0) ((a a) (b b) (ks ks) (t t) (t-prime t-prime) (l l) (k k))))) + (maps ((0) ((a a) (b b) (ks ks) (t t) (t-prime t-prime) (l l) (k k)))) + (origs (k (1 1)))) (defskeleton kerberos (vars (t t-prime l text) (a b ks name) (k skey)) @@ -554,6 +555,7 @@ (unrealized) (shape) (maps ((0) ((a a) (b b) (ks ks) (t t) (t-prime t-prime) (l l) (k k)))) + (origs (k (1 1))) (comment "1 in cohort - 1 not yet seen")) (defskeleton kerberos @@ -587,6 +589,7 @@ (unrealized) (shape) (maps ((0) ((a a) (b b) (ks ks) (t t) (t-prime t-prime) (l l) (k k)))) + (origs (k (1 1))) (comment "1 in cohort - 0 not yet seen")) (defskeleton kerberos @@ -620,6 +623,7 @@ (unrealized) (shape) (maps ((0) ((a a) (b b) (ks ks) (t t) (t-prime t-prime) (l l) (k k)))) + (origs (k (1 1))) (comment "1 in cohort - 0 not yet seen")) (defskeleton kerberos @@ -653,6 +657,7 @@ (unrealized) (shape) (maps ((0) ((a a) (b b) (ks ks) (t t) (t-prime t-prime) (l l) (k k)))) + (origs (k (1 1))) (comment "1 in cohort - 0 not yet seen")) (defskeleton kerberos @@ -710,6 +715,7 @@ (send (enc t-prime k)))) (label 24) (unrealized (0 0)) + (origs) (comment "2 in cohort - 2 not yet seen")) (defskeleton kerberos @@ -867,8 +873,8 @@ (parent 27) (unrealized) (shape) - (maps - ((0) ((a a) (b b) (ks ks) (t t) (t-prime t-prime) (l l) (k k))))) + (maps ((0) ((a a) (b b) (ks ks) (t t) (t-prime t-prime) (l l) (k k)))) + (origs (k (1 1)))) (defskeleton kerberos (vars (t t-prime l text) (a b ks name) (k skey)) @@ -893,8 +899,8 @@ (parent 29) (unrealized) (shape) - (maps - ((0) ((a a) (b b) (ks ks) (t t) (t-prime t-prime) (l l) (k k))))) + (maps ((0) ((a a) (b b) (ks ks) (t t) (t-prime t-prime) (l l) (k k)))) + (origs (k (1 1)))) (comment "Nothing left to do") @@ -926,6 +932,7 @@ (label 33) (unrealized) (shape) - (maps ((0) ((a a) (b b) (ks ks) (t t) (l l) (k k))))) + (maps ((0) ((a a) (b b) (ks ks) (t t) (l l) (k k)))) + (origs (k (0 1)))) (comment "Nothing left to do") diff --git a/tst/missing_contraction.tst b/tst/missing_contraction.tst --- a/tst/missing_contraction.tst +++ b/tst/missing_contraction.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol missing-contraction basic @@ -21,6 +21,7 @@ (label 0) (seen 2) (unrealized (1 0)) + (origs (m (0 0))) (comment "3 in cohort - 2 not yet seen")) (defskeleton missing-contraction @@ -37,7 +38,8 @@ (parent 0) (unrealized) (shape) - (maps ((0 1) ((m m) (a a) (c a) (n n) (b b))))) + (maps ((0 1) ((m m) (a a) (c a) (n n) (b b)))) + (origs (m (0 0)))) (defskeleton missing-contraction (vars (n text) (a c b name)) @@ -54,7 +56,8 @@ (parent 0) (unrealized) (shape) - (maps ((0 1) ((m n) (a a) (c c) (n n) (b b))))) + (maps ((0 1) ((m n) (a a) (c c) (n n) (b b)))) + (origs (n (0 0)))) (comment "Nothing left to do") @@ -92,6 +95,7 @@ (parent 3) (seen 6) (unrealized (1 0)) + (origs (m (0 0))) (comment "3 in cohort - 2 not yet seen")) (defskeleton missing-contraction @@ -108,7 +112,8 @@ (parent 4) (unrealized) (shape) - (maps ((0 1) ((m m) (a a) (c a))))) + (maps ((0 1) ((m m) (a a) (c a)))) + (origs (m (0 0)))) (defskeleton missing-contraction (vars (m text) (c a b name)) @@ -125,7 +130,8 @@ (parent 4) (unrealized) (shape) - (maps ((1 0) ((m m) (a a) (c c))))) + (maps ((1 0) ((m m) (a a) (c c)))) + (origs (m (1 0)))) (comment "Nothing left to do") @@ -149,6 +155,7 @@ (label 7) (seen 9) (unrealized (1 0)) + (origs (m (0 0))) (comment "3 in cohort - 2 not yet seen")) (defskeleton missing-contraction @@ -165,7 +172,8 @@ (parent 7) (unrealized) (shape) - (maps ((0 1) ((m m) (a a) (b b) (c a) (n n))))) + (maps ((0 1) ((m m) (a a) (b b) (c a) (n n)))) + (origs (m (0 0)))) (defskeleton missing-contraction (vars (n text) (a b c name)) @@ -181,6 +189,7 @@ (label 9) (parent 7) (unrealized (1 0)) + (origs (n (0 0))) (comment "2 in cohort - 2 not yet seen")) (defskeleton missing-contraction @@ -198,7 +207,8 @@ (parent 9) (unrealized) (shape) - (maps ((0 1) ((m n) (a a) (b b) (c b) (n n))))) + (maps ((0 1) ((m n) (a a) (b b) (c b) (n n)))) + (origs (n (0 0)))) (defskeleton missing-contraction (vars (n text) (a b name)) @@ -215,6 +225,7 @@ (parent 9) (seen 8) (unrealized) + (origs (n (0 0))) (comment "1 in cohort - 0 not yet seen")) (comment "Nothing left to do") diff --git a/tst/neuman-stubblebine-reauth.tst b/tst/neuman-stubblebine-reauth.tst --- a/tst/neuman-stubblebine-reauth.tst +++ b/tst/neuman-stubblebine-reauth.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol neuman-stubblebine-reauth basic @@ -41,6 +41,7 @@ (send (cat rb-prime (enc ra-prime k))) (recv (enc rb-prime k)))) (label 0) (unrealized (0 2) (1 0)) + (origs (rb (0 1)) (rb-prime (1 1))) (comment "1 in cohort - 1 not yet seen")) (defskeleton neuman-stubblebine-reauth @@ -1237,7 +1238,8 @@ (maps ((0 1) ((ra ra) (tb tb) (rb ra-prime) (a a) (b b) (ks ks) (k k) - (ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))) + (ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb)))) + (origs (k (2 1)) (ra-prime (0 1)) (rb-prime (1 1)))) (defskeleton neuman-stubblebine-reauth (vars (ra tb rb ra-prime rb-prime rb-0 rb-prime-0 text) (a b ks name) @@ -1633,6 +1635,7 @@ ((0 1) ((ra ra) (tb tb) (rb ra-prime) (a a) (b b) (ks ks) (k k) (ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb)))) + (origs (k (2 1)) (ra-prime (0 1)) (rb-prime (1 1))) (comment "1 in cohort - 0 not yet seen")) (defskeleton neuman-stubblebine-reauth @@ -1822,7 +1825,8 @@ (maps ((0 1) ((ra ra) (tb tb) (rb ra-prime) (a a) (b b) (ks ks) (k k) - (ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))) + (ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb)))) + (origs (k (2 1)) (ra (3 0)) (ra-prime (0 1)) (rb-prime (1 1)))) (defskeleton neuman-stubblebine-reauth (vars (ra tb rb ra-prime rb-prime rb-0 text) (a b ks name) (k skey)) @@ -2227,6 +2231,7 @@ ((0 1) ((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k) (ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb)))) + (origs (k (2 1)) (rb (0 1)) (rb-prime (1 1))) (comment "1 in cohort - 0 not yet seen")) (defskeleton neuman-stubblebine-reauth @@ -2396,6 +2401,7 @@ ((0 1) ((ra ra) (tb tb) (rb ra-prime) (a a) (b b) (ks ks) (k k) (ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb)))) + (origs (k (2 1)) (ra-prime (0 1)) (rb-prime (1 1))) (comment "1 in cohort - 0 not yet seen")) (defskeleton neuman-stubblebine-reauth @@ -3038,6 +3044,7 @@ ((0 1) ((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k) (ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb)))) + (origs (k (2 1)) (rb (0 1)) (rb-prime (1 1))) (comment "2 in cohort - 0 not yet seen")) (defskeleton neuman-stubblebine-reauth @@ -3160,6 +3167,7 @@ ((0 1) ((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k) (ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb)))) + (origs (k (2 1)) (ra (3 0)) (rb (0 1)) (rb-prime (1 1))) (comment "1 in cohort - 0 not yet seen")) (defskeleton neuman-stubblebine-reauth @@ -3585,7 +3593,8 @@ (maps ((0 1) ((ra ra) (tb tb) (rb ra-prime) (a a) (b b) (ks ks) (k k) - (ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))) + (ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb)))) + (origs (k (2 1)) (ra-prime (0 1)) (rb-prime (1 1)))) (defskeleton neuman-stubblebine-reauth (vars (ra tb rb ra-prime rb-prime rb-0 ra-prime-0 rb-prime-0 text) @@ -3737,7 +3746,8 @@ (maps ((0 1) ((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k) - (ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))) + (ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb)))) + (origs (k (2 1)) (rb (0 1)) (ra-prime (3 1)) (rb-prime (1 1)))) (defskeleton neuman-stubblebine-reauth (vars (ra tb rb ra-prime rb-prime rb-0 rb-prime-0 text) (a b ks name) @@ -3776,7 +3786,8 @@ (maps ((0 1) ((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k) - (ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))) + (ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb)))) + (origs (k (2 1)) (ra (4 0)) (rb (0 1)) (rb-prime (1 1)))) (defskeleton neuman-stubblebine-reauth (vars @@ -3944,7 +3955,8 @@ (maps ((0 1) ((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k) - (ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))) + (ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb)))) + (origs (k (2 1)) (rb (0 1)) (ra-prime (4 1)) (rb-prime (1 1)))) (defskeleton neuman-stubblebine-reauth (vars (ra tb rb ra-prime rb-prime rb-0 rb-prime-0 ra-prime-0 text) @@ -4114,6 +4126,7 @@ ((0 1) ((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k) (ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb)))) + (origs (k (2 1)) (rb (0 1)) (rb-prime (1 1))) (comment "2 in cohort - 0 not yet seen")) (defskeleton neuman-stubblebine-reauth @@ -4536,6 +4549,7 @@ ((0 1) ((ra ra) (tb tb) (rb ra-prime) (a a) (b b) (ks ks) (k k) (ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb)))) + (origs (k (2 1)) (ra-prime (0 1)) (rb-prime (1 1))) (comment "1 in cohort - 0 not yet seen")) (defskeleton neuman-stubblebine-reauth @@ -4703,6 +4717,7 @@ ((0 1) ((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k) (ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb)))) + (origs (k (2 1)) (rb (0 1)) (ra-prime (4 1)) (rb-prime (1 1))) (comment "1 in cohort - 0 not yet seen")) (defskeleton neuman-stubblebine-reauth @@ -4748,6 +4763,7 @@ ((0 1) ((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k) (ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb)))) + (origs (k (2 1)) (rb (0 1)) (rb-prime (1 1))) (comment "1 in cohort - 0 not yet seen")) (defskeleton neuman-stubblebine-reauth @@ -4933,6 +4949,7 @@ ((0 1) ((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k) (ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb)))) + (origs (k (2 1)) (rb (0 1)) (ra-prime (5 1)) (rb-prime (1 1))) (comment "1 in cohort - 0 not yet seen")) (defskeleton neuman-stubblebine-reauth @@ -5157,7 +5174,9 @@ (maps ((0 1) ((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k) - (ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))) + (ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb)))) + (origs (k (2 1)) (ra (3 0)) (rb (0 1)) (ra-prime (4 1)) + (rb-prime (1 1)))) (defskeleton neuman-stubblebine-reauth (vars (ra tb rb ra-prime rb-prime rb-0 ra-prime-0 text) (a b ks name) @@ -5381,7 +5400,8 @@ (maps ((0 1) ((ra ra) (tb tb) (rb ra-prime) (a a) (b b) (ks ks) (k k) - (ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))) + (ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb)))) + (origs (k (2 1)) (ra (4 0)) (ra-prime (0 1)) (rb-prime (1 1)))) (defskeleton neuman-stubblebine-reauth (vars (ra tb rb ra-prime rb-prime rb-0 ra-prime-0 text) (a b ks name) @@ -5868,6 +5888,7 @@ ((0 1) ((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k) (ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb)))) + (origs (k (2 1)) (rb (0 1)) (rb-prime (1 1))) (comment "2 in cohort - 0 not yet seen")) (defskeleton neuman-stubblebine-reauth @@ -5907,7 +5928,9 @@ (maps ((0 1) ((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k) - (ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))) + (ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb)))) + (origs (k (2 1)) (ra (4 0)) (rb (0 1)) (ra-prime (3 1)) + (rb-prime (1 1)))) (defskeleton neuman-stubblebine-reauth (vars (ra tb rb ra-prime rb-prime rb-0 ra-prime-0 ra-0 tb-0 text) @@ -6215,6 +6238,7 @@ ((0 1) ((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k) (ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb)))) + (origs (k (2 1)) (rb (0 1)) (rb-prime (1 1))) (comment "1 in cohort - 0 not yet seen")) (defskeleton neuman-stubblebine-reauth @@ -6261,7 +6285,8 @@ (maps ((0 1) ((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k) - (ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))) + (ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb)))) + (origs (k (2 1)) (rb (0 1)) (rb-prime (1 1)))) (defskeleton neuman-stubblebine-reauth (vars @@ -6458,6 +6483,7 @@ ((0 1) ((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k) (ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb)))) + (origs (k (2 1)) (rb (0 1)) (ra-prime (5 1)) (rb-prime (1 1))) (comment "1 in cohort - 0 not yet seen")) (defskeleton neuman-stubblebine-reauth @@ -6699,6 +6725,7 @@ ((0 1) ((ra ra) (tb tb) (rb ra-prime) (a a) (b b) (ks ks) (k k) (ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb)))) + (origs (k (2 1)) (ra-prime (0 1)) (rb-prime (1 1))) (comment "1 in cohort - 0 not yet seen")) (defskeleton neuman-stubblebine-reauth diff --git a/tst/neuman-stubblebine.tst b/tst/neuman-stubblebine.tst --- a/tst/neuman-stubblebine.tst +++ b/tst/neuman-stubblebine.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol neuman-stubblebine basic @@ -29,6 +29,7 @@ (send (cat (enc a k tb (ltk b ks)) (enc rb k))))) (label 0) (unrealized (0 1)) + (origs (ra (0 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton neuman-stubblebine @@ -76,7 +77,8 @@ (parent 1) (unrealized) (shape) - (maps ((0) ((a a) (b b) (ks ks) (ra ra) (rb rb) (k k) (tb tb))))) + (maps ((0) ((a a) (b b) (ks ks) (ra ra) (rb rb) (k k) (tb tb)))) + (origs (k (1 1)) (ra (0 0)))) (comment "Nothing left to do") @@ -107,6 +109,7 @@ (recv (cat (enc a k tb (ltk b ks)) (enc rb k))))) (label 3) (unrealized (0 2)) + (origs (rb (0 1))) (comment "1 in cohort - 1 not yet seen")) (defskeleton neuman-stubblebine @@ -370,6 +373,7 @@ (unrealized) (shape) (maps ((0) ((a a) (b b) (ks ks) (ra ra) (rb rb) (k k) (tb tb)))) + (origs (k (1 1)) (rb (0 1))) (comment "1 in cohort - 0 not yet seen")) (defskeleton neuman-stubblebine @@ -396,7 +400,8 @@ (parent 12) (unrealized) (shape) - (maps ((0) ((a a) (b b) (ks ks) (ra ra) (rb rb) (k k) (tb tb))))) + (maps ((0) ((a a) (b b) (ks ks) (ra ra) (rb rb) (k k) (tb tb)))) + (origs (k (1 1)) (ra (2 0)) (rb (0 1)))) (comment "Nothing left to do") @@ -429,6 +434,7 @@ (cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb)))) (label 15) (unrealized (0 0)) + (origs (k (0 1))) (comment "1 in cohort - 1 not yet seen")) (defskeleton neuman-stubblebine @@ -450,6 +456,7 @@ (parent 15) (unrealized) (shape) - (maps ((0) ((a a) (b b) (ks ks) (ra ra) (rb rb) (k k) (tb tb))))) + (maps ((0) ((a a) (b b) (ks ks) (ra ra) (rb rb) (k k) (tb tb)))) + (origs (k (0 1)))) (comment "Nothing left to do") diff --git a/tst/no_contraction.tst b/tst/no_contraction.tst --- a/tst/no_contraction.tst +++ b/tst/no_contraction.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol no-contraction basic @@ -35,6 +35,7 @@ (parent 0) (seen 2) (unrealized (0 0)) + (origs (n (1 0))) (comment "2 in cohort - 1 not yet seen")) (defskeleton no-contraction @@ -52,6 +53,7 @@ (parent 1) (unrealized) (shape) - (maps ((0 1) ((a a) (n n) (a-0 a) (b b))))) + (maps ((0 1) ((a a) (n n) (a-0 a) (b b)))) + (origs (n (1 0)))) (comment "Nothing left to do") diff --git a/tst/non_transforming.tst b/tst/non_transforming.tst --- a/tst/non_transforming.tst +++ b/tst/non_transforming.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol non_transforming basic @@ -27,6 +27,7 @@ ((send (enc a d (pubk B0)))) ((send (enc c b (pubk B1))))) (label 0) (unrealized (0 0) (0 1)) + (origs (c (2 0)) (d (1 0)) (a (1 0)) (b (2 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton non_transforming @@ -85,7 +86,8 @@ (parent 2) (unrealized) (shape) - (maps ((0 1 1) ((a d) (b d) (c d) (d d) (B B0) (B0 B0) (B1 B0))))) + (maps ((0 1 1) ((a d) (b d) (c d) (d d) (B B0) (B0 B0) (B1 B0)))) + (origs (d (1 0)))) (defskeleton non_transforming (vars (a b c d text) (B0 B1 name)) @@ -127,7 +129,8 @@ (parent 2) (unrealized) (shape) - (maps ((0 1 1) ((a c) (b b) (c c) (d b) (B B1) (B0 B1) (B1 B1))))) + (maps ((0 1 1) ((a c) (b b) (c c) (d b) (B B1) (B0 B1) (B1 B1)))) + (origs (c (1 0)) (b (1 0)))) (defskeleton non_transforming (vars (a c d text) (B0 B1 name)) @@ -174,6 +177,7 @@ (unrealized) (shape) (maps ((0 1 2) ((a a) (b b) (c c) (d d) (B B1) (B0 B1) (B1 B1)))) + (origs (c (2 0)) (d (1 0)) (a (1 0)) (b (2 0))) (comment "2 in cohort - 0 not yet seen")) (defskeleton non_transforming @@ -220,6 +224,7 @@ (unrealized) (shape) (maps ((0 1 1) ((a a) (b d) (c a) (d d) (B B0) (B0 B0) (B1 B0)))) + (origs (a (1 0)) (d (1 0))) (comment "1 in cohort - 0 not yet seen")) (defskeleton non_transforming @@ -244,6 +249,7 @@ (unrealized) (shape) (maps ((0 1 2) ((a a) (b c) (c c) (d d) (B B1) (B0 B1) (B1 B1)))) + (origs (c (2 0)) (d (1 0)) (a (1 0))) (comment "2 in cohort - 0 not yet seen")) (defskeleton non_transforming diff --git a/tst/nonaug-prune.tst b/tst/nonaug-prune.tst --- a/tst/nonaug-prune.tst +++ b/tst/nonaug-prune.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol nonaug-prune basic @@ -30,6 +30,7 @@ (label 0) (seen 2) (unrealized (0 0) (1 0) (2 2)) + (origs (n (2 0))) (comment "4 in cohort - 3 not yet seen")) (defskeleton nonaug-prune @@ -49,6 +50,7 @@ (parent 0) (seen 4) (unrealized (0 0) (1 2) (2 1)) + (origs (n (1 0))) (comment "2 in cohort - 1 not yet seen")) (defskeleton nonaug-prune @@ -68,6 +70,7 @@ (parent 0) (seen 5) (unrealized (0 0) (2 0)) + (origs (n (1 0))) (comment "2 in cohort - 1 not yet seen")) (defskeleton nonaug-prune @@ -103,6 +106,7 @@ (parent 1) (seen 7) (unrealized (0 0) (1 2)) + (origs (n (1 0))) (comment "2 in cohort - 1 not yet seen")) (defskeleton nonaug-prune @@ -121,6 +125,7 @@ (parent 2) (seen 8) (unrealized (0 0)) + (origs (n (1 0))) (comment "2 in cohort - 1 not yet seen")) (defskeleton nonaug-prune @@ -137,7 +142,8 @@ (parent 3) (unrealized) (shape) - (maps ((0 0 1) ((n n) (A B) (B B) (k k))))) + (maps ((0 0 1) ((n n) (A B) (B B) (k k)))) + (origs (n (1 0)))) (defskeleton nonaug-prune (vars (n text) (B C name) (k akey)) @@ -158,6 +164,7 @@ (parent 4) (seen 9) (unrealized (2 0)) + (origs (n (0 0))) (comment "2 in cohort - 1 not yet seen")) (defskeleton nonaug-prune @@ -176,6 +183,7 @@ (parent 5) (seen 6) (unrealized (0 0)) + (origs (n (1 0))) (comment "4 in cohort - 3 not yet seen")) (defskeleton nonaug-prune @@ -196,6 +204,7 @@ (parent 7) (seen 6) (unrealized) + (origs (n (0 0))) (comment "1 in cohort - 0 not yet seen")) (defskeleton nonaug-prune @@ -258,6 +267,7 @@ (label 12) (parent 8) (unrealized (0 0)) + (origs (n (1 0))) (comment "2 in cohort - 2 not yet seen")) (defskeleton nonaug-prune @@ -316,6 +326,7 @@ (parent 12) (seen 17) (unrealized) + (origs (n (1 0))) (comment "1 in cohort - 0 not yet seen")) (defskeleton nonaug-prune @@ -358,6 +369,7 @@ (unrealized) (shape) (maps ((0 2 1) ((n n) (A B) (B B) (k k)))) + (origs (n (1 0))) (comment "1 in cohort - 0 not yet seen")) (defskeleton nonaug-prune diff --git a/tst/ns.tst b/tst/ns.tst --- a/tst/ns.tst +++ b/tst/ns.tst @@ -1,6 +1,6 @@ (herald "Needham-Schroeder Public-Key Protocol Variants") -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol ns basic @@ -25,6 +25,7 @@ (send (enc n2 (pubk b))))) (label 0) (unrealized (0 1)) + (origs (n1 (0 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton ns @@ -62,7 +63,8 @@ (parent 1) (unrealized) (shape) - (maps ((0) ((a a) (b b) (n1 n1) (n2 n2))))) + (maps ((0) ((a a) (b b) (n1 n1) (n2 n2)))) + (origs (n1 (0 0)))) (comment "Nothing left to do") @@ -91,6 +93,7 @@ (send (enc n2-0 (pubk b))))) (label 3) (unrealized (0 1) (1 1)) + (origs (n1 (0 0)) (n1-0 (1 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton ns @@ -109,6 +112,7 @@ (label 4) (parent 3) (unrealized (0 1)) + (origs (n1 (0 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton ns @@ -128,7 +132,8 @@ (parent 4) (unrealized) (shape) - (maps ((0 0) ((a a) (b b) (n1 n1) (n1-0 n1) (n2 n2) (n2-0 n2))))) + (maps ((0 0) ((a a) (b b) (n1 n1) (n1-0 n1) (n2 n2) (n2-0 n2)))) + (origs (n1 (0 0)))) (comment "Nothing left to do") @@ -154,6 +159,7 @@ (recv (enc n2 (pubk b))))) (label 6) (unrealized (0 2)) + (origs (n2 (0 1))) (comment "1 in cohort - 1 not yet seen")) (defskeleton ns @@ -174,7 +180,8 @@ (parent 6) (unrealized) (shape) - (maps ((0) ((a a) (n2 n2) (b b) (n1 n1))))) + (maps ((0) ((a a) (n2 n2) (b b) (n1 n1)))) + (origs (n2 (0 1)))) (comment "Nothing left to do") @@ -204,6 +211,7 @@ (send (enc n2 (pubk b))))) (label 8) (unrealized (0 1)) + (origs (n1 (0 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton ns-role-origs @@ -241,7 +249,8 @@ (parent 9) (unrealized) (shape) - (maps ((0) ((a a) (b b) (n1 n1) (n2 n2))))) + (maps ((0) ((a a) (b b) (n1 n1) (n2 n2)))) + (origs (n2 (1 1)) (n1 (0 0)))) (comment "Nothing left to do") @@ -271,6 +280,7 @@ (recv (enc n2 (pubk b))))) (label 11) (unrealized (0 2)) + (origs (n2 (0 1))) (comment "1 in cohort - 1 not yet seen")) (defskeleton ns-role-origs @@ -310,7 +320,8 @@ (parent 12) (unrealized) (shape) - (maps ((0) ((b b) (a a) (n2 n2) (n1 n1))))) + (maps ((0) ((b b) (a a) (n2 n2) (n1 n1)))) + (origs (n1 (1 0)) (n2 (0 1)))) (defskeleton ns-role-origs (vars (n2 n1 n2-0 text) (b a b-0 name)) @@ -379,6 +390,7 @@ (send (enc n2 (pubk b))))) (label 16) (unrealized (0 1)) + (origs (n1 (0 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton ns2 @@ -416,7 +428,8 @@ (parent 17) (unrealized) (shape) - (maps ((0) ((a a) (b b) (n1 n3) (n2 n2) (n3 n3))))) + (maps ((0) ((a a) (b b) (n1 n3) (n2 n2) (n3 n3)))) + (origs (n3 (0 0)))) (comment "Nothing left to do") @@ -445,7 +458,8 @@ (label 19) (unrealized) (shape) - (maps ((0 1) ((n1 n1) (n2 n2) (a a) (b b))))) + (maps ((0 1) ((n1 n1) (n2 n2) (a a) (b b)))) + (origs (n1 (0 0)))) (comment "Nothing left to do") @@ -486,6 +500,7 @@ (label 21) (parent 20) (unrealized (1 0)) + (origs (n2 (0 1))) (comment "2 in cohort - 2 not yet seen")) (defskeleton nsl-typeless @@ -525,6 +540,7 @@ (parent 21) (unrealized) (shape) - (maps ((0 1) ((a a) (b b) (n2 n2) (n1 a-0))))) + (maps ((0 1) ((a a) (b b) (n2 n2) (n1 a-0)))) + (origs (n2 (0 1)))) (comment "Nothing left to do") diff --git a/tst/nsl3.tst b/tst/nsl3.tst --- a/tst/nsl3.tst +++ b/tst/nsl3.tst @@ -1,6 +1,6 @@ (herald "Three Party Needham-Schroeder-Lowe Protocol") -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol nsl3 basic @@ -52,6 +52,7 @@ (pubk b))))) (label 0) (unrealized (0 1)) + (origs (na1 (0 0)) (na0 (0 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton nsl3 @@ -164,7 +165,9 @@ (maps ((0) ((a a) (b b) (c c) (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) - (nc0 nc0) (nc1 nc1))))) + (nc0 nc0) (nc1 nc1)))) + (origs (nc0 (2 1)) (nc1 (2 1)) (nb0 (1 1)) (nb1 (1 1)) (na1 (0 0)) + (na0 (0 0)))) (comment "Nothing left to do") @@ -217,6 +220,7 @@ (pubk b))) (send (enc nc0 (enc nc1 (pubk c)) (pubk c))))) (label 4) (unrealized (0 2)) + (origs (nb1 (0 1)) (nb0 (0 1))) (comment "1 in cohort - 1 not yet seen")) (defskeleton nsl3 @@ -337,7 +341,9 @@ (maps ((0) ((a a) (b b) (c c) (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) - (nc0 nc0) (nc1 nc1))))) + (nc0 nc0) (nc1 nc1)))) + (origs (na0 (2 0)) (na1 (2 0)) (nc0 (1 1)) (nc1 (1 1)) (nb1 (0 1)) + (nb0 (0 1)))) (comment "Nothing left to do") @@ -390,6 +396,7 @@ (recv (enc nc0 (enc nc1 (pubk c)) (pubk c))))) (label 8) (unrealized (0 2)) + (origs (nc1 (0 1)) (nc0 (0 1))) (comment "1 in cohort - 1 not yet seen")) (defskeleton nsl3 @@ -689,7 +696,9 @@ (maps ((0) ((a a) (b b) (c c) (na0 na0) (na1 na1) (nb0 nb0) (nb1 nb1) - (nc0 nc0) (nc1 nc1))))) + (nc0 nc0) (nc1 nc1)))) + (origs (na0 (1 0)) (na1 (1 0)) (nb0 (2 1)) (nb1 (2 1)) (nc1 (0 1)) + (nc0 (0 1)))) (defskeleton nsl3 (vars (nc0 nc1 nb0 nb1 nc0-0 nc1-0 na0 na1 text) (a b c name)) diff --git a/tst/nsl4cm1.tst b/tst/nsl4cm1.tst --- a/tst/nsl4cm1.tst +++ b/tst/nsl4cm1.tst @@ -1,6 +1,6 @@ (herald "Four Party Needham-Schroeder-Lowe Protocol") -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol nsl4cm basic @@ -37,6 +37,7 @@ (send (enc nb nc nd (pubk b))))) (label 0) (unrealized (0 1)) + (origs (na (0 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton nsl4cm diff --git a/tst/nslsk.tst b/tst/nslsk.tst --- a/tst/nslsk.tst +++ b/tst/nslsk.tst @@ -1,6 +1,6 @@ (herald "Needham-Schroeder-Lowe Protocol with symmetric encryption") -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol nslsk basic @@ -23,6 +23,7 @@ (recv (enc t k)))) (label 0) (unrealized (0 2)) + (origs (k (0 1))) (comment "2 in cohort - 2 not yet seen")) (defskeleton nslsk @@ -77,7 +78,8 @@ (parent 1) (unrealized) (shape) - (maps ((0) ((a a) (k k) (b b) (n n) (t t))))) + (maps ((0) ((a a) (k k) (b b) (n n) (t t)))) + (origs (k (0 1)))) (comment "Nothing left to do") @@ -101,6 +103,7 @@ (send (enc t k)))) (label 4) (unrealized (0 1)) + (origs (n (0 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton nslsk @@ -120,7 +123,8 @@ (parent 4) (unrealized) (shape) - (maps ((0) ((b b) (n n) (a a) (k k) (t t))))) + (maps ((0) ((b b) (n n) (a a) (k k) (t t)))) + (origs (n (0 0)))) (comment "Nothing left to do") @@ -144,6 +148,7 @@ (recv (enc "t" k)))) (label 6) (unrealized (0 2)) + (origs (k (0 1))) (comment "2 in cohort - 2 not yet seen")) (defskeleton nslsk-tag-term @@ -198,7 +203,8 @@ (parent 7) (unrealized) (shape) - (maps ((0) ((a a) (k k) (b b) (n n))))) + (maps ((0) ((a a) (k k) (b b) (n n)))) + (origs (k (0 1)))) (comment "Nothing left to do") @@ -222,6 +228,7 @@ (send (enc "t" k)))) (label 10) (unrealized (0 1)) + (origs (n (0 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton nslsk-tag-term @@ -241,6 +248,7 @@ (parent 10) (unrealized) (shape) - (maps ((0) ((b b) (n n) (a a) (k k))))) + (maps ((0) ((b b) (n n) (a a) (k k)))) + (origs (n (0 0)))) (comment "Nothing left to do") diff --git a/tst/or.tst b/tst/or.tst --- a/tst/or.tst +++ b/tst/or.tst @@ -1,7 +1,7 @@ (herald "Otway-Rees Protocol" (comment "Standard version using variables of sort mesg")) -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol or basic @@ -32,6 +32,7 @@ (recv (cat m y (enc nb k (ltk b s)))) (send y))) (label 0) (unrealized (0 2)) + (origs (nb (0 1))) (comment "2 in cohort - 2 not yet seen")) (defskeleton or @@ -140,7 +141,8 @@ (parent 3) (unrealized) (shape) - (maps ((0) ((nb nb) (s s) (a a) (b a) (k k) (m m) (x x) (y y))))) + (maps ((0) ((nb nb) (s s) (a a) (b a) (k k) (m m) (x x) (y y)))) + (origs (k (1 1)) (nb (0 1)))) (defskeleton or (vars (x y x-0 mesg) (nb m nb-0 text) (s a name) (k skey)) @@ -166,6 +168,7 @@ (unrealized) (shape) (maps ((0) ((nb nb) (s s) (a a) (b a) (k k) (m m) (x x) (y y)))) + (origs (k (1 1)) (nb (0 1))) (comment "1 in cohort - 0 not yet seen")) (defskeleton or @@ -187,7 +190,8 @@ (parent 3) (unrealized) (shape) - (maps ((0) ((nb nb) (s s) (a a) (b a) (k k) (m m) (x x) (y y))))) + (maps ((0) ((nb nb) (s s) (a a) (b a) (k k) (m m) (x x) (y y)))) + (origs (k (1 1)) (nb (0 1)))) (defskeleton or (vars (x y mesg) (nb m na text) (s a b name) (k skey)) @@ -210,7 +214,8 @@ (parent 4) (unrealized) (shape) - (maps ((0) ((nb nb) (s s) (a a) (b b) (k k) (m m) (x x) (y y))))) + (maps ((0) ((nb nb) (s s) (a a) (b b) (k k) (m m) (x x) (y y)))) + (origs (k (1 1)) (nb (0 1)))) (defskeleton or (vars (x y x-0 mesg) (nb m na text) (s a name) (k skey)) @@ -236,6 +241,7 @@ (unrealized) (shape) (maps ((0) ((nb nb) (s s) (a a) (b a) (k k) (m m) (x x) (y y)))) + (origs (k (1 1)) (nb (0 1))) (comment "1 in cohort - 0 not yet seen")) (comment "Nothing left to do") diff --git a/tst/pca.tst b/tst/pca.tst --- a/tst/pca.tst +++ b/tst/pca.tst @@ -1,7 +1,7 @@ (herald "Privacy Certificate Authority" (comment "Generation of an Attestation Identity Certificate")) -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol pca basic @@ -29,6 +29,7 @@ (traces ((recv (enc ki a t (invk kp))))) (label 0) (unrealized (0 0)) + (origs) (comment "1 in cohort - 1 not yet seen")) (defskeleton pca @@ -209,6 +210,7 @@ (unrealized) (shape) (maps ((0) ((ki ki) (kp kp) (t t) (a a)))) + (origs (ki (3 0)) (ki-0 (2 0))) (comment "1 in cohort - 0 not yet seen")) (defskeleton pca @@ -258,7 +260,8 @@ (parent 6) (unrealized) (shape) - (maps ((0) ((ki ki) (kp kp) (t t) (a a))))) + (maps ((0) ((ki ki) (kp kp) (t t) (a a)))) + (origs (ki (2 0)))) (defskeleton pca (vars (t a a-0 a-1 text) (ki kp ke km ki-0 km-0 ke-0 km-1 ki-1 akey)) diff --git a/tst/pkinit.tst b/tst/pkinit.tst --- a/tst/pkinit.tst +++ b/tst/pkinit.tst @@ -1,6 +1,6 @@ (herald "Kerberos PK init") -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol pkinit basic @@ -32,6 +32,7 @@ (enc ak n1 tk t k))))) (label 0) (unrealized (0 1)) + (origs (n2 (0 0)) (n1 (0 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton pkinit @@ -62,6 +63,7 @@ (maps ((0) ((c c) (as as) (t t) (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) - (k k) (ak ak))))) + (k k) (ak ak)))) + (origs (k (1 1)) (ak-0 (1 1)) (n2 (0 0)) (n1 (0 0)))) (comment "Nothing left to do") diff --git a/tst/pruning1.tst b/tst/pruning1.tst --- a/tst/pruning1.tst +++ b/tst/pruning1.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol prune basic @@ -24,6 +24,7 @@ (recv (enc n (privk b) (pubk a))))) (label 0) (unrealized (0 1) (0 2)) + (origs (n (0 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton prune @@ -105,7 +106,8 @@ (parent 3) (unrealized) (shape) - (maps ((0) ((a a) (b b) (n n))))) + (maps ((0) ((a a) (b b) (n n)))) + (origs (n (0 0)))) (comment "Nothing left to do") @@ -140,6 +142,7 @@ (label 5) (unrealized) (shape) - (maps ((0 1 2) ((n n) (a a) (b b))))) + (maps ((0 1 2) ((n n) (a a) (b b)))) + (origs (n (0 0)))) (comment "Nothing left to do") diff --git a/tst/sigenc.tst b/tst/sigenc.tst --- a/tst/sigenc.tst +++ b/tst/sigenc.tst @@ -1,7 +1,7 @@ (herald "Signed Encrypted Message Example" (comment "Shows examples of key usage of asymmetric keys")) -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol mult-keys-sig-enc basic @@ -27,6 +27,7 @@ (send (enc (enc n2 (privk "sig" a)) (pubk "enc" b))))) (label 0) (unrealized (0 1)) + (origs (n1 (0 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton mult-keys-sig-enc @@ -69,7 +70,8 @@ (parent 1) (unrealized) (shape) - (maps ((0) ((a a) (b b) (n1 n1) (n2 n2))))) + (maps ((0) ((a a) (b b) (n1 n1) (n2 n2)))) + (origs (n1 (0 0)))) (comment "Nothing left to do") @@ -96,6 +98,7 @@ (recv (enc (enc n2 (privk "sig" a)) (pubk "enc" b))))) (label 3) (unrealized (0 0) (0 2)) + (origs (n2 (0 1))) (comment "1 in cohort - 1 not yet seen")) (defskeleton mult-keys-sig-enc @@ -141,6 +144,7 @@ (unrealized) (shape) (maps ((0) ((a a) (b b) (n2 n2) (n1 n1)))) + (origs (n2 (0 1))) (comment "1 in cohort - 0 not yet seen")) (defskeleton mult-keys-sig-enc @@ -163,7 +167,8 @@ (parent 4) (unrealized) (shape) - (maps ((0) ((a a) (b b) (n2 n2) (n1 n1))))) + (maps ((0) ((a a) (b b) (n2 n2) (n1 n1)))) + (origs (n2 (0 1)))) (comment "Nothing left to do") @@ -190,6 +195,7 @@ (recv (enc (enc n2 (privk "sig" a)) (pubk "enc" b))))) (label 7) (unrealized (0 2)) + (origs (n2 (0 1))) (comment "1 in cohort - 1 not yet seen")) (defskeleton mult-keys-sig-enc @@ -212,7 +218,8 @@ (parent 7) (unrealized) (shape) - (maps ((0) ((a a) (b b) (n2 n2) (n1 n1))))) + (maps ((0) ((a a) (b b) (n2 n2) (n1 n1)))) + (origs (n2 (0 1)))) (comment "Nothing left to do") @@ -239,6 +246,7 @@ (recv (enc (enc n2 (privk "sig" a)) (pubk "enc" b))))) (label 9) (unrealized (0 0) (0 2)) + (origs (n2 (0 1))) (comment "1 in cohort - 1 not yet seen")) (defskeleton mult-keys-sig-enc @@ -328,6 +336,7 @@ (unrealized) (shape) (maps ((0) ((a a) (b b) (n2 n2) (n1 n1)))) + (origs (n2 (0 1))) (comment "1 in cohort - 0 not yet seen")) (defskeleton mult-keys-sig-enc @@ -404,7 +413,8 @@ (parent 12) (unrealized) (shape) - (maps ((0) ((a a) (b b) (n2 n2) (n1 n1))))) + (maps ((0) ((a a) (b b) (n2 n2) (n1 n1)))) + (origs (n2 (0 1)))) (defskeleton mult-keys-sig-enc (vars (n2 n1 text) (a b b-0 name)) diff --git a/tst/sorted_epmo_acctnum.tst b/tst/sorted_epmo_acctnum.tst --- a/tst/sorted_epmo_acctnum.tst +++ b/tst/sorted_epmo_acctnum.tst @@ -4,7 +4,7 @@ "This version uses sorts to avoid confusion" "between a nonce and other data")) -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (comment "Displacement disabled") @@ -98,6 +98,7 @@ (send (enc (enc "hash" b m nb nm (pubk hash)) (privk m))))) (label 0) (unrealized (0 2)) + (origs (nm (0 1))) (comment "1 in cohort - 1 not yet seen")) (defskeleton sorted_epmo_acctnum @@ -390,7 +391,8 @@ (maps ((0) ((b b) (m m) (c c) (nm nm) (nc nc) (nb nb) (hash hash) - (goods goods) (price price))))) + (goods goods) (price price)))) + (origs (nc (2 0)) (nm (0 1)) (nb (1 1)))) (defskeleton sorted_epmo_acctnum (vars (price acctnum goods price-0 text) (nm nc nb nm-0 data) @@ -839,6 +841,7 @@ (recv (enc (enc "hash" b m nb nm (pubk hash)) (privk m))))) (label 17) (unrealized (0 2)) + (origs (nb (0 1))) (comment "1 in cohort - 1 not yet seen")) (defskeleton sorted_epmo_acctnum @@ -1238,7 +1241,8 @@ (maps ((0) ((b b) (m m) (c c) (nm nm) (nb nb) (nc nc) (hash hash) - (acctnum acctnum) (price price))))) + (acctnum acctnum) (price price)))) + (origs (nc (2 0)) (nm (1 1)) (nb (0 1)))) (defskeleton sorted_epmo_acctnum (vars (acctnum price acctnum-0 goods text) (nm nb nc nb-0 data) diff --git a/tst/targetterms2.tst b/tst/targetterms2.tst --- a/tst/targetterms2.tst +++ b/tst/targetterms2.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol targetterms2 basic @@ -22,6 +22,7 @@ (recv (enc n (enc n (enc n (pubk a)) (pubk a)) (pubk a))))) (label 0) (unrealized (0 1)) + (origs (n (0 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton targetterms2 @@ -142,7 +143,8 @@ (parent 4) (unrealized) (shape) - (maps ((0) ((a a) (n n))))) + (maps ((0) ((a a) (n n)))) + (origs (n (0 0)))) (defskeleton targetterms2 (vars (n text) (a name)) diff --git a/tst/targetterms6.tst b/tst/targetterms6.tst --- a/tst/targetterms6.tst +++ b/tst/targetterms6.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol targetterms6 basic @@ -26,6 +26,7 @@ (enc n (enc n (pubk a)) (pubk a)))))) (label 0) (unrealized (0 1)) + (origs (n (0 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton targetterms6 @@ -167,7 +168,8 @@ (parent 4) (unrealized) (shape) - (maps ((0) ((a a) (n n))))) + (maps ((0) ((a a) (n n)))) + (origs (n (0 0)))) (defskeleton targetterms6 (vars (m mesg) (n text) (a name)) @@ -232,6 +234,7 @@ (label 8) (unrealized) (shape) - (maps ((0 1 2) ((n n) (a a))))) + (maps ((0 1 2) ((n n) (a a)))) + (origs (n (0 0)))) (comment "Nothing left to do") diff --git a/tst/targetterms8.tst b/tst/targetterms8.tst --- a/tst/targetterms8.tst +++ b/tst/targetterms8.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol targetterms8 basic @@ -20,6 +20,7 @@ (label 0) (seen 1) (unrealized (0 1)) + (origs (n1 (0 0))) (comment "2 in cohort - 1 not yet seen")) (defskeleton targetterms8 @@ -33,6 +34,7 @@ (label 1) (parent 0) (unrealized (0 1)) + (origs (n2 (0 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton targetterms8 @@ -50,7 +52,8 @@ (parent 1) (unrealized) (shape) - (maps ((0) ((a a) (n1 n2) (n2 n2) (k k))))) + (maps ((0) ((a a) (n1 n2) (n2 n2) (k k)))) + (origs (n2 (0 0)))) (comment "Nothing left to do") @@ -72,6 +75,7 @@ (traces ((send (enc n1 (enc a n1 k) k)) (recv (enc a n1 k)))) (label 3) (unrealized (0 1)) + (origs (n1 (0 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton targetterms8 @@ -89,6 +93,7 @@ (parent 3) (unrealized) (shape) - (maps ((0) ((a a) (n1 n1) (k k))))) + (maps ((0) ((a a) (n1 n1) (k k)))) + (origs (n1 (0 0)))) (comment "Nothing left to do") diff --git a/tst/tor.tst b/tst/tor.tst --- a/tst/tor.tst +++ b/tst/tor.tst @@ -1,7 +1,7 @@ (herald "Tor Circuit-Level Handshake Protocol" (algebra diffie-hellman) (comment "Achieves unilateral authentication")) -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol tor diffie-hellman @@ -28,6 +28,7 @@ (recv (cat (exp (gen) y) (enc "hash" (exp (exp (gen) x) y)))))) (label 0) (unrealized (0 1)) + (origs (x (0 0))) (comment "2 in cohort - 2 not yet seen")) (defskeleton tor @@ -85,7 +86,8 @@ (parent 1) (unrealized) (shape) - (maps ((0) ((b b) (x x) (y y))))) + (maps ((0) ((b b) (x x) (y y)))) + (origs (y (1 1)) (x (0 0)))) (defskeleton tor (vars (b b-0 name) (x y expn)) @@ -156,7 +158,8 @@ (label 6) (unrealized) (shape) - (maps ((0) ((b b) (x x) (y y) (n n))))) + (maps ((0) ((b b) (x x) (y y) (n n)))) + (origs (y (0 1)))) (comment "Nothing left to do") @@ -203,6 +206,7 @@ (label 8) (parent 7) (unrealized (0 1) (1 0)) + (origs (n (0 2)) (x (0 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton tor diff --git a/tst/uncarried_keys.tst b/tst/uncarried_keys.tst --- a/tst/uncarried_keys.tst +++ b/tst/uncarried_keys.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol uncarried-keys basic @@ -25,6 +25,7 @@ (send (enc a K (pubk B))) (recv (enc a A B K)))) (label 0) (unrealized (0 1) (0 3)) + (origs (K (0 2)) (a (0 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton uncarried-keys @@ -67,6 +68,7 @@ (unrealized) (shape) (maps ((0) ((a a) (A A) (B B) (K K)))) + (origs (K (0 2)) (a (0 0))) (comment "1 in cohort - 0 not yet seen")) (defskeleton uncarried-keys @@ -86,7 +88,8 @@ (parent 1) (unrealized) (shape) - (maps ((0) ((a a) (A A) (B B) (K K))))) + (maps ((0) ((a a) (A A) (B B) (K K)))) + (origs (K (0 2)) (a (0 0)))) (defskeleton uncarried-keys (vars (a text) (A B name)) @@ -126,7 +129,8 @@ (parent 1) (unrealized) (shape) - (maps ((0) ((a a) (A A) (B B) (K (pubk A)))))) + (maps ((0) ((a a) (A A) (B B) (K (pubk A))))) + (origs ((pubk A) (0 2)) (a (0 0)))) (defskeleton uncarried-keys (vars (a text) (A B name) (K akey)) diff --git a/tst/uo.tst b/tst/uo.tst --- a/tst/uo.tst +++ b/tst/uo.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol uniq-orig basic @@ -27,6 +27,7 @@ (parent 0) (unrealized) (shape) - (maps ((0 1) ((n n) (m m))))) + (maps ((0 1) ((n n) (m m)))) + (origs (n (0 0)))) (comment "Nothing left to do") diff --git a/tst/weird.tst b/tst/weird.tst --- a/tst/weird.tst +++ b/tst/weird.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol weird basic @@ -15,7 +15,8 @@ (label 0) (unrealized) (shape) - (maps ((0 1) ((k k) (a a))))) + (maps ((0 1) ((k k) (a a)))) + (origs (k (0 0)))) (comment "Nothing left to do") @@ -32,6 +33,7 @@ (traces ((send k)) ((recv (enc a k)))) (label 1) (unrealized (1 0)) + (origs (k (0 0))) (comment "2 in cohort - 2 not yet seen")) (defskeleton weird @@ -47,7 +49,8 @@ (parent 1) (unrealized) (shape) - (maps ((0 1) ((k k) (a a))))) + (maps ((0 1) ((k k) (a a)))) + (origs (k (0 0)))) (defskeleton weird (vars (a name) (k skey)) @@ -75,6 +78,7 @@ (parent 3) (unrealized) (shape) - (maps ((0 1) ((k k) (a a))))) + (maps ((0 1) ((k k) (a a)))) + (origs (k (0 0)))) (comment "Nothing left to do") diff --git a/tst/wide-mouth-frog.tst b/tst/wide-mouth-frog.tst --- a/tst/wide-mouth-frog.tst +++ b/tst/wide-mouth-frog.tst @@ -1,7 +1,7 @@ (herald "Wide-Mouth Frog Protocol" (comment "This protocol has an infinite number of shapes")) -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol wide-mouth-frog basic @@ -25,7 +25,8 @@ (label 0) (unrealized) (shape) - (maps ((0) ((a a) (t t) (k k) (b b) (ta ta))))) + (maps ((0) ((a a) (t t) (k k) (b b) (ta ta)))) + (origs (k (0 0)))) (comment "Nothing left to do") @@ -49,6 +50,7 @@ (traces ((recv (enc tb a k (ltk b t))))) (label 1) (unrealized (0 0)) + (origs) (comment "2 in cohort - 2 not yet seen")) (defskeleton wide-mouth-frog @@ -66,7 +68,8 @@ (parent 1) (unrealized) (shape) - (maps ((0) ((b b) (t t) (k k) (a a) (tb tb))))) + (maps ((0) ((b b) (t t) (k k) (a a) (tb tb)))) + (origs (k (1 0)))) (defskeleton wide-mouth-frog (vars (tb ta text) (b t a name) (k skey)) @@ -84,7 +87,8 @@ (parent 1) (unrealized) (shape) - (maps ((0) ((b b) (t t) (k k) (a a) (tb tb))))) + (maps ((0) ((b b) (t t) (k k) (a a) (tb tb)))) + (origs)) (comment "Nothing left to do") @@ -110,6 +114,7 @@ (send (enc tb a k (ltk b t))))) (label 4) (unrealized (0 0)) + (origs) (comment "2 in cohort - 2 not yet seen")) (defskeleton wide-mouth-frog @@ -129,7 +134,8 @@ (parent 4) (unrealized) (shape) - (maps ((0) ((a a) (b b) (t t) (k k) (ta ta) (tb tb))))) + (maps ((0) ((a a) (b b) (t t) (k k) (ta ta) (tb tb)))) + (origs (k (1 0)))) (defskeleton wide-mouth-frog (vars (ta tb ta-0 text) (a b t name) (k skey)) @@ -170,7 +176,8 @@ (parent 6) (unrealized) (shape) - (maps ((0) ((a a) (b b) (t t) (k k) (ta ta) (tb tb))))) + (maps ((0) ((a a) (b b) (t t) (k k) (ta ta) (tb tb)))) + (origs (k (2 0)))) (defskeleton wide-mouth-frog (vars (ta tb ta-0 ta-1 text) (a b t name) (k skey)) @@ -217,7 +224,8 @@ (parent 8) (unrealized) (shape) - (maps ((0) ((a a) (b b) (t t) (k k) (ta ta) (tb tb))))) + (maps ((0) ((a a) (b b) (t t) (k k) (ta ta) (tb tb)))) + (origs (k (3 0)))) (defskeleton wide-mouth-frog (vars (ta tb ta-0 ta-1 ta-2 text) (a b t name) (k skey)) @@ -270,7 +278,8 @@ (parent 10) (unrealized) (shape) - (maps ((0) ((a a) (b b) (t t) (k k) (ta ta) (tb tb))))) + (maps ((0) ((a a) (b b) (t t) (k k) (ta ta) (tb tb)))) + (origs (k (4 0)))) (defskeleton wide-mouth-frog (vars (ta tb ta-0 ta-1 ta-2 ta-3 text) (a b t name) (k skey)) @@ -330,7 +339,8 @@ (parent 12) (unrealized) (shape) - (maps ((0) ((a a) (b b) (t t) (k k) (ta ta) (tb tb))))) + (maps ((0) ((a a) (b b) (t t) (k k) (ta ta) (tb tb)))) + (origs (k (5 0)))) (defskeleton wide-mouth-frog (vars (ta tb ta-0 ta-1 ta-2 ta-3 ta-4 text) (a b t name) (k skey)) @@ -397,7 +407,8 @@ (parent 14) (unrealized) (shape) - (maps ((0) ((a a) (b b) (t t) (k k) (ta ta) (tb tb))))) + (maps ((0) ((a a) (b b) (t t) (k k) (ta ta) (tb tb)))) + (origs (k (6 0)))) (defskeleton wide-mouth-frog (vars (ta tb ta-0 ta-1 ta-2 ta-3 ta-4 ta-5 text) (a b t name) diff --git a/tst/wonthull.tst b/tst/wonthull.tst --- a/tst/wonthull.tst +++ b/tst/wonthull.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol wonthull basic @@ -24,6 +24,7 @@ (label 0) (seen 1) (unrealized (0 1)) + (origs (x3 (0 0)) (x2 (0 0)) (x1 (0 0))) (comment "3 in cohort - 2 not yet seen")) (defskeleton wonthull @@ -39,6 +40,7 @@ (label 1) (parent 0) (unrealized (0 1)) + (origs (x1 (0 0)) (x2 (0 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton wonthull @@ -95,7 +97,8 @@ (parent 2) (unrealized) (shape) - (maps ((0) ((a a) (x1 x1) (x2 x2) (x3 y3) (x4 y3))))) + (maps ((0) ((a a) (x1 x1) (x2 x2) (x3 y3) (x4 y3)))) + (origs (y3 (0 0)) (x2 (0 0)) (x1 (0 0)))) (defskeleton wonthull (vars (x1 y3 text) (a name)) @@ -145,6 +148,7 @@ (label 6) (unrealized) (shape) - (maps ((0 1) ((a a) (x1 x1) (x3 x3))))) + (maps ((0 1) ((a a) (x1 x1) (x3 x3)))) + (origs (x3 (0 0)) (x1 (0 0)))) (comment "Nothing left to do") diff --git a/tst/wonthull2.tst b/tst/wonthull2.tst --- a/tst/wonthull2.tst +++ b/tst/wonthull2.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol wonthull2 basic @@ -23,6 +23,7 @@ (recv (enc "okay" x3 x4 (pubk a))))) (label 0) (unrealized (0 1)) + (origs (x3 (0 0))) (comment "2 in cohort - 2 not yet seen")) (defskeleton wonthull2 @@ -120,7 +121,8 @@ (parent 2) (unrealized) (shape) - (maps ((0) ((a a) (x1 x1) (x2 x2) (x3 y3) (x4 y3))))) + (maps ((0) ((a a) (x1 x1) (x2 x2) (x3 y3) (x4 y3)))) + (origs (y3 (0 0)))) (defskeleton wonthull2 (vars (x2 y3 y3-0 text) (a name)) @@ -202,7 +204,8 @@ (parent 6) (unrealized) (shape) - (maps ((0) ((a a) (x1 y3) (x2 x2) (x3 y3-0) (x4 y3))))) + (maps ((0) ((a a) (x1 y3) (x2 x2) (x3 y3-0) (x4 y3)))) + (origs (y3 (0 0)) (y3-0 (0 0)))) (defskeleton wonthull2 (vars (x2 y3 text) (a name)) @@ -251,6 +254,7 @@ (label 11) (seen 12) (unrealized (0 1)) + (origs (x3-0 (0 0))) (comment "7 in cohort - 5 not yet seen")) (defskeleton wonthull2 @@ -270,6 +274,7 @@ (label 12) (parent 11) (unrealized (1 0)) + (origs (x3 (0 0))) (comment "3 in cohort - 3 not yet seen")) (defskeleton wonthull2 @@ -311,6 +316,7 @@ (parent 11) (seen 18) (unrealized) + (origs (x3 (0 0))) (comment "1 in cohort - 0 not yet seen")) (defskeleton wonthull2 @@ -352,6 +358,7 @@ (parent 11) (seen 14 18 23 27) (unrealized (0 1)) + (origs (x1 (0 0))) (comment "7 in cohort - 0 not yet seen")) (defskeleton wonthull2 @@ -371,7 +378,8 @@ (parent 12) (unrealized) (shape) - (maps ((0 1) ((x1 x1) (x3 x3) (a a) (x1-0 x1) (x3-0 x3) (a-0 a))))) + (maps ((0 1) ((x1 x1) (x3 x3) (a a) (x1-0 x1) (x3-0 x3) (a-0 a)))) + (origs (x3 (0 0)))) (defskeleton wonthull2 (vars (x3 x1 text) (a name)) @@ -390,7 +398,8 @@ (parent 12) (unrealized) (shape) - (maps ((0 1) ((x1 x3) (x3 x3) (a a) (x1-0 x1) (x3-0 x3) (a-0 a))))) + (maps ((0 1) ((x1 x3) (x3 x3) (a a) (x1-0 x1) (x3-0 x3) (a-0 a)))) + (origs (x3 (0 0)))) (defskeleton wonthull2 (vars (x1 x3 x1-0 y3 text) (a a-0 name)) @@ -936,6 +945,7 @@ (unrealized) (shape) (maps ((0 1) ((x1 y3) (x3 x3) (a a) (x1-0 x1) (x3-0 y3) (a-0 a)))) + (origs (y3 (0 0))) (comment "1 in cohort - 0 not yet seen")) (defskeleton wonthull2 @@ -2592,6 +2602,7 @@ (unrealized) (shape) (maps ((0 1) ((x1 y3) (x3 x3) (a a) (x1-0 y3) (x3-0 y3-0) (a-0 a-0)))) + (origs (y3-0 (0 0))) (comment "1 in cohort - 0 not yet seen")) (defskeleton wonthull2 diff --git a/tst/wonthull3.tst b/tst/wonthull3.tst --- a/tst/wonthull3.tst +++ b/tst/wonthull3.tst @@ -1,4 +1,4 @@ -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol wonthull3 basic @@ -26,6 +26,7 @@ (label 0) (seen 1) (unrealized (0 2)) + (origs (x3 (0 0))) (comment "3 in cohort - 2 not yet seen")) (defskeleton wonthull3 @@ -42,6 +43,7 @@ (label 1) (parent 0) (unrealized (0 2)) + (origs (x2 (0 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton wonthull3 @@ -220,7 +222,8 @@ (parent 6) (unrealized) (shape) - (maps ((0) ((a a) (x1 x1) (x2 x2) (x3 y3) (x4 y3))))) + (maps ((0) ((a a) (x1 x1) (x2 x2) (x3 y3) (x4 y3)))) + (origs (y3 (0 0)))) (defskeleton wonthull3 (vars (y3 text) (a name)) @@ -273,6 +276,7 @@ (label 12) (seen 13) (unrealized (0 2)) + (origs (x3-0 (0 0))) (comment "5 in cohort - 3 not yet seen")) (defskeleton wonthull3 @@ -293,6 +297,7 @@ (label 13) (parent 12) (unrealized (1 0)) + (origs (x3 (0 0))) (comment "3 in cohort - 3 not yet seen")) (defskeleton wonthull3 @@ -336,6 +341,7 @@ (parent 12) (seen 17) (unrealized (0 2)) + (origs (x1 (0 0))) (comment "5 in cohort - 1 not yet seen")) (defskeleton wonthull3 @@ -356,7 +362,8 @@ (parent 13) (unrealized) (shape) - (maps ((0 1) ((x1 x1) (x3 x3) (a a) (x1-0 x1) (x3-0 x3) (a-0 a))))) + (maps ((0 1) ((x1 x1) (x3 x3) (a a) (x1-0 x1) (x3-0 x3) (a-0 a)))) + (origs (x3 (0 0)))) (defskeleton wonthull3 (vars (x3 x1 text) (a name)) @@ -376,7 +383,8 @@ (parent 13) (unrealized) (shape) - (maps ((0 1) ((x1 x3) (x3 x3) (a a) (x1-0 x1) (x3-0 x3) (a-0 a))))) + (maps ((0 1) ((x1 x3) (x3 x3) (a a) (x1-0 x1) (x3-0 x3) (a-0 a)))) + (origs (x3 (0 0)))) (defskeleton wonthull3 (vars (x1 x3 x1-0 y3 text) (a a-0 name)) @@ -1174,6 +1182,7 @@ (unrealized) (shape) (maps ((0 1) ((x1 y3) (x3 x3) (a a) (x1-0 x1) (x3-0 y3) (a-0 a)))) + (origs (y3 (0 0))) (comment "1 in cohort - 0 not yet seen")) (defskeleton wonthull3 @@ -1311,6 +1320,7 @@ (parent 38) (seen 17) (unrealized) + (origs (x1 (0 0))) (comment "1 in cohort - 0 not yet seen")) (defskeleton wonthull3 diff --git a/tst/woolam.tst b/tst/woolam.tst --- a/tst/woolam.tst +++ b/tst/woolam.tst @@ -1,6 +1,6 @@ (herald "Woo-Lam Protocol") -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol woolam basic @@ -31,6 +31,7 @@ (recv (enc a n (ltk b s))))) (label 0) (unrealized (0 2) (0 4)) + (origs (n (0 1))) (comment "1 in cohort - 1 not yet seen")) (defskeleton woolam @@ -96,6 +97,7 @@ (parent 2) (unrealized) (shape) - (maps ((0) ((a a) (s s) (b b) (n n))))) + (maps ((0) ((a a) (s s) (b b) (n n)))) + (origs (n (0 1)))) (comment "Nothing left to do") diff --git a/tst/yahalom-6.3.6.tst b/tst/yahalom-6.3.6.tst --- a/tst/yahalom-6.3.6.tst +++ b/tst/yahalom-6.3.6.tst @@ -4,7 +4,7 @@ "Yahalom Protocol, Section 6.3.6, Page 49") (url "http://www.eecs.umich.edu/acal/swerve/docs/49-1.pdf")) -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol yahalom basic @@ -36,6 +36,7 @@ (send (cat blob (enc n-b k))))) (label 0) (unrealized (0 1)) + (origs (n-a (0 0))) (comment "1 in cohort - 1 not yet seen")) (defskeleton yahalom @@ -79,8 +80,8 @@ (parent 1) (unrealized) (shape) - (maps - ((0) ((a a) (b b) (s s) (n-a n-a) (n-b n-b) (k k) (blob blob))))) + (maps ((0) ((a a) (b b) (s s) (n-a n-a) (n-b n-b) (k k) (blob blob)))) + (origs (k (1 1)) (n-a (0 0)) (n-b (2 1)))) (comment "Nothing left to do") @@ -113,6 +114,7 @@ (recv (cat (enc a k (ltk b s)) (enc n-b k)))) ((recv k) (send k))) (label 3) (unrealized (0 2)) + (origs (n-b (0 1))) (comment "1 in cohort - 1 not yet seen")) (defskeleton yahalom @@ -207,6 +209,7 @@ (recv (cat (enc a k (ltk b s)) (enc n-b k))))) (label 7) (unrealized (0 2)) + (origs (n-b (0 1))) (comment "1 in cohort - 1 not yet seen")) (defskeleton yahalom @@ -415,7 +418,8 @@ (parent 13) (unrealized) (shape) - (maps ((0) ((a a) (b b) (s s) (n-a n-a) (n-b n-b) (k k))))) + (maps ((0) ((a a) (b b) (s s) (n-a n-a) (n-b n-b) (k k)))) + (origs (k (1 1)) (n-a (2 0)) (n-b (0 1)))) (defskeleton yahalom (vars (blob blob-0 mesg) (n-a n-b n-a-0 text) (a b s a-0 b-0 s-0 name) @@ -685,6 +689,7 @@ (send (cat (enc b k n-a n-b (ltk a s)) (enc a k (ltk b s)))))) (label 24) (unrealized (0 0)) + (origs (k (0 1))) (comment "1 in cohort - 1 not yet seen")) (defskeleton yahalom @@ -704,6 +709,7 @@ (parent 24) (unrealized) (shape) - (maps ((0) ((a a) (b b) (s s) (n-a n-a) (n-b n-b) (k k))))) + (maps ((0) ((a a) (b b) (s s) (n-a n-a) (n-b n-b) (k k)))) + (origs (k (0 1)) (n-b (1 1)))) (comment "Nothing left to do") diff --git a/tst/yahalom.tst b/tst/yahalom.tst --- a/tst/yahalom.tst +++ b/tst/yahalom.tst @@ -1,6 +1,6 @@ (herald "Yahalom Protocol Without Forwarding") -(comment "CPSA 2.2.3") +(comment "CPSA 2.2.4") (comment "All input read") (defprotocol yahalom basic @@ -28,6 +28,7 @@ (recv (enc a k (ltk b c))) (recv (enc n-b k)))) (label 0) (unrealized (0 2) (0 3)) + (origs (n-b (0 1))) (comment "1 in cohort - 1 not yet seen")) (defskeleton yahalom @@ -255,7 +256,8 @@ (parent 6) (unrealized) (shape) - (maps ((0) ((a a) (b b) (c c) (n-b n-b) (n-a n-a) (k k))))) + (maps ((0) ((a a) (b b) (c c) (n-b n-b) (n-a n-a) (k k)))) + (origs (k (1 1)) (n-b (0 1)))) (defskeleton yahalom (vars (n-b n-a n-a-0 text) (a b c a-0 b-0 c-0 name) (k skey)) @@ -989,6 +991,7 @@ ((recv k) (send k))) (label 34) (unrealized (0 2) (0 3)) + (origs (n-b (0 1))) (comment "1 in cohort - 1 not yet seen")) (defskeleton yahalom