packages feed

cpsa 2.5.0 → 2.5.1

raw patch · 83 files changed

+2052/−1443 lines, 83 files

Files

ChangeLog view
@@ -1,3 +1,26 @@+2015-07-08  John D. Ramsdell  <ramsdell@mitre.org>++	* cpsa.cabal (Version): Tagged as version 2.5.1++2015-06-30  John D. Ramsdell  <ramsdell@mitre.org>++	* src/CPSA/Basic/Algebra.hs (occursIn): Restricted first argument+	of occursIn to variables as the implementation returns incorrect+	answers for other cases.  The code was called with a variable in+	its first argument, so this correction does not change any+	results.++2015-06-25  John D. Ramsdell  <ramsdell@mitre.org>++	* src/CPSA/Lib/Strand.hs (geq): Removed dynamic role specific test+	because it erroneously reports violations.  The existing static+	role specific test correctly does the job.++2015-06-18  John D. Ramsdell  <ramsdell@mitre.org>++	* doc/{cpsaprimer,cpsagoals}.tex: Repaired errors and made+	improvements in response to a review of this document.+ 2015-05-21  John D. Ramsdell  <ramsdell@mitre.org>  	* cpsa.cabal (Version): Tagged as version 2.5.0
NEWS view
@@ -1,5 +1,9 @@ CPSA NEWS -- history of user-visible changes. +* Changes in version 2.5.1++** CPSA Goals document updated+ * Changes in version 2.5.0  ** Added support for security goals
cpsa.cabal view
@@ -1,5 +1,5 @@ Name:			cpsa-Version:		2.5.0+Version:		2.5.1 Maintainer:		ramsdell@mitre.org Cabal-Version:		>= 1.6 License:		BSD3
doc/cpsadesign.pdf view

binary file changed (275306 → 275303 bytes)

doc/cpsagoals.pdf view

binary file changed (194012 → 194667 bytes)

doc/cpsagoals.tex view
@@ -137,7 +137,7 @@   (precedes ((0 0) (1 0)) ((1 1) (0 1)))   (non-orig (privk b))   (uniq-orig n1)-  (satisfied yes))+  (satisfies yes)) \end{verbatim} \caption{Needham-Schroeder Initiator Point of View} \label{fig:ns init}@@ -168,12 +168,13 @@  To be precise, a security goal is an order-sorted first-order logic sentence in a restricted form.  The sentence in Figure~\ref{fig:ns-  init} has the form shared by all security goals.  It is a universally-quantified implication.  The antecedent is a conjunction of atomic-formulas.  For this sentence, the conclusion is an existentially-quantified conjunction of atomic formulas, but in general, the-conclusion is a disjunction of existentially quantified conjunctions-of atomic formulas.  \sym{(false)} is a synonym for \sym{(or)}.+  init} has the form shared by all security goals.  It is a+universally quantified implication.  The antecedent is a conjunction+of atomic formulas.  For this sentence, the conclusion is an+existentially quantified conjunction of atomic formulas, but in+general, the conclusion is a disjunction of existentially quantified+conjunctions of atomic formulas.  In what follows, \sym{(false)} is a+synonym for \sym{(or)}.  \begin{center}\scshape   \begin{tabular}{rcl}@@ -194,17 +195,30 @@ implication.  The predicates used to construct an atomic formula (\textsc{atomic})-are listed in Table~\ref{tab:predicates}.  The first line gives the-syntax of a role position predicate.  It contains three tokens,-\texttt{p}, a string that names a role, and an integer that specifies-a position within the trace of the role.  That is, for role~$r$ with a-trace of length~$n$, there are~$n$ role position predicates,-\mbox{\texttt{p} $r$ $i$}, for $0\leq i < n$.  The second line gives-the syntax of a role parameter predicate.  It contains three tokens,-\texttt{p}, a string that names a role, and a string that names a role-variable.  For role~$r$, there is role parameter predicate for each-variable declared by~$r$.+are listed in Table~\ref{tab:predicates}.  There are two classes of+predicates, protocol specific and protocol independent predicates, and+two kinds of protocol specific predicates, role position and role+parameter predicates.  Protocol specific predicates are distinguished+from protocol independent predicates by being composed of three+tokens, the first of which is \texttt{p}. +The first line of the table gives the syntax of a role position+predicate.  It contains three tokens, \texttt{p}, a string that names+a role, and an integer that specifies a position within the trace of+the role.  That is, for role~$r$ with a trace of length~$n$, there+are~$n$ role position predicates, \mbox{\texttt{p} $r$ $i$}, for+$0\leq i < n$.  Thus \verb|(p "init" 2 z0)| is an atomic formula using+the role position predicate for position 2 in the \texttt{init} role+of the protocol in Figure~\ref{fig:ns roles}.++The second line gives the syntax of a role parameter predicate.  It+contains three tokens, \texttt{p}, a string that names a role, and a+string that names a role variable.  For role~$r$, there is role+parameter predicate for each variable declared by~$r$.  Thus+\verb|(p "init" 2 "n1" z0 n1)| is an atomic formula using the role+parameter predicate for parameter \text{n1} in the \texttt{init} role+of the protocol.+ The empty string names the listener role of a protocol.  The role has the variable \texttt{x} of sort \texttt{mesg} as its only role variable.  There are two positions in the listener role.@@ -437,8 +451,9 @@ \end{quote} The annotation includes a variable mapping for the shape that satisfies the antecedent of the goal but does not satisfy its-conclusion.  The mapping \texttt{(b b)} is the reason the shape does-not satisfy the goal.+conclusion.  The reason the shape does not satisfy the goal is because+the mapping \texttt{(b b)} maps the initiator's \texttt{b} parameter+to \texttt{b}, not \texttt{b-0} as is required to model the shape.  Galvin Lowe identified this authentication failure in Needham-Schroeder and provided a fix.  In the Needham-Schroeder-Lowe@@ -467,7 +482,7 @@  Figure~\ref{fig:ns secrecy} contains an analysis of Needham-Schroeder from the point of view of a complete run of the initiator under the-assumption that the responder's and its peer's private key are+assumption that the responder's and its peer's private keys are uncompromised and the nonce~\texttt{n1} it generates uniquely originates.  Futhermore, the point of view asserts that the nonce is leaked using a listener.@@ -486,7 +501,7 @@ this example, process the sample file \texttt{goal.scm} with {\cpsa} and display its output in a browser. -The protocol and its goal is shown in Figure~\ref{fig:unilateral}.+The protocol and its goal are shown in Figure~\ref{fig:unilateral}. The goal asserts that if a realized skeleton contains a full length initiator strand that uniquely generates \texttt{n1}, and peer~\texttt{a}'s private key is uncompromised, then the skeleton will@@ -594,7 +609,7 @@ {\cpsa} has demonstrated two ways in which Needham-Schroeder achieves the goals of the Unilateral Protocol. -\section{The Whole Story}\label{sec:whole story}+\section{The Rest of the Story}\label{sec:whole story}  The examples in the previous section demonstrate the typical way security goals are analyzed with {\cpsa}.  However, there are more@@ -608,7 +623,7 @@ It is wise to ensure that the antecedent in every sentence is identical.  When {\cpsa} performs satisfaction-checking on sentence~$\Phi$, it only determines if each shape it finds is-satisfied.  If the point of view skeleton in not the characteristic+satisfied.  If the point of view skeleton is not the characteristic skeleton of the antecedent of~$\Phi$, the fact that all skeletons satisfy~$\Phi$ cannot be used to conclude that~$\Phi$ is true in all executions of the protocol.@@ -649,7 +664,7 @@ \end{quote}  The program \texttt{cpsasas}, discussed in the next section, can be-used to generate an formula with an antecedent such that the input+used to generate a formula with an antecedent such that the input skeleton is the characteristic skeleton of the antecedent.  \subsection{Shape Analysis Sentences}\label{sec:sas}
doc/cpsaintroslides.pdf view

binary file changed (93099 → 93123 bytes)

doc/cpsaintroslides.tex view
@@ -221,7 +221,7 @@ \begin{mitreslide}{Blanchet Problem Statement} \begin{itemize} \item Analyze from the point-of-view of a full length responder-\item Assume $\privk{B}$ is uncompromised+\item Assume $\privk{A}$ and $\privk{B}$ are uncompromised \item Assume symmetric key~$S$ is freshly generated \hfill\raisebox{0ex}[0ex]{\includegraphics{blanchet-5.mps}} \end{itemize}@@ -230,7 +230,7 @@ (defskeleton blanchet   (vars (a b name) (s skey) (d data))   (defstrand resp 2 (a a) (b b) (s s) (d d))-  (non-orig (privk b))+  (non-orig (privk a) (privk b))   (uniq-orig s)) \end{verbatim} \end{quote}
doc/cpsaoverview.pdf view

binary file changed (128944 → 128941 bytes)

doc/cpsaprimer.pdf view

binary file changed (276659 → 276623 bytes)

doc/cpsaprimer.tex view
@@ -84,7 +84,7 @@ tools used to interpret the results.  The analyzer, \texttt{cpsa}, provides support for several algebras, one of which is the Basic Crypto Algebra.  Programs that assist in the interpretation of results-are \texttt{cpsashape} and \texttt{cpsagraph}.  The analyzer prints+are \texttt{cpsashapes} and \texttt{cpsagraph}.  The analyzer prints the steps it used to solve each problem.  The \texttt{cpsashapes} program extracts the shapes discovered by an analyzer run.  The \texttt{cpsagraph} program graphs both forms of output using Scalable@@ -145,7 +145,7 @@ \section{BCA Messages}  Each message exchanged in a protocol is represented by a term.  Terms-represent atomic values such text objects, principal names, and+represent atomic values such as text objects, principal names, and asymmetric and symmetric keys.  They also represent values composed from other values via encryption and concatenation. @@ -890,7 +890,7 @@  For each skeleton, a {\cpsa} analyzer computes a set of skeletons that refine it using a fixed set of operations based on authentication-tests.  The immediate descendants of a skeleton is called its+tests.  The immediate descendants of a skeleton are called its \index{cohort}\emph{cohort.}  A member of the cohort that is equivalent to a previously seen skeleton is replaced by that skeleton. Thus the skeletons in an analysis form a directed acyclic graph.  All@@ -1146,7 +1146,7 @@ This section contains advice derived from using {\cpsa}.  When specifying {\cpsa} input, one must decide when to specify terms as uniquely originating or non-originating in a role, and when to-specifying them in the initial skeleton.  If a flesh value is+specifying them in the initial skeleton.  If a fresh value is generated by all programs that implement a role in a protocol, the term that represents the fresh value should be assumed to be uniquely originating in the role.  Otherwise, unique origination assumptions
doc/cpsaspec.pdf view

binary file changed (387770 → 387769 bytes)

doc/macros.tex view
@@ -1,5 +1,5 @@ \newcommand{\cpsa}{\textsc{cpsa}}-\newcommand{\version}{2.5.0}+\newcommand{\version}{2.5.1} \newcommand{\cpsacopying}{\begingroup   \renewcommand{\thefootnote}{}\footnotetext{{\copyright} 2010 The     MITRE Corporation.  Permission to copy without fee all or part of
src/CPSA/Basic/Algebra.hs view
@@ -261,13 +261,17 @@ isAtom (D _) = False isAtom (P _) = False --- Does a term occur in another term?+-- Does a variable occur in a term? occursIn :: Term -> Term -> Bool-occursIn t t' =-    t == t' ||+occursIn t t' | isVar t =+  recur (I $ varId t) t'+  where+    recur t t' =+      t == t' ||       case t' of-        F _ u -> any (occursIn t) u+        F _ u -> any (recur t) u         _ -> False+occursIn t _ = error $ "Algebra.occursIn: Bad variable " ++ show t  -- Fold f through a term applying it to each variable in the term. foldVars :: (a -> Term -> a) -> a -> Term -> a
src/CPSA/DiffieHellman/Algebra.hs view
@@ -540,18 +540,20 @@   s == Text || s == Data || s == Name || s == Skey || s == Akey isAtom (G x) = isBasisVar x --- Does a term occur in another term?+-- Does a variable occur in a term?  -- This function is always called with a variable that answers true to--- isAcquiredVar as its first argument, so the first case never gets used.+-- isAcquiredVar as its first argument. occursIn :: Term -> Term -> Bool-occursIn (G t) (G t') =-  t == t'-occursIn t t' =-  t == t' ||-  case t' of-    F _ u -> any (occursIn t) u-    _ -> False+occursIn t t' | isVar t =+  recur (I $ varId t) t'+  where+    recur t t' =+      t == t' ||+      case t' of+        F _ u -> any (recur t) u+        _ -> False+occursIn t _ = error $ "Algebra.occursIn: Bad variable " ++ show t  -- Fold f through a term applying it to each variable in the term. foldVars :: (a -> Term -> a) -> a -> Term -> a
src/CPSA/Lib/Algebra.hs view
@@ -36,7 +36,7 @@     -- when applied to node variables.     isNodeVar :: t -> Bool -    -- Does a term occur in another term?+    -- Does a variable occur in a term?     occursIn :: t -> t -> Bool      -- Check to see if a list of terms is well-formed.
src/CPSA/Lib/Reduction.hs view
@@ -210,8 +210,8 @@         do           let ns = unrealized (content lk)           let shape = null ns-          wrt p h  (commentPreskel lk [] ns shape-                    (if shape then "" else "empty cohort"))+          wrt p h (commentPreskel lk [] ns shape+                   (if shape then "" else "empty cohort"))           step p h ks m oseen n seen todo tobig reducts     | otherwise =         do@@ -221,7 +221,7 @@           let u = size - length dups'           let msg = shows size $ showString " in cohort - " $                          shows u " not yet seen"-          wrt p h  (commentPreskel lk (reverse dups') ns cols msg)+          wrt p h (commentPreskel lk (reverse dups') ns cols msg)           step p h ks m oseen n' seen' todo' tobig reducts  -- Expands one branch in the derivation tree.
src/CPSA/Lib/Strand.hs view
@@ -1931,13 +1931,10 @@ satisfy (RolePred r i n) = grole r i n satisfy (ParamPred r v n t) = gparam r v n t --- Equality This isn't right.  Suppose t is a compound term which has--- some unbound variable.  Need static role specific check to--- eliminate this case.+-- Equality assumes there has been a static role specific check to+-- eliminate error cases. geq :: Algebra t p g s e c => t -> t -> Sem t g s e geq t t' _ (g, e)-  | t == ti = error ("Strand.geq: " ++ show t ++ " unbound")-  | t' == ti' = error ("Strand.geq: " ++ show t' ++ " unbound")   | ti == ti' = [(g, e)]   | otherwise = []   where@@ -2004,7 +2001,7 @@ gprec n n' k (g, e) =   case (nodeLookup e n, nodeLookup e n') of     (Just p, Just p')-      | inSkel k p && inSkel k p' && +      | inSkel k p && inSkel k p' &&         (strandPrec p p' || elem (p, p') tc) -> [(g, e)]     (Just _, Just _) -> []     (_, Just _) ->
tst/DH_hack.tst view
@@ -1,6 +1,6 @@ (herald "DH Hack" (bound 15)) -(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from DH_hack.scm") (comment "Strand count bounded at 15")
tst/blanchet.tst view
@@ -1,7 +1,7 @@ (herald "Blanchet's Simple Example Protocol"   (comment "There is a flaw in this protocol by design")) -(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from blanchet.scm")  (defprotocol blanchet basic
tst/completeness-test.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from completeness-test.scm")  (defprotocol completeness-test basic
tst/crushing.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from crushing.scm")  (defprotocol crushing basic
tst/dass_simple.tst view
@@ -1,6 +1,6 @@ (herald "Distributed Authentication Security Service Protocol Variants") -(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from dass_simple.scm")  (defprotocol dass-simple basic
tst/denning-sacco.tst view
@@ -1,6 +1,6 @@ (herald "Denning-Sacco Protocol") -(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from denning-sacco.scm")  (defprotocol denning-sacco basic
tst/deorig_contract.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from deorig_contract.scm")  (defprotocol deorig-contract basic
tst/deorig_mesg.tst view
@@ -1,6 +1,6 @@ (herald deorig-mesg) -(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from deorig_mesg.scm")  (defprotocol deorig-mesg basic
tst/deorig_simple.tst view
@@ -1,6 +1,6 @@ (herald deorig-simple) -(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from deorig_simple.scm")  (defprotocol deorig-simple basic
tst/dy.tst view
@@ -1,6 +1,6 @@ (herald "Example 1.3 from 1983 Dolev-Yao Paper") -(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from dy.lsp")  (defprotocol dy basic
tst/encsig.tst view
@@ -1,7 +1,7 @@ (herald "Encrypted Signed Message Example"   (comment "Shows examples of key usage of asymmetric keys")) -(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from encsig.scm")  (defprotocol mult-keys-enc-sig basic
tst/epmo-hash.tst view
@@ -1,7 +1,7 @@ (herald "Electronic Purchase with Money Order Protocol with Key Hashing"   (comment "Annotated with trust management formulas")) -(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from epmo-hash.scm")  (defprotocol epmo basic
tst/epmo-key-hash.tst view
@@ -1,7 +1,7 @@ (herald "Electronic Purchase with Money Order Protocol with Key Hashing"   (comment "Annotated with trust management formulas")) -(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from epmo-key-hash.scm")  (defprotocol epmo basic
tst/epmo.tst view
@@ -1,7 +1,7 @@ (herald "Electronic Purchase with Money Order Protocol"   (comment "Annotated with trust management formulas")) -(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from epmo.scm")  (defprotocol epmo basic
tst/epmo_acctnum-key-hash.tst view
@@ -2,7 +2,7 @@   "Electronic Purchase with Money Order Protocol Variant with Key Hashing"   (comment "This version includes account numbers in exchanges")) -(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from epmo_acctnum-key-hash.scm")  (defprotocol epmo_acctnum basic
tst/ffgg.tst view
@@ -1,7 +1,7 @@ (herald "The ffgg Protocol"   (comment "From A Necessarily Parallel Attack by Jon K. Millen")) -(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from ffgg.scm")  (defprotocol ffgg basic
tst/fragile_pruning.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from fragile_pruning.scm")  (defprotocol fragile_pruning basic
tst/goals.scm view
@@ -1,89 +1,146 @@ (herald goals) -;;; Some authentication goals+;;; Section 1 --- Examples from CPSA and Formal Security Goals -;;; Unilateral authentication+;;; Needham-Schroeder from Section 10 of the CPSA Primer -(defprotocol unilateral basic+(defprotocol ns basic   (defrole init-     (vars (a name) (n text))-     (trace-      (send (enc n (pubk a)))-      (recv n)))+    (vars (a b name) (n1 n2 text))+    (trace+     (send (enc n1 a (pubk b)))+     (recv (enc n1 n2 (pubk a)))+     (send (enc n2 (pubk b)))))   (defrole resp-     (vars (a name) (n text))-     (trace-      (recv (enc n (pubk a)))-      (send n))))+    (vars (b a name) (n2 n1 text))+    (trace+     (recv (enc n1 a (pubk b)))+     (send (enc n1 n2 (pubk a)))+     (recv (enc n2 (pubk b)))))+  (comment "Needham-Schroeder with no role origination assumptions")) -(defgoal unilateral-  (forall ((a name) (n text) (z0 node))-	  (implies-	   (and -	    (p "init" 1 z0)-	    (p "init" "n" z0 n)-	    (p "init" "a" z0 a)-	    (non (privk a))-	    (uniq n))-	   (exists ((z1 node))-		   (and-		    (p "resp" 1 z1)-		    (p "resp" "a" z1 a)))))-  (comment "Authentication goal"))+(defgoal ns+  (forall ((b name) (n1 text) (z0 node))+    (implies+     (and (p "init" 2 z0)+      (p "init" "n1" z0 n1) (p "init" "b" z0 b)+      (non (privk b)) (uniq n1))+     (exists ((z1 node))+	     (and (p "resp" 1 z1) (p "resp" "b" z1 b)))))+  (comment "Initiator point of view")+  (comment "Authentication goal: agreement on name b")) -(defprotocol ns basic+(defgoal ns+  (forall ((b name) (n1 text) (z0 node))+    (implies+     (and (p "init" 2 z0)+      (p "init" "n1" z0 n1) (p "init" "b" z0 b)+      (non (privk b)) (uniq n1))+     (exists ((z1 node))+	     (and (p "resp" 1 z1) (p "resp" "b" z1 b)+	      (prec z1 z0)))))+  (comment "Prec example"))++(defgoal ns+  (forall ((a b name) (n2 text) (z0 node))+    (implies+     (and (p "resp" 2 z0) (p "resp" "n2" z0 n2)+      (p "resp" "a" z0 a) (p "resp" "b" z0 b)+      (non (privk a)) (uniq n2))+     (exists ((z1 node))+      (and (p "init" 1 z1) (p "init" "b" z1 b)))))+  (comment "Responder point of view")+  (comment "Failed authentication goal: agreement on name b"))++(defprotocol nsl basic   (defrole init     (vars (a b name) (n1 n2 text))     (trace      (send (enc n1 a (pubk b)))-     (recv (enc n1 n2 (pubk a)))+     (recv (enc n1 n2 b (pubk a)))      (send (enc n2 (pubk b)))))   (defrole resp-    (vars (a b name) (n1 n2 text))+    (vars (b a name) (n2 n1 text))     (trace      (recv (enc n1 a (pubk b)))-     (send (enc n1 n2 (pubk a)))+     (send (enc n1 n2 b (pubk a)))      (recv (enc n2 (pubk b)))))-  (comment "Needham-Schroeder"))+  (comment "Needham-Schroeder-Lowe with no role origination assumptions")) +(defgoal nsl+  (forall ((a b name) (n2 text) (z0 node))+    (implies+     (and (p "resp" 2 z0) (p "resp" "n2" z0 n2)+      (p "resp" "a" z0 a) (p "resp" "b" z0 b)+      (non (privk a)) (uniq n2))+     (exists ((z1 node))+      (and (p "init" 1 z1) (p "init" "b" z1 b)))))+  (comment "Responder point of view")+  (comment "Authentication goal: agreement on name b"))++(defgoal ns+  (forall ((a b name) (n1 text) (z0 z1 node))+    (implies+     (and (p "init" 2 z0) (p "init" "n1" z0 n1)+      (p "init" "a" z0 a) (p "init" "b" z0 b)+      (p "" 0 z1) (p "" "x" z1 n1)+      (non (privk a)) (non (privk b)) (uniq n1))+     (false)))+  (comment "Initiator point of view")+  (comment "Secrecy goal: nonce n1 not revealed"))++(defprotocol unilateral basic+  (defrole init+    (vars (a name) (n text))+    (trace+     (send (enc n (pubk a)))+     (recv n)))+  (defrole resp+    (vars (a name) (n text))+    (trace+     (recv (enc n (pubk a)))+     (send n)))+  (comment "Unilateral authentication"))++(defgoal unilateral+  (forall ((a name) (n text)+           (z0 node))+   (implies+    (and (p "init" 1 z0)+     (p "init" "n" z0 n)+     (p "init" "a" z0 a)+     (non (privk a)) (uniq n))+    (exists ((z1 node))+     (and (p "resp" 1 z1)+      (p "resp" "a" z1 a)))))+  (comment "Unilateral authentication goal"))+ ;;; Does initiator satisfy the unilateral authentication goal?  ;;; Note that the goal requires translation of some of the role ;;; specific predicates. (defgoal ns   (forall ((a name) (n text) (z0 node))-	  (implies-	   (and -	    (p "init" 1 z0)-	    (p "init" "n1" z0 n)-	    (p "init" "b" z0 a)-	    (non (privk a))-	    (uniq n))-	   (exists ((z1 node))-		   (and-		    (p "resp" 1 z1)-		    (p "resp" "b" z1 a)))))+   (implies+    (and (p "init" 1 z0) (p "init" "n1" z0 n)+     (p "init" "b" z0 a) (non (privk a)) (uniq n))+    (exists ((z1 node))+     (and (p "resp" 1 z1) (p "resp" "b" z1 a)))))   (comment "Initiator authentication goal")   (comment "Same as unilateral goal under the predicate mapping:")   (comment (p "init" "n") "->" (p "init" "n1") "and")   (comment (p "init" "a") "->" (p "init" "b") "and")   (comment (p "resp" "a") "->" (p "resp" "b")))-  + ;;; Does responder satisfy the unilateral authentication goal?  (defgoal ns   (forall ((a name) (n text) (z0 node))-	  (implies-	   (and -	    (p "resp" 2 z0)-	    (p "resp" "n2" z0 n)-	    (p "resp" "a" z0 a)-	    (non (privk a))-	    (uniq n))-	   (exists ((z1 node))-		   (and-		    (p "init" 2 z1)-		    (p "init" "a" z1 a)))))+   (implies+    (and (p "resp" 2 z0) (p "resp" "n2" z0 n)+     (p "resp" "a" z0 a) (non (privk a)) (uniq n))+    (exists ((z1 node))+     (and (p "init" 2 z1) (p "init" "a" z1 a)))))   (comment "Responder authentication goal")   (comment "Same as unilateral goal under the predicate mapping:")   (comment (p "init" 1) "->" (p "resp" 2) "and")@@ -94,172 +151,175 @@  (defgoal ns   (forall ((a b name) (n text) (z0 node))-	  (implies-	   (and -	    (p "init" 1 z0)-	    (p "init" "n1" z0 n)-	    (p "init" "a" z0 a)-	    (p "init" "b" z0 b)-	    (non (privk a))-	    (non (privk b))-	    (uniq n))-	   (exists ((z1 node))-		   (and-		    (p "resp" 1 z1)-		    (p "resp" "b" z1 b)))))+    (implies+     (and+      (p "init" 1 z0) (p "init" "n1" z0 n)+      (p "init" "a" z0 a) (p "init" "b" z0 b)+      (non (privk a)) (non (privk b)) (uniq n))+     (exists ((z1 node))+      (and (p "resp" 1 z1) (p "resp" "b" z1 b)))))   (forall ((a b name) (n text) (z0 node))-	  (implies-	   (and -	    (p "init" 1 z0)-	    (p "init" "n1" z0 n)-	    (p "init" "a" z0 a)-	    (p "init" "b" z0 b)-	    (non (privk a))-	    (non (privk b))-	    (uniq n))-	   (exists ((z1 node))-		   (and-		    (p "resp" 1 z1)-		    (p "resp" "a" z1 a)))))-  (comment "Double initiator authentication goal"))-  +   (implies+     (and+      (p "init" 1 z0) (p "init" "n1" z0 n)+      (p "init" "a" z0 a) (p "init" "b" z0 b)+      (non (privk a)) (non (privk b)) (uniq n))+     (exists ((z1 node))+      (and (p "resp" 1 z1) (p "resp" "a" z1 a)))))+  (comment "Two initiator authentication goals"))++;;; The shape analysis sentence as input (kind of useless)+ (defgoal ns-  (forall ((a b name) (n text) (z0 node))-	  (implies-	   (and -	    (p "resp" 2 z0)-	    (p "resp" "n2" z0 n)-	    (p "resp" "a" z0 a)-	    (p "resp" "b" z0 b)-	    (non (privk a))-	    (non (privk b))-	    (uniq n))-	   (exists ((z1 node))-		   (and-		    (p "init" 2 z1)-		    (p "init" "a" z1 a)))))-  (forall ((a b name) (n text) (z0 node))-	  (implies-	   (and -	    (p "resp" 2 z0)-	    (p "resp" "n2" z0 n)-	    (p "resp" "a" z0 a)-	    (p "resp" "b" z0 b)-	    (non (privk a))-	    (non (privk b))-	    (uniq n))-	   (exists ((z1 node))-		   (and-		    (p "init" 2 z1)-		    (p "init" "b" z1 b)))))-  (comment "Double responder authentication goal"))+  (forall ((n1 n2 text) (b a name) (z z-0 node))+    (implies+      (and (p "init" 0 z) (p "init" 2 z-0)+        (p "init" "n1" z-0 n1) (p "init" "n2" z-0 n2)+        (p "init" "a" z-0 a) (p "init" "b" z-0 b)+        (str-prec z z-0) (non (privk b)) (uniq-at n1 z))+      (exists ((n2-0 text) (z-1 z-2 z-3 node))+        (and (p "init" 1 z-1) (p "resp" 0 z-2)+          (p "resp" 1 z-3) (p "resp" "n2" z-3 n2-0)+          (p "resp" "n1" z-3 n1) (p "resp" "b" z-3 b)+          (p "resp" "a" z-3 a) (prec z z-2) (prec z-3 z-1)+          (str-prec z z-1) (str-prec z-1 z-0)+          (str-prec z-2 z-3)))))+  (comment "Shape analysis sentence")) -;;; Old stuff+;;; Section 2 --- Additional Examples -;;; The initiator point-of-view+(defgoal ns+  (forall ((a b name) (n2 text) (z0 z1 node))+    (implies+     (and+      (p "resp" 2 z0) (p "resp" "n2" z0 n2)+      (p "resp" "a" z0 a) (p "resp" "b" z0 b)+      (p "" 0 z1) (p "" "x" z1 n2)+      (non (privk a)) (non (privk b)) (uniq n2))+     (false)))+  (comment "Responder point of view")+  (comment "Failed secrecy goal: nonce n2 not revealed"))++;;; Double initiator point of view (defskeleton ns-  (vars (a b name) (n1 text))+  (vars (a b name) (n1 n1-0 text))   (defstrand init 3 (a a) (b b) (n1 n1))+  (defstrand init 3 (a a) (b b) (n1 n1-0))   (non-orig (privk b) (privk a))-  (uniq-orig n1)+  (uniq-orig n1 n1-0)   (goals-   (forall ((a b name) (n1 text) (no nu node))-	   (implies-	    (and (p "init" 2 no)-		 (p "init" "a" no a)-		 (p "init" "b" no b)-		 (p "init" "n1" no n1)-		 (p "init" 0 nu)-		 (str-prec nu no)-		 (non (privk a))-		 (non (privk b))-		 (uniq-at n1 nu))-	    (exists ((na nb node))-		    (and (p "init" 2 na)-			 (p "resp" 1 nb)-			 (p "init" "b" na b)-			 (p "resp" "b" nb b))))))-  (comment "Initiator point-of-view"))+   (forall ((n1 n1-0 n2 n2-0 text) (a b name) (z z-0 z-1 z-2 node))+    (implies+     (and+      (p "init" 0 z) (p "init" 2 z-0) (p "init" 0 z-1)+      (p "init" 2 z-2) (p "init" "n1" z-0 n1) (p "init" "n2" z-0 n2)+      (p "init" "a" z-0 a) (p "init" "b" z-0 b)+      (p "init" "n1" z-2 n1-0) (p "init" "n2" z-2 n2-0)+      (p "init" "a" z-2 a) (p "init" "b" z-2 b) (str-prec z z-0)+      (str-prec z-1 z-2) (non (privk a)) (non (privk b))+      (uniq-at n1 z) (uniq-at n1-0 z-1))+     (= z-1 z))))+  (comment "Double initiator point of view")) -(defgoal ns-  (forall ((a b name) (n1 text) (no nu node))-	  (implies-	   (and (p "init" 2 no)-		(p "init" "a" no a)-		(p "init" "b" no b)-		(p "init" "n1" no n1)-		(p "init" 0 nu)-		(str-prec nu no)-		(non (privk a))-		(non (privk b))-		(uniq-at n1 nu))-	   (exists ((na nb node))-		   (and (p "init" 2 na)-			(p "resp" 1 nb)-			(p "init" "b" na b)-			(p "resp" "b" nb b)))))-  (comment "Initiator point-of-view"))+(defprotocol nsl-typeless basic+  (defrole init+    (vars (a b name) (n1 text) (n2 mesg))+    (trace+     (send (enc a n1 (pubk b)))+     (recv (enc n1 n2 b (pubk a)))+     (send (enc n2 (pubk b)))))+  (defrole resp+    (vars (b a name) (n2 text) (n1 mesg))+    (trace+     (recv (enc a n1 (pubk b)))+     (send (enc n1 n2 b (pubk a)))+     (recv (enc n2 (pubk b)))))+  (comment "Needham-Schroeder-Lowe with untyped nonces")) -;;; The responder point-of-view+;;; The responder point of view+(defgoal nsl-typeless+  (forall ((n2 text) (a b name) (z z-0 node))+    (implies+      (and (p "resp" 1 z) (p "" 0 z-0)+        (p "resp" "n2" z n2) (p "resp" "b" z b) (p "resp" "a" z a)+        (p "" "x" z-0 n2) (non (privk a)) (non (privk b)) (uniq n2))+      (false)))+  (comment "Shows typeflaw in typeless NSL"))+ (defskeleton ns   (vars (a name) (n2 text))   (defstrand resp 3 (a a) (n2 n2))   (non-orig (privk a))   (uniq-orig n2)   (goals-  (forall ((n2 n1 text) (a b name) (z z-0 node))+   (forall ((n1 n2 text) (a b name) (z z-0 node))     (implies-      (and (p "resp" 1 z) (p "resp" 2 z-0) (p "resp" "n2" z-0 n2)-        (p "resp" "n1" z-0 n1) (p "resp" "b" z-0 b) (p "resp" "a" z-0 a)-        (str-prec z z-0) (non (privk a)) (uniq-at n2 z))-      (exists ((b-0 name) (z-1 z-2 node))-        (and (p "init" 1 z-1) (p "init" 2 z-2) (p "init" "n1" z-2 n1)-          (p "init" "n2" z-2 n2) (p "init" "a" z-2 a)-          (p "init" "b" z-2 b-0) (prec z z-1) (prec z-2 z-0)-          (str-prec z-1 z-2))))))-  (comment "Responder point-of-view"))+      (and (p "init" 0 z) (p "init" 2 z-0)+        (p "init" "n1" z-0 n1) (p "init" "n2" z-0 n2)+        (p "init" "a" z-0 a) (p "init" "b" z-0 b)+        (str-prec z z-0) (non (privk a)) (non (privk b))+        (uniq-at n1 z))+      (exists ((z-1 z-2 z-3 node))+        (and (p "init" 1 z-1) (p "resp" 0 z-2)+          (p "resp" 1 z-3) (p "resp" "n2" z-3 n2)+          (p "resp" "n1" z-3 n1) (p "resp" "b" z-3 b)+          (p "resp" "a" z-3 a) (prec z z-2) (prec z-3 z-1)+          (str-prec z z-1) (str-prec z-1 z-0)+          (str-prec z-2 z-3))))))+  (comment "Responder point of view with SAS")) -;;; The responder point-of-view (defskeleton ns   (vars (a name) (n2 text))   (defstrand resp 3 (a a) (n2 n2))   (non-orig (privk a))   (uniq-orig n2)   (goals-   (forall ((n2 n1 text) (a b name) (z z-0 node))+   (forall ((n1 n2 text) (a b name) (z z-0 node))     (implies-      (and (p "resp" 1 z) (p "resp" 2 z-0) (p "resp" "n2" z-0 n2)-        (p "resp" "n1" z-0 n1) (p "resp" "b" z-0 b) (p "resp" "a" z-0 a)-        (str-prec z z-0) (non (privk a)) (uniq-at n2 z))-      (exists ((b-0 name) (z-1 z-2 node))-        (and (p "init" 1 z-1) (p "init" 2 z-2) (p "init" "n1" z-2 n1)-          (p "init" "n2" z-2 n2) (p "init" "a" z-2 a)-          (p "init" "b" z-2 b-0) (prec z z-1) (prec z-2 z-0)-          (str-prec z-1 z-2))))))-  (comment "Responder point-of-view"))+      (and (p "init" 0 z) (p "init" 2 z-0)+        (p "init" "n1" z-0 n1) (p "init" "n2" z-0 n2)+        (p "init" "a" z-0 a) (p "init" "b" z-0 b)+        (str-prec z z-0) (non (privk a)) (non (privk b))+        (uniq-at n1 z))+      (false))))+  (comment "Responder point of view with false as the conclusion")) -;;; Double initiator point-of-view (defskeleton ns-  (vars (a b name) (n1 n1-0 text))+  (vars (a b name) (n1 text))   (defstrand init 3 (a a) (b b) (n1 n1))-  (defstrand init 3 (a a) (b b) (n1 n1-0))   (non-orig (privk b) (privk a))-  (uniq-orig n1 n1-0)+  (uniq-orig n1)   (goals-   (forall ((n1 n1-0 n2 n2-0 text) (a b name) (z z-0 z-1 z-2 node))-	   (implies-	    (and (p "init" 0 z) (p "init" 2 z-0) (p "init" 0 z-1)-		 (p "init" 2 z-2) (p "init" "n1" z-0 n1) (p "init" "n2" z-0 n2)-		 (p "init" "a" z-0 a) (p "init" "b" z-0 b)-		 (p "init" "n1" z-2 n1-0) (p "init" "n2" z-2 n2-0)-		 (p "init" "a" z-2 a) (p "init" "b" z-2 b) (str-prec z z-0)-		 (str-prec z-1 z-2) (non (privk a)) (non (privk b))-		 (uniq-at n1 z) (uniq-at n1-0 z-1))-	    (= z-1 z))))-  (comment "Double initiator point-of-view"))+   (forall ((n1 n2 text) (a b name) (z z-0 node))+    (implies+      (and (p "init" 0 z) (p "init" 2 z-0)+        (p "init" "n1" z-0 n1) (p "init" "n2" z-0 n2)+        (p "init" "a" z-0 a) (p "init" "b" z-0 b)+        (str-prec z z-0) (non (privk a)) (non (privk b))+        (uniq-at n1 z))+      (false))))+  (comment "Initiator point of view with false as the conclusion")) +(defgoal ns+  (forall ((a b name) (n text) (z0 node))+   (implies+    (and+     (p "resp" 2 z0) (p "resp" "n2" z0 n)+     (p "resp" "a" z0 a) (p "resp" "b" z0 b)+     (non (privk a)) (non (privk b)) (uniq n))+    (exists ((z1 node))+     (and (p "init" 2 z1) (p "init" "a" z1 a)))))+  (forall ((a b name) (n text) (z0 node))+   (implies+    (and+     (p "resp" 2 z0) (p "resp" "n2" z0 n)+     (p "resp" "a" z0 a) (p "resp" "b" z0 b)+     (non (privk a)) (non (privk b)) (uniq n))+    (exists ((z1 node))+     (and (p "init" 2 z1) (p "init" "b" z1 b)))))+  (comment "Two responder authentication goals"))+ ;;; Needham-Schroeder Protocol with origination assumptions on roles-;;; This  (defprotocol ns-role-origs basic   (defrole init@@ -280,12 +340,12 @@     (uniq-orig n2))   (comment "Needham-Schroeder with role assumptions that are too strong")) -;;; The initiator point-of-view+;;; The initiator point of view (defskeleton ns-role-origs   (vars)   (defstrand init 3)) -;;; The responder point-of-view+;;; The responder point of view (defskeleton ns-role-origs   (vars)   (defstrand resp 3))@@ -329,27 +389,3 @@   (non-orig (privk a))   (uniq-orig n1)   (precedes ((1 1) (0 1))))--(defprotocol nsl-typeless basic-  (defrole init-    (vars (a b name) (n1 text) (n2 mesg))-    (trace-     (send (enc a n1 (pubk b)))-     (recv (enc n1 n2 b (pubk a)))-     (send (enc n2 (pubk b)))))-  (defrole resp-    (vars (b a name) (n2 text) (n1 mesg))-    (trace-     (recv (enc a n1 (pubk b)))-     (send (enc n1 n2 b (pubk a)))-     (recv (enc n2 (pubk b)))))-  (comment "Needham-Schroeder-Lowe with untyped nonces"))--;;; The responder point-of-view-(defskeleton nsl-typeless-  (vars (a b name) (n2 text))-  (defstrand resp 2 (a a) (n2 n2) (b b))-  (deflistener n2)-  (non-orig (privk a) (privk b))-  (uniq-orig n2)-  (comment "Shows typeflaw in typeless NSL"))
tst/goals.tst view
@@ -1,1117 +1,1645 @@ (herald goals) -(comment "CPSA 2.5.0")-(comment "All input read from goals.scm")--(defprotocol unilateral basic-  (defrole init-    (vars (a name) (n text))-    (trace (send (enc n (pubk a))) (recv n)))-  (defrole resp-    (vars (a name) (n text))-    (trace (recv (enc n (pubk a))) (send n))))--(defskeleton unilateral-  (vars (n text) (a name))-  (defstrand init 2 (n n) (a a))-  (non-orig (privk a))-  (uniq-orig n)-  (goals-    (forall ((a name) (n text) (z0 node))-      (implies-        (and (p "init" 1 z0) (p "init" "n" z0 n) (p "init" "a" z0 a)-          (non (privk a)) (uniq n))-        (exists ((z1 node))-          (and (p "resp" 1 z1) (p "resp" "a" z1 a))))))-  (comment "Authentication goal")-  (traces ((send (enc n (pubk a))) (recv n)))-  (label 0)-  (unrealized (0 1))-  (origs (n (0 0)))-  (comment "1 in cohort - 1 not yet seen"))--(defskeleton unilateral-  (vars (n text) (a name))-  (defstrand init 2 (n n) (a a))-  (defstrand resp 2 (n n) (a a))-  (precedes ((0 0) (1 0)) ((1 1) (0 1)))-  (non-orig (privk a))-  (uniq-orig n)-  (operation nonce-test (added-strand resp 2) n (0 1) (enc n (pubk a)))-  (traces ((send (enc n (pubk a))) (recv n))-    ((recv (enc n (pubk a))) (send n)))-  (label 1)-  (parent 0)-  (unrealized)-  (shape)-  (satisfies yes)-  (maps ((0) ((a a) (n n))))-  (origs (n (0 0))))--(comment "Nothing left to do")--(defprotocol ns basic-  (defrole init-    (vars (a b name) (n1 n2 text))-    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))-      (send (enc n2 (pubk b)))))-  (defrole resp-    (vars (a b name) (n1 n2 text))-    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))-      (recv (enc n2 (pubk b)))))-  (comment "Needham-Schroeder"))--(defskeleton ns-  (vars (n n2 text) (a a-0 name))-  (defstrand init 2 (n1 n) (n2 n2) (a a-0) (b a))-  (non-orig (privk a))-  (uniq-orig n)-  (goals-    (forall ((a name) (n text) (z0 node))-      (implies-        (and (p "init" 1 z0) (p "init" "n1" z0 n) (p "init" "b" z0 a)-          (non (privk a)) (uniq n))-        (exists ((z1 node))-          (and (p "resp" 1 z1) (p "resp" "b" z1 a))))))-  (comment "Initiator authentication goal"-    "Same as unilateral goal under the predicate mapping:"-    (p "init" "n") "->" (p "init" "n1") "and" (p "init" "a") "->"-    (p "init" "b") "and" (p "resp" "a") "->" (p "resp" "b"))-  (traces ((send (enc n a-0 (pubk a))) (recv (enc n n2 (pubk a-0)))))-  (label 2)-  (unrealized (0 1))-  (origs (n (0 0)))-  (comment "1 in cohort - 1 not yet seen"))--(defskeleton ns-  (vars (n n2 n2-0 text) (a a-0 name))-  (defstrand init 2 (n1 n) (n2 n2) (a a-0) (b a))-  (defstrand resp 2 (n1 n) (n2 n2-0) (a a-0) (b a))-  (precedes ((0 0) (1 0)) ((1 1) (0 1)))-  (non-orig (privk a))-  (uniq-orig n)-  (operation nonce-test (added-strand resp 2) n (0 1)-    (enc n a-0 (pubk a)))-  (traces ((send (enc n a-0 (pubk a))) (recv (enc n n2 (pubk a-0))))-    ((recv (enc n a-0 (pubk a))) (send (enc n n2-0 (pubk a-0)))))-  (label 3)-  (parent 2)-  (unrealized)-  (shape)-  (satisfies yes)-  (maps ((0) ((a a) (n n) (a-0 a-0) (n2 n2))))-  (origs (n (0 0))))--(comment "Nothing left to do")--(defprotocol ns basic-  (defrole init-    (vars (a b name) (n1 n2 text))-    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))-      (send (enc n2 (pubk b)))))-  (defrole resp-    (vars (a b name) (n1 n2 text))-    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))-      (recv (enc n2 (pubk b)))))-  (comment "Needham-Schroeder"))--(defskeleton ns-  (vars (n n1 text) (a b name))-  (defstrand resp 3 (n1 n1) (n2 n) (a a) (b b))-  (non-orig (privk a))-  (uniq-orig n)-  (goals-    (forall ((a name) (n text) (z0 node))-      (implies-        (and (p "resp" 2 z0) (p "resp" "n2" z0 n) (p "resp" "a" z0 a)-          (non (privk a)) (uniq n))-        (exists ((z1 node))-          (and (p "init" 2 z1) (p "init" "a" z1 a))))))-  (comment "Responder authentication goal"-    "Same as unilateral goal under the predicate mapping:" (p "init" 1)-    "->" (p "resp" 2) "and" (p "init" "n") "->" (p "resp" "n2") "and"-    (p "init" "a") "->" (p "resp" "a") "and" (p "resp" 1) "->"-    (p "init" 2) "and" (p "resp" "a") "->" (p "init" "a"))-  (traces-    ((recv (enc n1 a (pubk b))) (send (enc n1 n (pubk a)))-      (recv (enc n (pubk b)))))-  (label 4)-  (unrealized (0 2))-  (origs (n (0 1)))-  (comment "1 in cohort - 1 not yet seen"))--(defskeleton ns-  (vars (n n1 text) (a b b-0 name))-  (defstrand resp 3 (n1 n1) (n2 n) (a a) (b b))-  (defstrand init 3 (n1 n1) (n2 n) (a a) (b b-0))-  (precedes ((0 1) (1 1)) ((1 2) (0 2)))-  (non-orig (privk a))-  (uniq-orig n)-  (operation nonce-test (added-strand init 3) n (0 2)-    (enc n1 n (pubk a)))-  (traces-    ((recv (enc n1 a (pubk b))) (send (enc n1 n (pubk a)))-      (recv (enc n (pubk b))))-    ((send (enc n1 a (pubk b-0))) (recv (enc n1 n (pubk a)))-      (send (enc n (pubk b-0)))))-  (label 5)-  (parent 4)-  (unrealized)-  (shape)-  (satisfies yes)-  (maps ((0) ((a a) (n n) (b b) (n1 n1))))-  (origs (n (0 1))))--(comment "Nothing left to do")--(defprotocol ns basic-  (defrole init-    (vars (a b name) (n1 n2 text))-    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))-      (send (enc n2 (pubk b)))))-  (defrole resp-    (vars (a b name) (n1 n2 text))-    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))-      (recv (enc n2 (pubk b)))))-  (comment "Needham-Schroeder"))--(defskeleton ns-  (vars (n n2 text) (a b name))-  (defstrand init 2 (n1 n) (n2 n2) (a a) (b b))-  (non-orig (privk a) (privk b))-  (uniq-orig n)-  (goals-    (forall ((a b name) (n text) (z0 node))-      (implies-        (and (p "init" 1 z0) (p "init" "n1" z0 n) (p "init" "a" z0 a)-          (p "init" "b" z0 b) (non (privk a)) (non (privk b)) (uniq n))-        (exists ((z1 node)) (and (p "resp" 1 z1) (p "resp" "b" z1 b)))))-    (forall ((a b name) (n text) (z0 node))-      (implies-        (and (p "init" 1 z0) (p "init" "n1" z0 n) (p "init" "a" z0 a)-          (p "init" "b" z0 b) (non (privk a)) (non (privk b)) (uniq n))-        (exists ((z1 node))-          (and (p "resp" 1 z1) (p "resp" "a" z1 a))))))-  (comment "Double initiator authentication goal")-  (traces ((send (enc n a (pubk b))) (recv (enc n n2 (pubk a)))))-  (label 6)-  (unrealized (0 1))-  (origs (n (0 0)))-  (comment "1 in cohort - 1 not yet seen"))--(defskeleton ns-  (vars (n n2 n2-0 text) (a b name))-  (defstrand init 2 (n1 n) (n2 n2) (a a) (b b))-  (defstrand resp 2 (n1 n) (n2 n2-0) (a a) (b b))-  (precedes ((0 0) (1 0)) ((1 1) (0 1)))-  (non-orig (privk a) (privk b))-  (uniq-orig n)-  (operation nonce-test (added-strand resp 2) n (0 1)-    (enc n a (pubk b)))-  (traces ((send (enc n a (pubk b))) (recv (enc n n2 (pubk a))))-    ((recv (enc n a (pubk b))) (send (enc n n2-0 (pubk a)))))-  (label 7)-  (parent 6)-  (unrealized (0 1))-  (comment "1 in cohort - 1 not yet seen"))--(defskeleton ns-  (vars (n n2 text) (a b name))-  (defstrand init 2 (n1 n) (n2 n2) (a a) (b b))-  (defstrand resp 2 (n1 n) (n2 n2) (a a) (b b))-  (precedes ((0 0) (1 0)) ((1 1) (0 1)))-  (non-orig (privk a) (privk b))-  (uniq-orig n)-  (operation nonce-test (contracted (n2-0 n2)) n (0 1)-    (enc n n2 (pubk a)) (enc n a (pubk b)))-  (traces ((send (enc n a (pubk b))) (recv (enc n n2 (pubk a))))-    ((recv (enc n a (pubk b))) (send (enc n n2 (pubk a)))))-  (label 8)-  (parent 7)-  (unrealized)-  (shape)-  (satisfies yes yes)-  (maps ((0) ((a a) (b b) (n n) (n2 n2))))-  (origs (n (0 0))))--(comment "Nothing left to do")--(defprotocol ns basic-  (defrole init-    (vars (a b name) (n1 n2 text))-    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))-      (send (enc n2 (pubk b)))))-  (defrole resp-    (vars (a b name) (n1 n2 text))-    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))-      (recv (enc n2 (pubk b)))))-  (comment "Needham-Schroeder"))--(defskeleton ns-  (vars (n n1 text) (a b name))-  (defstrand resp 3 (n1 n1) (n2 n) (a a) (b b))-  (non-orig (privk a) (privk b))-  (uniq-orig n)-  (goals-    (forall ((a b name) (n text) (z0 node))-      (implies-        (and (p "resp" 2 z0) (p "resp" "n2" z0 n) (p "resp" "a" z0 a)-          (p "resp" "b" z0 b) (non (privk a)) (non (privk b)) (uniq n))-        (exists ((z1 node)) (and (p "init" 2 z1) (p "init" "a" z1 a)))))-    (forall ((a b name) (n text) (z0 node))-      (implies-        (and (p "resp" 2 z0) (p "resp" "n2" z0 n) (p "resp" "a" z0 a)-          (p "resp" "b" z0 b) (non (privk a)) (non (privk b)) (uniq n))-        (exists ((z1 node))-          (and (p "init" 2 z1) (p "init" "b" z1 b))))))-  (comment "Double responder authentication goal")-  (traces-    ((recv (enc n1 a (pubk b))) (send (enc n1 n (pubk a)))-      (recv (enc n (pubk b)))))-  (label 9)-  (unrealized (0 2))-  (origs (n (0 1)))-  (comment "1 in cohort - 1 not yet seen"))--(defskeleton ns-  (vars (n n1 text) (a b b-0 name))-  (defstrand resp 3 (n1 n1) (n2 n) (a a) (b b))-  (defstrand init 3 (n1 n1) (n2 n) (a a) (b b-0))-  (precedes ((0 1) (1 1)) ((1 2) (0 2)))-  (non-orig (privk a) (privk b))-  (uniq-orig n)-  (operation nonce-test (added-strand init 3) n (0 2)-    (enc n1 n (pubk a)))-  (traces-    ((recv (enc n1 a (pubk b))) (send (enc n1 n (pubk a)))-      (recv (enc n (pubk b))))-    ((send (enc n1 a (pubk b-0))) (recv (enc n1 n (pubk a)))-      (send (enc n (pubk b-0)))))-  (label 10)-  (parent 9)-  (unrealized)-  (shape)-  (satisfies yes (no (a a) (b b) (n n) (z0 (0 2))))-  (maps ((0) ((a a) (b b) (n n) (n1 n1))))-  (origs (n (0 1))))--(comment "Nothing left to do")--(defprotocol ns basic-  (defrole init-    (vars (a b name) (n1 n2 text))-    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))-      (send (enc n2 (pubk b)))))-  (defrole resp-    (vars (a b name) (n1 n2 text))-    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))-      (recv (enc n2 (pubk b)))))-  (comment "Needham-Schroeder"))--(defskeleton ns-  (vars (n1 n2 text) (a b name))-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))-  (non-orig (privk a) (privk b))-  (uniq-orig n1)-  (goals-    (forall ((a b name) (n1 text) (no nu node))-      (implies-        (and (p "init" 2 no) (p "init" "a" no a) (p "init" "b" no b)-          (p "init" "n1" no n1) (p "init" 0 nu) (str-prec nu no)-          (non (privk a)) (non (privk b)) (uniq-at n1 nu))-        (exists ((na nb node))-          (and (p "init" 2 na) (p "resp" 1 nb) (p "init" "b" na b)-            (p "resp" "b" nb b))))))-  (comment "Initiator point-of-view")-  (traces-    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))-      (send (enc n2 (pubk b)))))-  (label 11)-  (unrealized (0 1))-  (origs (n1 (0 0)))-  (comment "1 in cohort - 1 not yet seen"))--(defskeleton ns-  (vars (n1 n2 n2-0 text) (a b name))-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))-  (defstrand resp 2 (n1 n1) (n2 n2-0) (a a) (b b))-  (precedes ((0 0) (1 0)) ((1 1) (0 1)))-  (non-orig (privk a) (privk b))-  (uniq-orig n1)-  (operation nonce-test (added-strand resp 2) n1 (0 1)-    (enc n1 a (pubk b)))-  (traces-    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))-      (send (enc n2 (pubk b))))-    ((recv (enc n1 a (pubk b))) (send (enc n1 n2-0 (pubk a)))))-  (label 12)-  (parent 11)-  (unrealized (0 1))-  (comment "1 in cohort - 1 not yet seen"))--(defskeleton ns-  (vars (n1 n2 text) (a b name))-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))-  (defstrand resp 2 (n1 n1) (n2 n2) (a a) (b b))-  (precedes ((0 0) (1 0)) ((1 1) (0 1)))-  (non-orig (privk a) (privk b))-  (uniq-orig n1)-  (operation nonce-test (contracted (n2-0 n2)) n1 (0 1)-    (enc n1 n2 (pubk a)) (enc n1 a (pubk b)))-  (traces-    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))-      (send (enc n2 (pubk b))))-    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))))-  (label 13)-  (parent 12)-  (unrealized)-  (shape)-  (satisfies yes)-  (maps ((0) ((a a) (b b) (n1 n1) (n2 n2))))-  (origs (n1 (0 0))))--(comment "Nothing left to do")--(defprotocol ns basic-  (defrole init-    (vars (a b name) (n1 n2 text))-    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))-      (send (enc n2 (pubk b)))))-  (defrole resp-    (vars (a b name) (n1 n2 text))-    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))-      (recv (enc n2 (pubk b)))))-  (comment "Needham-Schroeder"))--(defskeleton ns-  (vars (n1 n2 text) (a b name))-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))-  (non-orig (privk a) (privk b))-  (uniq-orig n1)-  (goals-    (forall ((a b name) (n1 text) (no nu node))-      (implies-        (and (p "init" 2 no) (p "init" "a" no a) (p "init" "b" no b)-          (p "init" "n1" no n1) (p "init" 0 nu) (str-prec nu no)-          (non (privk a)) (non (privk b)) (uniq-at n1 nu))-        (exists ((na nb node))-          (and (p "init" 2 na) (p "resp" 1 nb) (p "init" "b" na b)-            (p "resp" "b" nb b))))))-  (comment "Initiator point-of-view")-  (traces-    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))-      (send (enc n2 (pubk b)))))-  (label 14)-  (unrealized (0 1))-  (origs (n1 (0 0)))-  (comment "1 in cohort - 1 not yet seen"))--(defskeleton ns-  (vars (n1 n2 n2-0 text) (a b name))-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))-  (defstrand resp 2 (n1 n1) (n2 n2-0) (a a) (b b))-  (precedes ((0 0) (1 0)) ((1 1) (0 1)))-  (non-orig (privk a) (privk b))-  (uniq-orig n1)-  (operation nonce-test (added-strand resp 2) n1 (0 1)-    (enc n1 a (pubk b)))-  (traces-    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))-      (send (enc n2 (pubk b))))-    ((recv (enc n1 a (pubk b))) (send (enc n1 n2-0 (pubk a)))))-  (label 15)-  (parent 14)-  (unrealized (0 1))-  (comment "1 in cohort - 1 not yet seen"))--(defskeleton ns-  (vars (n1 n2 text) (a b name))-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))-  (defstrand resp 2 (n1 n1) (n2 n2) (a a) (b b))-  (precedes ((0 0) (1 0)) ((1 1) (0 1)))-  (non-orig (privk a) (privk b))-  (uniq-orig n1)-  (operation nonce-test (contracted (n2-0 n2)) n1 (0 1)-    (enc n1 n2 (pubk a)) (enc n1 a (pubk b)))-  (traces-    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))-      (send (enc n2 (pubk b))))-    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))))-  (label 16)-  (parent 15)-  (unrealized)-  (shape)-  (satisfies yes)-  (maps ((0) ((a a) (b b) (n1 n1) (n2 n2))))-  (origs (n1 (0 0))))--(comment "Nothing left to do")--(defprotocol ns basic-  (defrole init-    (vars (a b name) (n1 n2 text))-    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))-      (send (enc n2 (pubk b)))))-  (defrole resp-    (vars (a b name) (n1 n2 text))-    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))-      (recv (enc n2 (pubk b)))))-  (comment "Needham-Schroeder"))--(defskeleton ns-  (vars (n2 n1 text) (a b name))-  (defstrand resp 3 (n1 n1) (n2 n2) (a a) (b b))-  (non-orig (privk a))-  (uniq-orig n2)-  (goals-    (forall ((n2 n1 text) (a b name) (z z-0 node))-      (implies-        (and (p "resp" 1 z) (p "resp" 2 z-0) (p "resp" "n2" z-0 n2)-          (p "resp" "n1" z-0 n1) (p "resp" "b" z-0 b)-          (p "resp" "a" z-0 a) (str-prec z z-0) (non (privk a))-          (uniq-at n2 z))-        (exists ((b-0 name) (z-1 z-2 node))-          (and (p "init" 1 z-1) (p "init" 2 z-2) (p "init" "n1" z-2 n1)-            (p "init" "n2" z-2 n2) (p "init" "a" z-2 a)-            (p "init" "b" z-2 b-0) (prec z z-1) (prec z-2 z-0)-            (str-prec z-1 z-2))))))-  (comment "Responder point-of-view")-  (traces-    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))-      (recv (enc n2 (pubk b)))))-  (label 17)-  (unrealized (0 2))-  (origs (n2 (0 1)))-  (comment "1 in cohort - 1 not yet seen"))--(defskeleton ns-  (vars (n2 n1 text) (a b b-0 name))-  (defstrand resp 3 (n1 n1) (n2 n2) (a a) (b b))-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b-0))-  (precedes ((0 1) (1 1)) ((1 2) (0 2)))-  (non-orig (privk a))-  (uniq-orig n2)-  (operation nonce-test (added-strand init 3) n2 (0 2)-    (enc n1 n2 (pubk a)))-  (traces-    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))-      (recv (enc n2 (pubk b))))-    ((send (enc n1 a (pubk b-0))) (recv (enc n1 n2 (pubk a)))-      (send (enc n2 (pubk b-0)))))-  (label 18)-  (parent 17)-  (unrealized)-  (shape)-  (satisfies yes)-  (maps ((0) ((a a) (n2 n2) (b b) (n1 n1))))-  (origs (n2 (0 1))))--(comment "Nothing left to do")--(defprotocol ns basic-  (defrole init-    (vars (a b name) (n1 n2 text))-    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))-      (send (enc n2 (pubk b)))))-  (defrole resp-    (vars (a b name) (n1 n2 text))-    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))-      (recv (enc n2 (pubk b)))))-  (comment "Needham-Schroeder"))--(defskeleton ns-  (vars (n2 n1 text) (a b name))-  (defstrand resp 3 (n1 n1) (n2 n2) (a a) (b b))-  (non-orig (privk a))-  (uniq-orig n2)-  (goals-    (forall ((n2 n1 text) (a b name) (z z-0 node))-      (implies-        (and (p "resp" 1 z) (p "resp" 2 z-0) (p "resp" "n2" z-0 n2)-          (p "resp" "n1" z-0 n1) (p "resp" "b" z-0 b)-          (p "resp" "a" z-0 a) (str-prec z z-0) (non (privk a))-          (uniq-at n2 z))-        (exists ((b-0 name) (z-1 z-2 node))-          (and (p "init" 1 z-1) (p "init" 2 z-2) (p "init" "n1" z-2 n1)-            (p "init" "n2" z-2 n2) (p "init" "a" z-2 a)-            (p "init" "b" z-2 b-0) (prec z z-1) (prec z-2 z-0)-            (str-prec z-1 z-2))))))-  (comment "Responder point-of-view")-  (traces-    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))-      (recv (enc n2 (pubk b)))))-  (label 19)-  (unrealized (0 2))-  (origs (n2 (0 1)))-  (comment "1 in cohort - 1 not yet seen"))--(defskeleton ns-  (vars (n2 n1 text) (a b b-0 name))-  (defstrand resp 3 (n1 n1) (n2 n2) (a a) (b b))-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b-0))-  (precedes ((0 1) (1 1)) ((1 2) (0 2)))-  (non-orig (privk a))-  (uniq-orig n2)-  (operation nonce-test (added-strand init 3) n2 (0 2)-    (enc n1 n2 (pubk a)))-  (traces-    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))-      (recv (enc n2 (pubk b))))-    ((send (enc n1 a (pubk b-0))) (recv (enc n1 n2 (pubk a)))-      (send (enc n2 (pubk b-0)))))-  (label 20)-  (parent 19)-  (unrealized)-  (shape)-  (satisfies yes)-  (maps ((0) ((a a) (n2 n2) (b b) (n1 n1))))-  (origs (n2 (0 1))))--(comment "Nothing left to do")--(defprotocol ns basic-  (defrole init-    (vars (a b name) (n1 n2 text))-    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))-      (send (enc n2 (pubk b)))))-  (defrole resp-    (vars (a b name) (n1 n2 text))-    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))-      (recv (enc n2 (pubk b)))))-  (comment "Needham-Schroeder"))--(defskeleton ns-  (vars (n1 n1-0 n2 n2-0 text) (a b name))-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))-  (defstrand init 3 (n1 n1-0) (n2 n2-0) (a a) (b b))-  (non-orig (privk a) (privk b))-  (uniq-orig n1 n1-0)-  (goals-    (forall ((n1 n1-0 n2 n2-0 text) (a b name) (z z-0 z-1 z-2 node))-      (implies-        (and (p "init" 0 z) (p "init" 2 z-0) (p "init" 0 z-1)-          (p "init" 2 z-2) (p "init" "n1" z-0 n1) (p "init" "n2" z-0 n2)-          (p "init" "a" z-0 a) (p "init" "b" z-0 b)-          (p "init" "n1" z-2 n1-0) (p "init" "n2" z-2 n2-0)-          (p "init" "a" z-2 a) (p "init" "b" z-2 b) (str-prec z z-0)-          (str-prec z-1 z-2) (non (privk a)) (non (privk b))-          (uniq-at n1 z) (uniq-at n1-0 z-1)) (= z-1 z))))-  (comment "Double initiator point-of-view")-  (traces-    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))-      (send (enc n2 (pubk b))))-    ((send (enc n1-0 a (pubk b))) (recv (enc n1-0 n2-0 (pubk a)))-      (send (enc n2-0 (pubk b)))))-  (label 21)-  (unrealized (0 1) (1 1))-  (origs (n1 (0 0)) (n1-0 (1 0)))-  (comment "1 in cohort - 1 not yet seen"))--(defskeleton ns-  (vars (n1 n2 text) (a b name))-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))-  (non-orig (privk a) (privk b))-  (uniq-orig n1)-  (operation collapsed 1 0)-  (traces-    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))-      (send (enc n2 (pubk b)))))-  (label 22)-  (parent 21)-  (unrealized (0 1))-  (comment "1 in cohort - 1 not yet seen"))--(defskeleton ns-  (vars (n1 n1-0 n2 n2-0 n2-1 text) (a b name))-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))-  (defstrand init 3 (n1 n1-0) (n2 n2-0) (a a) (b b))-  (defstrand resp 2 (n1 n1-0) (n2 n2-1) (a a) (b b))-  (precedes ((1 0) (2 0)) ((2 1) (1 1)))-  (non-orig (privk a) (privk b))-  (uniq-orig n1 n1-0)-  (operation nonce-test (added-strand resp 2) n1-0 (1 1)-    (enc n1-0 a (pubk b)))-  (traces-    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))-      (send (enc n2 (pubk b))))-    ((send (enc n1-0 a (pubk b))) (recv (enc n1-0 n2-0 (pubk a)))-      (send (enc n2-0 (pubk b))))-    ((recv (enc n1-0 a (pubk b))) (send (enc n1-0 n2-1 (pubk a)))))-  (label 23)-  (parent 21)-  (unrealized (0 1) (1 1))-  (comment "1 in cohort - 1 not yet seen"))--(defskeleton ns-  (vars (n1 n2 n2-0 text) (a b name))-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))-  (defstrand resp 2 (n1 n1) (n2 n2-0) (a a) (b b))-  (precedes ((0 0) (1 0)) ((1 1) (0 1)))-  (non-orig (privk a) (privk b))-  (uniq-orig n1)-  (operation nonce-test (added-strand resp 2) n1 (0 1)-    (enc n1 a (pubk b)))-  (traces-    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))-      (send (enc n2 (pubk b))))-    ((recv (enc n1 a (pubk b))) (send (enc n1 n2-0 (pubk a)))))-  (label 24)-  (parent 22)-  (unrealized (0 1))-  (origs (n1 (0 0)))-  (comment "1 in cohort - 1 not yet seen"))--(defskeleton ns-  (vars (n1 n1-0 n2 n2-0 text) (a b name))-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))-  (defstrand init 3 (n1 n1-0) (n2 n2-0) (a a) (b b))-  (defstrand resp 2 (n1 n1-0) (n2 n2-0) (a a) (b b))-  (precedes ((1 0) (2 0)) ((2 1) (1 1)))-  (non-orig (privk a) (privk b))-  (uniq-orig n1 n1-0)-  (operation nonce-test (contracted (n2-1 n2-0)) n1-0 (1 1)-    (enc n1-0 n2-0 (pubk a)) (enc n1-0 a (pubk b)))-  (traces-    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))-      (send (enc n2 (pubk b))))-    ((send (enc n1-0 a (pubk b))) (recv (enc n1-0 n2-0 (pubk a)))-      (send (enc n2-0 (pubk b))))-    ((recv (enc n1-0 a (pubk b))) (send (enc n1-0 n2-0 (pubk a)))))-  (label 25)-  (parent 23)-  (unrealized (0 1))-  (comment "1 in cohort - 1 not yet seen"))--(defskeleton ns-  (vars (n1 n2 text) (a b name))-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))-  (defstrand resp 2 (n1 n1) (n2 n2) (a a) (b b))-  (precedes ((0 0) (1 0)) ((1 1) (0 1)))-  (non-orig (privk a) (privk b))-  (uniq-orig n1)-  (operation nonce-test (contracted (n2-0 n2)) n1 (0 1)-    (enc n1 n2 (pubk a)) (enc n1 a (pubk b)))-  (traces-    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))-      (send (enc n2 (pubk b))))-    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))))-  (label 26)-  (parent 24)-  (unrealized)-  (shape)-  (satisfies yes)-  (maps ((0 0) ((a a) (b b) (n1 n1) (n1-0 n1) (n2 n2) (n2-0 n2))))-  (origs (n1 (0 0))))--(defskeleton ns-  (vars (n1 n1-0 n2 n2-0 n2-1 text) (a b name))-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))-  (defstrand init 3 (n1 n1-0) (n2 n2-0) (a a) (b b))-  (defstrand resp 2 (n1 n1-0) (n2 n2-0) (a a) (b b))-  (defstrand resp 2 (n1 n1) (n2 n2-1) (a a) (b b))-  (precedes ((0 0) (3 0)) ((1 0) (2 0)) ((2 1) (1 1)) ((3 1) (0 1)))-  (non-orig (privk a) (privk b))-  (uniq-orig n1 n1-0)-  (operation nonce-test (added-strand resp 2) n1 (0 1)-    (enc n1 a (pubk b)))-  (traces-    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))-      (send (enc n2 (pubk b))))-    ((send (enc n1-0 a (pubk b))) (recv (enc n1-0 n2-0 (pubk a)))-      (send (enc n2-0 (pubk b))))-    ((recv (enc n1-0 a (pubk b))) (send (enc n1-0 n2-0 (pubk a))))-    ((recv (enc n1 a (pubk b))) (send (enc n1 n2-1 (pubk a)))))-  (label 27)-  (parent 25)-  (unrealized (0 1))-  (comment "1 in cohort - 1 not yet seen"))--(defskeleton ns-  (vars (n1 n1-0 n2 n2-0 text) (a b name))-  (defstrand init 3 (n1 n1) (n2 n2-0) (a a) (b b))-  (defstrand init 3 (n1 n1-0) (n2 n2) (a a) (b b))-  (defstrand resp 2 (n1 n1-0) (n2 n2) (a a) (b b))-  (defstrand resp 2 (n1 n1) (n2 n2-0) (a a) (b b))-  (precedes ((0 0) (3 0)) ((1 0) (2 0)) ((2 1) (1 1)) ((3 1) (0 1)))-  (non-orig (privk a) (privk b))-  (uniq-orig n1 n1-0)-  (operation nonce-test (contracted (n2-1 n2-0)) n1 (0 1)-    (enc n1 n2-0 (pubk a)) (enc n1 a (pubk b)))-  (traces-    ((send (enc n1 a (pubk b))) (recv (enc n1 n2-0 (pubk a)))-      (send (enc n2-0 (pubk b))))-    ((send (enc n1-0 a (pubk b))) (recv (enc n1-0 n2 (pubk a)))-      (send (enc n2 (pubk b))))-    ((recv (enc n1-0 a (pubk b))) (send (enc n1-0 n2 (pubk a))))-    ((recv (enc n1 a (pubk b))) (send (enc n1 n2-0 (pubk a)))))-  (label 28)-  (parent 27)-  (unrealized)-  (shape)-  (satisfies-    (no (n1-0 n1) (n1 n1-0) (n2-0 n2-0) (n2 n2) (a a) (b b) (z-2 (0 0))-      (z-1 (0 2)) (z-0 (1 0)) (z (1 2))))-  (maps ((0 1) ((a a) (b b) (n1 n1) (n1-0 n1-0) (n2 n2-0) (n2-0 n2))))-  (origs (n1 (0 0)) (n1-0 (1 0))))--(comment "Nothing left to do")--(defprotocol ns-role-origs basic-  (defrole init-    (vars (a b name) (n1 n2 text))-    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))-      (send (enc n2 (pubk b))))-    (non-orig (privk b))-    (uniq-orig n1))-  (defrole resp-    (vars (b a name) (n2 n1 text))-    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))-      (recv (enc n2 (pubk b))))-    (non-orig (privk a))-    (uniq-orig n2))-  (comment-    "Needham-Schroeder with role assumptions that are too strong"))--(defskeleton ns-role-origs-  (vars (n1 n2 text) (a b name))-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))-  (non-orig (privk b))-  (uniq-orig n1)-  (traces-    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))-      (send (enc n2 (pubk b)))))-  (label 29)-  (unrealized (0 1))-  (origs (n1 (0 0)))-  (comment "1 in cohort - 1 not yet seen"))--(defskeleton ns-role-origs-  (vars (n1 n2 n2-0 text) (a b name))-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))-  (defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a))-  (precedes ((0 0) (1 0)) ((1 1) (0 1)))-  (non-orig (privk a) (privk b))-  (uniq-orig n1 n2-0)-  (operation nonce-test (added-strand resp 2) n1 (0 1)-    (enc n1 a (pubk b)))-  (traces-    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))-      (send (enc n2 (pubk b))))-    ((recv (enc n1 a (pubk b))) (send (enc n1 n2-0 (pubk a)))))-  (label 30)-  (parent 29)-  (unrealized (0 1))-  (comment "1 in cohort - 1 not yet seen"))--(defskeleton ns-role-origs-  (vars (n1 n2 text) (a b name))-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))-  (defstrand resp 2 (n2 n2) (n1 n1) (b b) (a a))-  (precedes ((0 0) (1 0)) ((1 1) (0 1)))-  (non-orig (privk a) (privk b))-  (uniq-orig n1 n2)-  (operation nonce-test (contracted (n2-0 n2)) n1 (0 1)-    (enc n1 n2 (pubk a)) (enc n1 a (pubk b)))-  (traces-    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))-      (send (enc n2 (pubk b))))-    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))))-  (label 31)-  (parent 30)-  (unrealized)-  (shape)-  (maps ((0) ((a a) (b b) (n1 n1) (n2 n2))))-  (origs (n2 (1 1)) (n1 (0 0))))--(comment "Nothing left to do")--(defprotocol ns-role-origs basic-  (defrole init-    (vars (a b name) (n1 n2 text))-    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))-      (send (enc n2 (pubk b))))-    (non-orig (privk b))-    (uniq-orig n1))-  (defrole resp-    (vars (b a name) (n2 n1 text))-    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))-      (recv (enc n2 (pubk b))))-    (non-orig (privk a))-    (uniq-orig n2))-  (comment-    "Needham-Schroeder with role assumptions that are too strong"))--(defskeleton ns-role-origs-  (vars (n2 n1 text) (b a name))-  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))-  (non-orig (privk a))-  (uniq-orig n2)-  (traces-    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))-      (recv (enc n2 (pubk b)))))-  (label 32)-  (unrealized (0 2))-  (origs (n2 (0 1)))-  (comment "1 in cohort - 1 not yet seen"))--(defskeleton ns-role-origs-  (vars (n2 n1 text) (b a b-0 name))-  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b-0))-  (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2)))-  (non-orig (privk a) (privk b-0))-  (uniq-orig n2 n1)-  (operation nonce-test (added-strand init 3) n2 (0 2)-    (enc n1 n2 (pubk a)))-  (traces-    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))-      (recv (enc n2 (pubk b))))-    ((send (enc n1 a (pubk b-0))) (recv (enc n1 n2 (pubk a)))-      (send (enc n2 (pubk b-0)))))-  (label 33)-  (parent 32)-  (unrealized (0 0) (0 2))-  (comment "2 in cohort - 2 not yet seen"))--(defskeleton ns-role-origs-  (vars (n2 n1 text) (a b name))-  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))-  (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2)))-  (non-orig (privk a) (privk b))-  (uniq-orig n2 n1)-  (operation nonce-test (contracted (b-0 b)) n1 (0 0)-    (enc n1 a (pubk b)))-  (traces-    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))-      (recv (enc n2 (pubk b))))-    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))-      (send (enc n2 (pubk b)))))-  (label 34)-  (parent 33)-  (unrealized)-  (shape)-  (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))-  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b-0))-  (defstrand resp 2 (n2 n2-0) (n1 n1) (b b-0) (a a))-  (precedes ((0 1) (1 1)) ((1 0) (2 0)) ((1 2) (0 2)) ((2 1) (0 0)))-  (non-orig (privk a) (privk b-0))-  (uniq-orig n2 n1 n2-0)-  (operation nonce-test (added-strand resp 2) n1 (0 0)-    (enc n1 a (pubk b-0)))-  (traces-    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))-      (recv (enc n2 (pubk b))))-    ((send (enc n1 a (pubk b-0))) (recv (enc n1 n2 (pubk a)))-      (send (enc n2 (pubk b-0))))-    ((recv (enc n1 a (pubk b-0))) (send (enc n1 n2-0 (pubk a)))))-  (label 35)-  (parent 33)-  (unrealized (0 0) (0 2))-  (comment "1 in cohort - 1 not yet seen"))--(defskeleton ns-role-origs-  (vars (n2 n1 n2-0 text) (a b name))-  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))-  (defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a))-  (precedes ((0 1) (1 1)) ((1 0) (2 0)) ((1 2) (0 2)) ((2 1) (0 0)))-  (non-orig (privk a) (privk b))-  (uniq-orig n2 n1 n2-0)-  (operation nonce-test (contracted (b-0 b)) n1 (0 0)-    (enc n1 n2-0 (pubk a)) (enc n1 a (pubk b)))-  (traces-    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))-      (recv (enc n2 (pubk b))))-    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))-      (send (enc n2 (pubk b))))-    ((recv (enc n1 a (pubk b))) (send (enc n1 n2-0 (pubk a)))))-  (label 36)-  (parent 35)-  (seen 34)-  (unrealized)-  (comment "1 in cohort - 0 not yet seen"))--(comment "Nothing left to do")--(defprotocol ns2 basic-  (defrole init-    (vars (a b name) (n1 n2 n3 text))-    (trace (send (enc n1 n3 a (pubk b))) (recv (enc n1 n2 (pubk a)))-      (send (enc n2 (pubk b)))))-  (defrole resp-    (vars (b a name) (n2 n1 text))-    (trace (recv (enc n1 n1 a (pubk b))) (send (enc n1 n2 (pubk a)))-      (recv (enc n2 (pubk b))))-    (note doubled nonce in the first message))-  (note that this protocol is derived from Needham-Schroeder))--(defskeleton ns2-  (vars (n1 n2 n3 text) (a b name))-  (defstrand init 3 (n1 n1) (n2 n2) (n3 n3) (a a) (b b))-  (non-orig (privk a) (privk b))-  (uniq-orig n1)-  (traces-    ((send (enc n1 n3 a (pubk b))) (recv (enc n1 n2 (pubk a)))-      (send (enc n2 (pubk b)))))-  (label 37)-  (unrealized (0 1))-  (origs (n1 (0 0)))-  (comment "1 in cohort - 1 not yet seen"))--(defskeleton ns2-  (vars (n2 n3 n2-0 text) (a b name))-  (defstrand init 3 (n1 n3) (n2 n2) (n3 n3) (a a) (b b))-  (defstrand resp 2 (n2 n2-0) (n1 n3) (b b) (a a))-  (precedes ((0 0) (1 0)) ((1 1) (0 1)))-  (non-orig (privk a) (privk b))-  (uniq-orig n3)-  (operation nonce-test (added-strand resp 2) n3 (0 1)-    (enc n3 n3 a (pubk b)))-  (traces-    ((send (enc n3 n3 a (pubk b))) (recv (enc n3 n2 (pubk a)))-      (send (enc n2 (pubk b))))-    ((recv (enc n3 n3 a (pubk b))) (send (enc n3 n2-0 (pubk a)))))-  (label 38)-  (parent 37)-  (unrealized (0 1))-  (comment "1 in cohort - 1 not yet seen"))--(defskeleton ns2-  (vars (n3 n2 text) (a b name))-  (defstrand init 3 (n1 n3) (n2 n2) (n3 n3) (a a) (b b))-  (defstrand resp 2 (n2 n2) (n1 n3) (b b) (a a))-  (precedes ((0 0) (1 0)) ((1 1) (0 1)))-  (non-orig (privk a) (privk b))-  (uniq-orig n3)-  (operation nonce-test (contracted (n2-0 n2)) n3 (0 1)-    (enc n3 n2 (pubk a)) (enc n3 n3 a (pubk b)))-  (traces-    ((send (enc n3 n3 a (pubk b))) (recv (enc n3 n2 (pubk a)))-      (send (enc n2 (pubk b))))-    ((recv (enc n3 n3 a (pubk b))) (send (enc n3 n2 (pubk a)))))-  (label 39)-  (parent 38)-  (unrealized)-  (shape)-  (maps ((0) ((a a) (b b) (n1 n3) (n2 n2) (n3 n3))))-  (origs (n3 (0 0))))--(comment "Nothing left to do")--(defprotocol ns basic-  (defrole init-    (vars (a b name) (n1 n2 text))-    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))-      (send (enc n2 (pubk b)))))-  (defrole resp-    (vars (a b name) (n1 n2 text))-    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))-      (recv (enc n2 (pubk b)))))-  (comment "Needham-Schroeder"))--(defskeleton ns-  (vars (n1 n2 text) (a b name))-  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))-  (defstrand resp 2 (n1 n1) (n2 n2) (a a) (b b))-  (precedes ((0 0) (1 0)) ((1 1) (0 1)))-  (non-orig (privk a) (privk b))-  (uniq-orig n1)-  (traces-    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))-      (send (enc n2 (pubk b))))-    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))))-  (label 40)-  (unrealized)-  (shape)-  (maps ((0 1) ((n1 n1) (n2 n2) (a a) (b b))))-  (origs (n1 (0 0))))--(comment "Nothing left to do")--(defprotocol nsl-typeless basic-  (defrole init-    (vars (a b name) (n1 text) (n2 mesg))-    (trace (send (enc a n1 (pubk b))) (recv (enc n1 n2 b (pubk a)))-      (send (enc n2 (pubk b)))))-  (defrole resp-    (vars (b a name) (n2 text) (n1 mesg))-    (trace (recv (enc a n1 (pubk b))) (send (enc n1 n2 b (pubk a)))-      (recv (enc n2 (pubk b)))))-  (comment "Needham-Schroeder-Lowe with untyped nonces"))--(defskeleton nsl-typeless-  (vars (n1 mesg) (n2 text) (a b name))-  (defstrand resp 2 (n1 n1) (n2 n2) (b b) (a a))-  (deflistener n2)-  (non-orig (privk a) (privk b))-  (uniq-orig n2)-  (comment "Shows typeflaw in typeless NSL")-  (traces ((recv (enc a n1 (pubk b))) (send (enc n1 n2 b (pubk a))))-    ((recv n2) (send n2)))-  (label 41)-  (unrealized (1 0))-  (preskeleton)-  (comment "Not a skeleton"))--(defskeleton nsl-typeless-  (vars (n1 mesg) (n2 text) (a b name))-  (defstrand resp 2 (n1 n1) (n2 n2) (b b) (a a))-  (deflistener n2)-  (precedes ((0 1) (1 0)))-  (non-orig (privk a) (privk b))-  (uniq-orig n2)-  (traces ((recv (enc a n1 (pubk b))) (send (enc n1 n2 b (pubk a))))-    ((recv n2) (send n2)))-  (label 42)-  (parent 41)-  (unrealized (1 0))-  (origs (n2 (0 1)))-  (comment "2 in cohort - 2 not yet seen"))--(defskeleton nsl-typeless-  (vars (n2 n1 text) (a b name))-  (defstrand resp 2 (n1 n1) (n2 n2) (b b) (a a))-  (deflistener n2)-  (defstrand init 3 (n2 n2) (n1 n1) (a a) (b b))-  (precedes ((0 1) (2 1)) ((2 2) (1 0)))-  (non-orig (privk a) (privk b))-  (uniq-orig n2)-  (operation nonce-test (added-strand init 3) n2 (1 0)-    (enc n1 n2 b (pubk a)))-  (traces ((recv (enc a n1 (pubk b))) (send (enc n1 n2 b (pubk a))))-    ((recv n2) (send n2))-    ((send (enc a n1 (pubk b))) (recv (enc n1 n2 b (pubk a)))-      (send (enc n2 (pubk b)))))-  (label 43)-  (parent 42)-  (unrealized (1 0))-  (comment "empty cohort"))--(defskeleton nsl-typeless-  (vars (n2 n2-0 text) (a b a-0 name))-  (defstrand resp 2 (n1 a-0) (n2 n2) (b b) (a a))-  (deflistener n2)-  (defstrand resp 2 (n1 (cat n2 b)) (n2 n2-0) (b a) (a a-0))-  (precedes ((0 1) (2 0)) ((2 1) (1 0)))-  (non-orig (privk a) (privk b))-  (uniq-orig n2)-  (operation nonce-test (added-strand resp 2) n2 (1 0)-    (enc a-0 n2 b (pubk a)))-  (traces ((recv (enc a a-0 (pubk b))) (send (enc a-0 n2 b (pubk a))))-    ((recv n2) (send n2))-    ((recv (enc a-0 n2 b (pubk a)))-      (send (enc (cat n2 b) n2-0 a (pubk a-0)))))-  (label 44)-  (parent 42)-  (unrealized)-  (shape)-  (maps ((0 1) ((a a) (b b) (n2 n2) (n1 a-0))))-  (origs (n2 (0 1))))+(comment "CPSA 2.5.1")+(comment "All input read from goals.scm")++(defprotocol ns basic+  (defrole init+    (vars (a b name) (n1 n2 text))+    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b)))))+  (defrole resp+    (vars (b a name) (n2 n1 text))+    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))+      (recv (enc n2 (pubk b)))))+  (comment "Needham-Schroeder with no role origination assumptions"))++(defskeleton ns+  (vars (n1 n2 text) (b a name))+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))+  (non-orig (privk b))+  (uniq-orig n1)+  (goals+    (forall ((b name) (n1 text) (z0 node))+      (implies+        (and (p "init" 2 z0) (p "init" "n1" z0 n1) (p "init" "b" z0 b)+          (non (privk b)) (uniq n1))+        (exists ((z1 node))+          (and (p "resp" 1 z1) (p "resp" "b" z1 b))))))+  (comment "Initiator point of view"+    "Authentication goal: agreement on name b")+  (traces+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b)))))+  (label 0)+  (unrealized (0 1))+  (origs (n1 (0 0)))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton ns+  (vars (n1 n2 n2-0 text) (b a name))+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))+  (defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a))+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (privk b))+  (uniq-orig n1)+  (operation nonce-test (added-strand resp 2) n1 (0 1)+    (enc n1 a (pubk b)))+  (traces+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b))))+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2-0 (pubk a)))))+  (label 1)+  (parent 0)+  (unrealized)+  (shape)+  (satisfies yes)+  (maps ((0) ((b b) (n1 n1) (a a) (n2 n2))))+  (origs (n1 (0 0))))++(comment "Nothing left to do")++(defprotocol ns basic+  (defrole init+    (vars (a b name) (n1 n2 text))+    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b)))))+  (defrole resp+    (vars (b a name) (n2 n1 text))+    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))+      (recv (enc n2 (pubk b)))))+  (comment "Needham-Schroeder with no role origination assumptions"))++(defskeleton ns+  (vars (n1 n2 text) (b a name))+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))+  (non-orig (privk b))+  (uniq-orig n1)+  (goals+    (forall ((b name) (n1 text) (z0 node))+      (implies+        (and (p "init" 2 z0) (p "init" "n1" z0 n1) (p "init" "b" z0 b)+          (non (privk b)) (uniq n1))+        (exists ((z1 node))+          (and (p "resp" 1 z1) (p "resp" "b" z1 b) (prec z1 z0))))))+  (comment "Prec example")+  (traces+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b)))))+  (label 2)+  (unrealized (0 1))+  (origs (n1 (0 0)))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton ns+  (vars (n1 n2 n2-0 text) (b a name))+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))+  (defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a))+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (privk b))+  (uniq-orig n1)+  (operation nonce-test (added-strand resp 2) n1 (0 1)+    (enc n1 a (pubk b)))+  (traces+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b))))+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2-0 (pubk a)))))+  (label 3)+  (parent 2)+  (unrealized)+  (shape)+  (satisfies yes)+  (maps ((0) ((b b) (n1 n1) (a a) (n2 n2))))+  (origs (n1 (0 0))))++(comment "Nothing left to do")++(defprotocol ns basic+  (defrole init+    (vars (a b name) (n1 n2 text))+    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b)))))+  (defrole resp+    (vars (b a name) (n2 n1 text))+    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))+      (recv (enc n2 (pubk b)))))+  (comment "Needham-Schroeder with no role origination assumptions"))++(defskeleton ns+  (vars (n2 n1 text) (a b name))+  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))+  (non-orig (privk a))+  (uniq-orig n2)+  (goals+    (forall ((a b name) (n2 text) (z0 node))+      (implies+        (and (p "resp" 2 z0) (p "resp" "n2" z0 n2) (p "resp" "a" z0 a)+          (p "resp" "b" z0 b) (non (privk a)) (uniq n2))+        (exists ((z1 node))+          (and (p "init" 1 z1) (p "init" "b" z1 b))))))+  (comment "Responder point of view"+    "Failed authentication goal: agreement on name b")+  (traces+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))+      (recv (enc n2 (pubk b)))))+  (label 4)+  (unrealized (0 2))+  (origs (n2 (0 1)))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton ns+  (vars (n2 n1 text) (a b b-0 name))+  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b-0))+  (precedes ((0 1) (1 1)) ((1 2) (0 2)))+  (non-orig (privk a))+  (uniq-orig n2)+  (operation nonce-test (added-strand init 3) n2 (0 2)+    (enc n1 n2 (pubk a)))+  (traces+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))+      (recv (enc n2 (pubk b))))+    ((send (enc n1 a (pubk b-0))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b-0)))))+  (label 5)+  (parent 4)+  (unrealized)+  (shape)+  (satisfies (no (a a) (b b) (n2 n2) (z0 (0 2))))+  (maps ((0) ((a a) (b b) (n2 n2) (n1 n1))))+  (origs (n2 (0 1))))++(comment "Nothing left to do")++(defprotocol nsl basic+  (defrole init+    (vars (a b name) (n1 n2 text))+    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 b (pubk a)))+      (send (enc n2 (pubk b)))))+  (defrole resp+    (vars (b a name) (n2 n1 text))+    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 b (pubk a)))+      (recv (enc n2 (pubk b)))))+  (comment+    "Needham-Schroeder-Lowe with no role origination assumptions"))++(defskeleton nsl+  (vars (n2 n1 text) (a b name))+  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))+  (non-orig (privk a))+  (uniq-orig n2)+  (goals+    (forall ((a b name) (n2 text) (z0 node))+      (implies+        (and (p "resp" 2 z0) (p "resp" "n2" z0 n2) (p "resp" "a" z0 a)+          (p "resp" "b" z0 b) (non (privk a)) (uniq n2))+        (exists ((z1 node))+          (and (p "init" 1 z1) (p "init" "b" z1 b))))))+  (comment "Responder point of view"+    "Authentication goal: agreement on name b")+  (traces+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 b (pubk a)))+      (recv (enc n2 (pubk b)))))+  (label 6)+  (unrealized (0 2))+  (origs (n2 (0 1)))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton nsl+  (vars (n2 n1 text) (a b name))+  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))+  (precedes ((0 1) (1 1)) ((1 2) (0 2)))+  (non-orig (privk a))+  (uniq-orig n2)+  (operation nonce-test (added-strand init 3) n2 (0 2)+    (enc n1 n2 b (pubk a)))+  (traces+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 b (pubk a)))+      (recv (enc n2 (pubk b))))+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 b (pubk a)))+      (send (enc n2 (pubk b)))))+  (label 7)+  (parent 6)+  (unrealized)+  (shape)+  (satisfies yes)+  (maps ((0) ((a a) (b b) (n2 n2) (n1 n1))))+  (origs (n2 (0 1))))++(comment "Nothing left to do")++(defprotocol ns basic+  (defrole init+    (vars (a b name) (n1 n2 text))+    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b)))))+  (defrole resp+    (vars (b a name) (n2 n1 text))+    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))+      (recv (enc n2 (pubk b)))))+  (comment "Needham-Schroeder with no role origination assumptions"))++(defskeleton ns+  (vars (n1 n2 text) (a b name))+  (deflistener n1)+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))+  (non-orig (privk a) (privk b))+  (uniq-orig n1)+  (goals+    (forall ((a b name) (n1 text) (z0 z1 node))+      (implies+        (and (p "init" 2 z0) (p "init" "n1" z0 n1) (p "init" "a" z0 a)+          (p "init" "b" z0 b) (p "" 0 z1) (p "" "x" z1 n1)+          (non (privk a)) (non (privk b)) (uniq n1)) (false))))+  (comment "Initiator point of view"+    "Secrecy goal: nonce n1 not revealed")+  (traces ((recv n1))+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b)))))+  (label 8)+  (unrealized (0 0) (1 1))+  (preskeleton)+  (comment "Not a skeleton"))++(defskeleton ns+  (vars (n1 n2 text) (a b name))+  (deflistener n1)+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))+  (precedes ((1 0) (0 0)))+  (non-orig (privk a) (privk b))+  (uniq-orig n1)+  (traces ((recv n1))+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b)))))+  (label 9)+  (parent 8)+  (unrealized (0 0) (1 1))+  (origs (n1 (1 0)))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton ns+  (vars (n1 n2 n2-0 text) (a b name))+  (deflistener n1)+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))+  (defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a))+  (precedes ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (1 1)))+  (non-orig (privk a) (privk b))+  (uniq-orig n1)+  (operation nonce-test (added-strand resp 2) n1 (1 1)+    (enc n1 a (pubk b)))+  (traces ((recv n1))+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b))))+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2-0 (pubk a)))))+  (label 10)+  (parent 9)+  (unrealized (0 0) (1 1))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton ns+  (vars (n1 n2 text) (a b name))+  (deflistener n1)+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))+  (defstrand resp 2 (n2 n2) (n1 n1) (b b) (a a))+  (precedes ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (1 1)))+  (non-orig (privk a) (privk b))+  (uniq-orig n1)+  (operation nonce-test (contracted (n2-0 n2)) n1 (1 1)+    (enc n1 n2 (pubk a)) (enc n1 a (pubk b)))+  (traces ((recv n1))+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b))))+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))))+  (label 11)+  (parent 10)+  (unrealized (0 0))+  (comment "2 in cohort - 2 not yet seen"))++(defskeleton ns+  (vars (n1 n2 text) (a b name))+  (deflistener n1)+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))+  (defstrand resp 2 (n2 n2) (n1 n1) (b b) (a a))+  (precedes ((1 0) (2 0)) ((2 1) (0 0)) ((2 1) (1 1)))+  (non-orig (privk a) (privk b))+  (uniq-orig n1)+  (operation nonce-test (displaced 3 2 resp 2) n1 (0 0)+    (enc n1 a (pubk b)))+  (traces ((recv n1))+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b))))+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))))+  (label 12)+  (parent 11)+  (unrealized (0 0))+  (comment "2 in cohort - 2 not yet seen"))++(defskeleton ns+  (vars (n1 n2 n2-0 text) (a b name))+  (deflistener n1)+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))+  (defstrand resp 2 (n2 n2) (n1 n1) (b b) (a a))+  (defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a))+  (precedes ((1 0) (2 0)) ((1 0) (3 0)) ((2 1) (1 1)) ((3 1) (0 0)))+  (non-orig (privk a) (privk b))+  (uniq-orig n1)+  (operation nonce-test (added-strand resp 2) n1 (0 0)+    (enc n1 a (pubk b)))+  (traces ((recv n1))+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b))))+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a))))+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2-0 (pubk a)))))+  (label 13)+  (parent 11)+  (seen 15)+  (unrealized (0 0))+  (comment "1 in cohort - 0 not yet seen"))++(defskeleton ns+  (vars (n2 text) (a b name))+  (deflistener n2)+  (defstrand init 3 (n1 n2) (n2 n2) (a a) (b b))+  (defstrand resp 2 (n2 n2) (n1 n2) (b b) (a a))+  (precedes ((1 0) (2 0)) ((1 2) (0 0)) ((2 1) (1 1)))+  (non-orig (privk a) (privk b))+  (uniq-orig n2)+  (operation nonce-test (displaced 3 1 init 3) n2 (0 0)+    (enc n2 n2 (pubk a)) (enc n2 a (pubk b)))+  (traces ((recv n2))+    ((send (enc n2 a (pubk b))) (recv (enc n2 n2 (pubk a)))+      (send (enc n2 (pubk b))))+    ((recv (enc n2 a (pubk b))) (send (enc n2 n2 (pubk a)))))+  (label 14)+  (parent 12)+  (unrealized (0 0))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton ns+  (vars (n1 n2 n2-0 text) (a b name))+  (deflistener n1)+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))+  (defstrand resp 2 (n2 n2) (n1 n1) (b b) (a a))+  (defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a))+  (precedes ((1 0) (2 0)) ((1 0) (3 0)) ((2 1) (0 0)) ((2 1) (1 1))+    ((3 1) (0 0)))+  (non-orig (privk a) (privk b))+  (uniq-orig n1)+  (operation nonce-test (added-strand resp 2) n1 (0 0)+    (enc n1 n2 (pubk a)) (enc n1 a (pubk b)))+  (traces ((recv n1))+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b))))+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a))))+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2-0 (pubk a)))))+  (label 15)+  (parent 12)+  (seen 16)+  (unrealized (0 0))+  (comment "1 in cohort - 0 not yet seen"))++(defskeleton ns+  (vars (n2 n2-0 text) (a b name))+  (deflistener n2)+  (defstrand init 3 (n1 n2) (n2 n2) (a a) (b b))+  (defstrand resp 2 (n2 n2) (n1 n2) (b b) (a a))+  (defstrand resp 2 (n2 n2-0) (n1 n2) (b b) (a a))+  (precedes ((1 0) (2 0)) ((1 0) (3 0)) ((1 2) (0 0)) ((2 1) (1 1))+    ((3 1) (0 0)))+  (non-orig (privk a) (privk b))+  (uniq-orig n2)+  (operation nonce-test (added-strand resp 2) n2 (0 0) (enc n2 (pubk b))+    (enc n2 n2 (pubk a)) (enc n2 a (pubk b)))+  (traces ((recv n2))+    ((send (enc n2 a (pubk b))) (recv (enc n2 n2 (pubk a)))+      (send (enc n2 (pubk b))))+    ((recv (enc n2 a (pubk b))) (send (enc n2 n2 (pubk a))))+    ((recv (enc n2 a (pubk b))) (send (enc n2 n2-0 (pubk a)))))+  (label 16)+  (parent 14)+  (unrealized (0 0))+  (comment "empty cohort"))++(comment "Nothing left to do")++(defprotocol unilateral basic+  (defrole init+    (vars (a name) (n text))+    (trace (send (enc n (pubk a))) (recv n)))+  (defrole resp+    (vars (a name) (n text))+    (trace (recv (enc n (pubk a))) (send n)))+  (comment "Unilateral authentication"))++(defskeleton unilateral+  (vars (n text) (a name))+  (defstrand init 2 (n n) (a a))+  (non-orig (privk a))+  (uniq-orig n)+  (goals+    (forall ((a name) (n text) (z0 node))+      (implies+        (and (p "init" 1 z0) (p "init" "n" z0 n) (p "init" "a" z0 a)+          (non (privk a)) (uniq n))+        (exists ((z1 node))+          (and (p "resp" 1 z1) (p "resp" "a" z1 a))))))+  (comment "Unilateral authentication goal")+  (traces ((send (enc n (pubk a))) (recv n)))+  (label 17)+  (unrealized (0 1))+  (origs (n (0 0)))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton unilateral+  (vars (n text) (a name))+  (defstrand init 2 (n n) (a a))+  (defstrand resp 2 (n n) (a a))+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (privk a))+  (uniq-orig n)+  (operation nonce-test (added-strand resp 2) n (0 1) (enc n (pubk a)))+  (traces ((send (enc n (pubk a))) (recv n))+    ((recv (enc n (pubk a))) (send n)))+  (label 18)+  (parent 17)+  (unrealized)+  (shape)+  (satisfies yes)+  (maps ((0) ((a a) (n n))))+  (origs (n (0 0))))++(comment "Nothing left to do")++(defprotocol ns basic+  (defrole init+    (vars (a b name) (n1 n2 text))+    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b)))))+  (defrole resp+    (vars (b a name) (n2 n1 text))+    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))+      (recv (enc n2 (pubk b)))))+  (comment "Needham-Schroeder with no role origination assumptions"))++(defskeleton ns+  (vars (n n2 text) (a a-0 name))+  (defstrand init 2 (n1 n) (n2 n2) (a a-0) (b a))+  (non-orig (privk a))+  (uniq-orig n)+  (goals+    (forall ((a name) (n text) (z0 node))+      (implies+        (and (p "init" 1 z0) (p "init" "n1" z0 n) (p "init" "b" z0 a)+          (non (privk a)) (uniq n))+        (exists ((z1 node))+          (and (p "resp" 1 z1) (p "resp" "b" z1 a))))))+  (comment "Initiator authentication goal"+    "Same as unilateral goal under the predicate mapping:"+    (p "init" "n") "->" (p "init" "n1") "and" (p "init" "a") "->"+    (p "init" "b") "and" (p "resp" "a") "->" (p "resp" "b"))+  (traces ((send (enc n a-0 (pubk a))) (recv (enc n n2 (pubk a-0)))))+  (label 19)+  (unrealized (0 1))+  (origs (n (0 0)))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton ns+  (vars (n n2 n2-0 text) (a a-0 name))+  (defstrand init 2 (n1 n) (n2 n2) (a a-0) (b a))+  (defstrand resp 2 (n2 n2-0) (n1 n) (b a) (a a-0))+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (privk a))+  (uniq-orig n)+  (operation nonce-test (added-strand resp 2) n (0 1)+    (enc n a-0 (pubk a)))+  (traces ((send (enc n a-0 (pubk a))) (recv (enc n n2 (pubk a-0))))+    ((recv (enc n a-0 (pubk a))) (send (enc n n2-0 (pubk a-0)))))+  (label 20)+  (parent 19)+  (unrealized)+  (shape)+  (satisfies yes)+  (maps ((0) ((a a) (n n) (a-0 a-0) (n2 n2))))+  (origs (n (0 0))))++(comment "Nothing left to do")++(defprotocol ns basic+  (defrole init+    (vars (a b name) (n1 n2 text))+    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b)))))+  (defrole resp+    (vars (b a name) (n2 n1 text))+    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))+      (recv (enc n2 (pubk b)))))+  (comment "Needham-Schroeder with no role origination assumptions"))++(defskeleton ns+  (vars (n n1 text) (a b name))+  (defstrand resp 3 (n2 n) (n1 n1) (b b) (a a))+  (non-orig (privk a))+  (uniq-orig n)+  (goals+    (forall ((a name) (n text) (z0 node))+      (implies+        (and (p "resp" 2 z0) (p "resp" "n2" z0 n) (p "resp" "a" z0 a)+          (non (privk a)) (uniq n))+        (exists ((z1 node))+          (and (p "init" 2 z1) (p "init" "a" z1 a))))))+  (comment "Responder authentication goal"+    "Same as unilateral goal under the predicate mapping:" (p "init" 1)+    "->" (p "resp" 2) "and" (p "init" "n") "->" (p "resp" "n2") "and"+    (p "init" "a") "->" (p "resp" "a") "and" (p "resp" 1) "->"+    (p "init" 2) "and" (p "resp" "a") "->" (p "init" "a"))+  (traces+    ((recv (enc n1 a (pubk b))) (send (enc n1 n (pubk a)))+      (recv (enc n (pubk b)))))+  (label 21)+  (unrealized (0 2))+  (origs (n (0 1)))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton ns+  (vars (n n1 text) (a b b-0 name))+  (defstrand resp 3 (n2 n) (n1 n1) (b b) (a a))+  (defstrand init 3 (n1 n1) (n2 n) (a a) (b b-0))+  (precedes ((0 1) (1 1)) ((1 2) (0 2)))+  (non-orig (privk a))+  (uniq-orig n)+  (operation nonce-test (added-strand init 3) n (0 2)+    (enc n1 n (pubk a)))+  (traces+    ((recv (enc n1 a (pubk b))) (send (enc n1 n (pubk a)))+      (recv (enc n (pubk b))))+    ((send (enc n1 a (pubk b-0))) (recv (enc n1 n (pubk a)))+      (send (enc n (pubk b-0)))))+  (label 22)+  (parent 21)+  (unrealized)+  (shape)+  (satisfies yes)+  (maps ((0) ((a a) (n n) (b b) (n1 n1))))+  (origs (n (0 1))))++(comment "Nothing left to do")++(defprotocol ns basic+  (defrole init+    (vars (a b name) (n1 n2 text))+    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b)))))+  (defrole resp+    (vars (b a name) (n2 n1 text))+    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))+      (recv (enc n2 (pubk b)))))+  (comment "Needham-Schroeder with no role origination assumptions"))++(defskeleton ns+  (vars (n n2 text) (a b name))+  (defstrand init 2 (n1 n) (n2 n2) (a a) (b b))+  (non-orig (privk a) (privk b))+  (uniq-orig n)+  (goals+    (forall ((a b name) (n text) (z0 node))+      (implies+        (and (p "init" 1 z0) (p "init" "n1" z0 n) (p "init" "a" z0 a)+          (p "init" "b" z0 b) (non (privk a)) (non (privk b)) (uniq n))+        (exists ((z1 node)) (and (p "resp" 1 z1) (p "resp" "b" z1 b)))))+    (forall ((a b name) (n text) (z0 node))+      (implies+        (and (p "init" 1 z0) (p "init" "n1" z0 n) (p "init" "a" z0 a)+          (p "init" "b" z0 b) (non (privk a)) (non (privk b)) (uniq n))+        (exists ((z1 node))+          (and (p "resp" 1 z1) (p "resp" "a" z1 a))))))+  (comment "Two initiator authentication goals")+  (traces ((send (enc n a (pubk b))) (recv (enc n n2 (pubk a)))))+  (label 23)+  (unrealized (0 1))+  (origs (n (0 0)))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton ns+  (vars (n n2 n2-0 text) (a b name))+  (defstrand init 2 (n1 n) (n2 n2) (a a) (b b))+  (defstrand resp 2 (n2 n2-0) (n1 n) (b b) (a a))+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (privk a) (privk b))+  (uniq-orig n)+  (operation nonce-test (added-strand resp 2) n (0 1)+    (enc n a (pubk b)))+  (traces ((send (enc n a (pubk b))) (recv (enc n n2 (pubk a))))+    ((recv (enc n a (pubk b))) (send (enc n n2-0 (pubk a)))))+  (label 24)+  (parent 23)+  (unrealized (0 1))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton ns+  (vars (n n2 text) (a b name))+  (defstrand init 2 (n1 n) (n2 n2) (a a) (b b))+  (defstrand resp 2 (n2 n2) (n1 n) (b b) (a a))+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (privk a) (privk b))+  (uniq-orig n)+  (operation nonce-test (contracted (n2-0 n2)) n (0 1)+    (enc n n2 (pubk a)) (enc n a (pubk b)))+  (traces ((send (enc n a (pubk b))) (recv (enc n n2 (pubk a))))+    ((recv (enc n a (pubk b))) (send (enc n n2 (pubk a)))))+  (label 25)+  (parent 24)+  (unrealized)+  (shape)+  (satisfies yes yes)+  (maps ((0) ((a a) (b b) (n n) (n2 n2))))+  (origs (n (0 0))))++(comment "Nothing left to do")++(defprotocol ns basic+  (defrole init+    (vars (a b name) (n1 n2 text))+    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b)))))+  (defrole resp+    (vars (b a name) (n2 n1 text))+    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))+      (recv (enc n2 (pubk b)))))+  (comment "Needham-Schroeder with no role origination assumptions"))++(defskeleton ns+  (vars (n1 n2 text) (b a name))+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))+  (non-orig (privk b))+  (uniq-orig n1)+  (goals+    (forall ((n1 n2 text) (b a name) (z z-0 node))+      (implies+        (and (p "init" 0 z) (p "init" 2 z-0) (p "init" "n1" z-0 n1)+          (p "init" "n2" z-0 n2) (p "init" "a" z-0 a)+          (p "init" "b" z-0 b) (str-prec z z-0) (non (privk b))+          (uniq-at n1 z))+        (exists ((n2-0 text) (z-1 z-2 z-3 node))+          (and (p "init" 1 z-1) (p "resp" 0 z-2) (p "resp" 1 z-3)+            (p "resp" "n2" z-3 n2-0) (p "resp" "n1" z-3 n1)+            (p "resp" "b" z-3 b) (p "resp" "a" z-3 a) (prec z z-2)+            (prec z-3 z-1) (str-prec z z-1) (str-prec z-1 z-0)+            (str-prec z-2 z-3))))))+  (comment "Shape analysis sentence")+  (traces+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b)))))+  (label 26)+  (unrealized (0 1))+  (origs (n1 (0 0)))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton ns+  (vars (n1 n2 n2-0 text) (b a name))+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))+  (defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a))+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (privk b))+  (uniq-orig n1)+  (operation nonce-test (added-strand resp 2) n1 (0 1)+    (enc n1 a (pubk b)))+  (traces+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b))))+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2-0 (pubk a)))))+  (label 27)+  (parent 26)+  (unrealized)+  (shape)+  (satisfies yes)+  (maps ((0) ((n1 n1) (n2 n2) (b b) (a a))))+  (origs (n1 (0 0))))++(comment "Nothing left to do")++(defprotocol ns basic+  (defrole init+    (vars (a b name) (n1 n2 text))+    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b)))))+  (defrole resp+    (vars (b a name) (n2 n1 text))+    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))+      (recv (enc n2 (pubk b)))))+  (comment "Needham-Schroeder with no role origination assumptions"))++(defskeleton ns+  (vars (n2 n1 text) (a b name))+  (deflistener n2)+  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))+  (non-orig (privk a) (privk b))+  (uniq-orig n2)+  (goals+    (forall ((a b name) (n2 text) (z0 z1 node))+      (implies+        (and (p "resp" 2 z0) (p "resp" "n2" z0 n2) (p "resp" "a" z0 a)+          (p "resp" "b" z0 b) (p "" 0 z1) (p "" "x" z1 n2)+          (non (privk a)) (non (privk b)) (uniq n2)) (false))))+  (comment "Responder point of view"+    "Failed secrecy goal: nonce n2 not revealed")+  (traces ((recv n2))+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))+      (recv (enc n2 (pubk b)))))+  (label 28)+  (unrealized (0 0) (1 2))+  (preskeleton)+  (comment "Not a skeleton"))++(defskeleton ns+  (vars (n2 n1 text) (a b name))+  (deflistener n2)+  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))+  (precedes ((1 1) (0 0)))+  (non-orig (privk a) (privk b))+  (uniq-orig n2)+  (traces ((recv n2))+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))+      (recv (enc n2 (pubk b)))))+  (label 29)+  (parent 28)+  (unrealized (0 0) (1 2))+  (origs (n2 (1 1)))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton ns+  (vars (n2 n1 text) (a b b-0 name))+  (deflistener n2)+  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b-0))+  (precedes ((1 1) (0 0)) ((1 1) (2 1)) ((2 2) (1 2)))+  (non-orig (privk a) (privk b))+  (uniq-orig n2)+  (operation nonce-test (added-strand init 3) n2 (1 2)+    (enc n1 n2 (pubk a)))+  (traces ((recv n2))+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))+      (recv (enc n2 (pubk b))))+    ((send (enc n1 a (pubk b-0))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b-0)))))+  (label 30)+  (parent 29)+  (unrealized (0 0))+  (comment "2 in cohort - 2 not yet seen"))++(defskeleton ns+  (vars (n2 n1 text) (a b b-0 name))+  (deflistener n2)+  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b-0))+  (precedes ((1 1) (2 1)) ((2 2) (0 0)) ((2 2) (1 2)))+  (non-orig (privk a) (privk b))+  (uniq-orig n2)+  (operation nonce-test (displaced 3 2 init 3) n2 (0 0)+    (enc n1 n2 (pubk a)))+  (traces ((recv n2))+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))+      (recv (enc n2 (pubk b))))+    ((send (enc n1 a (pubk b-0))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b-0)))))+  (label 31)+  (parent 30)+  (unrealized)+  (shape)+  (satisfies (no (a a) (b b) (n2 n2) (z0 (1 2)) (z1 (0 0))))+  (maps ((0 1) ((a a) (b b) (n2 n2) (n1 n1))))+  (origs (n2 (1 1))))++(defskeleton ns+  (vars (n2 n1 text) (a b b-0 b-1 name))+  (deflistener n2)+  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b-0))+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b-1))+  (precedes ((1 1) (2 1)) ((1 1) (3 1)) ((2 2) (1 2)) ((3 2) (0 0)))+  (non-orig (privk a) (privk b))+  (uniq-orig n2)+  (operation nonce-test (added-strand init 3) n2 (0 0)+    (enc n1 n2 (pubk a)))+  (traces ((recv n2))+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))+      (recv (enc n2 (pubk b))))+    ((send (enc n1 a (pubk b-0))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b-0))))+    ((send (enc n1 a (pubk b-1))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b-1)))))+  (label 32)+  (parent 30)+  (unrealized)+  (shape)+  (satisfies (no (a a) (b b) (n2 n2) (z0 (1 2)) (z1 (0 0))))+  (maps ((0 1) ((a a) (b b) (n2 n2) (n1 n1))))+  (origs (n2 (1 1))))++(comment "Nothing left to do")++(defprotocol ns basic+  (defrole init+    (vars (a b name) (n1 n2 text))+    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b)))))+  (defrole resp+    (vars (b a name) (n2 n1 text))+    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))+      (recv (enc n2 (pubk b)))))+  (comment "Needham-Schroeder with no role origination assumptions"))++(defskeleton ns+  (vars (n1 n1-0 n2 n2-0 text) (a b name))+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))+  (defstrand init 3 (n1 n1-0) (n2 n2-0) (a a) (b b))+  (non-orig (privk a) (privk b))+  (uniq-orig n1 n1-0)+  (goals+    (forall ((n1 n1-0 n2 n2-0 text) (a b name) (z z-0 z-1 z-2 node))+      (implies+        (and (p "init" 0 z) (p "init" 2 z-0) (p "init" 0 z-1)+          (p "init" 2 z-2) (p "init" "n1" z-0 n1) (p "init" "n2" z-0 n2)+          (p "init" "a" z-0 a) (p "init" "b" z-0 b)+          (p "init" "n1" z-2 n1-0) (p "init" "n2" z-2 n2-0)+          (p "init" "a" z-2 a) (p "init" "b" z-2 b) (str-prec z z-0)+          (str-prec z-1 z-2) (non (privk a)) (non (privk b))+          (uniq-at n1 z) (uniq-at n1-0 z-1)) (= z-1 z))))+  (comment "Double initiator point of view")+  (traces+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b))))+    ((send (enc n1-0 a (pubk b))) (recv (enc n1-0 n2-0 (pubk a)))+      (send (enc n2-0 (pubk b)))))+  (label 33)+  (unrealized (0 1) (1 1))+  (origs (n1 (0 0)) (n1-0 (1 0)))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton ns+  (vars (n1 n2 text) (a b name))+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))+  (non-orig (privk a) (privk b))+  (uniq-orig n1)+  (operation collapsed 1 0)+  (traces+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b)))))+  (label 34)+  (parent 33)+  (unrealized (0 1))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton ns+  (vars (n1 n1-0 n2 n2-0 n2-1 text) (a b name))+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))+  (defstrand init 3 (n1 n1-0) (n2 n2-0) (a a) (b b))+  (defstrand resp 2 (n2 n2-1) (n1 n1-0) (b b) (a a))+  (precedes ((1 0) (2 0)) ((2 1) (1 1)))+  (non-orig (privk a) (privk b))+  (uniq-orig n1 n1-0)+  (operation nonce-test (added-strand resp 2) n1-0 (1 1)+    (enc n1-0 a (pubk b)))+  (traces+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b))))+    ((send (enc n1-0 a (pubk b))) (recv (enc n1-0 n2-0 (pubk a)))+      (send (enc n2-0 (pubk b))))+    ((recv (enc n1-0 a (pubk b))) (send (enc n1-0 n2-1 (pubk a)))))+  (label 35)+  (parent 33)+  (unrealized (0 1) (1 1))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton ns+  (vars (n1 n2 n2-0 text) (a b name))+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))+  (defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a))+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (privk a) (privk b))+  (uniq-orig n1)+  (operation nonce-test (added-strand resp 2) n1 (0 1)+    (enc n1 a (pubk b)))+  (traces+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b))))+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2-0 (pubk a)))))+  (label 36)+  (parent 34)+  (unrealized (0 1))+  (origs (n1 (0 0)))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton ns+  (vars (n1 n1-0 n2 n2-0 text) (a b name))+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))+  (defstrand init 3 (n1 n1-0) (n2 n2-0) (a a) (b b))+  (defstrand resp 2 (n2 n2-0) (n1 n1-0) (b b) (a a))+  (precedes ((1 0) (2 0)) ((2 1) (1 1)))+  (non-orig (privk a) (privk b))+  (uniq-orig n1 n1-0)+  (operation nonce-test (contracted (n2-1 n2-0)) n1-0 (1 1)+    (enc n1-0 n2-0 (pubk a)) (enc n1-0 a (pubk b)))+  (traces+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b))))+    ((send (enc n1-0 a (pubk b))) (recv (enc n1-0 n2-0 (pubk a)))+      (send (enc n2-0 (pubk b))))+    ((recv (enc n1-0 a (pubk b))) (send (enc n1-0 n2-0 (pubk a)))))+  (label 37)+  (parent 35)+  (unrealized (0 1))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton ns+  (vars (n1 n2 text) (a b name))+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))+  (defstrand resp 2 (n2 n2) (n1 n1) (b b) (a a))+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (privk a) (privk b))+  (uniq-orig n1)+  (operation nonce-test (contracted (n2-0 n2)) n1 (0 1)+    (enc n1 n2 (pubk a)) (enc n1 a (pubk b)))+  (traces+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b))))+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))))+  (label 38)+  (parent 36)+  (unrealized)+  (shape)+  (satisfies yes)+  (maps ((0 0) ((a a) (b b) (n1 n1) (n1-0 n1) (n2 n2) (n2-0 n2))))+  (origs (n1 (0 0))))++(defskeleton ns+  (vars (n1 n1-0 n2 n2-0 n2-1 text) (a b name))+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))+  (defstrand init 3 (n1 n1-0) (n2 n2-0) (a a) (b b))+  (defstrand resp 2 (n2 n2-0) (n1 n1-0) (b b) (a a))+  (defstrand resp 2 (n2 n2-1) (n1 n1) (b b) (a a))+  (precedes ((0 0) (3 0)) ((1 0) (2 0)) ((2 1) (1 1)) ((3 1) (0 1)))+  (non-orig (privk a) (privk b))+  (uniq-orig n1 n1-0)+  (operation nonce-test (added-strand resp 2) n1 (0 1)+    (enc n1 a (pubk b)))+  (traces+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b))))+    ((send (enc n1-0 a (pubk b))) (recv (enc n1-0 n2-0 (pubk a)))+      (send (enc n2-0 (pubk b))))+    ((recv (enc n1-0 a (pubk b))) (send (enc n1-0 n2-0 (pubk a))))+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2-1 (pubk a)))))+  (label 39)+  (parent 37)+  (unrealized (0 1))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton ns+  (vars (n1 n1-0 n2 n2-0 text) (a b name))+  (defstrand init 3 (n1 n1) (n2 n2-0) (a a) (b b))+  (defstrand init 3 (n1 n1-0) (n2 n2) (a a) (b b))+  (defstrand resp 2 (n2 n2) (n1 n1-0) (b b) (a a))+  (defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a))+  (precedes ((0 0) (3 0)) ((1 0) (2 0)) ((2 1) (1 1)) ((3 1) (0 1)))+  (non-orig (privk a) (privk b))+  (uniq-orig n1 n1-0)+  (operation nonce-test (contracted (n2-1 n2-0)) n1 (0 1)+    (enc n1 n2-0 (pubk a)) (enc n1 a (pubk b)))+  (traces+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2-0 (pubk a)))+      (send (enc n2-0 (pubk b))))+    ((send (enc n1-0 a (pubk b))) (recv (enc n1-0 n2 (pubk a)))+      (send (enc n2 (pubk b))))+    ((recv (enc n1-0 a (pubk b))) (send (enc n1-0 n2 (pubk a))))+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2-0 (pubk a)))))+  (label 40)+  (parent 39)+  (unrealized)+  (shape)+  (satisfies+    (no (n1-0 n1) (n1 n1-0) (n2-0 n2-0) (n2 n2) (a a) (b b) (z-2 (0 0))+      (z-1 (0 2)) (z-0 (1 0)) (z (1 2))))+  (maps ((0 1) ((a a) (b b) (n1 n1) (n1-0 n1-0) (n2 n2-0) (n2-0 n2))))+  (origs (n1 (0 0)) (n1-0 (1 0))))++(comment "Nothing left to do")++(defprotocol nsl-typeless basic+  (defrole init+    (vars (a b name) (n1 text) (n2 mesg))+    (trace (send (enc a n1 (pubk b))) (recv (enc n1 n2 b (pubk a)))+      (send (enc n2 (pubk b)))))+  (defrole resp+    (vars (b a name) (n2 text) (n1 mesg))+    (trace (recv (enc a n1 (pubk b))) (send (enc n1 n2 b (pubk a)))+      (recv (enc n2 (pubk b)))))+  (comment "Needham-Schroeder-Lowe with untyped nonces"))++(defskeleton nsl-typeless+  (vars (n1 mesg) (n2 text) (a b name))+  (deflistener n2)+  (defstrand resp 2 (n1 n1) (n2 n2) (b b) (a a))+  (non-orig (privk a) (privk b))+  (uniq-orig n2)+  (goals+    (forall ((n2 text) (a b name) (z z-0 node))+      (implies+        (and (p "resp" 1 z) (p "" 0 z-0) (p "resp" "n2" z n2)+          (p "resp" "b" z b) (p "resp" "a" z a) (p "" "x" z-0 n2)+          (non (privk a)) (non (privk b)) (uniq n2)) (false))))+  (comment "Shows typeflaw in typeless NSL")+  (traces ((recv n2))+    ((recv (enc a n1 (pubk b))) (send (enc n1 n2 b (pubk a)))))+  (label 41)+  (unrealized (0 0))+  (preskeleton)+  (comment "Not a skeleton"))++(defskeleton nsl-typeless+  (vars (n1 mesg) (n2 text) (a b name))+  (deflistener n2)+  (defstrand resp 2 (n1 n1) (n2 n2) (b b) (a a))+  (precedes ((1 1) (0 0)))+  (non-orig (privk a) (privk b))+  (uniq-orig n2)+  (traces ((recv n2))+    ((recv (enc a n1 (pubk b))) (send (enc n1 n2 b (pubk a)))))+  (label 42)+  (parent 41)+  (unrealized (0 0))+  (origs (n2 (1 1)))+  (comment "2 in cohort - 2 not yet seen"))++(defskeleton nsl-typeless+  (vars (n2 n1 text) (a b name))+  (deflistener n2)+  (defstrand resp 2 (n1 n1) (n2 n2) (b b) (a a))+  (defstrand init 3 (n2 n2) (n1 n1) (a a) (b b))+  (precedes ((1 1) (2 1)) ((2 2) (0 0)))+  (non-orig (privk a) (privk b))+  (uniq-orig n2)+  (operation nonce-test (added-strand init 3) n2 (0 0)+    (enc n1 n2 b (pubk a)))+  (traces ((recv n2))+    ((recv (enc a n1 (pubk b))) (send (enc n1 n2 b (pubk a))))+    ((send (enc a n1 (pubk b))) (recv (enc n1 n2 b (pubk a)))+      (send (enc n2 (pubk b)))))+  (label 43)+  (parent 42)+  (unrealized (0 0))+  (comment "empty cohort"))++(defskeleton nsl-typeless+  (vars (n2 n2-0 text) (a b a-0 name))+  (deflistener n2)+  (defstrand resp 2 (n1 a-0) (n2 n2) (b b) (a a))+  (defstrand resp 2 (n1 (cat n2 b)) (n2 n2-0) (b a) (a a-0))+  (precedes ((1 1) (2 0)) ((2 1) (0 0)))+  (non-orig (privk a) (privk b))+  (uniq-orig n2)+  (operation nonce-test (added-strand resp 2) n2 (0 0)+    (enc a-0 n2 b (pubk a)))+  (traces ((recv n2))+    ((recv (enc a a-0 (pubk b))) (send (enc a-0 n2 b (pubk a))))+    ((recv (enc a-0 n2 b (pubk a)))+      (send (enc (cat n2 b) n2-0 a (pubk a-0)))))+  (label 44)+  (parent 42)+  (unrealized)+  (shape)+  (satisfies (no (n2 n2) (a a) (b b) (z-0 (1 1)) (z (0 0))))+  (maps ((0 1) ((n2 n2) (a a) (b b) (n1 a-0))))+  (origs (n2 (1 1))))++(comment "Nothing left to do")++(defprotocol ns basic+  (defrole init+    (vars (a b name) (n1 n2 text))+    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b)))))+  (defrole resp+    (vars (b a name) (n2 n1 text))+    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))+      (recv (enc n2 (pubk b)))))+  (comment "Needham-Schroeder with no role origination assumptions"))++(defskeleton ns+  (vars (n2 n1 text) (a b name))+  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))+  (non-orig (privk a))+  (uniq-orig n2)+  (goals+    (forall ((n1 n2 text) (a b name) (z z-0 node))+      (implies+        (and (p "init" 0 z) (p "init" 2 z-0) (p "init" "n1" z-0 n1)+          (p "init" "n2" z-0 n2) (p "init" "a" z-0 a)+          (p "init" "b" z-0 b) (str-prec z z-0) (non (privk a))+          (non (privk b)) (uniq-at n1 z))+        (exists ((z-1 z-2 z-3 node))+          (and (p "init" 1 z-1) (p "resp" 0 z-2) (p "resp" 1 z-3)+            (p "resp" "n2" z-3 n2) (p "resp" "n1" z-3 n1)+            (p "resp" "b" z-3 b) (p "resp" "a" z-3 a) (prec z z-2)+            (prec z-3 z-1) (str-prec z z-1) (str-prec z-1 z-0)+            (str-prec z-2 z-3))))))+  (comment "Responder point of view with SAS")+  (traces+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))+      (recv (enc n2 (pubk b)))))+  (label 45)+  (unrealized (0 2))+  (origs (n2 (0 1)))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton ns+  (vars (n2 n1 text) (a b b-0 name))+  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b-0))+  (precedes ((0 1) (1 1)) ((1 2) (0 2)))+  (non-orig (privk a))+  (uniq-orig n2)+  (operation nonce-test (added-strand init 3) n2 (0 2)+    (enc n1 n2 (pubk a)))+  (traces+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))+      (recv (enc n2 (pubk b))))+    ((send (enc n1 a (pubk b-0))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b-0)))))+  (label 46)+  (parent 45)+  (unrealized)+  (shape)+  (satisfies yes)+  (maps ((0) ((a a) (n2 n2) (b b) (n1 n1))))+  (origs (n2 (0 1))))++(comment "Nothing left to do")++(defprotocol ns basic+  (defrole init+    (vars (a b name) (n1 n2 text))+    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b)))))+  (defrole resp+    (vars (b a name) (n2 n1 text))+    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))+      (recv (enc n2 (pubk b)))))+  (comment "Needham-Schroeder with no role origination assumptions"))++(defskeleton ns+  (vars (n2 n1 text) (a b name))+  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))+  (non-orig (privk a))+  (uniq-orig n2)+  (goals+    (forall ((n1 n2 text) (a b name) (z z-0 node))+      (implies+        (and (p "init" 0 z) (p "init" 2 z-0) (p "init" "n1" z-0 n1)+          (p "init" "n2" z-0 n2) (p "init" "a" z-0 a)+          (p "init" "b" z-0 b) (str-prec z z-0) (non (privk a))+          (non (privk b)) (uniq-at n1 z)) (false))))+  (comment "Responder point of view with false as the conclusion")+  (traces+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))+      (recv (enc n2 (pubk b)))))+  (label 47)+  (unrealized (0 2))+  (origs (n2 (0 1)))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton ns+  (vars (n2 n1 text) (a b b-0 name))+  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b-0))+  (precedes ((0 1) (1 1)) ((1 2) (0 2)))+  (non-orig (privk a))+  (uniq-orig n2)+  (operation nonce-test (added-strand init 3) n2 (0 2)+    (enc n1 n2 (pubk a)))+  (traces+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))+      (recv (enc n2 (pubk b))))+    ((send (enc n1 a (pubk b-0))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b-0)))))+  (label 48)+  (parent 47)+  (unrealized)+  (shape)+  (satisfies yes)+  (maps ((0) ((a a) (n2 n2) (b b) (n1 n1))))+  (origs (n2 (0 1))))++(comment "Nothing left to do")++(defprotocol ns basic+  (defrole init+    (vars (a b name) (n1 n2 text))+    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b)))))+  (defrole resp+    (vars (b a name) (n2 n1 text))+    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))+      (recv (enc n2 (pubk b)))))+  (comment "Needham-Schroeder with no role origination assumptions"))++(defskeleton ns+  (vars (n1 n2 text) (a b name))+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))+  (non-orig (privk a) (privk b))+  (uniq-orig n1)+  (goals+    (forall ((n1 n2 text) (a b name) (z z-0 node))+      (implies+        (and (p "init" 0 z) (p "init" 2 z-0) (p "init" "n1" z-0 n1)+          (p "init" "n2" z-0 n2) (p "init" "a" z-0 a)+          (p "init" "b" z-0 b) (str-prec z z-0) (non (privk a))+          (non (privk b)) (uniq-at n1 z)) (false))))+  (comment "Initiator point of view with false as the conclusion")+  (traces+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b)))))+  (label 49)+  (unrealized (0 1))+  (origs (n1 (0 0)))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton ns+  (vars (n1 n2 n2-0 text) (a b name))+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))+  (defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a))+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (privk a) (privk b))+  (uniq-orig n1)+  (operation nonce-test (added-strand resp 2) n1 (0 1)+    (enc n1 a (pubk b)))+  (traces+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b))))+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2-0 (pubk a)))))+  (label 50)+  (parent 49)+  (unrealized (0 1))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton ns+  (vars (n1 n2 text) (a b name))+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))+  (defstrand resp 2 (n2 n2) (n1 n1) (b b) (a a))+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (privk a) (privk b))+  (uniq-orig n1)+  (operation nonce-test (contracted (n2-0 n2)) n1 (0 1)+    (enc n1 n2 (pubk a)) (enc n1 a (pubk b)))+  (traces+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b))))+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))))+  (label 51)+  (parent 50)+  (unrealized)+  (shape)+  (satisfies (no (n1 n1) (n2 n2) (a a) (b b) (z-0 (0 0)) (z (0 2))))+  (maps ((0) ((a a) (b b) (n1 n1) (n2 n2))))+  (origs (n1 (0 0))))++(comment "Nothing left to do")++(defprotocol ns basic+  (defrole init+    (vars (a b name) (n1 n2 text))+    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b)))))+  (defrole resp+    (vars (b a name) (n2 n1 text))+    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))+      (recv (enc n2 (pubk b)))))+  (comment "Needham-Schroeder with no role origination assumptions"))++(defskeleton ns+  (vars (n n1 text) (a b name))+  (defstrand resp 3 (n2 n) (n1 n1) (b b) (a a))+  (non-orig (privk a) (privk b))+  (uniq-orig n)+  (goals+    (forall ((a b name) (n text) (z0 node))+      (implies+        (and (p "resp" 2 z0) (p "resp" "n2" z0 n) (p "resp" "a" z0 a)+          (p "resp" "b" z0 b) (non (privk a)) (non (privk b)) (uniq n))+        (exists ((z1 node)) (and (p "init" 2 z1) (p "init" "a" z1 a)))))+    (forall ((a b name) (n text) (z0 node))+      (implies+        (and (p "resp" 2 z0) (p "resp" "n2" z0 n) (p "resp" "a" z0 a)+          (p "resp" "b" z0 b) (non (privk a)) (non (privk b)) (uniq n))+        (exists ((z1 node))+          (and (p "init" 2 z1) (p "init" "b" z1 b))))))+  (comment "Two responder authentication goals")+  (traces+    ((recv (enc n1 a (pubk b))) (send (enc n1 n (pubk a)))+      (recv (enc n (pubk b)))))+  (label 52)+  (unrealized (0 2))+  (origs (n (0 1)))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton ns+  (vars (n n1 text) (a b b-0 name))+  (defstrand resp 3 (n2 n) (n1 n1) (b b) (a a))+  (defstrand init 3 (n1 n1) (n2 n) (a a) (b b-0))+  (precedes ((0 1) (1 1)) ((1 2) (0 2)))+  (non-orig (privk a) (privk b))+  (uniq-orig n)+  (operation nonce-test (added-strand init 3) n (0 2)+    (enc n1 n (pubk a)))+  (traces+    ((recv (enc n1 a (pubk b))) (send (enc n1 n (pubk a)))+      (recv (enc n (pubk b))))+    ((send (enc n1 a (pubk b-0))) (recv (enc n1 n (pubk a)))+      (send (enc n (pubk b-0)))))+  (label 53)+  (parent 52)+  (unrealized)+  (shape)+  (satisfies yes (no (a a) (b b) (n n) (z0 (0 2))))+  (maps ((0) ((a a) (b b) (n n) (n1 n1))))+  (origs (n (0 1))))++(comment "Nothing left to do")++(defprotocol ns-role-origs basic+  (defrole init+    (vars (a b name) (n1 n2 text))+    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b))))+    (non-orig (privk b))+    (uniq-orig n1))+  (defrole resp+    (vars (b a name) (n2 n1 text))+    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))+      (recv (enc n2 (pubk b))))+    (non-orig (privk a))+    (uniq-orig n2))+  (comment+    "Needham-Schroeder with role assumptions that are too strong"))++(defskeleton ns-role-origs+  (vars (n1 n2 text) (a b name))+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))+  (non-orig (privk b))+  (uniq-orig n1)+  (traces+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b)))))+  (label 54)+  (unrealized (0 1))+  (origs (n1 (0 0)))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton ns-role-origs+  (vars (n1 n2 n2-0 text) (a b name))+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))+  (defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a))+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (privk a) (privk b))+  (uniq-orig n1 n2-0)+  (operation nonce-test (added-strand resp 2) n1 (0 1)+    (enc n1 a (pubk b)))+  (traces+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b))))+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2-0 (pubk a)))))+  (label 55)+  (parent 54)+  (unrealized (0 1))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton ns-role-origs+  (vars (n1 n2 text) (a b name))+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))+  (defstrand resp 2 (n2 n2) (n1 n1) (b b) (a a))+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (privk a) (privk b))+  (uniq-orig n1 n2)+  (operation nonce-test (contracted (n2-0 n2)) n1 (0 1)+    (enc n1 n2 (pubk a)) (enc n1 a (pubk b)))+  (traces+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b))))+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))))+  (label 56)+  (parent 55)+  (unrealized)+  (shape)+  (maps ((0) ((a a) (b b) (n1 n1) (n2 n2))))+  (origs (n2 (1 1)) (n1 (0 0))))++(comment "Nothing left to do")++(defprotocol ns-role-origs basic+  (defrole init+    (vars (a b name) (n1 n2 text))+    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b))))+    (non-orig (privk b))+    (uniq-orig n1))+  (defrole resp+    (vars (b a name) (n2 n1 text))+    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))+      (recv (enc n2 (pubk b))))+    (non-orig (privk a))+    (uniq-orig n2))+  (comment+    "Needham-Schroeder with role assumptions that are too strong"))++(defskeleton ns-role-origs+  (vars (n2 n1 text) (b a name))+  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))+  (non-orig (privk a))+  (uniq-orig n2)+  (traces+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))+      (recv (enc n2 (pubk b)))))+  (label 57)+  (unrealized (0 2))+  (origs (n2 (0 1)))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton ns-role-origs+  (vars (n2 n1 text) (b a b-0 name))+  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b-0))+  (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2)))+  (non-orig (privk a) (privk b-0))+  (uniq-orig n2 n1)+  (operation nonce-test (added-strand init 3) n2 (0 2)+    (enc n1 n2 (pubk a)))+  (traces+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))+      (recv (enc n2 (pubk b))))+    ((send (enc n1 a (pubk b-0))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b-0)))))+  (label 58)+  (parent 57)+  (unrealized (0 0) (0 2))+  (comment "2 in cohort - 2 not yet seen"))++(defskeleton ns-role-origs+  (vars (n2 n1 text) (a b name))+  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))+  (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2)))+  (non-orig (privk a) (privk b))+  (uniq-orig n2 n1)+  (operation nonce-test (contracted (b-0 b)) n1 (0 0)+    (enc n1 a (pubk b)))+  (traces+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))+      (recv (enc n2 (pubk b))))+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b)))))+  (label 59)+  (parent 58)+  (unrealized)+  (shape)+  (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))+  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b-0))+  (defstrand resp 2 (n2 n2-0) (n1 n1) (b b-0) (a a))+  (precedes ((0 1) (1 1)) ((1 0) (2 0)) ((1 2) (0 2)) ((2 1) (0 0)))+  (non-orig (privk a) (privk b-0))+  (uniq-orig n2 n1 n2-0)+  (operation nonce-test (added-strand resp 2) n1 (0 0)+    (enc n1 a (pubk b-0)))+  (traces+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))+      (recv (enc n2 (pubk b))))+    ((send (enc n1 a (pubk b-0))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b-0))))+    ((recv (enc n1 a (pubk b-0))) (send (enc n1 n2-0 (pubk a)))))+  (label 60)+  (parent 58)+  (unrealized (0 0) (0 2))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton ns-role-origs+  (vars (n2 n1 n2-0 text) (a b name))+  (defstrand resp 3 (n2 n2) (n1 n1) (b b) (a a))+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))+  (defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a))+  (precedes ((0 1) (1 1)) ((1 0) (2 0)) ((1 2) (0 2)) ((2 1) (0 0)))+  (non-orig (privk a) (privk b))+  (uniq-orig n2 n1 n2-0)+  (operation nonce-test (contracted (b-0 b)) n1 (0 0)+    (enc n1 n2-0 (pubk a)) (enc n1 a (pubk b)))+  (traces+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))+      (recv (enc n2 (pubk b))))+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b))))+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2-0 (pubk a)))))+  (label 61)+  (parent 60)+  (seen 59)+  (unrealized)+  (comment "1 in cohort - 0 not yet seen"))++(comment "Nothing left to do")++(defprotocol ns2 basic+  (defrole init+    (vars (a b name) (n1 n2 n3 text))+    (trace (send (enc n1 n3 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b)))))+  (defrole resp+    (vars (b a name) (n2 n1 text))+    (trace (recv (enc n1 n1 a (pubk b))) (send (enc n1 n2 (pubk a)))+      (recv (enc n2 (pubk b))))+    (note doubled nonce in the first message))+  (note that this protocol is derived from Needham-Schroeder))++(defskeleton ns2+  (vars (n1 n2 n3 text) (a b name))+  (defstrand init 3 (n1 n1) (n2 n2) (n3 n3) (a a) (b b))+  (non-orig (privk a) (privk b))+  (uniq-orig n1)+  (traces+    ((send (enc n1 n3 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b)))))+  (label 62)+  (unrealized (0 1))+  (origs (n1 (0 0)))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton ns2+  (vars (n2 n3 n2-0 text) (a b name))+  (defstrand init 3 (n1 n3) (n2 n2) (n3 n3) (a a) (b b))+  (defstrand resp 2 (n2 n2-0) (n1 n3) (b b) (a a))+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (privk a) (privk b))+  (uniq-orig n3)+  (operation nonce-test (added-strand resp 2) n3 (0 1)+    (enc n3 n3 a (pubk b)))+  (traces+    ((send (enc n3 n3 a (pubk b))) (recv (enc n3 n2 (pubk a)))+      (send (enc n2 (pubk b))))+    ((recv (enc n3 n3 a (pubk b))) (send (enc n3 n2-0 (pubk a)))))+  (label 63)+  (parent 62)+  (unrealized (0 1))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton ns2+  (vars (n3 n2 text) (a b name))+  (defstrand init 3 (n1 n3) (n2 n2) (n3 n3) (a a) (b b))+  (defstrand resp 2 (n2 n2) (n1 n3) (b b) (a a))+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (privk a) (privk b))+  (uniq-orig n3)+  (operation nonce-test (contracted (n2-0 n2)) n3 (0 1)+    (enc n3 n2 (pubk a)) (enc n3 n3 a (pubk b)))+  (traces+    ((send (enc n3 n3 a (pubk b))) (recv (enc n3 n2 (pubk a)))+      (send (enc n2 (pubk b))))+    ((recv (enc n3 n3 a (pubk b))) (send (enc n3 n2 (pubk a)))))+  (label 64)+  (parent 63)+  (unrealized)+  (shape)+  (maps ((0) ((a a) (b b) (n1 n3) (n2 n2) (n3 n3))))+  (origs (n3 (0 0))))++(comment "Nothing left to do")++(defprotocol ns basic+  (defrole init+    (vars (a b name) (n1 n2 text))+    (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b)))))+  (defrole resp+    (vars (b a name) (n2 n1 text))+    (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))+      (recv (enc n2 (pubk b)))))+  (comment "Needham-Schroeder with no role origination assumptions"))++(defskeleton ns+  (vars (n1 n2 text) (a b name))+  (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b))+  (defstrand resp 2 (n2 n2) (n1 n1) (b b) (a a))+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (privk a) (privk b))+  (uniq-orig n1)+  (traces+    ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))+      (send (enc n2 (pubk b))))+    ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))))+  (label 65)+  (unrealized)+  (shape)+  (maps ((0 1) ((n1 n1) (n2 n2) (a a) (b b))))+  (origs (n1 (0 0))))  (comment "Nothing left to do")
tst/hashtest-key-hash.tst view
@@ -1,6 +1,6 @@ (herald "Hashtest") -(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from hashtest-key-hash.scm")  (defprotocol hashtest basic
tst/hashtest.tst view
@@ -1,6 +1,6 @@ (herald "Hashtest") -(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from hashtest.scm")  (defprotocol hashtest basic
tst/incompleteness_example.tst view
@@ -1,7 +1,7 @@ (herald incompleteness-example   (comment "Shows a shape not found by CPSA")) -(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from incompleteness_example.scm")  (defprotocol incompleteness-example basic
tst/isoreject.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from isoreject.scm")  (defprotocol isoreject basic
tst/kelly1.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from kelly1.scm")  (defprotocol kelly1 basic
tst/kerberos.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from kerberos.scm")  (defprotocol kerberos basic
tst/mass.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from mass.lsp")  (defprotocol mass basic
tst/mass2.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from mass2.lsp")  (defprotocol mass2 basic
tst/missing_contraction.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from missing_contraction.scm")  (defprotocol missing-contraction basic
tst/neuman-stubblebine-reauth.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from neuman-stubblebine-reauth.lsp")  (defprotocol neuman-stubblebine-reauth basic
tst/neuman-stubblebine.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from neuman-stubblebine.scm")  (defprotocol neuman-stubblebine basic
tst/no_contraction.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from no_contraction.scm")  (defprotocol no-contraction basic
tst/non_transforming.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from non_transforming.scm")  (defprotocol non_transforming basic
tst/nonaug-prune.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from nonaug-prune.scm")  (defprotocol nonaug-prune basic
tst/ns-l.tst view
@@ -1,7 +1,7 @@ (herald "Needham-Schroeder-Low Public-Key Protocol"   (comment "With deflistener's")) -(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from ns-l.scm")  (defprotocol ns basic
tst/ns.tst view
@@ -1,6 +1,6 @@ (herald "Needham-Schroeder Public-Key Protocol Variants") -(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from ns.scm")  (defprotocol ns basic
tst/nsl3.tst view
@@ -1,6 +1,6 @@ (herald "Three Party Needham-Schroeder-Lowe Protocol") -(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from nsl3.scm")  (defprotocol nsl3 basic
tst/nsl4cm1.tst view

file too large to diff

tst/nslsk.tst view
@@ -1,6 +1,6 @@ (herald "Needham-Schroeder-Lowe Protocol with symmetric encryption") -(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from nslsk.scm")  (defprotocol nslsk basic
tst/or.tst view
@@ -1,7 +1,7 @@ (herald "Otway-Rees Protocol"   (comment "Standard version using variables of sort mesg")) -(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from or.scm")  (defprotocol or basic
tst/pca.tst view
@@ -1,7 +1,7 @@ (herald "Privacy Certificate Authority" (bound 15)   (comment "Generation of an Attestation Identity Certificate")) -(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from pca.scm") (comment "Strand count bounded at 15")
tst/pen-non-orig-test.tst view
@@ -1,6 +1,6 @@ (herald "pen-non-orig test") -(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from pen-non-orig-test.scm")  (defprotocol pennonorigtest basic
tst/pkinit.tst view
@@ -1,6 +1,6 @@ (herald "Kerberos PK init") -(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from pkinit.scm")  (defprotocol pkinit basic
tst/preprocess.tst view
@@ -1,6 +1,6 @@ (herald "Pre-processing test example: modified NS with two responders") -(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from preprocess.scm")  (defprotocol ns basic
tst/print.tst view
@@ -1,7 +1,7 @@ (herald "Print Test"   (comment "See if read forms look like printed ones")) -(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from print.scm")  (defprotocol print-test basic
tst/pruning1.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from pruning1.scm")  (defprotocol prune basic
tst/sigenc.tst view
@@ -1,7 +1,7 @@ (herald "Signed Encrypted Message Example"   (comment "Shows examples of key usage of asymmetric keys")) -(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from sigenc.scm")  (defprotocol mult-keys-sig-enc basic
tst/sorted_epmo_acctnum.tst view
@@ -4,7 +4,7 @@     "This version uses sorts to avoid confusion"     "between a nonce and other data")) -(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from sorted_epmo_acctnum.scm") (comment "Strand count bounded at 12")
tst/targetterms2.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from targetterms2.scm")  (defprotocol targetterms2 basic
tst/targetterms6.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from targetterms6.scm")  (defprotocol targetterms6 basic
tst/targetterms8.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from targetterms8.scm")  (defprotocol targetterms8 basic
tst/timestamping.tst view
@@ -1,6 +1,6 @@ (herald timestamping-service) -(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from timestamping.scm")  (defprotocol timestamping-service basic
tst/uncarried_keys.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from uncarried_keys.scm")  (defprotocol uncarried-keys basic
tst/unilateral.tst view
@@ -1,6 +1,6 @@ (herald unilateral) -(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from unilateral.scm")  (defprotocol unilateral basic
tst/uo.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from uo.scm")  (defprotocol uniq-orig basic
tst/wang-hash.tst view
@@ -1,6 +1,6 @@ (herald "Wang's Fair Exchange Protocol" (bound 10)) -(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from wang-hash.scm") (comment "Strand count bounded at 10")
tst/wang-key-hash.tst view
@@ -1,6 +1,6 @@ (herald "Wang's Fair Exchange Protocol" (bound 10)) -(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from wang-key-hash.scm") (comment "Strand count bounded at 10")
tst/weird.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from weird.scm")  (defprotocol weird basic
tst/wide-mouth-frog-scyther.tst view
@@ -1,7 +1,7 @@ (herald "Wide-Mouth Frog Protocol from Scyther"   (comment "This protocol has an infinite number of shapes")) -(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from wide-mouth-frog-scyther.lsp")  (defprotocol wide-mouth-frog basic
tst/wide-mouth-frog.tst view
@@ -1,7 +1,7 @@ (herald "Wide-Mouth Frog Protocol"   (comment "This protocol has an infinite number of shapes")) -(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from wide-mouth-frog.lsp")  (defprotocol wide-mouth-frog basic
tst/wonthull.tst view
@@ -1,6 +1,6 @@ (herald wonthull (bound 9)) -(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from wonthull.scm") (comment "Strand count bounded at 9")
tst/wonthull2.tst view
@@ -1,6 +1,6 @@ (herald wonthull2 (bound 9)) -(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from wonthull2.scm") (comment "Strand count bounded at 9")
tst/wonthull3.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from wonthull3.scm")  (defprotocol wonthull3 basic
tst/woolam.tst view
@@ -1,6 +1,6 @@ (herald "Woo-Lam Protocol") -(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from woolam.scm")  (defprotocol woolam basic
tst/yahalom-6.3.6.tst view
@@ -5,7 +5,7 @@   (url "http://www.eecs.umich.edu/acal/swerve/docs/49-1.pdf")   (bound 15)) -(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from yahalom-6.3.6.scm") (comment "Strand count bounded at 15")
tst/yahalom.tst view
@@ -1,6 +1,6 @@ (herald "Yahalom Protocol Without Forwarding" (bound 15)) -(comment "CPSA 2.5.0")+(comment "CPSA 2.5.1") (comment "All input read from yahalom.scm") (comment "Strand count bounded at 15")