packages feed

cpsa 4.4.1 → 4.4.2

raw patch · 140 files changed

+1747/−140 lines, 140 files

Files

NEWS view
@@ -1,5 +1,30 @@ CPSA NEWS -- history of user-visible changes. +* Changes in version 4.4.2++** Fixed message equivalence test in cpsa4graph.++** Removed the cribsheet from the manual because it hasn't been+   updated to reflect CPSA4 syntax.++** We now allow (defstrandmax role-name bindings) in defskeleton forms.+   This declares an instance of the named role with the given+   bindings of maximal height for that role.  It is convenient when+   developing protocols, since the height may vary as the role is+   revised.++** Exponent variables received in exponentiated values and extracted by a role+   are now rejected, since this is unimplementable.  The loader raises+   an error.++** If the earliest occurrence of an exponent variable is in a transmission,+   the variable must be of rndx sort, not the more  general expt.  ++** An asymmetric key and its inverse are both considered to be generated+   at the first point either of them is created.++** Bugs in generalization that occasionally appear have been eliminated.  + * Changes in version 4.4.1  ** A bug concerning goal satisfaction was found and corrected.@@ -14,6 +39,9 @@    does not re-insert the original trace annotations in its output,    meaning that the rules would not be re-generated automatically when    reading the output file.++** Fixed cpsa4sas so that it makes use of a lang field specified+   within a protocol.  * Changes in version 4.4.0
cpsa.cabal view
@@ -1,5 +1,5 @@ Name:                   cpsa-Version:                4.4.1+Version:                4.4.2 Maintainer:             ramsdell@mitre.org Cabal-Version:          >= 1.10 License:                BSD3@@ -249,7 +249,8 @@   tst/wonthull.tst tst/wonthull2.scm tst/wonthull2.tst   tst/wonthull3.scm tst/wonthull3.tst tst/woolam.scm tst/woolam.tst   tst/wrap_decrypt.tst tst/yahalom-6.3.6.scm tst/yahalom-6.3.6.tst-  tst/yahalom.scm tst/yahalom.tst+  tst/yahalom.scm tst/yahalom.tst tst/blanchet-strandmax.scm+  tst/blanchet-strandmax.tst tst/ugo.scm tst/ugo.tst   coq/Sem_tactics.v coq/Comp.v coq/Alt_sem.v coq/Match.v coq/Alg.v   coq/Exec.v coq/Intro.v coq/Nonce.v coq/Preamble.v   coq/Unilateral_proof.v coq/Makefile coq/Run.v coq/procdoc.tex
doc/cpsa4manual.pdf view

binary file changed (1186650 → 1066017 bytes)

doc/src/cpsa4manual/algebra.tex view
@@ -129,8 +129,8 @@ Will {\cpsa} find this attack?  See \texttt{kerb.xhtml} for the results of the analysis for the point-of-view skeleton described in Figure~\ref{fig:kerb-flawed-pov}.  Note the use of-\texttt{defstrandmax}; this is a shortcut you can use in \cpsa to-specify a full-height instance of a role.+\texttt{defstrandmax}\ttindex{defstrandmax}; this is a shortcut you+can use in {\cpsa} to specify a full-height instance of a role.  \begin{figure} \centering
doc/src/cpsa4manual/cpsa4manual.tex view
@@ -94,8 +94,9 @@  \printindex -\newpage-\includepdf[angle=90]{CPSA_cribsheet}+% The cribsheet needs to be updated to show CPSA4 syntax.+% \newpage+% \includepdf[angle=90]{CPSA_cribsheet}  \end{document}
doc/src/macros.tex view
@@ -1,5 +1,5 @@ \newcommand{\cpsa}{\textsc{cpsa}}-\newcommand{\version}{4.4.1}+\newcommand{\version}{4.4.2} \newcommand{\cpsacopying}{\begingroup   \renewcommand{\thefootnote}{}\footnotetext{{\copyright} 2010 The     MITRE Corporation.  Permission to copy without fee all or part of
src/CPSA/Algebra.hs view
@@ -712,7 +712,8 @@ isAtom :: Term -> Bool isAtom (F Base _) = False isAtom (F s _) = varSym s-isAtom (G x) = isBasisVar x+isAtom (G x) = isBasisVar x     -- NOT:  isGroupVar x.  Used for nons+                                -- and uniqs  isAtom _ = False  -- Is the term numeric?@@ -740,7 +741,7 @@   any (subterm t) u subterm (I x) (G t') =   M.member x t'-subterm (G t) (G t') | isBasisVar t = -- For constituent+subterm (G t) (G t') | isBasisVar t = -- For constituent.  COULD ALSO BE :  isGroupVar   M.member (getGroupVar t) t' subterm _ _ = False
src/CPSA/Graph/Preskeleton.hs view
@@ -51,7 +51,8 @@ -- Ignore channels for message equality test msgEquiv :: SExpr Pos -> SExpr Pos -> Bool msgEquiv src dest | src == dest = True-msgEquiv (L _ [_, _, src]) (L _ [_, _, dest]) = src == dest+msgEquiv (L _ [S _ ch_src, _, src]) (L _ [S _ ch_dst, _, dest])+    | ch_src == "ch-msg" && ch_dst == "ch-msg" = src == dest msgEquiv _ _ = False  -- Add a strand node
src/CPSA/Loader.hs view
@@ -634,6 +634,63 @@     | otherwise = badKey keys xs badKey _ _ = return () +-- Given a list of events, and a list of vars, check that the vars in+-- the Group sorts (rndxs and expts) have the following properties:+--+-- 1.  If the earliest occurrence of a rndx is an In event, that's a+-- state node, ie a load.++-- IMPORTANT:  For now we will not enforce this.  It seems disruptive+-- to examples that use this for certified long-term values,+-- tst/dhcr_um{3,x}.scm, for example.++-- 2.  If the earliest occurrence of a group var is in an In event,+-- then the group var does not *originate* in a later event.  Ie its+-- earliest *carried* occurrence will not be a later transmission.  ++-- 3.  If the earliest occurrence of a group var is an Out event, that+-- must be an rndx.++badGroupMemberOccurrences :: [Term] -> Trace -> Maybe ([Term], Int) +badGroupMemberOccurrences vars events =+    loop groupVars events 0    +    where+      groupVars = filter isVarExpr vars+      usedAndRemaining e = L.partition (flip occursIn $ evtTerm e)++      checkGroupVar (Out _) v = isRndx v+      -- See IMPORTANT note above+      checkGroupVar (In (Plain _)) v = not (isRndx v) || True +      checkGroupVar (In (ChMsg c _)) v = not (isRndx v) || isLocn c || True++      loop _ [] _ = Nothing +      loop gvs (e : evts) i =+          let (fsts,rest) = usedAndRemaining e gvs in+          case L.filter (not . checkGroupVar e) fsts of+            [] -> loop rest evts (i+1) +            bad -> Just (bad,i) ++badOrigNotGen :: [Term] -> Trace -> [(Term,Int)]+badOrigNotGen vars events =+    foldr+    (\v soFar -> case recvButOrig v events of+                   Nothing -> soFar+                   Just p -> (v,p) : soFar) [] groupVars +    where+      groupVars = filter isVarExpr vars+      recvButOrig v c =+          if (originates v c &&   -- first carried outbound +              not(generates v c)) -- first occurs inbound +          then +              firstOccursPos v c+          else+              Nothing ++              +    +++ loadTrace :: MonadFail m => Sig -> Gen -> [Term] ->              [SExpr Pos] -> m (Gen, [Term], [Term], PreRules, Trace) loadTrace sig gen vars xs =@@ -643,11 +700,22 @@                     -> Trace -> [SExpr Pos]                     -> m (Gen, [Term], [Term], PreRules, Trace)       loadTraceLoop gen newVars uniqs pr events [] =-          return (gen, (vars ++ (reverse newVars)), (reverse uniqs), pr,-                  (reverse events))+          let events' = reverse events in +          case badGroupMemberOccurrences vars events' of+            Nothing ->+                case badOrigNotGen vars events' of+                  [] -> return (gen, (vars ++ (reverse newVars)),+                                       (reverse uniqs), pr, events')+                  (v,p) : _ ->+                      fail (shows xs $ " Var received non-carried, the sent carried:  " +++                                      (show v) ++ " at event " ++ (show p))+            Just (_,i) ->+                fail (shows xs $ " Expts must first be received, rndxs first sent:  " +++                                " at event " ++ (show i))       loadTraceLoop gen newVars uniqs pr events ((L _ [S _ "recv", t]) : rest) =           do-            t <- loadTerm sig vars True t+            t <- loadTerm sig vars -- True+                 False t             loadTraceLoop gen newVars uniqs pr ((In $ Plain t) : events) rest       loadTraceLoop gen newVars uniqs pr events ((L _ [S _ "send", t]) : rest) =           do@@ -656,7 +724,8 @@       loadTraceLoop gen newVars uniqs pr events ((L _ [S _ "recv", ch, t]) : rest) =           do             ch <- loadChan sig vars ch-            t <- loadTerm sig vars True t+            t <- loadTerm sig vars -- True+                 False t             loadTraceLoop gen newVars uniqs pr ((In $ ChMsg ch t) : events) rest       loadTraceLoop gen newVars uniqs pr events ((L _ [S _ "send", ch, t]) : rest) =           do@@ -666,7 +735,8 @@       loadTraceLoop gen newVars uniqs pr events ((L _ [S pos "load", ch, t]) : rest) =           do             ch <- loadLocn sig vars ch-            t <- loadTerm sig vars True t+            t <- loadTerm sig vars -- True+                 False t             (gen, pt, pt_t) <- loadLocnTerm sig gen (S pos "pt") (S pos "pval") t             loadTraceLoop gen (pt : newVars) uniqs pr                               ((In $ ChMsg ch pt_t) : events) rest@@ -829,6 +899,14 @@             loadInsts sig top p kvars gen (i : insts) xs       _ ->           fail (shows pos "Malformed defstrand")+loadInsts sig top p kvars gen insts (L pos (S _ "defstrandmax" : x) : xs) =+    case x of+      S _ role : env ->+          do+            (gen, i) <- loadInstMax sig pos p kvars gen role env+            loadInsts sig top p kvars gen (i : insts) xs+      _ ->+          fail (shows pos "Malformed defstrandmax") loadInsts sig top p kvars gen insts (L pos (S _ "deflistener" : x) : xs) =     case x of       [term] ->@@ -881,6 +959,17 @@               (gen', env') <- foldM (loadMaplet sig kvars vars)                               (gen, emptyEnv) env               return (mkInstance gen' r env' height)++loadInstMax :: MonadFail m => Sig -> Pos -> Prot -> [Term] -> Gen -> String ->+               [SExpr Pos] -> m (Gen, Instance)+loadInstMax sig pos p kvars gen role env =+    do+      r <- lookupRole pos p role+      let height = length (rtrace r) +      let vars = rvars r+      (gen', env') <- foldM (loadMaplet sig kvars vars)+                      (gen, emptyEnv) env+      return (mkInstance gen' r env' height)  loadMaplet :: MonadFail m => Sig -> [Term] -> [Term] ->               (Gen, Env) -> SExpr Pos -> m (Gen, Env)
src/CPSA/Protocol.hs view
@@ -8,7 +8,7 @@  module CPSA.Protocol (Event (..), evtCm, evtTerm, evtChan, evtMap, evt,     inbnd, outbnd, Trace, tterms, originates, originationPos,-    generates, generationPos,+    generates, generationPos, firstOccursPos,      acquiredPos, gainedPos, genGainedPos, usedPos, insPrecedeOuts,     Role, rname, rvars, rtrace, rnon, rpnon, runique, runiqgen, rabsent,     rconf, rauth, rcomment, rsearch, rnorig, rpnorig, ruorig, rugen, rabs,@@ -178,6 +178,27 @@       loop pos (In t' : c)           | test t (cmTerm t') ||             testMaybe maybeInv (cmTerm t') = Nothing -- Term does not generate+          | otherwise = loop (pos + 1) c++firstOccursPos :: Term -> Trace -> Maybe Int+firstOccursPos t c =+    loop 0 c+    where+      maybeInv = invertKey t++      testMaybe Nothing _ = False+      testMaybe (Just tInv) ct = tInv `occursIn` ct+      test t ct = t `occursIn` ct++      loop _ [] = Nothing       -- Term does not occur+      loop pos (Out t' : c)+          | test t (cmTerm t') ||+            testMaybe maybeInv (cmTerm t') = Just pos -- Found it+          | otherwise = loop (pos + 1) c+      loop pos (In t' : c)+          | test t (cmTerm t') ||+            testMaybe maybeInv (cmTerm t') = Just pos -- Found it+                                                      -- incoming            | otherwise = loop (pos + 1) c  -- At what position is a term acquired in a trace?
tst/DH_hack.tst view
@@ -1,6 +1,6 @@ (herald "DH Hack" (bound 15)) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/DH_hack.scm") (comment "Strand count bounded at 15")
tst/ab.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/ab.scm")  (defprotocol ab basic
tst/abc.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/abc.scm")  (defprotocol abc basic
tst/aik.tst view
@@ -1,6 +1,6 @@ (herald "Anonymous identity protocol from TCG") -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/aik.scm")  (defprotocol aikprot basic
tst/atomic-open-closed.tst view
@@ -1,6 +1,6 @@ (herald atomic-open-closed (bound 44)) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/atomic-open-closed.scm") (comment "Strand count bounded at 44")
tst/attest.tst view
@@ -1,6 +1,6 @@ (herald attest-door) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/attest.scm")  (defprotocol attest-door basic
tst/auth-enc.tst view
@@ -1,6 +1,6 @@ (herald auth-enc) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/auth-enc.scm")  (defprotocol auth-enc basic
tst/auth-hash.tst view
@@ -1,6 +1,6 @@ (herald auth-hash) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/auth-hash.scm")  (defprotocol auth-hash basic
+ tst/blanchet-strandmax.scm view
@@ -0,0 +1,131 @@+(herald "Blanchet's Simple Example Protocol (strand max)"+  (comment "There is a flaw in this protocol by design"))++(defprotocol blanchet-max basic+  (defrole init+    (vars (a b name) (s skey) (d data))+    (trace+     (send (enc (enc s (privk a)) (pubk b)))+     (recv (enc d s))))+  (defrole resp+    (vars (a b name) (s skey) (d data))+    (trace+     (recv (enc (enc s (privk a)) (pubk b)))+     (send (enc d s))))+  (comment "Blanchet's protocol using named asymmetric keys"))++(defskeleton blanchet-max+  (vars (a b name) (s skey) (d data))+  (defstrandmax init (a a) (b b) (s s) (d d))+  (non-orig (privk b))+  (uniq-orig s)+  (comment "Analyze from the initiator's perspective"))++(defskeleton blanchet-max+  (vars (a b name) (s skey) (d data))+  (defstrandmax init (a a) (b b) (s s) (d d))+  (deflistener d)+  (non-orig (privk b))+  (uniq-orig s d)+  (comment "From the initiator's perspective, is the secret leaked?"))++(defskeleton blanchet-max+  (vars (a b name) (s skey) (d data))+  (defstrandmax resp (a a) (b b) (s s) (d d))+  (non-orig (privk a) (privk b))+  (uniq-orig s)+  (comment "Analyze from the responder's perspective"))++(defskeleton blanchet-max+  (vars (a b name) (s skey) (d data))+  (defstrandmax resp (a a) (b b) (s s) (d d))+  (deflistener d)+  (non-orig (privk a) (privk b))+  (uniq-orig s d)+  (comment "From the responders's perspective, is the secret leaked?"))++(defprotocol blanchet-max-akey basic+  (defrole init+    (vars (a b akey) (s skey) (d data))+    (trace+     (send (enc (enc s (invk a)) b))+     (recv (enc d s))))+  (defrole resp+    (vars (a b akey) (s skey) (d data))+    (trace+     (recv (enc (enc s (invk a)) b))+     (send (enc d s))))+  (comment "Blanchet's protocol using unnamed asymmetric keys"))++(defskeleton blanchet-max-akey+  (vars (a b akey) (s skey) (d data))+  (defstrand init 2 (a a) (b b) (s s) (d d))+  (non-orig (invk b))+  (uniq-orig s)+  (comment "Analyze from the initiator's perspective"))++(defskeleton blanchet-max-akey+  (vars (a b akey) (s skey) (d data))+  (defstrand init 2 (a a) (b b) (s s) (d d))+  (deflistener d)+  (non-orig (invk b))+  (uniq-orig s d)+  (comment "From the initiator's perspective, is the secret leaked?"))++(defskeleton blanchet-max-akey+  (vars (a b akey) (s skey) (d data))+  (defstrand resp 2 (a a) (b b) (s s) (d d))+  (non-orig (invk a) (invk b))+  (uniq-orig s)+  (comment "Analyze from the responder's perspective"))++(defskeleton blanchet-max-akey+  (vars (a b akey) (s skey) (d data))+  (defstrand resp 2 (a a) (b b) (s s) (d d))+  (deflistener d)+  (non-orig (invk a) (invk b))+  (uniq-orig s d)+  (comment "From the responders's perspective, is the secret leaked?"))++(defprotocol blanchet-max-fixed basic+  (defrole init+    (vars (a b name) (s skey) (d data))+    (trace+     (send (enc (enc s b (privk a)) (pubk b)))+     (recv (enc d s))))+  (defrole resp+    (vars (a b name) (s skey) (d data))+    (trace+     (recv (enc (enc s b (privk a)) (pubk b)))+     (send (enc d s))))+  (comment "Fixed Blanchet's protocol using named asymmetric keys"))++(defskeleton blanchet-max-fixed+  (vars (a b name) (s skey) (d data))+  (defstrand init 2 (a a) (b b) (s s) (d d))+  (non-orig (privk b))+  (uniq-orig s)+  (comment "Analyze from the initiator's perspective"))++(defskeleton blanchet-max-fixed+  (vars (a b name) (s skey) (d data))+  (defstrand init 2 (a a) (b b) (s s) (d d))+  (deflistener d)+  (non-orig (privk b))+  (uniq-orig s d)+  (comment "From the initiator's perspective, is the secret leaked?"))++(defskeleton blanchet-max-fixed+  (vars (a b name) (s skey) (d data))+  (defstrand resp 2 (a a) (b b) (s s) (d d))+  (non-orig (privk a) (privk b))+  (uniq-orig s)+  (comment "Analyze from the responder's perspective"))++(defskeleton blanchet-max-fixed+  (vars (a b name) (s skey) (d data))+  (defstrand resp 2 (a a) (b b) (s s) (d d))+  (deflistener d)+  (non-orig (privk a) (privk b))+  (uniq-orig s d)+  (comment "From the responders's perspective, is the secret leaked?"))
+ tst/blanchet-strandmax.tst view
@@ -0,0 +1,907 @@+(herald "Blanchet's Simple Example Protocol (strand max)"+  (comment "There is a flaw in this protocol by design"))++(comment "CPSA 4.4.2")+(comment "All input read from tst/blanchet-strandmax.scm")++(defprotocol blanchet-max basic+  (defrole init+    (vars (a b name) (s skey) (d data))+    (trace (send (enc (enc s (privk a)) (pubk b))) (recv (enc d s))))+  (defrole resp+    (vars (a b name) (s skey) (d data))+    (trace (recv (enc (enc s (privk a)) (pubk b))) (send (enc d s))))+  (defgenrule neqRl_indx+    (forall ((x indx)) (implies (fact neq x x) (false))))+  (defgenrule neqRl_strd+    (forall ((x strd)) (implies (fact neq x x) (false))))+  (defgenrule neqRl_mesg+    (forall ((x mesg)) (implies (fact neq x x) (false))))+  (comment "Blanchet's protocol using named asymmetric keys"))++(defskeleton blanchet-max+  (vars (d data) (s skey) (a b name))+  (defstrand init 2 (d d) (s s) (a a) (b b))+  (non-orig (privk b))+  (uniq-orig s)+  (comment "Analyze from the initiator's perspective")+  (traces ((send (enc (enc s (privk a)) (pubk b))) (recv (enc d s))))+  (label 0)+  (unrealized (0 1))+  (origs (s (0 0)))+  (comment "2 in cohort - 2 not yet seen"))++(defskeleton blanchet-max+  (vars (d data) (s skey) (a b a-0 b-0 name))+  (defstrand init 2 (d d) (s s) (a a) (b b))+  (defstrand resp 2 (d d) (s s) (a a-0) (b b-0))+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (privk b))+  (uniq-orig s)+  (operation encryption-test (added-strand resp 2) (enc d s) (0 1))+  (traces ((send (enc (enc s (privk a)) (pubk b))) (recv (enc d s)))+    ((recv (enc (enc s (privk a-0)) (pubk b-0))) (send (enc d s))))+  (label 1)+  (parent 0)+  (unrealized (1 0))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton blanchet-max+  (vars (d data) (s skey) (a b name))+  (defstrand init 2 (d d) (s s) (a a) (b b))+  (deflistener s)+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (privk b))+  (uniq-orig s)+  (operation encryption-test (added-listener s) (enc d s) (0 1))+  (traces ((send (enc (enc s (privk a)) (pubk b))) (recv (enc d s)))+    ((recv s) (send s)))+  (label 2)+  (parent 0)+  (unrealized (1 0))+  (dead)+  (comment "empty cohort"))++(defskeleton blanchet-max+  (vars (d data) (s skey) (a b name))+  (defstrand init 2 (d d) (s s) (a a) (b b))+  (defstrand resp 2 (d d) (s s) (a a) (b b))+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (privk b))+  (uniq-orig s)+  (operation nonce-test (contracted (a-0 a) (b-0 b)) s (1 0)+    (enc (enc s (privk a)) (pubk b)))+  (traces ((send (enc (enc s (privk a)) (pubk b))) (recv (enc d s)))+    ((recv (enc (enc s (privk a)) (pubk b))) (send (enc d s))))+  (label 3)+  (parent 1)+  (realized)+  (shape)+  (maps ((0) ((a a) (b b) (s s) (d d))))+  (origs (s (0 0))))++(comment "Nothing left to do")++(defprotocol blanchet-max basic+  (defrole init+    (vars (a b name) (s skey) (d data))+    (trace (send (enc (enc s (privk a)) (pubk b))) (recv (enc d s))))+  (defrole resp+    (vars (a b name) (s skey) (d data))+    (trace (recv (enc (enc s (privk a)) (pubk b))) (send (enc d s))))+  (defgenrule neqRl_indx+    (forall ((x indx)) (implies (fact neq x x) (false))))+  (defgenrule neqRl_strd+    (forall ((x strd)) (implies (fact neq x x) (false))))+  (defgenrule neqRl_mesg+    (forall ((x mesg)) (implies (fact neq x x) (false))))+  (comment "Blanchet's protocol using named asymmetric keys"))++(defskeleton blanchet-max+  (vars (d data) (s skey) (a b name))+  (defstrand init 2 (d d) (s s) (a a) (b b))+  (deflistener d)+  (non-orig (privk b))+  (uniq-orig d s)+  (comment "From the initiator's perspective, is the secret leaked?")+  (traces ((send (enc (enc s (privk a)) (pubk b))) (recv (enc d s)))+    ((recv d) (send d)))+  (label 4)+  (unrealized (0 1))+  (origs (s (0 0)))+  (comment "2 in cohort - 2 not yet seen"))++(defskeleton blanchet-max+  (vars (d data) (s skey) (a b a-0 b-0 name))+  (defstrand init 2 (d d) (s s) (a a) (b b))+  (deflistener d)+  (defstrand resp 2 (d d) (s s) (a a-0) (b b-0))+  (precedes ((0 0) (2 0)) ((2 1) (0 1)) ((2 1) (1 0)))+  (non-orig (privk b))+  (uniq-orig d s)+  (operation encryption-test (added-strand resp 2) (enc d s) (0 1))+  (traces ((send (enc (enc s (privk a)) (pubk b))) (recv (enc d s)))+    ((recv d) (send d))+    ((recv (enc (enc s (privk a-0)) (pubk b-0))) (send (enc d s))))+  (label 5)+  (parent 4)+  (unrealized (1 0) (2 0))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton blanchet-max+  (vars (d data) (s skey) (a b name))+  (defstrand init 2 (d d) (s s) (a a) (b b))+  (deflistener d)+  (deflistener s)+  (precedes ((0 0) (2 0)) ((2 1) (0 1)))+  (non-orig (privk b))+  (uniq-orig d s)+  (operation encryption-test (added-listener s) (enc d s) (0 1))+  (traces ((send (enc (enc s (privk a)) (pubk b))) (recv (enc d s)))+    ((recv d) (send d)) ((recv s) (send s)))+  (label 6)+  (parent 4)+  (unrealized (2 0))+  (dead)+  (comment "empty cohort"))++(defskeleton blanchet-max+  (vars (d data) (s skey) (a b name))+  (defstrand init 2 (d d) (s s) (a a) (b b))+  (deflistener d)+  (defstrand resp 2 (d d) (s s) (a a) (b b))+  (precedes ((0 0) (2 0)) ((2 1) (0 1)) ((2 1) (1 0)))+  (non-orig (privk b))+  (uniq-orig d s)+  (operation nonce-test (contracted (a-0 a) (b-0 b)) s (2 0)+    (enc (enc s (privk a)) (pubk b)))+  (traces ((send (enc (enc s (privk a)) (pubk b))) (recv (enc d s)))+    ((recv d) (send d))+    ((recv (enc (enc s (privk a)) (pubk b))) (send (enc d s))))+  (label 7)+  (parent 5)+  (unrealized (1 0))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton blanchet-max+  (vars (d data) (s skey) (a b name))+  (defstrand init 2 (d d) (s s) (a a) (b b))+  (deflistener d)+  (defstrand resp 2 (d d) (s s) (a a) (b b))+  (deflistener s)+  (precedes ((0 0) (2 0)) ((0 0) (3 0)) ((2 1) (0 1)) ((2 1) (1 0))+    ((3 1) (1 0)))+  (non-orig (privk b))+  (uniq-orig d s)+  (operation nonce-test (added-listener s) d (1 0) (enc d s))+  (traces ((send (enc (enc s (privk a)) (pubk b))) (recv (enc d s)))+    ((recv d) (send d))+    ((recv (enc (enc s (privk a)) (pubk b))) (send (enc d s)))+    ((recv s) (send s)))+  (label 8)+  (parent 7)+  (unrealized (3 0))+  (dead)+  (comment "empty cohort"))++(comment "Nothing left to do")++(defprotocol blanchet-max basic+  (defrole init+    (vars (a b name) (s skey) (d data))+    (trace (send (enc (enc s (privk a)) (pubk b))) (recv (enc d s))))+  (defrole resp+    (vars (a b name) (s skey) (d data))+    (trace (recv (enc (enc s (privk a)) (pubk b))) (send (enc d s))))+  (defgenrule neqRl_indx+    (forall ((x indx)) (implies (fact neq x x) (false))))+  (defgenrule neqRl_strd+    (forall ((x strd)) (implies (fact neq x x) (false))))+  (defgenrule neqRl_mesg+    (forall ((x mesg)) (implies (fact neq x x) (false))))+  (comment "Blanchet's protocol using named asymmetric keys"))++(defskeleton blanchet-max+  (vars (d data) (s skey) (a b name))+  (defstrand resp 2 (d d) (s s) (a a) (b b))+  (non-orig (privk a) (privk b))+  (uniq-orig s)+  (comment "Analyze from the responder's perspective")+  (traces ((recv (enc (enc s (privk a)) (pubk b))) (send (enc d s))))+  (label 9)+  (unrealized (0 0))+  (origs)+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton blanchet-max+  (vars (d data) (s skey) (a b b-0 name))+  (defstrand resp 2 (d d) (s s) (a a) (b b))+  (defstrand init 1 (s s) (a a) (b b-0))+  (precedes ((1 0) (0 0)))+  (non-orig (privk a) (privk b))+  (uniq-orig s)+  (operation encryption-test (added-strand init 1) (enc s (privk a))+    (0 0))+  (traces ((recv (enc (enc s (privk a)) (pubk b))) (send (enc d s)))+    ((send (enc (enc s (privk a)) (pubk b-0)))))+  (label 10)+  (parent 9)+  (realized)+  (shape)+  (maps ((0) ((a a) (b b) (s s) (d d))))+  (origs (s (1 0))))++(comment "Nothing left to do")++(defprotocol blanchet-max basic+  (defrole init+    (vars (a b name) (s skey) (d data))+    (trace (send (enc (enc s (privk a)) (pubk b))) (recv (enc d s))))+  (defrole resp+    (vars (a b name) (s skey) (d data))+    (trace (recv (enc (enc s (privk a)) (pubk b))) (send (enc d s))))+  (defgenrule neqRl_indx+    (forall ((x indx)) (implies (fact neq x x) (false))))+  (defgenrule neqRl_strd+    (forall ((x strd)) (implies (fact neq x x) (false))))+  (defgenrule neqRl_mesg+    (forall ((x mesg)) (implies (fact neq x x) (false))))+  (comment "Blanchet's protocol using named asymmetric keys"))++(defskeleton blanchet-max+  (vars (d data) (s skey) (a b name))+  (defstrand resp 2 (d d) (s s) (a a) (b b))+  (deflistener d)+  (non-orig (privk a) (privk b))+  (uniq-orig d s)+  (comment "From the responders's perspective, is the secret leaked?")+  (traces ((recv (enc (enc s (privk a)) (pubk b))) (send (enc d s)))+    ((recv d) (send d)))+  (label 11)+  (unrealized (0 0) (1 0))+  (preskeleton)+  (origs (d (0 1)))+  (comment "Not a skeleton"))++(defskeleton blanchet-max+  (vars (d data) (s skey) (a b name))+  (defstrand resp 2 (d d) (s s) (a a) (b b))+  (deflistener d)+  (precedes ((0 1) (1 0)))+  (non-orig (privk a) (privk b))+  (uniq-orig d s)+  (traces ((recv (enc (enc s (privk a)) (pubk b))) (send (enc d s)))+    ((recv d) (send d)))+  (label 12)+  (parent 11)+  (unrealized (0 0))+  (origs (d (0 1)))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton blanchet-max+  (vars (d data) (s skey) (a b b-0 name))+  (defstrand resp 2 (d d) (s s) (a a) (b b))+  (deflistener d)+  (defstrand init 1 (s s) (a a) (b b-0))+  (precedes ((0 1) (1 0)) ((2 0) (0 0)))+  (non-orig (privk a) (privk b))+  (uniq-orig d s)+  (operation encryption-test (added-strand init 1) (enc s (privk a))+    (0 0))+  (traces ((recv (enc (enc s (privk a)) (pubk b))) (send (enc d s)))+    ((recv d) (send d)) ((send (enc (enc s (privk a)) (pubk b-0)))))+  (label 13)+  (parent 12)+  (realized)+  (shape)+  (maps ((0 1) ((a a) (b b) (s s) (d d))))+  (origs (s (2 0)) (d (0 1))))++(comment "Nothing left to do")++(defprotocol blanchet-max-akey basic+  (defrole init+    (vars (a b akey) (s skey) (d data))+    (trace (send (enc (enc s (invk a)) b)) (recv (enc d s))))+  (defrole resp+    (vars (a b akey) (s skey) (d data))+    (trace (recv (enc (enc s (invk a)) b)) (send (enc d s))))+  (defgenrule neqRl_indx+    (forall ((x indx)) (implies (fact neq x x) (false))))+  (defgenrule neqRl_strd+    (forall ((x strd)) (implies (fact neq x x) (false))))+  (defgenrule neqRl_mesg+    (forall ((x mesg)) (implies (fact neq x x) (false))))+  (comment "Blanchet's protocol using unnamed asymmetric keys"))++(defskeleton blanchet-max-akey+  (vars (d data) (s skey) (a b akey))+  (defstrand init 2 (d d) (s s) (a a) (b b))+  (non-orig (invk b))+  (uniq-orig s)+  (comment "Analyze from the initiator's perspective")+  (traces ((send (enc (enc s (invk a)) b)) (recv (enc d s))))+  (label 14)+  (unrealized (0 1))+  (origs (s (0 0)))+  (comment "2 in cohort - 2 not yet seen"))++(defskeleton blanchet-max-akey+  (vars (d data) (s skey) (a b a-0 b-0 akey))+  (defstrand init 2 (d d) (s s) (a a) (b b))+  (defstrand resp 2 (d d) (s s) (a a-0) (b b-0))+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (invk b))+  (uniq-orig s)+  (operation encryption-test (added-strand resp 2) (enc d s) (0 1))+  (traces ((send (enc (enc s (invk a)) b)) (recv (enc d s)))+    ((recv (enc (enc s (invk a-0)) b-0)) (send (enc d s))))+  (label 15)+  (parent 14)+  (unrealized (1 0))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton blanchet-max-akey+  (vars (d data) (s skey) (a b akey))+  (defstrand init 2 (d d) (s s) (a a) (b b))+  (deflistener s)+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (invk b))+  (uniq-orig s)+  (operation encryption-test (added-listener s) (enc d s) (0 1))+  (traces ((send (enc (enc s (invk a)) b)) (recv (enc d s)))+    ((recv s) (send s)))+  (label 16)+  (parent 14)+  (unrealized (1 0))+  (dead)+  (comment "empty cohort"))++(defskeleton blanchet-max-akey+  (vars (d data) (s skey) (a b akey))+  (defstrand init 2 (d d) (s s) (a a) (b b))+  (defstrand resp 2 (d d) (s s) (a a) (b b))+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (invk b))+  (uniq-orig s)+  (operation nonce-test (contracted (a-0 a) (b-0 b)) s (1 0)+    (enc (enc s (invk a)) b))+  (traces ((send (enc (enc s (invk a)) b)) (recv (enc d s)))+    ((recv (enc (enc s (invk a)) b)) (send (enc d s))))+  (label 17)+  (parent 15)+  (realized)+  (shape)+  (maps ((0) ((a a) (b b) (s s) (d d))))+  (origs (s (0 0))))++(comment "Nothing left to do")++(defprotocol blanchet-max-akey basic+  (defrole init+    (vars (a b akey) (s skey) (d data))+    (trace (send (enc (enc s (invk a)) b)) (recv (enc d s))))+  (defrole resp+    (vars (a b akey) (s skey) (d data))+    (trace (recv (enc (enc s (invk a)) b)) (send (enc d s))))+  (defgenrule neqRl_indx+    (forall ((x indx)) (implies (fact neq x x) (false))))+  (defgenrule neqRl_strd+    (forall ((x strd)) (implies (fact neq x x) (false))))+  (defgenrule neqRl_mesg+    (forall ((x mesg)) (implies (fact neq x x) (false))))+  (comment "Blanchet's protocol using unnamed asymmetric keys"))++(defskeleton blanchet-max-akey+  (vars (d data) (s skey) (a b akey))+  (defstrand init 2 (d d) (s s) (a a) (b b))+  (deflistener d)+  (non-orig (invk b))+  (uniq-orig d s)+  (comment "From the initiator's perspective, is the secret leaked?")+  (traces ((send (enc (enc s (invk a)) b)) (recv (enc d s)))+    ((recv d) (send d)))+  (label 18)+  (unrealized (0 1))+  (origs (s (0 0)))+  (comment "2 in cohort - 2 not yet seen"))++(defskeleton blanchet-max-akey+  (vars (d data) (s skey) (a b a-0 b-0 akey))+  (defstrand init 2 (d d) (s s) (a a) (b b))+  (deflistener d)+  (defstrand resp 2 (d d) (s s) (a a-0) (b b-0))+  (precedes ((0 0) (2 0)) ((2 1) (0 1)) ((2 1) (1 0)))+  (non-orig (invk b))+  (uniq-orig d s)+  (operation encryption-test (added-strand resp 2) (enc d s) (0 1))+  (traces ((send (enc (enc s (invk a)) b)) (recv (enc d s)))+    ((recv d) (send d))+    ((recv (enc (enc s (invk a-0)) b-0)) (send (enc d s))))+  (label 19)+  (parent 18)+  (unrealized (1 0) (2 0))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton blanchet-max-akey+  (vars (d data) (s skey) (a b akey))+  (defstrand init 2 (d d) (s s) (a a) (b b))+  (deflistener d)+  (deflistener s)+  (precedes ((0 0) (2 0)) ((2 1) (0 1)))+  (non-orig (invk b))+  (uniq-orig d s)+  (operation encryption-test (added-listener s) (enc d s) (0 1))+  (traces ((send (enc (enc s (invk a)) b)) (recv (enc d s)))+    ((recv d) (send d)) ((recv s) (send s)))+  (label 20)+  (parent 18)+  (unrealized (2 0))+  (dead)+  (comment "empty cohort"))++(defskeleton blanchet-max-akey+  (vars (d data) (s skey) (a b akey))+  (defstrand init 2 (d d) (s s) (a a) (b b))+  (deflistener d)+  (defstrand resp 2 (d d) (s s) (a a) (b b))+  (precedes ((0 0) (2 0)) ((2 1) (0 1)) ((2 1) (1 0)))+  (non-orig (invk b))+  (uniq-orig d s)+  (operation nonce-test (contracted (a-0 a) (b-0 b)) s (2 0)+    (enc (enc s (invk a)) b))+  (traces ((send (enc (enc s (invk a)) b)) (recv (enc d s)))+    ((recv d) (send d))+    ((recv (enc (enc s (invk a)) b)) (send (enc d s))))+  (label 21)+  (parent 19)+  (unrealized (1 0))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton blanchet-max-akey+  (vars (d data) (s skey) (a b akey))+  (defstrand init 2 (d d) (s s) (a a) (b b))+  (deflistener d)+  (defstrand resp 2 (d d) (s s) (a a) (b b))+  (deflistener s)+  (precedes ((0 0) (2 0)) ((0 0) (3 0)) ((2 1) (0 1)) ((2 1) (1 0))+    ((3 1) (1 0)))+  (non-orig (invk b))+  (uniq-orig d s)+  (operation nonce-test (added-listener s) d (1 0) (enc d s))+  (traces ((send (enc (enc s (invk a)) b)) (recv (enc d s)))+    ((recv d) (send d))+    ((recv (enc (enc s (invk a)) b)) (send (enc d s)))+    ((recv s) (send s)))+  (label 22)+  (parent 21)+  (unrealized (3 0))+  (dead)+  (comment "empty cohort"))++(comment "Nothing left to do")++(defprotocol blanchet-max-akey basic+  (defrole init+    (vars (a b akey) (s skey) (d data))+    (trace (send (enc (enc s (invk a)) b)) (recv (enc d s))))+  (defrole resp+    (vars (a b akey) (s skey) (d data))+    (trace (recv (enc (enc s (invk a)) b)) (send (enc d s))))+  (defgenrule neqRl_indx+    (forall ((x indx)) (implies (fact neq x x) (false))))+  (defgenrule neqRl_strd+    (forall ((x strd)) (implies (fact neq x x) (false))))+  (defgenrule neqRl_mesg+    (forall ((x mesg)) (implies (fact neq x x) (false))))+  (comment "Blanchet's protocol using unnamed asymmetric keys"))++(defskeleton blanchet-max-akey+  (vars (d data) (s skey) (a b akey))+  (defstrand resp 2 (d d) (s s) (a a) (b b))+  (non-orig (invk a) (invk b))+  (uniq-orig s)+  (comment "Analyze from the responder's perspective")+  (traces ((recv (enc (enc s (invk a)) b)) (send (enc d s))))+  (label 23)+  (unrealized (0 0))+  (origs)+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton blanchet-max-akey+  (vars (d data) (s skey) (a b b-0 akey))+  (defstrand resp 2 (d d) (s s) (a a) (b b))+  (defstrand init 1 (s s) (a a) (b b-0))+  (precedes ((1 0) (0 0)))+  (non-orig (invk a) (invk b))+  (uniq-orig s)+  (operation encryption-test (added-strand init 1) (enc s (invk a))+    (0 0))+  (traces ((recv (enc (enc s (invk a)) b)) (send (enc d s)))+    ((send (enc (enc s (invk a)) b-0))))+  (label 24)+  (parent 23)+  (realized)+  (shape)+  (maps ((0) ((a a) (b b) (s s) (d d))))+  (origs (s (1 0))))++(comment "Nothing left to do")++(defprotocol blanchet-max-akey basic+  (defrole init+    (vars (a b akey) (s skey) (d data))+    (trace (send (enc (enc s (invk a)) b)) (recv (enc d s))))+  (defrole resp+    (vars (a b akey) (s skey) (d data))+    (trace (recv (enc (enc s (invk a)) b)) (send (enc d s))))+  (defgenrule neqRl_indx+    (forall ((x indx)) (implies (fact neq x x) (false))))+  (defgenrule neqRl_strd+    (forall ((x strd)) (implies (fact neq x x) (false))))+  (defgenrule neqRl_mesg+    (forall ((x mesg)) (implies (fact neq x x) (false))))+  (comment "Blanchet's protocol using unnamed asymmetric keys"))++(defskeleton blanchet-max-akey+  (vars (d data) (s skey) (a b akey))+  (defstrand resp 2 (d d) (s s) (a a) (b b))+  (deflistener d)+  (non-orig (invk a) (invk b))+  (uniq-orig d s)+  (comment "From the responders's perspective, is the secret leaked?")+  (traces ((recv (enc (enc s (invk a)) b)) (send (enc d s)))+    ((recv d) (send d)))+  (label 25)+  (unrealized (0 0) (1 0))+  (preskeleton)+  (origs (d (0 1)))+  (comment "Not a skeleton"))++(defskeleton blanchet-max-akey+  (vars (d data) (s skey) (a b akey))+  (defstrand resp 2 (d d) (s s) (a a) (b b))+  (deflistener d)+  (precedes ((0 1) (1 0)))+  (non-orig (invk a) (invk b))+  (uniq-orig d s)+  (traces ((recv (enc (enc s (invk a)) b)) (send (enc d s)))+    ((recv d) (send d)))+  (label 26)+  (parent 25)+  (unrealized (0 0))+  (origs (d (0 1)))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton blanchet-max-akey+  (vars (d data) (s skey) (a b b-0 akey))+  (defstrand resp 2 (d d) (s s) (a a) (b b))+  (deflistener d)+  (defstrand init 1 (s s) (a a) (b b-0))+  (precedes ((0 1) (1 0)) ((2 0) (0 0)))+  (non-orig (invk a) (invk b))+  (uniq-orig d s)+  (operation encryption-test (added-strand init 1) (enc s (invk a))+    (0 0))+  (traces ((recv (enc (enc s (invk a)) b)) (send (enc d s)))+    ((recv d) (send d)) ((send (enc (enc s (invk a)) b-0))))+  (label 27)+  (parent 26)+  (realized)+  (shape)+  (maps ((0 1) ((a a) (b b) (s s) (d d))))+  (origs (s (2 0)) (d (0 1))))++(comment "Nothing left to do")++(defprotocol blanchet-max-fixed basic+  (defrole init+    (vars (a b name) (s skey) (d data))+    (trace (send (enc (enc s b (privk a)) (pubk b))) (recv (enc d s))))+  (defrole resp+    (vars (a b name) (s skey) (d data))+    (trace (recv (enc (enc s b (privk a)) (pubk b))) (send (enc d s))))+  (defgenrule neqRl_indx+    (forall ((x indx)) (implies (fact neq x x) (false))))+  (defgenrule neqRl_strd+    (forall ((x strd)) (implies (fact neq x x) (false))))+  (defgenrule neqRl_mesg+    (forall ((x mesg)) (implies (fact neq x x) (false))))+  (comment "Fixed Blanchet's protocol using named asymmetric keys"))++(defskeleton blanchet-max-fixed+  (vars (d data) (s skey) (a b name))+  (defstrand init 2 (d d) (s s) (a a) (b b))+  (non-orig (privk b))+  (uniq-orig s)+  (comment "Analyze from the initiator's perspective")+  (traces ((send (enc (enc s b (privk a)) (pubk b))) (recv (enc d s))))+  (label 28)+  (unrealized (0 1))+  (origs (s (0 0)))+  (comment "2 in cohort - 2 not yet seen"))++(defskeleton blanchet-max-fixed+  (vars (d data) (s skey) (a b a-0 b-0 name))+  (defstrand init 2 (d d) (s s) (a a) (b b))+  (defstrand resp 2 (d d) (s s) (a a-0) (b b-0))+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (privk b))+  (uniq-orig s)+  (operation encryption-test (added-strand resp 2) (enc d s) (0 1))+  (traces ((send (enc (enc s b (privk a)) (pubk b))) (recv (enc d s)))+    ((recv (enc (enc s b-0 (privk a-0)) (pubk b-0))) (send (enc d s))))+  (label 29)+  (parent 28)+  (unrealized (1 0))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton blanchet-max-fixed+  (vars (d data) (s skey) (a b name))+  (defstrand init 2 (d d) (s s) (a a) (b b))+  (deflistener s)+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (privk b))+  (uniq-orig s)+  (operation encryption-test (added-listener s) (enc d s) (0 1))+  (traces ((send (enc (enc s b (privk a)) (pubk b))) (recv (enc d s)))+    ((recv s) (send s)))+  (label 30)+  (parent 28)+  (unrealized (1 0))+  (dead)+  (comment "empty cohort"))++(defskeleton blanchet-max-fixed+  (vars (d data) (s skey) (a b name))+  (defstrand init 2 (d d) (s s) (a a) (b b))+  (defstrand resp 2 (d d) (s s) (a a) (b b))+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (privk b))+  (uniq-orig s)+  (operation nonce-test (contracted (a-0 a) (b-0 b)) s (1 0)+    (enc (enc s b (privk a)) (pubk b)))+  (traces ((send (enc (enc s b (privk a)) (pubk b))) (recv (enc d s)))+    ((recv (enc (enc s b (privk a)) (pubk b))) (send (enc d s))))+  (label 31)+  (parent 29)+  (realized)+  (shape)+  (maps ((0) ((a a) (b b) (s s) (d d))))+  (origs (s (0 0))))++(comment "Nothing left to do")++(defprotocol blanchet-max-fixed basic+  (defrole init+    (vars (a b name) (s skey) (d data))+    (trace (send (enc (enc s b (privk a)) (pubk b))) (recv (enc d s))))+  (defrole resp+    (vars (a b name) (s skey) (d data))+    (trace (recv (enc (enc s b (privk a)) (pubk b))) (send (enc d s))))+  (defgenrule neqRl_indx+    (forall ((x indx)) (implies (fact neq x x) (false))))+  (defgenrule neqRl_strd+    (forall ((x strd)) (implies (fact neq x x) (false))))+  (defgenrule neqRl_mesg+    (forall ((x mesg)) (implies (fact neq x x) (false))))+  (comment "Fixed Blanchet's protocol using named asymmetric keys"))++(defskeleton blanchet-max-fixed+  (vars (d data) (s skey) (a b name))+  (defstrand init 2 (d d) (s s) (a a) (b b))+  (deflistener d)+  (non-orig (privk b))+  (uniq-orig d s)+  (comment "From the initiator's perspective, is the secret leaked?")+  (traces ((send (enc (enc s b (privk a)) (pubk b))) (recv (enc d s)))+    ((recv d) (send d)))+  (label 32)+  (unrealized (0 1))+  (origs (s (0 0)))+  (comment "2 in cohort - 2 not yet seen"))++(defskeleton blanchet-max-fixed+  (vars (d data) (s skey) (a b a-0 b-0 name))+  (defstrand init 2 (d d) (s s) (a a) (b b))+  (deflistener d)+  (defstrand resp 2 (d d) (s s) (a a-0) (b b-0))+  (precedes ((0 0) (2 0)) ((2 1) (0 1)) ((2 1) (1 0)))+  (non-orig (privk b))+  (uniq-orig d s)+  (operation encryption-test (added-strand resp 2) (enc d s) (0 1))+  (traces ((send (enc (enc s b (privk a)) (pubk b))) (recv (enc d s)))+    ((recv d) (send d))+    ((recv (enc (enc s b-0 (privk a-0)) (pubk b-0))) (send (enc d s))))+  (label 33)+  (parent 32)+  (unrealized (1 0) (2 0))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton blanchet-max-fixed+  (vars (d data) (s skey) (a b name))+  (defstrand init 2 (d d) (s s) (a a) (b b))+  (deflistener d)+  (deflistener s)+  (precedes ((0 0) (2 0)) ((2 1) (0 1)))+  (non-orig (privk b))+  (uniq-orig d s)+  (operation encryption-test (added-listener s) (enc d s) (0 1))+  (traces ((send (enc (enc s b (privk a)) (pubk b))) (recv (enc d s)))+    ((recv d) (send d)) ((recv s) (send s)))+  (label 34)+  (parent 32)+  (unrealized (2 0))+  (dead)+  (comment "empty cohort"))++(defskeleton blanchet-max-fixed+  (vars (d data) (s skey) (a b name))+  (defstrand init 2 (d d) (s s) (a a) (b b))+  (deflistener d)+  (defstrand resp 2 (d d) (s s) (a a) (b b))+  (precedes ((0 0) (2 0)) ((2 1) (0 1)) ((2 1) (1 0)))+  (non-orig (privk b))+  (uniq-orig d s)+  (operation nonce-test (contracted (a-0 a) (b-0 b)) s (2 0)+    (enc (enc s b (privk a)) (pubk b)))+  (traces ((send (enc (enc s b (privk a)) (pubk b))) (recv (enc d s)))+    ((recv d) (send d))+    ((recv (enc (enc s b (privk a)) (pubk b))) (send (enc d s))))+  (label 35)+  (parent 33)+  (unrealized (1 0))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton blanchet-max-fixed+  (vars (d data) (s skey) (a b name))+  (defstrand init 2 (d d) (s s) (a a) (b b))+  (deflistener d)+  (defstrand resp 2 (d d) (s s) (a a) (b b))+  (deflistener s)+  (precedes ((0 0) (2 0)) ((0 0) (3 0)) ((2 1) (0 1)) ((2 1) (1 0))+    ((3 1) (1 0)))+  (non-orig (privk b))+  (uniq-orig d s)+  (operation nonce-test (added-listener s) d (1 0) (enc d s))+  (traces ((send (enc (enc s b (privk a)) (pubk b))) (recv (enc d s)))+    ((recv d) (send d))+    ((recv (enc (enc s b (privk a)) (pubk b))) (send (enc d s)))+    ((recv s) (send s)))+  (label 36)+  (parent 35)+  (unrealized (3 0))+  (dead)+  (comment "empty cohort"))++(comment "Nothing left to do")++(defprotocol blanchet-max-fixed basic+  (defrole init+    (vars (a b name) (s skey) (d data))+    (trace (send (enc (enc s b (privk a)) (pubk b))) (recv (enc d s))))+  (defrole resp+    (vars (a b name) (s skey) (d data))+    (trace (recv (enc (enc s b (privk a)) (pubk b))) (send (enc d s))))+  (defgenrule neqRl_indx+    (forall ((x indx)) (implies (fact neq x x) (false))))+  (defgenrule neqRl_strd+    (forall ((x strd)) (implies (fact neq x x) (false))))+  (defgenrule neqRl_mesg+    (forall ((x mesg)) (implies (fact neq x x) (false))))+  (comment "Fixed Blanchet's protocol using named asymmetric keys"))++(defskeleton blanchet-max-fixed+  (vars (d data) (s skey) (a b name))+  (defstrand resp 2 (d d) (s s) (a a) (b b))+  (non-orig (privk a) (privk b))+  (uniq-orig s)+  (comment "Analyze from the responder's perspective")+  (traces ((recv (enc (enc s b (privk a)) (pubk b))) (send (enc d s))))+  (label 37)+  (unrealized (0 0))+  (origs)+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton blanchet-max-fixed+  (vars (d data) (s skey) (a b name))+  (defstrand resp 2 (d d) (s s) (a a) (b b))+  (defstrand init 1 (s s) (a a) (b b))+  (precedes ((1 0) (0 0)))+  (non-orig (privk a) (privk b))+  (uniq-orig s)+  (operation encryption-test (added-strand init 1) (enc s b (privk a))+    (0 0))+  (traces ((recv (enc (enc s b (privk a)) (pubk b))) (send (enc d s)))+    ((send (enc (enc s b (privk a)) (pubk b)))))+  (label 38)+  (parent 37)+  (realized)+  (shape)+  (maps ((0) ((a a) (b b) (s s) (d d))))+  (origs (s (1 0))))++(comment "Nothing left to do")++(defprotocol blanchet-max-fixed basic+  (defrole init+    (vars (a b name) (s skey) (d data))+    (trace (send (enc (enc s b (privk a)) (pubk b))) (recv (enc d s))))+  (defrole resp+    (vars (a b name) (s skey) (d data))+    (trace (recv (enc (enc s b (privk a)) (pubk b))) (send (enc d s))))+  (defgenrule neqRl_indx+    (forall ((x indx)) (implies (fact neq x x) (false))))+  (defgenrule neqRl_strd+    (forall ((x strd)) (implies (fact neq x x) (false))))+  (defgenrule neqRl_mesg+    (forall ((x mesg)) (implies (fact neq x x) (false))))+  (comment "Fixed Blanchet's protocol using named asymmetric keys"))++(defskeleton blanchet-max-fixed+  (vars (d data) (s skey) (a b name))+  (defstrand resp 2 (d d) (s s) (a a) (b b))+  (deflistener d)+  (non-orig (privk a) (privk b))+  (uniq-orig d s)+  (comment "From the responders's perspective, is the secret leaked?")+  (traces ((recv (enc (enc s b (privk a)) (pubk b))) (send (enc d s)))+    ((recv d) (send d)))+  (label 39)+  (unrealized (0 0) (1 0))+  (preskeleton)+  (origs (d (0 1)))+  (comment "Not a skeleton"))++(defskeleton blanchet-max-fixed+  (vars (d data) (s skey) (a b name))+  (defstrand resp 2 (d d) (s s) (a a) (b b))+  (deflistener d)+  (precedes ((0 1) (1 0)))+  (non-orig (privk a) (privk b))+  (uniq-orig d s)+  (traces ((recv (enc (enc s b (privk a)) (pubk b))) (send (enc d s)))+    ((recv d) (send d)))+  (label 40)+  (parent 39)+  (unrealized (0 0))+  (origs (d (0 1)))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton blanchet-max-fixed+  (vars (d data) (s skey) (a b name))+  (defstrand resp 2 (d d) (s s) (a a) (b b))+  (deflistener d)+  (defstrand init 1 (s s) (a a) (b b))+  (precedes ((0 1) (1 0)) ((2 0) (0 0)))+  (non-orig (privk a) (privk b))+  (uniq-orig d s)+  (operation encryption-test (added-strand init 1) (enc s b (privk a))+    (0 0))+  (traces ((recv (enc (enc s b (privk a)) (pubk b))) (send (enc d s)))+    ((recv d) (send d)) ((send (enc (enc s b (privk a)) (pubk b)))))+  (label 41)+  (parent 40)+  (unrealized (1 0))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton blanchet-max-fixed+  (vars (d data) (s skey) (a b name))+  (defstrand resp 2 (d d) (s s) (a a) (b b))+  (deflistener d)+  (defstrand init 1 (s s) (a a) (b b))+  (deflistener s)+  (precedes ((0 1) (1 0)) ((2 0) (0 0)) ((2 0) (3 0)) ((3 1) (1 0)))+  (non-orig (privk a) (privk b))+  (uniq-orig d s)+  (operation nonce-test (added-listener s) d (1 0) (enc d s))+  (traces ((recv (enc (enc s b (privk a)) (pubk b))) (send (enc d s)))+    ((recv d) (send d)) ((send (enc (enc s b (privk a)) (pubk b))))+    ((recv s) (send s)))+  (label 42)+  (parent 41)+  (unrealized (3 0))+  (dead)+  (comment "empty cohort"))++(comment "Nothing left to do")
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 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/blanchet.scm")  (defprotocol blanchet basic
tst/bug_example.tst view
@@ -1,6 +1,6 @@ (herald bug_example (bound 20)) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/bug_example.scm") (comment "Strand count bounded at 20")
tst/cert_lang.tst view
@@ -1,6 +1,6 @@ (herald cert-lang) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/cert_lang.scm")  (defprotocol cert-uni basic
tst/chan-envelope.tst view
@@ -1,6 +1,6 @@ (herald "Envelope Protocol With Channels" (bound 15)) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/chan-envelope.scm") (comment "Strand count bounded at 15")
tst/chan-perrig-song.tst view
@@ -1,6 +1,6 @@ (herald perrig-song) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/chan-perrig-song.scm")  (defprotocol perrig-song basic
tst/chan-unilateral.tst view
@@ -1,6 +1,6 @@ (herald chan-unilateral) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/chan-unilateral.scm")  (defprotocol unilateral basic
tst/chan-yahalom-role-decl.tst view
@@ -1,6 +1,6 @@ (herald "Yahalom Protocol Without Forwarding" (bound 15)) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/chan-yahalom-role-decl.scm") (comment "Strand count bounded at 15")
tst/chan-yahalom.tst view
@@ -1,6 +1,6 @@ (herald "Yahalom Protocol Without Forwarding" (bound 15)) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/chan-yahalom.scm") (comment "Strand count bounded at 15")
tst/commitment.tst view
@@ -1,6 +1,6 @@ (herald commitment) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/commitment.scm")  (defprotocol commit basic
tst/comp_test.tst view
@@ -1,6 +1,6 @@ (herald "Main Example") -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/comp_test.scm")  (defprotocol main-ex-src basic
tst/completeness-test.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/completeness-test.scm")  (defprotocol completeness-test basic
tst/crushing.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/crushing.scm")  (defprotocol crushing basic
tst/dass_simple.tst view
@@ -1,6 +1,6 @@ (herald "Distributed Authentication Security Service Protocol Variants") -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/dass_simple.scm")  (defprotocol dass-simple basic
tst/denning-sacco.tst view
@@ -1,6 +1,6 @@ (herald "Denning-Sacco Protocol") -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/denning-sacco.scm")  (defprotocol denning-sacco basic
tst/deorig_contract.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/deorig_contract.scm")  (defprotocol deorig-contract basic
tst/deorig_mesg.tst view
@@ -1,6 +1,6 @@ (herald deorig-mesg) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/deorig_mesg.scm")  (defprotocol deorig-mesg basic
tst/deorig_simple.tst view
@@ -1,6 +1,6 @@ (herald deorig-simple) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/deorig_simple.scm")  (defprotocol deorig-simple basic
tst/dh-ca_hack.tst view
@@ -1,6 +1,6 @@ (herald dhca (algebra basic) (bound 12)) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/dh-ca_hack.scm") (comment "Strand count bounded at 12")
tst/dh_encrypt_hack.tst view
@@ -1,6 +1,6 @@ (herald dhencrypt (algebra basic)) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/dh_encrypt_hack.scm")  (defprotocol dhencrypt basic
tst/dh_group_sig.tst view
@@ -1,7 +1,7 @@ (herald "Signed group DH exchange (improved version)"   (algebra diffie-hellman) (limit 100)) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/dh_group_sig.scm") (comment "Step count limited to 100")
tst/dh_group_sig_auth_failure.tst view
@@ -1,7 +1,7 @@ (herald "Signed group DH exchange (version with auth failure)"   (algebra diffie-hellman) (limit 100)) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/dh_group_sig_auth_failure.scm") (comment "Step count limited to 100")
tst/dh_mim_hack.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/dh_mim_hack.scm")  (defprotocol dh_mim basic
tst/dhcr_um.tst view
@@ -1,7 +1,7 @@ (herald "DHCR: unified model (UM) original" (bound 20) (limit 325)   (algebra diffie-hellman)) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/dhcr_um.scm") (comment "Step count limited to 325") (comment "Strand count bounded at 20")
tst/dhcr_um3.tst view
@@ -1,7 +1,7 @@ (herald "DHCR: unified model (UM) three-part" (bound 20) (limit 8000)   (algebra diffie-hellman)) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/dhcr_um3.scm") (comment "Step count limited to 8000") (comment "Strand count bounded at 20")
tst/dhcr_um_exercise_resolved_bug.tst view
@@ -1,7 +1,7 @@ (herald "DHCR: unified model (UM) original" (bound 20) (limit 12000)   (algebra diffie-hellman)) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/dhcr_um_exercise_resolved_bug.scm") (comment "Step count limited to 12000") (comment "Strand count bounded at 20")
tst/dhcr_um_expt.tst view

file too large to diff

tst/dhcr_umx.tst view
@@ -1,7 +1,7 @@ (herald "DHCR: unified model (UM) criss-cross" (bound 20) (limit 8000)   (algebra diffie-hellman)) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/dhcr_umx.scm") (comment "Step count limited to 8000") (comment "Strand count bounded at 20")
tst/dhnsl_hack.tst view
@@ -1,7 +1,7 @@ (herald "Diffie-Hellman enhanced Needham-Schroeder-Lowe Protocol"   (algebra basic)) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/dhnsl_hack.scm")  (defprotocol dhnsl basic
tst/dhstatic-state.tst view
@@ -1,6 +1,6 @@ (herald dhstatic-state (algebra diffie-hellman) (bound 16)) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/dhstatic-state.scm") (comment "Strand count bounded at 16")
tst/disclosure.tst view
@@ -1,6 +1,6 @@ (herald disclosure) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/disclosure.scm")  (defprotocol disc basic
tst/doorsep.tst view
@@ -1,6 +1,6 @@ (herald doorsep (comment "Door Simple Example Protocol")) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/doorsep.scm")  (defprotocol doorsep basic
tst/doorsep2invk.tst view
@@ -1,6 +1,6 @@ (herald doorsep2invk (comment "Door Simple Example Protocol")) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/doorsep2invk.scm")  (defprotocol doorsep basic
tst/dy.tst view

file too large to diff

tst/encsig.tst view
@@ -1,7 +1,7 @@ (herald "Encrypted Signed Message Example"   (comment "Shows examples of key usage of asymmetric keys")) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/encsig.scm")  (defprotocol mult-keys-enc-sig basic
tst/envelope.tst view
@@ -1,6 +1,6 @@ (herald "Envelope Protocol" (bound 15)) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/envelope.scm") (comment "Strand count bounded at 15")
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 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/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 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/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 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/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 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/epmo_acctnum-key-hash.scm")  (defprotocol epmo_acctnum basic
tst/expand.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "Expanded macros")  (herald expand (expand) (comment "test macro expansion"))
tst/facts.tst view
@@ -1,6 +1,6 @@ (herald facts) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/facts.scm")  (defprotocol unilateral basic
tst/factvar.tst view
@@ -1,6 +1,6 @@ (herald factvar) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/factvar.scm")  (defprotocol free-fact-var 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 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/ffgg.scm")  (defprotocol ffgg basic
tst/fluffy_draft03_gske.tst view
@@ -3,7 +3,7 @@   (comment     "Based on the Internet-Draft: https://www.ietf.org/archive/id/draft-hardjono-ace-fluffy-03.txt")) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/fluffy_draft03_gske.scm")  (defprotocol fluffy basic
tst/fragile_pruning.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/fragile_pruning.scm")  (defprotocol fragile_pruning basic
tst/goals.tst view
@@ -1,6 +1,6 @@ (herald goals) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/goals.scm")  (defprotocol ns basic
tst/hashtest-key-hash.tst view
@@ -1,6 +1,6 @@ (herald "Hashtest") -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/hashtest-key-hash.scm")  (defprotocol hashtest basic
tst/hashtest.tst view
@@ -1,6 +1,6 @@ (herald "Hashtest") -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/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 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/incompleteness_example.scm")  (defprotocol incompleteness-example basic
tst/isoreject-corrected.tst view
@@ -1,6 +1,6 @@ (herald isoreject-corrected) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/isoreject-corrected.scm")  (defprotocol isofix basic
tst/isoreject.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/isoreject.scm")  (defprotocol isoreject basic
tst/kelly1.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/kelly1.scm")  (defprotocol kelly1 basic
tst/kerberos.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/kerberos.scm")  (defprotocol kerberos basic
tst/locn_envelope.tst view
@@ -1,7 +1,7 @@ (herald "Envelope Protocol, location-based version" (bound 30)   (limit 1200)) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/locn_envelope.scm") (comment "Step count limited to 1200") (comment "Strand count bounded at 30")
tst/mass.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/mass.lsp")  (defprotocol mass basic
tst/mass2.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/mass2.lsp")  (defprotocol mass2 basic
tst/missing_contraction.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/missing_contraction.scm")  (defprotocol missing-contraction basic
tst/neq_test.tst view
@@ -2,7 +2,7 @@   (comment "First skeleton should have a shape,"     "second should be dead.")) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/neq_test.scm")  (defprotocol neq-test basic
tst/neuman-stubblebine-reauth.tst view
@@ -1,6 +1,6 @@ (herald neuman-stubblebine-reauth (bound 8)) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/neuman-stubblebine-reauth.lsp")  (defprotocol neuman-stubblebine-reauth basic
tst/neuman-stubblebine.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/neuman-stubblebine.scm")  (defprotocol neuman-stubblebine basic
tst/no_contraction.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/no_contraction.scm")  (defprotocol no-contraction basic
tst/non_transforming.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/non_transforming.scm")  (defprotocol non_transforming basic
tst/nonaug-prune.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/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 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/ns-l.scm")  (defprotocol ns basic
tst/ns-rebinding.tst view
@@ -1,6 +1,6 @@ (herald "ALternate Needham-Schroeder Public-Key Protocol Variants") -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/ns-rebinding.scm")  (defprotocol ns basic
tst/ns.tst view
@@ -1,6 +1,6 @@ (herald "Needham-Schroeder Public-Key Protocol Variants") -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/ns.scm")  (defprotocol ns basic
tst/nsl3.tst view
@@ -1,6 +1,6 @@ (herald "Three Party Needham-Schroeder-Lowe Protocol") -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/nsl3.scm")  (defprotocol nsl3 basic
tst/nslsk.tst view
@@ -1,6 +1,6 @@ (herald "Needham-Schroeder-Lowe Protocol with symmetric encryption") -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/nslsk.scm")  (defprotocol nslsk basic
tst/open-closed-multiloc.tst view
@@ -1,6 +1,6 @@ (herald open-closed (bound 44)) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/open-closed-multiloc.scm") (comment "Strand count bounded at 44")
tst/open-closed-tag.tst view
@@ -1,6 +1,6 @@ (herald open-closed (bound 44)) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/open-closed-tag.scm") (comment "Strand count bounded at 44")
tst/open-closed.tst view
@@ -1,6 +1,6 @@ (herald open-closed (bound 44)) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/open-closed.scm") (comment "Strand count bounded at 44")
tst/or.tst view
@@ -1,7 +1,7 @@ (herald "Otway-Rees Protocol"   (comment "Standard version using variables of sort mesg")) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/or.scm")  (defprotocol or basic
tst/ordered.tst view
@@ -1,6 +1,6 @@ (herald ordered) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/ordered.scm")  (defprotocol ordered basic
tst/pca.tst view
@@ -1,7 +1,7 @@ (herald "Privacy Certificate Authority" (bound 15)   (comment "Generation of an Attestation Identity Certificate")) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/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 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/pen-non-orig-test.scm")  (defprotocol pennonorigtest basic
tst/pfs-via-pubkey.tst view
@@ -1,6 +1,6 @@ (herald pfs-via-pubkey) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/pfs-via-pubkey.scm")  (defprotocol pfs-easy basic
tst/pkinit.tst view
@@ -1,6 +1,6 @@ (herald "Kerberos PK init") -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/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 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/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 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/print.scm")  (defprotocol print-test basic
tst/prottrans.tst view
@@ -1,6 +1,6 @@ (herald "Protocol Transformations With Rules") -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/prottrans.scm")  (defprotocol ns basic
tst/pruning1.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/pruning1.scm")  (defprotocol prune basic
tst/puzzle_example.tst view
@@ -1,6 +1,6 @@ (herald puzzle_example) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/puzzle_example.scm")  (defprotocol puzzle basic
tst/reflect.tst view
@@ -1,6 +1,6 @@ (herald reflect) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/reflect.scm")  (defprotocol reflect basic
tst/renamings.tst view
@@ -2,7 +2,7 @@   (comment "There is a flaw in this protocol by design")   (comment "It also shows how variable renaming works")) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/renamings.scm")  (defprotocol blanchet basic
tst/role_uniq.tst view
@@ -1,6 +1,6 @@ (herald "Role Unique Origination") -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/role_uniq.scm")  (defprotocol blanchet basic
tst/rule-node.tst view
@@ -1,6 +1,6 @@ (herald rule-node) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/rule-node.scm")  (defprotocol rule-order basic
tst/rule-order.tst view
@@ -1,6 +1,6 @@ (herald rule-order) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/rule-order.scm")  (defprotocol rule-order 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 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/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 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/sorted_epmo_acctnum.scm") (comment "Strand count bounded at 12")
tst/sts.tst view
@@ -1,7 +1,7 @@ (herald "Station-to-station protocol" (bound 20)   (algebra diffie-hellman)) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/sts.scm") (comment "Strand count bounded at 20")
tst/sts_unflip.tst view
@@ -1,7 +1,7 @@ (herald "Station-to-station protocol unflipped"   (algebra diffie-hellman)) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/sts_unflip.scm")  (defprotocol station-to-station-unflip diffie-hellman
tst/sts_weak.tst view
@@ -1,7 +1,7 @@ (herald "Station-to-station protocol:  Weakened version"   (algebra diffie-hellman)) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/sts_weak.scm")  (defprotocol station-weak diffie-hellman
tst/subatomic-open-closed-test-genrule.tst view
@@ -1,6 +1,6 @@ (herald subatomic-open-closed-test-genrule (bound 40)) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment   "All input read from tst/subatomic-open-closed-test-genrule.scm") (comment "Strand count bounded at 40")
tst/subatomic-open-closed.tst view
@@ -1,6 +1,6 @@ (herald subatomic-open-closed (bound 40)) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/subatomic-open-closed.scm") (comment "Strand count bounded at 40")
tst/sync_locn_envelope.tst view
@@ -1,7 +1,7 @@ (herald "Envelope Protocol, location-based version" (check-nonces)   (bound 30) (limit 6000)) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/sync_locn_envelope.scm") (comment "Step count limited to 6000") (comment "Strand count bounded at 30")
tst/targetterms1.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/targetterms1.scm")  (defprotocol targetterms basic
tst/targetterms2.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/targetterms2.scm")  (defprotocol targetterms2 basic
tst/targetterms6.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/targetterms6.scm")  (defprotocol targetterms6 basic
tst/targetterms8.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/targetterms8.scm")  (defprotocol targetterms8 basic
tst/thisthat.tst view
@@ -1,6 +1,6 @@ (herald "Needham-Schroeder Public-Key Protocol This-That Variant") -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/thisthat.scm")  (defprotocol thisthat basic
tst/tickle-unique.tst view
@@ -1,6 +1,6 @@ (herald tickle-unique) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/tickle-unique.scm")  (defprotocol tickle basic
tst/timestamping.tst view
@@ -1,6 +1,6 @@ (herald timestamping-service) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/timestamping.scm")  (defprotocol timestamping-service basic
tst/trust-anchor.tst view
@@ -1,7 +1,7 @@ (herald trust-anchor   (comment "Tests rule application on initial skeleton")) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/trust-anchor.scm")  (defprotocol trust-anchor basic
+ tst/ugo.scm view
@@ -0,0 +1,75 @@+(herald uniq-gen-and-orig-example+	(comment "Non-executable role examples"))++;;; These two protocols show examples where generation and origination+;;; of asymmetric key pairs lead to shapes that cannot be+;;; implemented.  Note that key pairs must generate or originate at+;;; the same node in a skeleton.++;;; CPSA computes the shapes that would be possible, assuming that the+;;; responder, given u, could magically determine (invk u).+;;; Presumably, the specifier who writes a protocol like this is+;;; committed to this possibility.  I.e. we consider this the+;;; specifier's responsibility to avoid, not CPSA's responsibility to+;;; detect.  ++(defprotocol uniq-gen-example basic+  (defrole init+    (vars (u akey) (k skey))+    (trace+     (send (enc u k))+     (recv (invk u))+     (send u))+    (uniq-gen u)+    (non-orig k)+    (comment+     "Instances of this role generate u and (invk u)"+     "at their first event."))+  (defrole resp+    (vars (u akey) (k skey))+    (trace+     (recv (enc u k))+     (send (invk u))+     (recv u))+    (non-orig k)+    (comment+     "Instances of this role appear to generate (invk u)"+     "at their second event.")))++(defskeleton uniq-gen-example+  (vars)+  (defstrandmax resp)+  (comment "How is the responder able to send (invk u)?"))++(defskeleton uniq-gen-example+  (vars (u akey))+  (defstrandmax resp (u u))+  (uniq-gen (invk u))+  (comment "How is the responder able to send (invk u)?"))++(defprotocol uniq-orig-example basic+  (defrole init+    (vars (u akey) (k skey))+    (trace+     (send (enc u k))+     (recv (invk u))+     (send u))+    (uniq-orig u)+    (non-orig k))+  (defrole resp+    (vars (u akey) (k skey))+    (trace+     (recv (enc u k))+     (send (invk u))+     (recv u))+    (non-orig k))+  (comment "Similar to the above, but with uniq-orig instead of uniq-gen."))++(defskeleton uniq-orig-example+  (vars)+  (defstrandmax resp))++(defskeleton uniq-orig-example+  (vars (u akey))+  (defstrandmax resp (u u))+  (uniq-orig (invk u)))
+ tst/ugo.tst view
@@ -0,0 +1,352 @@+(herald uniq-gen-and-orig-example+  (comment "Non-executable role examples"))++(comment "CPSA 4.4.2")+(comment "All input read from ugo.scm")++(defprotocol uniq-gen-example basic+  (defrole init+    (vars (u akey) (k skey))+    (trace (send (enc u k)) (recv (invk u)) (send u))+    (non-orig k)+    (uniq-gen u)+    (comment "Instances of this role generate u and (invk u)"+      "at their first event."))+  (defrole resp+    (vars (u akey) (k skey))+    (trace (recv (enc u k)) (send (invk u)) (recv u))+    (non-orig k)+    (comment "Instances of this role appear to generate (invk u)"+      "at their second event."))+  (defgenrule neqRl_indx+    (forall ((x indx)) (implies (fact neq x x) (false))))+  (defgenrule neqRl_strd+    (forall ((x strd)) (implies (fact neq x x) (false))))+  (defgenrule neqRl_mesg+    (forall ((x mesg)) (implies (fact neq x x) (false)))))++(defskeleton uniq-gen-example+  (vars (k skey) (u akey))+  (defstrand resp 3 (k k) (u u))+  (non-orig k)+  (comment "How is the responder able to send (invk u)?")+  (traces ((recv (enc u k)) (send (invk u)) (recv u)))+  (label 0)+  (unrealized (0 0))+  (origs)+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton uniq-gen-example+  (vars (k skey) (u akey))+  (defstrand resp 3 (k k) (u u))+  (defstrand init 1 (k k) (u u))+  (precedes ((1 0) (0 0)))+  (non-orig k)+  (uniq-gen u)+  (operation encryption-test (added-strand init 1) (enc u k) (0 0))+  (traces ((recv (enc u k)) (send (invk u)) (recv u))+    ((send (enc u k))))+  (label 1)+  (parent 0)+  (unrealized (0 2))+  (comment "2 in cohort - 2 not yet seen"))++(defskeleton uniq-gen-example+  (vars (k skey) (u akey))+  (defstrand resp 3 (k k) (u u))+  (defstrand init 3 (k k) (u u))+  (precedes ((1 0) (0 0)) ((1 2) (0 2)))+  (non-orig k)+  (uniq-gen u)+  (operation nonce-test (displaced 1 2 init 3) u (0 2) (enc u k))+  (traces ((recv (enc u k)) (send (invk u)) (recv u))+    ((send (enc u k)) (recv (invk u)) (send u)))+  (label 2)+  (parent 1)+  (realized)+  (shape)+  (maps ((0) ((u u) (k k))))+  (origs))++(defskeleton uniq-gen-example+  (vars (k k-0 skey) (u akey))+  (defstrand resp 3 (k k) (u (invk u)))+  (defstrand init 1 (k k) (u (invk u)))+  (defstrand resp 2 (k k-0) (u u))+  (precedes ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 2)))+  (non-orig k k-0)+  (uniq-gen (invk u))+  (operation nonce-test (added-strand resp 2) (invk u) (0 2)+    (enc (invk u) k))+  (traces ((recv (enc (invk u) k)) (send u) (recv (invk u)))+    ((send (enc (invk u) k))) ((recv (enc u k-0)) (send (invk u))))+  (label 3)+  (parent 1)+  (unrealized (2 0))+  (dead)+  (comment "empty cohort"))++(comment "Nothing left to do")++(defprotocol uniq-gen-example basic+  (defrole init+    (vars (u akey) (k skey))+    (trace (send (enc u k)) (recv (invk u)) (send u))+    (non-orig k)+    (uniq-gen u)+    (comment "Instances of this role generate u and (invk u)"+      "at their first event."))+  (defrole resp+    (vars (u akey) (k skey))+    (trace (recv (enc u k)) (send (invk u)) (recv u))+    (non-orig k)+    (comment "Instances of this role appear to generate (invk u)"+      "at their second event."))+  (defgenrule neqRl_indx+    (forall ((x indx)) (implies (fact neq x x) (false))))+  (defgenrule neqRl_strd+    (forall ((x strd)) (implies (fact neq x x) (false))))+  (defgenrule neqRl_mesg+    (forall ((x mesg)) (implies (fact neq x x) (false)))))++(defskeleton uniq-gen-example+  (vars (k skey) (u akey))+  (defstrand resp 3 (k k) (u u))+  (non-orig k)+  (uniq-gen (invk u))+  (comment "How is the responder able to send (invk u)?")+  (traces ((recv (enc u k)) (send (invk u)) (recv u)))+  (label 4)+  (unrealized (0 0))+  (origs)+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton uniq-gen-example+  (vars (k skey) (u akey))+  (defstrand resp 3 (k k) (u u))+  (defstrand init 1 (k k) (u u))+  (precedes ((1 0) (0 0)))+  (non-orig k)+  (uniq-gen u (invk u))+  (operation encryption-test (added-strand init 1) (enc u k) (0 0))+  (traces ((recv (enc u k)) (send (invk u)) (recv u))+    ((send (enc u k))))+  (label 5)+  (parent 4)+  (unrealized (0 2))+  (comment "2 in cohort - 2 not yet seen"))++(defskeleton uniq-gen-example+  (vars (k skey) (u akey))+  (defstrand resp 3 (k k) (u u))+  (defstrand init 3 (k k) (u u))+  (precedes ((1 0) (0 0)) ((1 2) (0 2)))+  (non-orig k)+  (uniq-gen u (invk u))+  (operation nonce-test (displaced 1 2 init 3) u (0 2) (enc u k))+  (traces ((recv (enc u k)) (send (invk u)) (recv u))+    ((send (enc u k)) (recv (invk u)) (send u)))+  (label 6)+  (parent 5)+  (unrealized (1 1))+  (comment "2 in cohort - 2 not yet seen"))++(defskeleton uniq-gen-example+  (vars (k k-0 skey) (u akey))+  (defstrand resp 3 (k k) (u (invk u)))+  (defstrand init 1 (k k) (u (invk u)))+  (defstrand resp 2 (k k-0) (u u))+  (precedes ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 2)))+  (non-orig k k-0)+  (uniq-gen u (invk u))+  (operation nonce-test (added-strand resp 2) (invk u) (0 2)+    (enc (invk u) k))+  (traces ((recv (enc (invk u) k)) (send u) (recv (invk u)))+    ((send (enc (invk u) k))) ((recv (enc u k-0)) (send (invk u))))+  (label 7)+  (parent 5)+  (unrealized (2 0))+  (dead)+  (comment "empty cohort"))++(defskeleton uniq-gen-example+  (vars (k skey) (u akey))+  (defstrand resp 3 (k k) (u u))+  (defstrand init 3 (k k) (u u))+  (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2)))+  (non-orig k)+  (uniq-gen u (invk u))+  (operation nonce-test (displaced 2 0 resp 2) (invk u) (1 1))+  (traces ((recv (enc u k)) (send (invk u)) (recv u))+    ((send (enc u k)) (recv (invk u)) (send u)))+  (label 8)+  (parent 6)+  (realized)+  (shape)+  (maps ((0) ((u u) (k k))))+  (origs))++(defskeleton uniq-gen-example+  (vars (k k-0 skey) (u akey))+  (defstrand resp 3 (k k) (u u))+  (defstrand init 3 (k k) (u u))+  (defstrand resp 2 (k k-0) (u u))+  (precedes ((1 0) (0 0)) ((1 0) (2 0)) ((1 2) (0 2)) ((2 1) (1 1)))+  (non-orig k k-0)+  (uniq-gen u (invk u))+  (operation nonce-test (added-strand resp 2) (invk u) (1 1))+  (traces ((recv (enc u k)) (send (invk u)) (recv u))+    ((send (enc u k)) (recv (invk u)) (send u))+    ((recv (enc u k-0)) (send (invk u))))+  (label 9)+  (parent 6)+  (unrealized (2 0))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton uniq-gen-example+  (vars (k skey) (u akey))+  (defstrand resp 3 (k k) (u u))+  (defstrand init 3 (k k) (u u))+  (defstrand resp 2 (k k) (u u))+  (precedes ((1 0) (0 0)) ((1 0) (2 0)) ((1 2) (0 2)) ((2 1) (1 1)))+  (non-orig k)+  (uniq-gen u (invk u))+  (operation encryption-test (displaced 3 1 init 1) (enc u k-0) (2 0))+  (traces ((recv (enc u k)) (send (invk u)) (recv u))+    ((send (enc u k)) (recv (invk u)) (send u))+    ((recv (enc u k)) (send (invk u))))+  (label 10)+  (parent 9)+  (realized)+  (shape)+  (maps ((0) ((u u) (k k))))+  (origs))++(comment "Nothing left to do")++(defprotocol uniq-orig-example basic+  (defrole init+    (vars (u akey) (k skey))+    (trace (send (enc u k)) (recv (invk u)) (send u))+    (non-orig k)+    (uniq-orig u))+  (defrole resp+    (vars (u akey) (k skey))+    (trace (recv (enc u k)) (send (invk u)) (recv u))+    (non-orig k))+  (defgenrule neqRl_indx+    (forall ((x indx)) (implies (fact neq x x) (false))))+  (defgenrule neqRl_strd+    (forall ((x strd)) (implies (fact neq x x) (false))))+  (defgenrule neqRl_mesg+    (forall ((x mesg)) (implies (fact neq x x) (false))))+  (comment+    "Similar to the above, but with uniq-orig instead of uniq-gen."))++(defskeleton uniq-orig-example+  (vars (k skey) (u akey))+  (defstrand resp 3 (k k) (u u))+  (non-orig k)+  (traces ((recv (enc u k)) (send (invk u)) (recv u)))+  (label 11)+  (unrealized (0 0))+  (origs)+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton uniq-orig-example+  (vars (k skey) (u akey))+  (defstrand resp 3 (k k) (u u))+  (defstrand init 1 (k k) (u u))+  (precedes ((1 0) (0 0)))+  (non-orig k)+  (uniq-orig u)+  (operation encryption-test (added-strand init 1) (enc u k) (0 0))+  (traces ((recv (enc u k)) (send (invk u)) (recv u))+    ((send (enc u k))))+  (label 12)+  (parent 11)+  (unrealized (0 2))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton uniq-orig-example+  (vars (k skey) (u akey))+  (defstrand resp 3 (k k) (u u))+  (defstrand init 3 (k k) (u u))+  (precedes ((1 0) (0 0)) ((1 2) (0 2)))+  (non-orig k)+  (uniq-orig u)+  (operation nonce-test (displaced 1 2 init 3) u (0 2) (enc u k))+  (traces ((recv (enc u k)) (send (invk u)) (recv u))+    ((send (enc u k)) (recv (invk u)) (send u)))+  (label 13)+  (parent 12)+  (realized)+  (shape)+  (maps ((0) ((u u) (k k))))+  (origs (u (1 0))))++(comment "Nothing left to do")++(defprotocol uniq-orig-example basic+  (defrole init+    (vars (u akey) (k skey))+    (trace (send (enc u k)) (recv (invk u)) (send u))+    (non-orig k)+    (uniq-orig u))+  (defrole resp+    (vars (u akey) (k skey))+    (trace (recv (enc u k)) (send (invk u)) (recv u))+    (non-orig k))+  (defgenrule neqRl_indx+    (forall ((x indx)) (implies (fact neq x x) (false))))+  (defgenrule neqRl_strd+    (forall ((x strd)) (implies (fact neq x x) (false))))+  (defgenrule neqRl_mesg+    (forall ((x mesg)) (implies (fact neq x x) (false))))+  (comment+    "Similar to the above, but with uniq-orig instead of uniq-gen."))++(defskeleton uniq-orig-example+  (vars (k skey) (u akey))+  (defstrand resp 3 (k k) (u u))+  (non-orig k)+  (uniq-orig (invk u))+  (traces ((recv (enc u k)) (send (invk u)) (recv u)))+  (label 14)+  (unrealized (0 0))+  (origs ((invk u) (0 1)))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton uniq-orig-example+  (vars (k skey) (u akey))+  (defstrand resp 3 (k k) (u u))+  (defstrand init 1 (k k) (u u))+  (precedes ((1 0) (0 0)))+  (non-orig k)+  (uniq-orig u (invk u))+  (operation encryption-test (added-strand init 1) (enc u k) (0 0))+  (traces ((recv (enc u k)) (send (invk u)) (recv u))+    ((send (enc u k))))+  (label 15)+  (parent 14)+  (unrealized (0 2))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton uniq-orig-example+  (vars (k skey) (u akey))+  (defstrand resp 3 (k k) (u u))+  (defstrand init 3 (k k) (u u))+  (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2)))+  (non-orig k)+  (uniq-orig u (invk u))+  (operation nonce-test (displaced 1 2 init 3) u (0 2) (enc u k))+  (traces ((recv (enc u k)) (send (invk u)) (recv u))+    ((send (enc u k)) (recv (invk u)) (send u)))+  (label 16)+  (parent 15)+  (realized)+  (shape)+  (maps ((0) ((u u) (k k))))+  (origs (u (1 0)) ((invk u) (0 1))))++(comment "Nothing left to do")
tst/uncarried_keys.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/uncarried_keys.scm")  (defprotocol uncarried-keys basic
tst/unilateral.tst view
@@ -1,6 +1,6 @@ (herald unilateral) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/unilateral.scm")  (defprotocol unilateral basic
tst/uniq-gen-test.tst view
@@ -1,7 +1,7 @@ (herald "Unique generation test protocols."   (comment "Skeletons 2, 4, and 7 should have no shapes.")) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/uniq-gen-test.scm")  (defprotocol uniqgentest basic
tst/uo.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/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 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/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 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/wang-key-hash.scm") (comment "Strand count bounded at 10")
tst/weird.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/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 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/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 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/wide-mouth-frog.lsp")  (defprotocol wide-mouth-frog basic
tst/wonthull.tst view
@@ -1,6 +1,6 @@ (herald wonthull (bound 9)) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/wonthull.scm") (comment "Strand count bounded at 9")
tst/wonthull2.tst view
@@ -1,6 +1,6 @@ (herald wonthull2 (bound 9)) -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/wonthull2.scm") (comment "Strand count bounded at 9")
tst/wonthull3.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/wonthull3.scm")  (defprotocol wonthull3 basic
tst/woolam.tst view
@@ -1,6 +1,6 @@ (herald "Woo-Lam Protocol") -(comment "CPSA 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/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 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/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 4.4.1")+(comment "CPSA 4.4.2") (comment "All input read from tst/yahalom.scm") (comment "Strand count bounded at 15")