diff --git a/NEWS b/NEWS --- a/NEWS +++ b/NEWS @@ -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 diff --git a/cpsa.cabal b/cpsa.cabal --- a/cpsa.cabal +++ b/cpsa.cabal @@ -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 diff --git a/doc/cpsa4manual.pdf b/doc/cpsa4manual.pdf Binary files a/doc/cpsa4manual.pdf and b/doc/cpsa4manual.pdf differ diff --git a/doc/src/cpsa4manual/algebra.tex b/doc/src/cpsa4manual/algebra.tex --- a/doc/src/cpsa4manual/algebra.tex +++ b/doc/src/cpsa4manual/algebra.tex @@ -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 diff --git a/doc/src/cpsa4manual/cpsa4manual.tex b/doc/src/cpsa4manual/cpsa4manual.tex --- a/doc/src/cpsa4manual/cpsa4manual.tex +++ b/doc/src/cpsa4manual/cpsa4manual.tex @@ -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} diff --git a/doc/src/macros.tex b/doc/src/macros.tex --- a/doc/src/macros.tex +++ b/doc/src/macros.tex @@ -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 diff --git a/src/CPSA/Algebra.hs b/src/CPSA/Algebra.hs --- a/src/CPSA/Algebra.hs +++ b/src/CPSA/Algebra.hs @@ -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 diff --git a/src/CPSA/Graph/Preskeleton.hs b/src/CPSA/Graph/Preskeleton.hs --- a/src/CPSA/Graph/Preskeleton.hs +++ b/src/CPSA/Graph/Preskeleton.hs @@ -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 diff --git a/src/CPSA/Loader.hs b/src/CPSA/Loader.hs --- a/src/CPSA/Loader.hs +++ b/src/CPSA/Loader.hs @@ -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) diff --git a/src/CPSA/Protocol.hs b/src/CPSA/Protocol.hs --- a/src/CPSA/Protocol.hs +++ b/src/CPSA/Protocol.hs @@ -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? diff --git a/tst/DH_hack.tst b/tst/DH_hack.tst --- a/tst/DH_hack.tst +++ b/tst/DH_hack.tst @@ -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") diff --git a/tst/ab.tst b/tst/ab.tst --- a/tst/ab.tst +++ b/tst/ab.tst @@ -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 diff --git a/tst/abc.tst b/tst/abc.tst --- a/tst/abc.tst +++ b/tst/abc.tst @@ -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 diff --git a/tst/aik.tst b/tst/aik.tst --- a/tst/aik.tst +++ b/tst/aik.tst @@ -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 diff --git a/tst/atomic-open-closed.tst b/tst/atomic-open-closed.tst --- a/tst/atomic-open-closed.tst +++ b/tst/atomic-open-closed.tst @@ -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") diff --git a/tst/attest.tst b/tst/attest.tst --- a/tst/attest.tst +++ b/tst/attest.tst @@ -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 diff --git a/tst/auth-enc.tst b/tst/auth-enc.tst --- a/tst/auth-enc.tst +++ b/tst/auth-enc.tst @@ -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 diff --git a/tst/auth-hash.tst b/tst/auth-hash.tst --- a/tst/auth-hash.tst +++ b/tst/auth-hash.tst @@ -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 diff --git a/tst/blanchet-strandmax.scm b/tst/blanchet-strandmax.scm new file mode 100644 --- /dev/null +++ b/tst/blanchet-strandmax.scm @@ -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?")) diff --git a/tst/blanchet-strandmax.tst b/tst/blanchet-strandmax.tst new file mode 100644 --- /dev/null +++ b/tst/blanchet-strandmax.tst @@ -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") diff --git a/tst/blanchet.tst b/tst/blanchet.tst --- a/tst/blanchet.tst +++ b/tst/blanchet.tst @@ -1,7 +1,7 @@ (herald "Blanchet's Simple Example Protocol" (comment "There is a flaw in this protocol by design")) -(comment "CPSA 4.4.1") +(comment "CPSA 4.4.2") (comment "All input read from tst/blanchet.scm") (defprotocol blanchet basic diff --git a/tst/bug_example.tst b/tst/bug_example.tst --- a/tst/bug_example.tst +++ b/tst/bug_example.tst @@ -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") diff --git a/tst/cert_lang.tst b/tst/cert_lang.tst --- a/tst/cert_lang.tst +++ b/tst/cert_lang.tst @@ -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 diff --git a/tst/chan-envelope.tst b/tst/chan-envelope.tst --- a/tst/chan-envelope.tst +++ b/tst/chan-envelope.tst @@ -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") diff --git a/tst/chan-perrig-song.tst b/tst/chan-perrig-song.tst --- a/tst/chan-perrig-song.tst +++ b/tst/chan-perrig-song.tst @@ -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 diff --git a/tst/chan-unilateral.tst b/tst/chan-unilateral.tst --- a/tst/chan-unilateral.tst +++ b/tst/chan-unilateral.tst @@ -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 diff --git a/tst/chan-yahalom-role-decl.tst b/tst/chan-yahalom-role-decl.tst --- a/tst/chan-yahalom-role-decl.tst +++ b/tst/chan-yahalom-role-decl.tst @@ -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") diff --git a/tst/chan-yahalom.tst b/tst/chan-yahalom.tst --- a/tst/chan-yahalom.tst +++ b/tst/chan-yahalom.tst @@ -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") diff --git a/tst/commitment.tst b/tst/commitment.tst --- a/tst/commitment.tst +++ b/tst/commitment.tst @@ -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 diff --git a/tst/comp_test.tst b/tst/comp_test.tst --- a/tst/comp_test.tst +++ b/tst/comp_test.tst @@ -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 diff --git a/tst/completeness-test.tst b/tst/completeness-test.tst --- a/tst/completeness-test.tst +++ b/tst/completeness-test.tst @@ -1,4 +1,4 @@ -(comment "CPSA 4.4.1") +(comment "CPSA 4.4.2") (comment "All input read from tst/completeness-test.scm") (defprotocol completeness-test basic diff --git a/tst/crushing.tst b/tst/crushing.tst --- a/tst/crushing.tst +++ b/tst/crushing.tst @@ -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 diff --git a/tst/dass_simple.tst b/tst/dass_simple.tst --- a/tst/dass_simple.tst +++ b/tst/dass_simple.tst @@ -1,6 +1,6 @@ (herald "Distributed Authentication Security Service Protocol Variants") -(comment "CPSA 4.4.1") +(comment "CPSA 4.4.2") (comment "All input read from tst/dass_simple.scm") (defprotocol dass-simple basic diff --git a/tst/denning-sacco.tst b/tst/denning-sacco.tst --- a/tst/denning-sacco.tst +++ b/tst/denning-sacco.tst @@ -1,6 +1,6 @@ (herald "Denning-Sacco Protocol") -(comment "CPSA 4.4.1") +(comment "CPSA 4.4.2") (comment "All input read from tst/denning-sacco.scm") (defprotocol denning-sacco basic diff --git a/tst/deorig_contract.tst b/tst/deorig_contract.tst --- a/tst/deorig_contract.tst +++ b/tst/deorig_contract.tst @@ -1,4 +1,4 @@ -(comment "CPSA 4.4.1") +(comment "CPSA 4.4.2") (comment "All input read from tst/deorig_contract.scm") (defprotocol deorig-contract basic diff --git a/tst/deorig_mesg.tst b/tst/deorig_mesg.tst --- a/tst/deorig_mesg.tst +++ b/tst/deorig_mesg.tst @@ -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 diff --git a/tst/deorig_simple.tst b/tst/deorig_simple.tst --- a/tst/deorig_simple.tst +++ b/tst/deorig_simple.tst @@ -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 diff --git a/tst/dh-ca_hack.tst b/tst/dh-ca_hack.tst --- a/tst/dh-ca_hack.tst +++ b/tst/dh-ca_hack.tst @@ -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") diff --git a/tst/dh_encrypt_hack.tst b/tst/dh_encrypt_hack.tst --- a/tst/dh_encrypt_hack.tst +++ b/tst/dh_encrypt_hack.tst @@ -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 diff --git a/tst/dh_group_sig.tst b/tst/dh_group_sig.tst --- a/tst/dh_group_sig.tst +++ b/tst/dh_group_sig.tst @@ -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") diff --git a/tst/dh_group_sig_auth_failure.tst b/tst/dh_group_sig_auth_failure.tst --- a/tst/dh_group_sig_auth_failure.tst +++ b/tst/dh_group_sig_auth_failure.tst @@ -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") diff --git a/tst/dh_mim_hack.tst b/tst/dh_mim_hack.tst --- a/tst/dh_mim_hack.tst +++ b/tst/dh_mim_hack.tst @@ -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 diff --git a/tst/dhcr_um.tst b/tst/dhcr_um.tst --- a/tst/dhcr_um.tst +++ b/tst/dhcr_um.tst @@ -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") diff --git a/tst/dhcr_um3.tst b/tst/dhcr_um3.tst --- a/tst/dhcr_um3.tst +++ b/tst/dhcr_um3.tst @@ -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") diff --git a/tst/dhcr_um_exercise_resolved_bug.tst b/tst/dhcr_um_exercise_resolved_bug.tst --- a/tst/dhcr_um_exercise_resolved_bug.tst +++ b/tst/dhcr_um_exercise_resolved_bug.tst @@ -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") diff --git a/tst/dhcr_um_expt.tst b/tst/dhcr_um_expt.tst # file too large to diff: tst/dhcr_um_expt.tst diff --git a/tst/dhcr_umx.tst b/tst/dhcr_umx.tst --- a/tst/dhcr_umx.tst +++ b/tst/dhcr_umx.tst @@ -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") diff --git a/tst/dhnsl_hack.tst b/tst/dhnsl_hack.tst --- a/tst/dhnsl_hack.tst +++ b/tst/dhnsl_hack.tst @@ -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 diff --git a/tst/dhstatic-state.tst b/tst/dhstatic-state.tst --- a/tst/dhstatic-state.tst +++ b/tst/dhstatic-state.tst @@ -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") diff --git a/tst/disclosure.tst b/tst/disclosure.tst --- a/tst/disclosure.tst +++ b/tst/disclosure.tst @@ -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 diff --git a/tst/doorsep.tst b/tst/doorsep.tst --- a/tst/doorsep.tst +++ b/tst/doorsep.tst @@ -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 diff --git a/tst/doorsep2invk.tst b/tst/doorsep2invk.tst --- a/tst/doorsep2invk.tst +++ b/tst/doorsep2invk.tst @@ -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 diff --git a/tst/dy.tst b/tst/dy.tst # file too large to diff: tst/dy.tst diff --git a/tst/encsig.tst b/tst/encsig.tst --- a/tst/encsig.tst +++ b/tst/encsig.tst @@ -1,7 +1,7 @@ (herald "Encrypted Signed Message Example" (comment "Shows examples of key usage of asymmetric keys")) -(comment "CPSA 4.4.1") +(comment "CPSA 4.4.2") (comment "All input read from tst/encsig.scm") (defprotocol mult-keys-enc-sig basic diff --git a/tst/envelope.tst b/tst/envelope.tst --- a/tst/envelope.tst +++ b/tst/envelope.tst @@ -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") diff --git a/tst/epmo-hash.tst b/tst/epmo-hash.tst --- a/tst/epmo-hash.tst +++ b/tst/epmo-hash.tst @@ -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 diff --git a/tst/epmo-key-hash.tst b/tst/epmo-key-hash.tst --- a/tst/epmo-key-hash.tst +++ b/tst/epmo-key-hash.tst @@ -1,7 +1,7 @@ (herald "Electronic Purchase with Money Order Protocol with Key Hashing" (comment "Annotated with trust management formulas")) -(comment "CPSA 4.4.1") +(comment "CPSA 4.4.2") (comment "All input read from tst/epmo-key-hash.scm") (defprotocol epmo basic diff --git a/tst/epmo.tst b/tst/epmo.tst --- a/tst/epmo.tst +++ b/tst/epmo.tst @@ -1,7 +1,7 @@ (herald "Electronic Purchase with Money Order Protocol" (comment "Annotated with trust management formulas")) -(comment "CPSA 4.4.1") +(comment "CPSA 4.4.2") (comment "All input read from tst/epmo.scm") (defprotocol epmo basic diff --git a/tst/epmo_acctnum-key-hash.tst b/tst/epmo_acctnum-key-hash.tst --- a/tst/epmo_acctnum-key-hash.tst +++ b/tst/epmo_acctnum-key-hash.tst @@ -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 diff --git a/tst/expand.tst b/tst/expand.tst --- a/tst/expand.tst +++ b/tst/expand.tst @@ -1,4 +1,4 @@ -(comment "CPSA 4.4.1") +(comment "CPSA 4.4.2") (comment "Expanded macros") (herald expand (expand) (comment "test macro expansion")) diff --git a/tst/facts.tst b/tst/facts.tst --- a/tst/facts.tst +++ b/tst/facts.tst @@ -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 diff --git a/tst/factvar.tst b/tst/factvar.tst --- a/tst/factvar.tst +++ b/tst/factvar.tst @@ -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 diff --git a/tst/ffgg.tst b/tst/ffgg.tst --- a/tst/ffgg.tst +++ b/tst/ffgg.tst @@ -1,7 +1,7 @@ (herald "The ffgg Protocol" (comment "From A Necessarily Parallel Attack by Jon K. Millen")) -(comment "CPSA 4.4.1") +(comment "CPSA 4.4.2") (comment "All input read from tst/ffgg.scm") (defprotocol ffgg basic diff --git a/tst/fluffy_draft03_gske.tst b/tst/fluffy_draft03_gske.tst --- a/tst/fluffy_draft03_gske.tst +++ b/tst/fluffy_draft03_gske.tst @@ -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 diff --git a/tst/fragile_pruning.tst b/tst/fragile_pruning.tst --- a/tst/fragile_pruning.tst +++ b/tst/fragile_pruning.tst @@ -1,4 +1,4 @@ -(comment "CPSA 4.4.1") +(comment "CPSA 4.4.2") (comment "All input read from tst/fragile_pruning.scm") (defprotocol fragile_pruning basic diff --git a/tst/goals.tst b/tst/goals.tst --- a/tst/goals.tst +++ b/tst/goals.tst @@ -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 diff --git a/tst/hashtest-key-hash.tst b/tst/hashtest-key-hash.tst --- a/tst/hashtest-key-hash.tst +++ b/tst/hashtest-key-hash.tst @@ -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 diff --git a/tst/hashtest.tst b/tst/hashtest.tst --- a/tst/hashtest.tst +++ b/tst/hashtest.tst @@ -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 diff --git a/tst/incompleteness_example.tst b/tst/incompleteness_example.tst --- a/tst/incompleteness_example.tst +++ b/tst/incompleteness_example.tst @@ -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 diff --git a/tst/isoreject-corrected.tst b/tst/isoreject-corrected.tst --- a/tst/isoreject-corrected.tst +++ b/tst/isoreject-corrected.tst @@ -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 diff --git a/tst/isoreject.tst b/tst/isoreject.tst --- a/tst/isoreject.tst +++ b/tst/isoreject.tst @@ -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 diff --git a/tst/kelly1.tst b/tst/kelly1.tst --- a/tst/kelly1.tst +++ b/tst/kelly1.tst @@ -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 diff --git a/tst/kerberos.tst b/tst/kerberos.tst --- a/tst/kerberos.tst +++ b/tst/kerberos.tst @@ -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 diff --git a/tst/locn_envelope.tst b/tst/locn_envelope.tst --- a/tst/locn_envelope.tst +++ b/tst/locn_envelope.tst @@ -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") diff --git a/tst/mass.tst b/tst/mass.tst --- a/tst/mass.tst +++ b/tst/mass.tst @@ -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 diff --git a/tst/mass2.tst b/tst/mass2.tst --- a/tst/mass2.tst +++ b/tst/mass2.tst @@ -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 diff --git a/tst/missing_contraction.tst b/tst/missing_contraction.tst --- a/tst/missing_contraction.tst +++ b/tst/missing_contraction.tst @@ -1,4 +1,4 @@ -(comment "CPSA 4.4.1") +(comment "CPSA 4.4.2") (comment "All input read from tst/missing_contraction.scm") (defprotocol missing-contraction basic diff --git a/tst/neq_test.tst b/tst/neq_test.tst --- a/tst/neq_test.tst +++ b/tst/neq_test.tst @@ -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 diff --git a/tst/neuman-stubblebine-reauth.tst b/tst/neuman-stubblebine-reauth.tst --- a/tst/neuman-stubblebine-reauth.tst +++ b/tst/neuman-stubblebine-reauth.tst @@ -1,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 diff --git a/tst/neuman-stubblebine.tst b/tst/neuman-stubblebine.tst --- a/tst/neuman-stubblebine.tst +++ b/tst/neuman-stubblebine.tst @@ -1,4 +1,4 @@ -(comment "CPSA 4.4.1") +(comment "CPSA 4.4.2") (comment "All input read from tst/neuman-stubblebine.scm") (defprotocol neuman-stubblebine basic diff --git a/tst/no_contraction.tst b/tst/no_contraction.tst --- a/tst/no_contraction.tst +++ b/tst/no_contraction.tst @@ -1,4 +1,4 @@ -(comment "CPSA 4.4.1") +(comment "CPSA 4.4.2") (comment "All input read from tst/no_contraction.scm") (defprotocol no-contraction basic diff --git a/tst/non_transforming.tst b/tst/non_transforming.tst --- a/tst/non_transforming.tst +++ b/tst/non_transforming.tst @@ -1,4 +1,4 @@ -(comment "CPSA 4.4.1") +(comment "CPSA 4.4.2") (comment "All input read from tst/non_transforming.scm") (defprotocol non_transforming basic diff --git a/tst/nonaug-prune.tst b/tst/nonaug-prune.tst --- a/tst/nonaug-prune.tst +++ b/tst/nonaug-prune.tst @@ -1,4 +1,4 @@ -(comment "CPSA 4.4.1") +(comment "CPSA 4.4.2") (comment "All input read from tst/nonaug-prune.scm") (defprotocol nonaug-prune basic diff --git a/tst/ns-l.tst b/tst/ns-l.tst --- a/tst/ns-l.tst +++ b/tst/ns-l.tst @@ -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 diff --git a/tst/ns-rebinding.tst b/tst/ns-rebinding.tst --- a/tst/ns-rebinding.tst +++ b/tst/ns-rebinding.tst @@ -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 diff --git a/tst/ns.tst b/tst/ns.tst --- a/tst/ns.tst +++ b/tst/ns.tst @@ -1,6 +1,6 @@ (herald "Needham-Schroeder Public-Key Protocol Variants") -(comment "CPSA 4.4.1") +(comment "CPSA 4.4.2") (comment "All input read from tst/ns.scm") (defprotocol ns basic diff --git a/tst/nsl3.tst b/tst/nsl3.tst --- a/tst/nsl3.tst +++ b/tst/nsl3.tst @@ -1,6 +1,6 @@ (herald "Three Party Needham-Schroeder-Lowe Protocol") -(comment "CPSA 4.4.1") +(comment "CPSA 4.4.2") (comment "All input read from tst/nsl3.scm") (defprotocol nsl3 basic diff --git a/tst/nslsk.tst b/tst/nslsk.tst --- a/tst/nslsk.tst +++ b/tst/nslsk.tst @@ -1,6 +1,6 @@ (herald "Needham-Schroeder-Lowe Protocol with symmetric encryption") -(comment "CPSA 4.4.1") +(comment "CPSA 4.4.2") (comment "All input read from tst/nslsk.scm") (defprotocol nslsk basic diff --git a/tst/open-closed-multiloc.tst b/tst/open-closed-multiloc.tst --- a/tst/open-closed-multiloc.tst +++ b/tst/open-closed-multiloc.tst @@ -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") diff --git a/tst/open-closed-tag.tst b/tst/open-closed-tag.tst --- a/tst/open-closed-tag.tst +++ b/tst/open-closed-tag.tst @@ -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") diff --git a/tst/open-closed.tst b/tst/open-closed.tst --- a/tst/open-closed.tst +++ b/tst/open-closed.tst @@ -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") diff --git a/tst/or.tst b/tst/or.tst --- a/tst/or.tst +++ b/tst/or.tst @@ -1,7 +1,7 @@ (herald "Otway-Rees Protocol" (comment "Standard version using variables of sort mesg")) -(comment "CPSA 4.4.1") +(comment "CPSA 4.4.2") (comment "All input read from tst/or.scm") (defprotocol or basic diff --git a/tst/ordered.tst b/tst/ordered.tst --- a/tst/ordered.tst +++ b/tst/ordered.tst @@ -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 diff --git a/tst/pca.tst b/tst/pca.tst --- a/tst/pca.tst +++ b/tst/pca.tst @@ -1,7 +1,7 @@ (herald "Privacy Certificate Authority" (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") diff --git a/tst/pen-non-orig-test.tst b/tst/pen-non-orig-test.tst --- a/tst/pen-non-orig-test.tst +++ b/tst/pen-non-orig-test.tst @@ -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 diff --git a/tst/pfs-via-pubkey.tst b/tst/pfs-via-pubkey.tst --- a/tst/pfs-via-pubkey.tst +++ b/tst/pfs-via-pubkey.tst @@ -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 diff --git a/tst/pkinit.tst b/tst/pkinit.tst --- a/tst/pkinit.tst +++ b/tst/pkinit.tst @@ -1,6 +1,6 @@ (herald "Kerberos PK init") -(comment "CPSA 4.4.1") +(comment "CPSA 4.4.2") (comment "All input read from tst/pkinit.scm") (defprotocol pkinit basic diff --git a/tst/preprocess.tst b/tst/preprocess.tst --- a/tst/preprocess.tst +++ b/tst/preprocess.tst @@ -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 diff --git a/tst/print.tst b/tst/print.tst --- a/tst/print.tst +++ b/tst/print.tst @@ -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 diff --git a/tst/prottrans.tst b/tst/prottrans.tst --- a/tst/prottrans.tst +++ b/tst/prottrans.tst @@ -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 diff --git a/tst/pruning1.tst b/tst/pruning1.tst --- a/tst/pruning1.tst +++ b/tst/pruning1.tst @@ -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 diff --git a/tst/puzzle_example.tst b/tst/puzzle_example.tst --- a/tst/puzzle_example.tst +++ b/tst/puzzle_example.tst @@ -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 diff --git a/tst/reflect.tst b/tst/reflect.tst --- a/tst/reflect.tst +++ b/tst/reflect.tst @@ -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 diff --git a/tst/renamings.tst b/tst/renamings.tst --- a/tst/renamings.tst +++ b/tst/renamings.tst @@ -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 diff --git a/tst/role_uniq.tst b/tst/role_uniq.tst --- a/tst/role_uniq.tst +++ b/tst/role_uniq.tst @@ -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 diff --git a/tst/rule-node.tst b/tst/rule-node.tst --- a/tst/rule-node.tst +++ b/tst/rule-node.tst @@ -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 diff --git a/tst/rule-order.tst b/tst/rule-order.tst --- a/tst/rule-order.tst +++ b/tst/rule-order.tst @@ -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 diff --git a/tst/sigenc.tst b/tst/sigenc.tst --- a/tst/sigenc.tst +++ b/tst/sigenc.tst @@ -1,7 +1,7 @@ (herald "Signed Encrypted Message Example" (comment "Shows examples of key usage of asymmetric keys")) -(comment "CPSA 4.4.1") +(comment "CPSA 4.4.2") (comment "All input read from tst/sigenc.scm") (defprotocol mult-keys-sig-enc basic diff --git a/tst/sorted_epmo_acctnum.tst b/tst/sorted_epmo_acctnum.tst --- a/tst/sorted_epmo_acctnum.tst +++ b/tst/sorted_epmo_acctnum.tst @@ -4,7 +4,7 @@ "This version uses sorts to avoid confusion" "between a nonce and other data")) -(comment "CPSA 4.4.1") +(comment "CPSA 4.4.2") (comment "All input read from tst/sorted_epmo_acctnum.scm") (comment "Strand count bounded at 12") diff --git a/tst/sts.tst b/tst/sts.tst --- a/tst/sts.tst +++ b/tst/sts.tst @@ -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") diff --git a/tst/sts_unflip.tst b/tst/sts_unflip.tst --- a/tst/sts_unflip.tst +++ b/tst/sts_unflip.tst @@ -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 diff --git a/tst/sts_weak.tst b/tst/sts_weak.tst --- a/tst/sts_weak.tst +++ b/tst/sts_weak.tst @@ -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 diff --git a/tst/subatomic-open-closed-test-genrule.tst b/tst/subatomic-open-closed-test-genrule.tst --- a/tst/subatomic-open-closed-test-genrule.tst +++ b/tst/subatomic-open-closed-test-genrule.tst @@ -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") diff --git a/tst/subatomic-open-closed.tst b/tst/subatomic-open-closed.tst --- a/tst/subatomic-open-closed.tst +++ b/tst/subatomic-open-closed.tst @@ -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") diff --git a/tst/sync_locn_envelope.tst b/tst/sync_locn_envelope.tst --- a/tst/sync_locn_envelope.tst +++ b/tst/sync_locn_envelope.tst @@ -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") diff --git a/tst/targetterms1.tst b/tst/targetterms1.tst --- a/tst/targetterms1.tst +++ b/tst/targetterms1.tst @@ -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 diff --git a/tst/targetterms2.tst b/tst/targetterms2.tst --- a/tst/targetterms2.tst +++ b/tst/targetterms2.tst @@ -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 diff --git a/tst/targetterms6.tst b/tst/targetterms6.tst --- a/tst/targetterms6.tst +++ b/tst/targetterms6.tst @@ -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 diff --git a/tst/targetterms8.tst b/tst/targetterms8.tst --- a/tst/targetterms8.tst +++ b/tst/targetterms8.tst @@ -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 diff --git a/tst/thisthat.tst b/tst/thisthat.tst --- a/tst/thisthat.tst +++ b/tst/thisthat.tst @@ -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 diff --git a/tst/tickle-unique.tst b/tst/tickle-unique.tst --- a/tst/tickle-unique.tst +++ b/tst/tickle-unique.tst @@ -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 diff --git a/tst/timestamping.tst b/tst/timestamping.tst --- a/tst/timestamping.tst +++ b/tst/timestamping.tst @@ -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 diff --git a/tst/trust-anchor.tst b/tst/trust-anchor.tst --- a/tst/trust-anchor.tst +++ b/tst/trust-anchor.tst @@ -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 diff --git a/tst/ugo.scm b/tst/ugo.scm new file mode 100644 --- /dev/null +++ b/tst/ugo.scm @@ -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))) diff --git a/tst/ugo.tst b/tst/ugo.tst new file mode 100644 --- /dev/null +++ b/tst/ugo.tst @@ -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") diff --git a/tst/uncarried_keys.tst b/tst/uncarried_keys.tst --- a/tst/uncarried_keys.tst +++ b/tst/uncarried_keys.tst @@ -1,4 +1,4 @@ -(comment "CPSA 4.4.1") +(comment "CPSA 4.4.2") (comment "All input read from tst/uncarried_keys.scm") (defprotocol uncarried-keys basic diff --git a/tst/unilateral.tst b/tst/unilateral.tst --- a/tst/unilateral.tst +++ b/tst/unilateral.tst @@ -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 diff --git a/tst/uniq-gen-test.tst b/tst/uniq-gen-test.tst --- a/tst/uniq-gen-test.tst +++ b/tst/uniq-gen-test.tst @@ -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 diff --git a/tst/uo.tst b/tst/uo.tst --- a/tst/uo.tst +++ b/tst/uo.tst @@ -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 diff --git a/tst/wang-hash.tst b/tst/wang-hash.tst --- a/tst/wang-hash.tst +++ b/tst/wang-hash.tst @@ -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") diff --git a/tst/wang-key-hash.tst b/tst/wang-key-hash.tst --- a/tst/wang-key-hash.tst +++ b/tst/wang-key-hash.tst @@ -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") diff --git a/tst/weird.tst b/tst/weird.tst --- a/tst/weird.tst +++ b/tst/weird.tst @@ -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 diff --git a/tst/wide-mouth-frog-scyther.tst b/tst/wide-mouth-frog-scyther.tst --- a/tst/wide-mouth-frog-scyther.tst +++ b/tst/wide-mouth-frog-scyther.tst @@ -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 diff --git a/tst/wide-mouth-frog.tst b/tst/wide-mouth-frog.tst --- a/tst/wide-mouth-frog.tst +++ b/tst/wide-mouth-frog.tst @@ -1,7 +1,7 @@ (herald "Wide-Mouth Frog Protocol" (comment "This protocol has an infinite number of shapes")) -(comment "CPSA 4.4.1") +(comment "CPSA 4.4.2") (comment "All input read from tst/wide-mouth-frog.lsp") (defprotocol wide-mouth-frog basic diff --git a/tst/wonthull.tst b/tst/wonthull.tst --- a/tst/wonthull.tst +++ b/tst/wonthull.tst @@ -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") diff --git a/tst/wonthull2.tst b/tst/wonthull2.tst --- a/tst/wonthull2.tst +++ b/tst/wonthull2.tst @@ -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") diff --git a/tst/wonthull3.tst b/tst/wonthull3.tst --- a/tst/wonthull3.tst +++ b/tst/wonthull3.tst @@ -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 diff --git a/tst/woolam.tst b/tst/woolam.tst --- a/tst/woolam.tst +++ b/tst/woolam.tst @@ -1,6 +1,6 @@ (herald "Woo-Lam Protocol") -(comment "CPSA 4.4.1") +(comment "CPSA 4.4.2") (comment "All input read from tst/woolam.scm") (defprotocol woolam basic diff --git a/tst/yahalom-6.3.6.tst b/tst/yahalom-6.3.6.tst --- a/tst/yahalom-6.3.6.tst +++ b/tst/yahalom-6.3.6.tst @@ -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") diff --git a/tst/yahalom.tst b/tst/yahalom.tst --- a/tst/yahalom.tst +++ b/tst/yahalom.tst @@ -1,6 +1,6 @@ (herald "Yahalom Protocol Without Forwarding" (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")