diff --git a/ChangeLog b/ChangeLog --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,41 @@ +2019-03-18 John D. Ramsdell + + * cpsa.cabal (Version): Tagged as 3.6.2 + +2019-02-22 John D. Ramsdell + + * src/CPSA/Lib/Reduction.hs (addAnnoKey): Added structured + annotations to skeleton output to facilitate post processing + programs besides cpsagraph. The new keys are (aborted), + (satisfied-all), and (dead). + +2019-02-04 John D. Ramsdell + + * src/CPSA/Lib/Reduction.hs (step): Changed default depth bound + to zero representing no bound and ignored the check when the bound + is not positive. This matches what is documented in the manual. + +2019-01-31 John D. Ramsdell + + * src/CPSA/Lib/Loader.hs (badKey): Added checks for bad keys in + alists for skeletons ("defstrand" and "deflistener") and protocols + ("defrole" and "defrule"). + +2018-11-28 John D. Ramsdell + + * src/CPSA/Lib/Protocol.hs (AForm): Added the leads-to predicate + to the goal language. + +2018-11-19 John D. Ramsdell + + * src/CPSA/Lib/Printer.hs (formula): Added special pretty + printing rules for formulas in defgoal and defrule. + +2018-11-09 John D. Ramsdell + + * src/CPSA/SAS/SAS.hs (loadPOV): Use a preskeleton as a POV + instead of insisting on using a skeleton. + 2018-08-29 John D. Ramsdell * cpsa.cabal (Version): Tagged as 3.6.1 diff --git a/NEWS b/NEWS --- a/NEWS +++ b/NEWS @@ -1,5 +1,14 @@ CPSA NEWS + March, 2019: + +* Release 3.6.2 adds the leads-to predicate to the rule language, adds + better checks for malformed input, and fixes a bug so that now the + default depth is infinite as is specified in the manual. It adds + structured annotations to skeleton output to facilitate post + processing programs besides cpsagraph. The sources for OCaml + programs for processing CPSA input and output are now included. + August, 2018: * Release 3.6.1 is a bug fix release. It includes updates to the CPSA diff --git a/cpsa.cabal b/cpsa.cabal --- a/cpsa.cabal +++ b/cpsa.cabal @@ -1,5 +1,5 @@ Name: cpsa -Version: 3.6.1 +Version: 3.6.2 Maintainer: mliskov@mitre.org Cabal-Version: >= 1.6 License: BSD3 @@ -77,6 +77,12 @@ Makefile ChangeLog README.txt NEWS ghci cpsatst setup.bat src/cpsa.el src/cpsaops.scm src/cpsa.pl src/pp.pl src/sexpr.pl src/ghcmemlimit src/cpsajson.py src/split.py + src/ocaml/Makefile src/ocaml/README src/ocaml/cpsa.d.itarget + src/ocaml/cpsa.itarget src/ocaml/cpsa.mllib src/ocaml/cpsa.mltop + src/ocaml/cpsa.odocl src/ocaml/expand.ml src/ocaml/main.ml + src/ocaml/main.mli src/ocaml/pp.ml src/ocaml/reader.ml + src/ocaml/reader.mli src/ocaml/scanner.mll src/ocaml/sexpr.ml + src/ocaml/sexpr.mli src/ocaml/sexpr_type.ml tst/checktst tst/updatetst tst/graphtst tst/Makefile tst/Make.hs tst/README tst/axiom2.scm tst/axiom2.tst tst/blanchet.scm tst/blanchet.tst diff --git a/doc/cpsamanual.pdf b/doc/cpsamanual.pdf Binary files a/doc/cpsamanual.pdf and b/doc/cpsamanual.pdf differ diff --git a/doc/examples/blanchet.xhtml b/doc/examples/blanchet.xhtml --- a/doc/examples/blanchet.xhtml +++ b/doc/examples/blanchet.xhtml @@ -1,5 +1,5 @@ - + Blanchet's Simple Example Protocol @@ -12,7 +12,7 @@ 
(herald "Blanchet's Simple Example Protocol"
   (comment "There is a flaw in this protocol by design"))
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.2")
 (comment "All input read from blanchet.scm")

Trees: 0 4 6 11 14 18 23 25.

@@ -852,6 +852,7 @@ (comment "From the responders's perspective, is the secret leaked?") (label 11) (unrealized (0 0) (1 0)) + (origs (d (0 1))) (preskeleton) (comment "Not a skeleton")) @@ -1816,6 +1817,7 @@ (comment "From the responders's perspective, is the secret leaked?") (label 25) (unrealized (0 0) (1 0)) + (origs (d (0 1))) (preskeleton) (comment "Not a skeleton")) diff --git a/doc/examples/bltk_or.xhtml b/doc/examples/bltk_or.xhtml --- a/doc/examples/bltk_or.xhtml +++ b/doc/examples/bltk_or.xhtml @@ -1,5 +1,5 @@ - + Otway-Rees Protocol @@ -13,7 +13,7 @@ 
(herald "Otway-Rees Protocol"
   (comment "Standard version using variables of sort mesg")
   (algebra diffie-hellman))
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.2")
 (comment "All input read from bltk_or.scm")

Tree 0.

diff --git a/doc/examples/dh_mim.xhtml b/doc/examples/dh_mim.xhtml # file too large to diff: doc/examples/dh_mim.xhtml diff --git a/doc/examples/envelope.xhtml b/doc/examples/envelope.xhtml --- a/doc/examples/envelope.xhtml +++ b/doc/examples/envelope.xhtml @@ -1,5 +1,5 @@ - + Envelope Protocol @@ -11,7 +11,7 @@ 
(herald "Envelope Protocol" (bound 20))
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.2")
 (comment "All input read from envelope.scm")
 (comment "Strand count bounded at 20")
@@ -495,6 +495,7 @@ (uniq-orig v n tno esk) (label 0) (unrealized (0 0) (1 0) (2 5)) + (origs (esk (2 0)) (n (2 2)) (tno (2 2)) (v (2 6))) (preskeleton) (comment "Not a skeleton")) @@ -14919,6 +14920,7 @@ (uniq-orig v n tno esk) (label 59) (unrealized (0 0) (1 5)) + (origs (esk (1 0)) (n (1 2)) (tno (1 2)) (v (1 6))) (preskeleton) (comment "Not a skeleton")) diff --git a/doc/examples/eq_test.xhtml b/doc/examples/eq_test.xhtml --- a/doc/examples/eq_test.xhtml +++ b/doc/examples/eq_test.xhtml @@ -1,5 +1,5 @@ - + Equality constraint test protocol @@ -13,7 +13,7 @@ 
(herald "Equality constraint test protocol"
   (comment "First skeleton should have a shape,"
     "second, and hird should be dead."))
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.2")
 (comment "All input read from eq_test.scm")

Trees: 0 2 4.

@@ -295,6 +295,7 @@ (uniq-orig n1 n2) (label 4) (unrealized (0 1)) + (origs (n1 (0 0)) (n2 (0 0))) (preskeleton) (comment "Not a skeleton")) diff --git a/doc/examples/ffgg.xhtml b/doc/examples/ffgg.xhtml --- a/doc/examples/ffgg.xhtml +++ b/doc/examples/ffgg.xhtml @@ -1,5 +1,5 @@ - + The ffgg Protocol @@ -12,7 +12,7 @@ 
(herald "The ffgg Protocol"
   (comment "From A Necessarily Parallel Attack by Jon K. Millen"))
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.2")
 (comment "All input read from ffgg.scm")

Tree 0.

@@ -110,6 +110,7 @@ (uniq-orig m) (label 0) (unrealized (1 0)) + (origs (m (0 2))) (preskeleton) (comment "Not a skeleton")) diff --git a/doc/examples/fnof_test.xhtml b/doc/examples/fnof_test.xhtml --- a/doc/examples/fnof_test.xhtml +++ b/doc/examples/fnof_test.xhtml @@ -1,5 +1,5 @@ - + Function constraint test protocol @@ -12,7 +12,7 @@ 
(herald "Function constraint test protocol"
   (comment "Skeletons 2, 4, and 7 should have no shapes."))
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.2")
 (comment "All input read from fnof_test.scm")

Trees: 0 2 3 5 6 8 10.

@@ -248,6 +248,7 @@ (uniq-orig n1) (label 3) (unrealized) + (origs (n1 (0 0))) (preskeleton) (comment "Not a skeleton")) @@ -350,6 +351,7 @@ (uniq-orig n1) (label 5) (unrealized) + (origs (n1 (0 0))) (comment "Input cannot be made into a skeleton--nothing to do"))

Tree 6.

diff --git a/doc/examples/fnof_yahalom.xhtml b/doc/examples/fnof_yahalom.xhtml --- a/doc/examples/fnof_yahalom.xhtml +++ b/doc/examples/fnof_yahalom.xhtml @@ -1,5 +1,5 @@ - + Yahalom Protocol with Forwarding Removed, using fnof to emulate ltk function @@ -13,7 +13,7 @@ 
(herald
   "Yahalom Protocol with Forwarding Removed, using fnof to emulate ltk function"
   (bound 12))
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.2")
 (comment "All input read from fnof_yahalom.scm")

Trees: 0 4 10 15.

diff --git a/doc/examples/goals.xhtml b/doc/examples/goals.xhtml --- a/doc/examples/goals.xhtml +++ b/doc/examples/goals.xhtml @@ -1,5 +1,5 @@ - + goals @@ -11,7 +11,7 @@ 
(herald goals)
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.2")
 (comment "All input read from goals.scm")

Trees: 0 2 4 6 8 17 19 21 23 26 28 33 41.

@@ -297,7 +297,7 @@ (parent 2) (unrealized) (shape) - (satisfies (no (b b) (n1 n1) (z0 0))) + (satisfies yes) (maps ((0) ((b b) (n1 n1) (a a) (n2 n2)))) (origs (n1 (0 0)))) @@ -729,6 +729,7 @@ "Secrecy goal: nonce n1 not revealed") (label 8) (unrealized (0 0) (1 1)) + (origs (n1 (1 0))) (preskeleton) (comment "Not a skeleton")) @@ -2212,6 +2213,7 @@ "Failed secrecy goal: nonce n2 not revealed") (label 28) (unrealized (0 0) (1 2)) + (origs (n2 (1 1))) (preskeleton) (comment "Not a skeleton")) @@ -3235,6 +3237,7 @@ (comment "Shows typeflaw in typeless NSL") (label 41) (unrealized (0 0)) + (origs (n2 (1 1))) (preskeleton) (comment "Not a skeleton")) diff --git a/doc/examples/iadh_um.xhtml b/doc/examples/iadh_um.xhtml # file too large to diff: doc/examples/iadh_um.xhtml diff --git a/doc/examples/kerb.xhtml b/doc/examples/kerb.xhtml --- a/doc/examples/kerb.xhtml +++ b/doc/examples/kerb.xhtml @@ -1,5 +1,5 @@ - + kerb-flawed @@ -10,7 +10,7 @@ -
(comment "CPSA 3.6.0")
+
(comment "CPSA 3.6.2")
 (comment "All input read from kerb.scm")

 
 
Trees: 0 5.

@@ -112,6 +112,7 @@
   (uniq-orig m n)
   (label 0)
   (unrealized (0 1) (1 0))
+  (origs (n (0 0)) (m (0 2)))
   (preskeleton)
   (comment "Not a skeleton"))
@@ -483,6 +484,7 @@ (uniq-orig m n) (label 5) (unrealized (0 1) (1 0)) + (origs (n (0 0)) (m (0 2))) (preskeleton) (comment "Not a skeleton")) diff --git a/doc/examples/lt_test.xhtml b/doc/examples/lt_test.xhtml --- a/doc/examples/lt_test.xhtml +++ b/doc/examples/lt_test.xhtml @@ -1,5 +1,5 @@ - + Less-than constraint test protocol @@ -13,7 +13,7 @@ 
(herald "Less-than constraint test protocol"
   (comment "First and third skeletons should have a shape,"
     "second and fourth should be dead."))
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.2")
 (comment "All input read from lt_test.scm")

Trees: 0 2 3 5.

diff --git a/doc/examples/neq_test.xhtml b/doc/examples/neq_test.xhtml --- a/doc/examples/neq_test.xhtml +++ b/doc/examples/neq_test.xhtml @@ -1,5 +1,5 @@ - + Inequality constraint test protocol @@ -13,7 +13,7 @@ 
(herald "Inequality constraint test protocol"
   (comment "First skeleton should have a shape,"
     "second, and hird should be dead."))
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.2")
 (comment "All input read from neq_test.scm")

Trees: 0 2 3.

diff --git a/doc/examples/ns.xhtml b/doc/examples/ns.xhtml --- a/doc/examples/ns.xhtml +++ b/doc/examples/ns.xhtml @@ -1,5 +1,5 @@ - + Needham-Schroeder Public-Key Protocol @@ -13,7 +13,7 @@ 
(herald "Needham-Schroeder Public-Key Protocol"
   (comment "This protocol contains a man-in-the-middle"
     "attack discovered by Galvin Lowe."))
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.2")
 (comment "All input read from ns.scm")

Trees: 0 3.

diff --git a/doc/examples/or.xhtml b/doc/examples/or.xhtml --- a/doc/examples/or.xhtml +++ b/doc/examples/or.xhtml @@ -1,5 +1,5 @@ - + Otway-Rees Protocol @@ -12,7 +12,7 @@ 
(herald "Otway-Rees Protocol"
   (comment "Standard version using variables of sort mesg"))
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.2")
 (comment "All input read from or.scm")

Tree 0.

diff --git a/doc/examples/pkinit.xhtml b/doc/examples/pkinit.xhtml --- a/doc/examples/pkinit.xhtml +++ b/doc/examples/pkinit.xhtml @@ -1,5 +1,5 @@ - + Kerberos PKINIT @@ -11,7 +11,7 @@ 
(herald "Kerberos PKINIT")
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.2")
 (comment "All input read from pkinit.scm")

Trees: 0 2 8 13 16 23.

@@ -1143,6 +1143,7 @@ (non (privk c))) (= c c-0)))) (label 13) (unrealized (1 1)) + (origs (n1-0 (1 0)) (n2-0 (1 0)) (k (0 1)) (ak (0 1))) (preskeleton) (comment "Not a skeleton")) @@ -1418,6 +1419,7 @@ (non (privk c))) (exists ((z-1 strd)) (p "client" z-1 2))))) (label 16) (unrealized (1 1)) + (origs (n1-0 (1 0)) (n2-0 (1 0)) (k (0 1)) (ak (0 1))) (preskeleton) (comment "Not a skeleton")) @@ -1978,6 +1980,7 @@ (non (privk c))) (exists ((z-1 strd)) (p "client" z-1 2))))) (label 23) (unrealized (1 1)) + (origs (n1-0 (1 0)) (n2-0 (1 0)) (k (0 1)) (ak (0 1))) (preskeleton) (comment "Not a skeleton")) diff --git a/doc/examples/plaindh.xhtml b/doc/examples/plaindh.xhtml --- a/doc/examples/plaindh.xhtml +++ b/doc/examples/plaindh.xhtml @@ -1,5 +1,5 @@ - + Plain diffie-hellman protocol with challenge-response @@ -12,7 +12,7 @@ 
(herald "Plain diffie-hellman protocol with challenge-response"
   (algebra diffie-hellman))
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.2")
 (comment "All input read from plaindh.scm")

Tree 0.

diff --git a/doc/examples/priority_test.xhtml b/doc/examples/priority_test.xhtml --- a/doc/examples/priority_test.xhtml +++ b/doc/examples/priority_test.xhtml @@ -1,5 +1,5 @@ - + Receive priority test protocol @@ -11,7 +11,7 @@ 
(herald "Receive priority test protocol")
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.2")
 (comment "All input read from priority_test.scm")

Trees: 0 3.

diff --git a/doc/examples/station.xhtml b/doc/examples/station.xhtml --- a/doc/examples/station.xhtml +++ b/doc/examples/station.xhtml @@ -1,5 +1,5 @@ - + Station-to-station protocol @@ -11,7 +11,7 @@ 
(herald "Station-to-station protocol" (algebra diffie-hellman))
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.2")
 (comment "All input read from station.scm")

Trees: 0 10 20 23.

diff --git a/doc/examples/subsort_test.xhtml b/doc/examples/subsort_test.xhtml --- a/doc/examples/subsort_test.xhtml +++ b/doc/examples/subsort_test.xhtml @@ -1,5 +1,5 @@ - + Subsort constraint test protocol @@ -13,7 +13,7 @@ 
(herald "Subsort constraint test protocol"
   (comment "First, third, and fourth skeletons should have a shape,"
     "second should be dead."))
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.2")
 (comment "All input read from subsort_test.scm")

Trees: 0 2 3 5.

diff --git a/doc/examples/woolam.xhtml b/doc/examples/woolam.xhtml --- a/doc/examples/woolam.xhtml +++ b/doc/examples/woolam.xhtml @@ -1,5 +1,5 @@ - + Woo-Lam Protocol @@ -11,7 +11,7 @@ 
(herald "Woo-Lam Protocol")
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.2")
 (comment "All input read from woolam.scm")

Tree 0.

diff --git a/doc/examples/yahalom.xhtml b/doc/examples/yahalom.xhtml --- a/doc/examples/yahalom.xhtml +++ b/doc/examples/yahalom.xhtml @@ -1,5 +1,5 @@ - + Yahalom Protocol with Forwarding Removed @@ -12,7 +12,7 @@ 
(herald "Yahalom Protocol with Forwarding Removed"
   (algebra diffie-hellman) (bound 12))
-(comment "CPSA 3.6.0")
+(comment "CPSA 3.6.2")
 (comment "All input read from yahalom.scm")

Trees: 0 52.

diff --git a/src/CPSA/Lib/Characteristic.hs b/src/CPSA/Lib/Characteristic.hs --- a/src/CPSA/Lib/Characteristic.hs +++ b/src/CPSA/Lib/Characteristic.hs @@ -144,6 +144,7 @@ mkSkel pos p goals nmap g insts as comment = do let o = foldr (mkPrec nmap) [] as + let lto = foldr (mkLeadsTo nmap) [] as let nr = foldr mkNon [] as let ar = foldr mkPnon [] as let ur = foldr mkUniq [] as @@ -151,7 +152,7 @@ let decls = mkDcls nr ar ur gr let fs = foldr (mkFact nmap) [] as let prios = [] - let k = mkPreskel g p goals insts o [] decls fs comment prios Nothing [] + let k = mkPreskel g p goals insts o lto decls fs comment prios Nothing [] mapM_ (checkUniqAt nmap k) as case termsWellFormed $ (termsInDlist decls) ++ kterms k of False -> fail (shows pos "Terms in skeleton not well formed") @@ -168,6 +169,12 @@ mkPrec nmap (_, Prec n n') o = (nMapLookup n nmap, nMapLookup n' nmap) : o mkPrec _ _ o = o + +mkLeadsTo :: Eq t => [(t, Sid)] -> + (Pos, AForm t) -> [Pair] -> [Pair] +mkLeadsTo nmap (_, LeadsTo n n') o = + (nMapLookup n nmap, nMapLookup n' nmap) : o +mkLeadsTo _ _ o = o mkDcls :: [t] -> [t] -> [t] -> [t] -> SkelDeclList t mkDcls nr ar ur gr = diff --git a/src/CPSA/Lib/Cohort.hs b/src/CPSA/Lib/Cohort.hs --- a/src/CPSA/Lib/Cohort.hs +++ b/src/CPSA/Lib/Cohort.hs @@ -134,12 +134,12 @@ -- pos = p -- ek = encription key if ct is an encyption else nothing -- escape = esc(k, v, t) --- k' = k --- (s, p) = v and n +-- k = k' +-- n = v -- subst = sigma solved :: Algebra t p g s e c => t -> p -> [t] -> Set t -> Preskel t g s e -> Node -> s -> [(t,t)] -> Bool -solved ct pos eks escape k (s, p) subst absent = +solved ct pos eks escape k n subst absent = -- Condition 1 isAncestorInSet escape' t pos || derivable a escape' ct' || -- Condition 2 @@ -155,7 +155,7 @@ -- Condition 6: hack! length (kabsent k) > length absent where - v = vertex k (s, p) -- Look up vertex in k + v = vertex k n -- Look up vertex in k t = evt id erro errs (event v) -- Term at v erro = const $ assertError "Cohort.solved: got an outbound term" errs = const $ assertError "Cohort.solved: got a state synchronization term" diff --git a/src/CPSA/Lib/Displayer.hs b/src/CPSA/Lib/Displayer.hs --- a/src/CPSA/Lib/Displayer.hs +++ b/src/CPSA/Lib/Displayer.hs @@ -84,6 +84,9 @@ displayForm ctx (Prec (x, i) (y, j)) = L () [S () "prec", displayTerm ctx x, N () i, displayTerm ctx y, N () j] +displayForm ctx (LeadsTo (x, i) (y, j)) = + L () [S () "leads-to", displayTerm ctx x, N () i, + displayTerm ctx y, N () j] displayForm ctx (Non t) = L () [S () "non", displayTerm ctx t] displayForm ctx (Pnon t) = diff --git a/src/CPSA/Lib/Entry.hs b/src/CPSA/Lib/Entry.hs --- a/src/CPSA/Lib/Entry.hs +++ b/src/CPSA/Lib/Entry.hs @@ -99,7 +99,7 @@ optGoalsSat = False, optLimit = 2000, optBound = 12, - optDepth = 32, + optDepth = 0, optMargin = 72, optIndent = 2 } diff --git a/src/CPSA/Lib/Expand.hs b/src/CPSA/Lib/Expand.hs --- a/src/CPSA/Lib/Expand.hs +++ b/src/CPSA/Lib/Expand.hs @@ -114,7 +114,7 @@ macroExpand :: Monad m => [Macro] -> Pos -> Int -> SExpr Pos -> m (SExpr Pos) macroExpand _ pos limit _ - | limit <= 0 = fail (shows pos "Expansion limit exceded") + | limit <= 0 = fail (shows pos "Expansion limit exceeded") macroExpand macs pos limit sexpr@(L _ (S _ sym : xs)) = case macroExpand1 macs sym xs of Nothing -> return sexpr -- Nothing to do diff --git a/src/CPSA/Lib/Loader.hs b/src/CPSA/Lib/Loader.hs --- a/src/CPSA/Lib/Loader.hs +++ b/src/CPSA/Lib/Loader.hs @@ -311,7 +311,8 @@ t2 <- loadTerm vars False x2 p <- loadIntMax height x3 return (declInstAux [t1,t2] [p] stag) -loadRoleTermPairPlusMaybeOneLoc _ _ _ _ = fail ("Malformed pair of terms") +loadRoleTermPairPlusMaybeOneLoc _ _ _ x = fail + (shows (annotation x) "Malformed pair of terms") loadSkelTermPair :: (Algebra t p g s e c, Monad m) => [t] -> String -> SExpr Pos -> m (SkelDeclInst t) @@ -320,7 +321,8 @@ t1 <- loadTerm vars False x1 t2 <- loadTerm vars False x2 return (declInstAux [t1,t2] [] stag) -loadSkelTermPair _ _ _ = fail ("Malformed pair of terms") +loadSkelTermPair _ _ x = fail + (shows (annotation x) "Malformed pair of terms") loadRolePriority :: Monad m => Int -> SExpr Pos -> m (Int, Int) loadRolePriority n (L _ [N _ i, N _ p]) @@ -344,7 +346,7 @@ (g, xs) <- loadVars g [L pos [S pos "x", S pos "mesg"]] case xs of [x] -> return (g, mkRole "" [x] [In x, Out x] [] [] [] False) - _ -> fail "Loader.mkListenerRole: Expection one variable" + _ -> fail (shows pos "Loader.mkListenerRole: Expecting one term") -- Protocol Rules @@ -355,8 +357,11 @@ (g, r) <- loadRule prot g pos x (g, rs, comment) <- loadRules prot g xs return (g, r : rs, comment) +loadRules _ _ (L pos (S _ "defrole" : S _ name : _) : _) = + fail (shows pos ("defrole " ++ name ++ " misplaced")) loadRules _ g xs = do + badKey ["defrole", "defrule"] xs comment <- alist [] xs -- Ensure remaining is an alist return (g, [], comment) @@ -412,6 +417,14 @@ f (L _ (S _ head : _)) = head == key f _ = False +-- Complain if alist has a bad key +badKey :: Monad m => [String] -> [SExpr Pos] -> m () +badKey keys (L _ (S pos key : _) : xs) + | elem key keys = + fail (shows pos (key ++ " declaration too late in enclosing form")) + | otherwise = badKey keys xs +badKey _ _ = return () + loadTrace :: (Algebra t p g s e c, Monad m) => [t] -> [SExpr Pos] -> m [Event t] loadTrace vars xs = mapM (loadEvt vars) xs @@ -565,6 +578,7 @@ fail (shows pos "Malformed deflistener") loadInsts top p kvars gen insts xs = do + badKey ["defstrand", "deflistener"] xs _ <- alist [] xs -- Check syntax of xs others <- loadGenSkelDecls heights kvars (assocDecls xs) predefs <- loadAllPredefSkelDecls heights kvars xs @@ -1069,6 +1083,11 @@ t <- loadNodeTerm kvars w x t' <- loadNodeTerm kvars y z return (pos, Prec t t') +loadPrimary _ _ kvars (L pos [S _ "leads-to", w, x, y, z]) = + do + t <- loadNodeTerm kvars w x + t' <- loadNodeTerm kvars y z + return (pos, LeadsTo t t') loadPrimary _ p kvars (L pos [S _ "p", Q _ name, x, N _ h]) = do r <- lookupRole pos p name @@ -1150,6 +1169,9 @@ roleSpecific unbound (pos, Prec (z, _) (z', _)) | L.notElem z unbound && L.notElem z' unbound = return unbound | otherwise = fail (shows pos "Unbound variable in prec") +roleSpecific unbound (pos, LeadsTo (z, _) (z', _)) + | L.notElem z unbound && L.notElem z' unbound = return unbound + | otherwise = fail (shows pos "Unbound variable in leadsto") roleSpecific unbound (pos, Non t) | allBound unbound t = return unbound | otherwise = fail (shows pos "Unbound variable in non") diff --git a/src/CPSA/Lib/Main.hs b/src/CPSA/Lib/Main.hs --- a/src/CPSA/Lib/Main.hs +++ b/src/CPSA/Lib/Main.hs @@ -214,7 +214,7 @@ Option ['b'] ["bound"] (ReqArg Bound "INT") ("strand count bound (default " ++ show defaultStrandBound ++ ")"), Option ['d'] ["depth"] (ReqArg Depth "INT") - ("tree depth bound (default " ++ show defaultDepthBound ++ ")"), + ("tree depth bound (default unbounded)"), Option ['m'] ["margin"] (ReqArg Margin "INT") ("set output margin (default " ++ show (optMargin defaultOptions) ++ ")"), Option ['e'] ["expand"] (NoArg Expand) diff --git a/src/CPSA/Lib/Printer.hs b/src/CPSA/Lib/Printer.hs --- a/src/CPSA/Lib/Printer.hs +++ b/src/CPSA/Lib/Printer.hs @@ -23,30 +23,60 @@ -- occur, all breaks are forced. Also, breaks are only placed before -- strings and lists. CPSA protocols are handled specially. Each -- defrole is handled as are top-level lists. + +-- Update: there are special layout rules for formulas in defgoal's +-- and defrule's. pretty :: Printer a pretty indent (L _ (x@(S _ "defprotocol") : xs)) = loop [block indent x, str "("] xs where loop es [] = grp indent (reverse (str ")" : es)) - loop es (x@(S _ _):xs) = loop (block indent x : str " " : es) xs - loop es (x@(Q _ _):xs) = loop (block indent x : brk 1 : es) xs - loop es (x@(N _ _):xs) = loop (block indent x : str " " : es) xs - loop es (x@(L _ (S _ "defrole": _)):xs) = + loop es (x@(S _ _) : xs) = loop (block indent x : str " " : es) xs + loop es (x@(Q _ _) : xs) = loop (block indent x : brk 1 : es) xs + loop es (x@(N _ _) : xs) = loop (block indent x : str " " : es) xs + loop es (x@(L _ (S _ "defrole" : _)) : xs) = loop (group indent x : brk 1 : es) xs - loop es (x@(L _ _):xs) = loop (block indent x : brk 1 : es) xs -pretty indent x@(L _ (S _ "defmacro" : _)) = block indent x + loop es ((L _ (x@(S _ "defrule") : forms)) : xs) = + loop (formula indent x forms : brk 1 : es) xs + loop es (x@(L _ _) : xs) = loop (block indent x : brk 1 : es) xs +pretty indent (L _ (x@(S _ "defgoal") : forms)) = formula indent x forms +pretty indent x@(L _ (S _ "defmacro" : _)) = group indent x pretty indent x@(L _ (S _ "herald" : _)) = block indent x pretty indent x = group indent x +formula :: Int -> SExpr a -> [SExpr a] -> Pretty +formula indent x xs = + loop [block indent x, str "("] xs + where + loop es [] = grp indent (reverse (str ")" : es)) + loop es (L _ [S _ "forall", decs, + L _ [S _ "implies", antec, concl]] : xs) = + loop + (blo indent + [str "(forall", brk 1, block indent decs, brk 1, + grp indent + [str "(implies", brk 1, + block indent antec, brk 1, + disj indent concl], + str "))"] : brk 1 : es) + xs + loop es (x@(S _ _) : xs) = loop (block indent x : str " " : es) xs + loop es (x@(N _ _) : xs) = loop (block indent x : str " " : es) xs + loop es (x : xs) = loop (block indent x : brk 1 : es) xs + +disj :: Int -> SExpr a -> Pretty +disj indent x@(L _ (S _ "or" : _)) = group indent x +disj indent x = block indent x + group :: Printer a group indent (L _ (x:xs)) = loop [block indent x, str "("] xs where loop es [] = grp indent (reverse (str ")" : es)) - loop es (x@(S _ _):xs) = loop (block indent x : str " " : es) xs - loop es (x@(Q _ _):xs) = loop (block indent x : brk 1 : es) xs - loop es (x@(N _ _):xs) = loop (block indent x : str " " : es) xs - loop es (x@(L _ _):xs) = loop (block indent x : brk 1 : es) xs + loop es (x@(S _ _) : xs) = loop (block indent x : str " " : es) xs + loop es (x@(Q _ _) : xs) = loop (block indent x : brk 1 : es) xs + loop es (x@(N _ _) : xs) = loop (block indent x : str " " : es) xs + loop es (x@(L _ _) : xs) = loop (block indent x : brk 1 : es) xs group indent x = block indent x -- A pretty printer for interior lists using block style breaking. @@ -55,7 +85,7 @@ block _ (Q _ s) = str (showQuoted s "") block _ (N _ n) = str (show n) block _ (L _ []) = str "()" -block indent (L _ (x:xs)) = +block indent (L _ (x : xs)) = loop [block indent x, str "("] xs where loop es [] = blo indent (reverse (str ")" : es)) diff --git a/src/CPSA/Lib/Protocol.hs b/src/CPSA/Lib/Protocol.hs --- a/src/CPSA/Lib/Protocol.hs +++ b/src/CPSA/Lib/Protocol.hs @@ -395,6 +395,7 @@ = Length (Role t) t Int | Param (Role t) t Int t t -- role param first-height strand value | Prec (NodeTerm t) (NodeTerm t) + | LeadsTo (NodeTerm t) (NodeTerm t) | Non t | Pnon t | Uniq t @@ -419,6 +420,7 @@ aFormOrder (Length _ _ _) (Length _ _ _) = EQ aFormOrder (Length _ _ _) (Param _ _ _ _ _) = LT aFormOrder (Length _ _ _) (Prec _ _) = LT +aFormOrder (Length _ _ _) (LeadsTo _ _) = LT aFormOrder (Length _ _ _) (Non _) = LT aFormOrder (Length _ _ _) (Pnon _) = LT aFormOrder (Length _ _ _) (Uniq _) = LT @@ -430,6 +432,7 @@ aFormOrder (Param _ _ _ _ _) (Length _ _ _) = GT aFormOrder (Param _ _ _ _ _) (Param _ _ _ _ _) = EQ aFormOrder (Param _ _ _ _ _) (Prec _ _) = LT +aFormOrder (Param _ _ _ _ _) (LeadsTo _ _) = LT aFormOrder (Param _ _ _ _ _) (Non _) = LT aFormOrder (Param _ _ _ _ _) (Pnon _) = LT aFormOrder (Param _ _ _ _ _) (Uniq _) = LT @@ -441,6 +444,7 @@ aFormOrder (Prec _ _) (Length _ _ _) = GT aFormOrder (Prec _ _) (Param _ _ _ _ _) = GT aFormOrder (Prec _ _) (Prec _ _) = EQ +aFormOrder (Prec _ _) (LeadsTo _ _) = LT aFormOrder (Prec _ _) (Non _) = LT aFormOrder (Prec _ _) (Pnon _) = LT aFormOrder (Prec _ _) (Uniq _) = LT @@ -449,9 +453,22 @@ aFormOrder (Prec _ _) (Ugen _) = LT aFormOrder (Prec _ _) (AFact _ _) = LT aFormOrder (Prec _ _) (Equals _ _) = LT +aFormOrder (LeadsTo _ _) (Length _ _ _) = GT +aFormOrder (LeadsTo _ _) (Param _ _ _ _ _) = GT +aFormOrder (LeadsTo _ _) (Prec _ _) = GT +aFormOrder (LeadsTo _ _) (LeadsTo _ _) = EQ +aFormOrder (LeadsTo _ _) (Non _) = LT +aFormOrder (LeadsTo _ _) (Pnon _) = LT +aFormOrder (LeadsTo _ _) (Uniq _) = LT +aFormOrder (LeadsTo _ _) (UniqAt _ _) = LT +aFormOrder (LeadsTo _ _) (UgenAt _ _) = LT +aFormOrder (LeadsTo _ _) (Ugen _) = LT +aFormOrder (LeadsTo _ _) (AFact _ _) = LT +aFormOrder (LeadsTo _ _) (Equals _ _) = LT aFormOrder (Non _) (Length _ _ _) = GT aFormOrder (Non _) (Param _ _ _ _ _) = GT aFormOrder (Non _) (Prec _ _) = GT +aFormOrder (Non _) (LeadsTo _ _) = GT aFormOrder (Non _) (Non _) = EQ aFormOrder (Non _) (Pnon _) = LT aFormOrder (Non _) (Uniq _) = LT @@ -463,6 +480,7 @@ aFormOrder (Pnon _) (Length _ _ _) = GT aFormOrder (Pnon _) (Param _ _ _ _ _) = GT aFormOrder (Pnon _) (Prec _ _) = GT +aFormOrder (Pnon _) (LeadsTo _ _) = GT aFormOrder (Pnon _) (Non _) = GT aFormOrder (Pnon _) (Pnon _) = EQ aFormOrder (Pnon _) (Uniq _) = LT @@ -474,6 +492,7 @@ aFormOrder (Uniq _) (Length _ _ _) = GT aFormOrder (Uniq _) (Param _ _ _ _ _) = GT aFormOrder (Uniq _) (Prec _ _) = GT +aFormOrder (Uniq _) (LeadsTo _ _) = GT aFormOrder (Uniq _) (Non _) = GT aFormOrder (Uniq _) (Pnon _) = GT aFormOrder (Uniq _) (Uniq _) = EQ @@ -485,6 +504,7 @@ aFormOrder (UniqAt _ _) (Length _ _ _) = GT aFormOrder (UniqAt _ _) (Param _ _ _ _ _) = GT aFormOrder (UniqAt _ _) (Prec _ _) = GT +aFormOrder (UniqAt _ _) (LeadsTo _ _) = GT aFormOrder (UniqAt _ _) (Non _) = GT aFormOrder (UniqAt _ _) (Pnon _) = GT aFormOrder (UniqAt _ _) (Uniq _) = GT @@ -496,6 +516,7 @@ aFormOrder (UgenAt _ _) (Length _ _ _) = GT aFormOrder (UgenAt _ _) (Param _ _ _ _ _) = GT aFormOrder (UgenAt _ _) (Prec _ _) = GT +aFormOrder (UgenAt _ _) (LeadsTo _ _) = GT aFormOrder (UgenAt _ _) (Non _) = GT aFormOrder (UgenAt _ _) (Pnon _) = GT aFormOrder (UgenAt _ _) (Uniq _) = GT @@ -507,6 +528,7 @@ aFormOrder (Ugen _) (Length _ _ _) = GT aFormOrder (Ugen _) (Param _ _ _ _ _) = GT aFormOrder (Ugen _) (Prec _ _) = GT +aFormOrder (Ugen _) (LeadsTo _ _) = GT aFormOrder (Ugen _) (Non _) = GT aFormOrder (Ugen _) (Pnon _) = GT aFormOrder (Ugen _) (Uniq _) = GT @@ -518,6 +540,7 @@ aFormOrder (AFact _ _) (Length _ _ _) = GT aFormOrder (AFact _ _) (Param _ _ _ _ _) = GT aFormOrder (AFact _ _) (Prec _ _) = GT +aFormOrder (AFact _ _) (LeadsTo _ _) = GT aFormOrder (AFact _ _) (Non _) = GT aFormOrder (AFact _ _) (Pnon _) = GT aFormOrder (AFact _ _) (Uniq _) = GT @@ -529,6 +552,7 @@ aFormOrder (Equals _ _) (Length _ _ _) = GT aFormOrder (Equals _ _) (Param _ _ _ _ _) = GT aFormOrder (Equals _ _) (Prec _ _) = GT +aFormOrder (Equals _ _) (LeadsTo _ _) = GT aFormOrder (Equals _ _) (Non _) = GT aFormOrder (Equals _ _) (Pnon _) = GT aFormOrder (Equals _ _) (Uniq _) = GT @@ -542,6 +566,7 @@ aFreeVars vars (Length _ z _) = addVars vars z aFreeVars vars (Param _ _ _ z t) = addVars (addVars vars z) t aFreeVars vars (Prec (x, _) (y, _)) = addVars (addVars vars x) y +aFreeVars vars (LeadsTo (x, _) (y, _)) = addVars (addVars vars x) y aFreeVars vars (Non t) = addVars vars t aFreeVars vars (Pnon t) = addVars vars t aFreeVars vars (Uniq t) = addVars vars t diff --git a/src/CPSA/Lib/Reduction.hs b/src/CPSA/Lib/Reduction.hs --- a/src/CPSA/Lib/Reduction.hs +++ b/src/CPSA/Lib/Reduction.hs @@ -138,7 +138,7 @@ [] -> -- Input cannot be made into a skeleton do let lk = LPreskel k n 0 Nothing - wrt p h (commentPreskel lk [] (unrealized k) Ordinary + wrt p h (commentPreskel lk [] (unrealized k) Ordinary Nada "Input cannot be made into a skeleton--nothing to do") solve p h ks (n + 1) ks' -> @@ -150,8 +150,8 @@ do let lk = LPreskel k n (-1) Nothing let ks'' = L.nubBy (\k1 k2 -> isomorphic (gist k1) (gist k2)) ks' - wrt p h (commentPreskel lk [] (unrealized k) Ordinary - "Not a skeleton") + wrt p h (commentPreskel lk [] (unrealized k) Ordinary + Preskeleton "Not a skeleton") let lk_nums = zip [(n+1) .. (n+length(ks'))] ks'' let lks' = map (\(n', k')-> withParent k' n' lk) lk_nums begin p h ks (n + optLimit p) (n+length(ks'')+1) @@ -173,7 +173,7 @@ Just kids -> do wrt p h (commentPreskel lk [] (unrealized k) Ordinary - "Not closed under rules") + Nada "Not closed under rules") let (n', seen', todo', _) = foldl (next lk) (n, seen, todo, []) kids loop n' seen' todo' lks @@ -256,7 +256,7 @@ do let ns = unrealized (content lk) let shape = if null ns then Shape else Fringe - wrt p h (commentPreskel lk [] ns shape "satisfies all") + wrt p h (commentPreskel lk [] ns shape SatisfiesAll "satisfies all") step p h ks m oseen n seen todo tobig reducts | size <= 0 = -- Interpret empty reducts do @@ -264,12 +264,13 @@ let shape = if null ns then Shape else Ordinary let live = null $ thresholdUnrealized (content lk) wrt p h (commentPreskel lk [] ns shape + (if live then Nada else Dead) (if live then "" else "empty cohort")) step p h ks m oseen n seen todo tobig reducts - | depth lk >= optDepth p = + | optDepth p > 0 && depth lk >= optDepth p = do let ns = unrealized (content lk) - wrt p h (commentPreskel lk [] ns Fringe "") + wrt p h (commentPreskel lk [] ns Fringe Nada "") step p h ks m oseen n seen todo tobig reducts | otherwise = do @@ -279,7 +280,7 @@ let u = size - length dups' let msg = shows size $ showString " in cohort - " $ shows u " not yet seen" - wrt p h (commentPreskel lk (reverse dups') ns Ordinary msg) + wrt p h (commentPreskel lk (reverse dups') ns Ordinary Nada msg) step p h ks m oseen n' seen' todo' tobig reducts -- Expands one branch in the derivation tree. @@ -356,7 +357,7 @@ let ks' = reduce (mkMode p) (content lk) let msg = show (length ks') ++ " in cohort" let shape = if null ns then Shape else Ordinary - wrt p h (commentPreskel lk [] ns shape msg) + wrt p h (commentPreskel lk [] ns shape Nada msg) let (n', todo') = foldl (children lk) (n, []) ks' fast p h ks m n' (todo ++ reverse todo') @@ -375,22 +376,22 @@ dump p h (lk : lks) msg = do let ns = unrealized $ content lk - wrt p h (commentPreskel lk [] ns Ordinary "aborted") + wrt p h (commentPreskel lk [] ns Aborted Nada "aborted") dump p h lks msg -- Add a label, maybe a parent, a list of seen preskeletons isomorphic -- to some members of this skeleton's cohort, and a list of unrealized -- nodes. If it's a shape, note this fact. Add a comment if present. commentPreskel :: Algebra t p g s e c => LPreskel t g s e -> - [Int] -> [Node] -> Kind -> String -> SExpr () -commentPreskel lk seen unrealized kind msg = + [Int] -> [Node] -> Kind -> Anno -> String -> SExpr () +commentPreskel lk seen unrealized kind anno msg = displayPreskel k $ addKeyValues "label" [N () (label lk)] $ maybeAddVKeyValues "parent" (\p -> [N () (label p)]) (parent lk) $ condAddKeyValues "seen" (not $ null seen) (map (N ()) (L.sort (L.nub seen))) $ addKeyValues "unrealized" (map displayNode $ L.sort unrealized) $ - addKindKey kind $ + addKindKey kind $ addAnnoKey anno $ condAddKeyValues "satisfies" (kind == Shape && (not $ null $ kgoals k)) (satisfies k) $ -- Structure preserving maps @@ -402,15 +403,13 @@ -- Messages case msg of "" -> [] - -- Preskeleton key added for cpsasas program - "Not a skeleton" -> addKeyValues "preskeleton" [] [comment msg] _ -> [comment msg] where - fringe = kind /= Ordinary + fringe = isFringe kind k = content lk starter k = -- True for the POV skeleton and case pov k of -- just a few others - Nothing -> False + Nothing -> True Just k' -> nstrands k == nstrands k' addKeyValues :: String -> [SExpr ()] -> [SExpr ()] -> [SExpr ()] @@ -434,12 +433,33 @@ = Ordinary | Shape | Fringe + | Aborted deriving (Eq, Show) addKindKey :: Kind -> [SExpr ()] -> [SExpr ()] addKindKey Ordinary xs = xs addKindKey Shape xs = addKeyValues "shape" [] xs addKindKey Fringe xs = addKeyValues "fringe" [] xs +addKindKey Aborted xs = addKeyValues "aborted" [] xs + +isFringe :: Kind -> Bool +isFringe Ordinary = False +isFringe Shape = True +isFringe Fringe = True +isFringe Aborted = False + +-- Skeleton annotations +data Anno + = Nada + | Preskeleton + | SatisfiesAll + | Dead + +addAnnoKey :: Anno -> [SExpr ()] -> [SExpr ()] +addAnnoKey Nada xs = xs +addAnnoKey Preskeleton xs = addKeyValues "preskeleton" [] xs +addAnnoKey SatisfiesAll xs = addKeyValues "satisfies-all" [] xs +addAnnoKey Dead xs = addKeyValues "dead" [] xs -- Variable assignments and security goals diff --git a/src/CPSA/Lib/Strand.hs b/src/CPSA/Lib/Strand.hs --- a/src/CPSA/Lib/Strand.hs +++ b/src/CPSA/Lib/Strand.hs @@ -2637,6 +2637,7 @@ satisfy (UgenAt t n) = gugenAt t n satisfy (Ugen t) = gugen t satisfy (Prec n n') = gprec n n' +satisfy (LeadsTo n n') = gleadsTo n n' satisfy (Length r n i) = glength r n i satisfy (Param r v f n t) = gparam r v f n t @@ -2767,6 +2768,18 @@ where tc = map graphPair $ graphClose $ graphEdges $ strands k +-- Node leads to +gleadsTo :: Algebra t p g s e c => NodeTerm t -> NodeTerm t -> Sem t g s e +gleadsTo n n' k (g, e) = + case (nodeLookup e n, nodeLookup e n') of + (Just p, Just p') + | inSkel k p && inSkel k p' && elem (p, p') (leadsto k) -> [(g, e)] + _ -> + do + (p, p') <- leadsto k + (g, e) <- nodeMatch n p (g, e) + nodeMatch n' p' (g, e) + -- Length predicate -- r and h determine the predicate, which has arity one. glength :: Algebra t p g s e c => Role t -> t -> Int -> Sem t g s e @@ -2952,6 +2965,7 @@ rwt _ (Length r z h) = rlength r z h rwt rule (Param r v i z t) = rparam rule r v i z t rwt rule (Prec n n') = rprec rule n n' +rwt rule (LeadsTo n n') = rleadsTo rule n n' rwt rule (Non t) = rlnon rule t rwt rule (Pnon t) = rlpnon rule t rwt rule (Uniq t) = rluniq rule t @@ -3102,6 +3116,23 @@ badIndex :: Algebra t p g s e c => Preskel t g s e -> Sid -> Int -> Bool badIndex k s i = i >= height (strandInst k s) + +rleadsTo :: Algebra t p g s e c => String -> NodeTerm t -> + NodeTerm t -> Rewrite t g s e +rleadsTo name (z, i) (z', i') k (g, e) = + case (strdLookup e z, strdLookup e z') of + (Just s, Just s') + | elem ((s, i), (s', i')) (leadsto k) -> [(k, (g, e))] + | badIndex k s i || badIndex k s' i' -> [] + | otherwise -> + do -- Add one ordering + let leadsto' = ((s, i), (s', i')) : leadsto k + let k' = newPreskel g (shared k) (insts k) (orderings k) + leadsto' (decls k) (kfacts k) (operation k) + (prob k) (kpriority k) (pov k) + return (k', (gen k, e)) + _ -> + error ("In rule " ++ name ++ ", leads to did not get a strand") withNewDecl :: Algebra t p g s e c => Preskel t g s e -> SkelDeclarations t -> Preskel t g s e diff --git a/src/CPSA/SAS/SAS.hs b/src/CPSA/SAS/SAS.hs --- a/src/CPSA/SAS/SAS.hs +++ b/src/CPSA/SAS/SAS.hs @@ -52,8 +52,8 @@ do p <- findProt pos ps xs k <- loadPreskel pos p (pgen p) xs - case (isSkeleton k, isFringe k) of - (True, False) -> + case (isFringe k) of + False -> do -- Found POV origCheck pos k -- Ensure uniqs originate return ((ps, [k]), Nothing) @@ -264,7 +264,6 @@ origs :: [(t, (t, Int))], -- ugen, ugenAt missing! facts :: [Fact t], - isSkeleton :: Bool, isFringe :: !Bool, -- Always looked at, so make it strict homomorphisms :: [SExpr Pos], -- Loaded later varmap :: VM t } @@ -297,7 +296,6 @@ uniqs = uniqs, origs = map g origs, facts = facts, - isSkeleton = not $ hasKey preskeletonKey xs, isFringe = hasKey shapeKey xs || hasKey fringeKey xs, homomorphisms = assoc mapsKey xs, varmap = varmap}) @@ -473,7 +471,7 @@ loadMap pov k (L _ [L _ strandMap, L _ algebraMap]) = do perm <- mapM loadPerm strandMap -- Load the strand map - let nh = map (loadStrandEq k perm) (M.assocs $ varmap pov) + nh <- mapM (loadStrandEq k perm) (M.assocs $ varmap pov) -- Load the algebra part of the homomorphism ah <- mapM (loadMaplet (kvars k) (kvars pov)) algebraMap return (nh, ah) @@ -484,11 +482,17 @@ loadPerm x = fail (shows (annotation x) "Expecting a natural number") -- Applies a strand permutation to a strand. --- Hope the strand map is valid, or !! will blow up. -loadStrandEq :: Preskel t g c -> [Int] -> (Strand, t) -> (t, t) +loadStrandEq :: Monad m => Preskel t g c -> [Int] -> (Strand, t) -> m (t, t) loadStrandEq k perm (z, v) = - (v, slookup (perm !! z) (varmap k)) + do + z <- index perm z + return (v, slookup z (varmap k)) +index :: Monad m => [a] -> Int -> m a +index (x : _) 0 = return x +index (_ : xs) i | i > 0 = index xs (i - 1) +index _ _ = fail "Bad strand map" + -- Association lists -- Lookup value in alist, appending values with the same key @@ -502,10 +506,6 @@ hasKey :: String -> [SExpr a] -> Bool hasKey key alist = any (keyPred key) alist - --- The key used to identify a non-skeleton -preskeletonKey :: String -preskeletonKey = "preskeleton" -- The key used to identify a shape shapeKey :: String diff --git a/src/ocaml/Makefile b/src/ocaml/Makefile new file mode 100644 --- /dev/null +++ b/src/ocaml/Makefile @@ -0,0 +1,25 @@ +# OCaml Makefile that relies on ocamlbuild +# +# Type "make cpsa.d.otarget" to make a debugable executable +# +# Enable warnings by adding to OCFLAGS: -cflags "-w +A-4" + +OCFLAGS = -classic-display -use-ocamlfind -cflags "-w +A-4" +OCB = ocamlbuild +# Define DEBUG during development +# DEBUG = d. +TARGET = cpsa.$(DEBUG)otarget + +all: + $(OCB) $(OCFLAGS) $(TARGET) + +clean: + $(OCB) $(OCFLAGS) -clean + +Makefile: + @echo make $@ + +%: force + $(OCB) $(OCFLAGS) $@ + +.PHONY: all clean force diff --git a/src/ocaml/README b/src/ocaml/README new file mode 100644 --- /dev/null +++ b/src/ocaml/README @@ -0,0 +1,5 @@ +This directory contains ocaml code for reading and writing CPSA +S-expressions. See sexpr.mli for exported functions on S-expressions. +Module Main provides a top-level loop for writing simple filters. +Module Pp is a simple example of using Main to pretty print +the S-expressions in a file. diff --git a/src/ocaml/cpsa.d.itarget b/src/ocaml/cpsa.d.itarget new file mode 100644 --- /dev/null +++ b/src/ocaml/cpsa.d.itarget @@ -0,0 +1,1 @@ +cpsa.d.cma diff --git a/src/ocaml/cpsa.itarget b/src/ocaml/cpsa.itarget new file mode 100644 --- /dev/null +++ b/src/ocaml/cpsa.itarget @@ -0,0 +1,5 @@ +pp.native +expand.native +cpsa.cma +cpsa.docdir/index.html +# cpsa.top diff --git a/src/ocaml/cpsa.mllib b/src/ocaml/cpsa.mllib new file mode 100644 --- /dev/null +++ b/src/ocaml/cpsa.mllib @@ -0,0 +1,5 @@ +Sexpr_type +Reader +Scanner +Sexpr +Main diff --git a/src/ocaml/cpsa.mltop b/src/ocaml/cpsa.mltop new file mode 100644 --- /dev/null +++ b/src/ocaml/cpsa.mltop @@ -0,0 +1,4 @@ +Sexpr_type +Reader +Scanner +Sexpr diff --git a/src/ocaml/cpsa.odocl b/src/ocaml/cpsa.odocl new file mode 100644 --- /dev/null +++ b/src/ocaml/cpsa.odocl @@ -0,0 +1,3 @@ +Sexpr +Reader +Main diff --git a/src/ocaml/expand.ml b/src/ocaml/expand.ml new file mode 100644 --- /dev/null +++ b/src/ocaml/expand.ml @@ -0,0 +1,152 @@ +(* Expand macros as is done by CPSA *) + +open Lexing +open Sexpr +open Reader +open Main + +(* The macro expand loop limit *) +let limit = 1000 + +(* Include depth bound *) +let bound = 16 + +type macro = { + name: string; + args: string list; + body: position sexpr; + } + +(**** Define a macro ****) + +let symbol = function + | S (_, s) -> s + | x -> failwith_msg (annotation x) "Expecting a symbol" + +let defmacro pos = function + | [L (_, name :: args); body] -> + { + name = symbol name; + args = List.map symbol args; + body = body; + } + | _ -> failwith_msg pos "Malformed macro" + +(**** Expand macros ****) + +(* lookup key in association list with default *) + +let rec lookup default x = function + | [] -> default + | (s, y) :: _ when s = x -> y + | _ :: xs -> lookup default x xs + +let rec subst env = function + | S (_, s) as x -> lookup x s env + | L (pos, xs) -> L (pos, List.map (subst env) xs) + | x -> x + +let rec zip xs ys = + match (xs, ys) with + | (x :: xs, y :: ys) -> (x, y) :: zip xs ys + | _ -> [] + +let apply mac args = + subst (zip mac.args args) mac.body + +let rec expand_one macs sym xs = + match macs with + | [] -> None + | mac :: _ when mac.name = sym && + List.length mac.args = List.length xs -> + Some (apply mac xs) + | _ :: macs -> expand_one macs sym xs + +let rec limited_expand macs pos limit = function + | L (_, S (_, sym) :: xs) as x when limit > 0 -> + (match expand_one macs sym xs with + | Some y -> limited_expand macs pos (limit - 1) y + | None -> x) + | _ when limit <= 0 -> + failwith_msg pos "Expansion limit exceeded" + | x -> x + +(* Splice sexprs that start with splice symbol. The splice symbol is + ^. *) + +let rec splice = function + | [] -> [] + | L (_, S (_, keyword) :: xs) :: ys when keyword = "^" -> + let rec loop xs ys = + match xs with + | [] -> splice ys + | x :: xs -> x :: loop xs ys in + loop xs ys + | x :: xs -> x :: splice xs + +let rec expand_all macs x = + match limited_expand macs (annotation x) limit x with + | L (pos, xs) -> + let ys = List.map (expand_all macs) xs in + L (pos, splice ys) + | x -> x + +let need_newline = ref false + +let expand o macs x = + if !need_newline + then print_newline (); + print_sexpr o (expand_all macs x); + need_newline := true + +(**** Include the contents of a file ****) + +let read_sexprs ch = + let rec loop xs = + try + let x = read_sexpr ch in + loop (x :: xs) + with + | End_of_file -> + List.rev xs in + loop [] + +(**** Main loop ****) + +(* o is the output channel + bound is the include bound + macs is the current list of defined macros *) + +let rec loop o bound macs = function + | [] -> macs (* Return the collected macros *) + | x :: xs -> dispatch o bound macs xs x + + and dispatch o bound macs xs = function + | L (pos, (S (_, keyword) :: rest)) when keyword = "defmacro" -> + loop o bound (defmacro pos rest :: macs) xs + | L (pos, (S (_, keyword) :: rest)) when keyword = "include" -> + loop o bound (incl o bound macs pos rest) xs + | x -> + expand o macs x; + loop o bound macs xs + + and incl o bound macs pos = function + | [Q (_, f)] when bound > 0 -> + let i = + try + open_in f + with Sys_error s -> failwith s + in + let lb = read_lexbuf f i in + let xs = read_sexprs lb in + loop o (bound - 1) macs xs + | [Q (_, f)] when bound <= 0 -> + failwith_msg pos ("Include depth exceeded with file " ^ f) + | _ -> failwith_msg pos "Malformed include directive" + +let start o xs = + let _ = loop o bound [] xs in + () + +let () = + main start diff --git a/src/ocaml/main.ml b/src/ocaml/main.ml new file mode 100644 --- /dev/null +++ b/src/ocaml/main.ml @@ -0,0 +1,73 @@ +(* Main entry point *) + +open Sexpr + +let read_sexprs ch = + let rec loop xs = + try + let x = read_sexpr ch in + loop (x :: xs) + with + | End_of_file -> + List.rev xs in + loop [] + +let go run f i ofile = + let lb = read_lexbuf f i in + let xs = read_sexprs lb in + close_in i; + let o = + if ofile = "" then + stdout + else + open_out ofile in + run o xs + +(* Command-line processing using Arg *) + +let help = ref false +let output = ref "" +let input = ref "" + +let usage = + "Usage: " ^ Sys.argv.(0) ^ " [OPTIONS] [INPUT]\n" ^ + "Options:" + +let speclist = +[("-o", Arg.Set_string(output), "output to file (default is standard output)"); + ("-h", Arg.Set(help), "print this message")] + +let anon s = + if !input = "" then + input := s + else + begin + prerr_endline "Bad command-line argument count\n"; + exit 1 + end + +let start run = + Arg.parse speclist anon usage; + if !help then + begin + Arg.usage speclist usage; + exit 0 + end + else + let (in_name, in_ch) = + match !input with + | "" -> ("", stdin) + | f -> + try + (f, open_in f) + with Sys_error s -> failwith s + in + go run in_name in_ch !output + +let main run = + try + start run + with + | Failure s -> + prerr_endline s; + exit 1 diff --git a/src/ocaml/main.mli b/src/ocaml/main.mli new file mode 100644 --- /dev/null +++ b/src/ocaml/main.mli @@ -0,0 +1,24 @@ +(** A main routine for processing S-expressions *) + +(** Build a program that processes S-expressions. The program + +{[ let () = main f]} + +reads an input file containing a sequence of S-expressions, and opens +an output file. It then invokes function [f] with the output channel +and the list of S-expressions read. + +If the name of the program is [prog], the input file and the output +file is specified on the command line as + +{[ $ prog -o OUTPUT INPUT]} + +where standard input is used when [INPUT] is omitted, and standard +output is used when [-o OUTPUT] is omitted. + +Function [f] is invoked in a context that catches {!exception:Failure} +exceptions, prints the failure message to standard error, and then +exits with error code 1. Function {!val:Reader.failwith_msg} raises +{!exception:Failure} exceptions after adding position information to +an error message. *) +val main : (out_channel -> Lexing.position Sexpr.sexpr list -> unit) -> unit diff --git a/src/ocaml/pp.ml b/src/ocaml/pp.ml new file mode 100644 --- /dev/null +++ b/src/ocaml/pp.ml @@ -0,0 +1,13 @@ +open Sexpr +open Main + +let need_newline = ref false + +let filter o x = + if !need_newline + then print_newline (); + print_sexpr o x; + need_newline := true + +let () = + main (fun o xs -> List.iter (filter o) xs) diff --git a/src/ocaml/reader.ml b/src/ocaml/reader.ml new file mode 100644 --- /dev/null +++ b/src/ocaml/reader.ml @@ -0,0 +1,58 @@ +open Sexpr_type +open Lexing + +type token = + | SYM of string + | STR of string + | NUM of int + | LPAR + | RPAR + | EOF + +let error_msg pos msg = + Printf.sprintf "%s:%d:%d: %s\n" pos.pos_fname pos.pos_lnum + (pos.pos_cnum - pos.pos_bol + 1) msg + +let failwith_msg pos msg = + failwith (error_msg pos msg) + +let parse_err = failwith_msg + +let rec parse_list lexfun lexbuf lpos list = + let tok = lexfun lexbuf in + let pos = lexeme_start_p lexbuf in + match tok with + | SYM s -> parse_list lexfun lexbuf lpos (S (pos, s) :: list) + | STR s -> parse_list lexfun lexbuf lpos (Q (pos, s) :: list) + | NUM n -> parse_list lexfun lexbuf lpos (N (pos, n) :: list) + | LPAR -> + let x = parse_list lexfun lexbuf pos [] in + parse_list lexfun lexbuf lpos (x :: list) + | RPAR -> L (lpos, List.rev list) + | EOF -> parse_err pos "End of file in list" + +let top lexfun lexbuf = + let tok = lexfun lexbuf in + let pos = lexeme_start_p lexbuf in + match tok with + | SYM s -> S (pos, s) + | STR s -> Q (pos, s) + | NUM n -> N (pos, n) + | LPAR -> parse_list lexfun lexbuf pos [] + | RPAR -> parse_err pos "Unmatched right parenthesis" + | EOF -> raise End_of_file + +let one lexfun lexbuf = + let tok = lexfun lexbuf in + let pos = lexeme_start_p lexbuf in + let x = + match tok with + | SYM s -> S (pos, s) + | STR s -> Q (pos, s) + | NUM n -> N (pos, n) + | LPAR -> parse_list lexfun lexbuf pos [] + | RPAR -> parse_err pos "Unmatched right parenthesis" + | EOF -> parse_err pos "Nothing in string" in + match lexfun lexbuf with + | EOF -> x + | _ -> parse_err (lexeme_start_p lexbuf) "Trailing garbage in string" diff --git a/src/ocaml/reader.mli b/src/ocaml/reader.mli new file mode 100644 --- /dev/null +++ b/src/ocaml/reader.mli @@ -0,0 +1,24 @@ +(** Operations on positions produced by {!val:Sexpr.read_sexpr} *) + +open Sexpr_type +open Lexing + +(**/**) + +type token = SYM of string | STR of string | NUM of int | LPAR | RPAR | EOF + +(**/**) + +(** Add position information to a message. *) +val error_msg : position -> string -> string + +(** Add position information to a message and fail. + @raise Failure always *) +val failwith_msg : position -> string -> 'a + +(**/**) + +val parse_err : position -> string -> 'a + +val top : (lexbuf -> token) -> lexbuf -> position sexpr +val one : (lexbuf -> token) -> lexbuf -> position sexpr diff --git a/src/ocaml/scanner.mll b/src/ocaml/scanner.mll new file mode 100644 --- /dev/null +++ b/src/ocaml/scanner.mll @@ -0,0 +1,21 @@ +{ +open Reader +open Lexing + +let parse_error pos = + parse_err pos "Bad token" +} +let special = ['*' '/' '<' '=' '>' '!' '?' ':' '$' '%' '_' '&' '~' '^'] +let start = ['a' - 'z' 'A' - 'Z'] | special +let part = start | ['-' '+' '0' - '9'] +rule token = parse + [' ' '\t'] { token lexbuf } + | '\n' { new_line lexbuf; token lexbuf } + | ';' [^ '\n']* { token lexbuf } + | start part* as s { SYM(s) } + | ['-' '+']? ['0'-'9']+ as n { NUM(int_of_string n) } + | '"' ([^ '\\' '"']* as s) '"' { STR(s) } + | '(' { LPAR } + | ')' { RPAR } + | eof { EOF } + | _ { parse_error (lexeme_start_p lexbuf) } diff --git a/src/ocaml/sexpr.ml b/src/ocaml/sexpr.ml new file mode 100644 --- /dev/null +++ b/src/ocaml/sexpr.ml @@ -0,0 +1,84 @@ +include Sexpr_type +open Lexing +open Format + +let annotation = function + | S (a, _) -> a + | Q (a, _) -> a + | N (a, _) -> a + | L (a, _) -> a + +let read_lexbuf fname ch = + let lexbuf = Lexing.from_channel ch in + lexbuf.lex_curr_p <- { lexbuf.lex_curr_p with pos_fname = fname }; + lexbuf + +let read_sexpr lexbuf = + Reader.top Scanner.token lexbuf + +let read_sexpr_from_string ch = + let lexbuf = Lexing.from_string ch in + Reader.one Scanner.token lexbuf + +let rec sexpr_printer f x = + match x with + | S (_, s) -> pp_print_string f s + | Q (_, s) -> + pp_print_char f '"'; + pp_print_string f s; + pp_print_char f '"' + | N (_, n) -> pp_print_int f n + | L (_, xs) -> print_list f xs +and print_list f x = + match x with + | [] -> pp_print_string f "()" + | x :: xs -> + pp_open_box f 2; + pp_print_string f "("; + sexpr_printer f x; + print_rest f xs +and print_rest f x = + match x with + | [] -> + pp_print_string f ")"; + pp_close_box f () + | x :: xs -> + pp_print_space f (); + sexpr_printer f x; + print_rest f xs + +let print_sexpr ch x = + let f = formatter_of_out_channel ch in + sexpr_printer f x; + pp_print_newline f () + +let sym x = S ((), x) +let quo x = Q ((), x) +let num x = N ((), x) +let lst x = L ((), x) + +let rec strip = function + | S (_, s) -> sym s + | Q (_, s) -> quo s + | N (_, i) -> num i + | L (_, l) -> lst (List.map strip l) + +let assoc key alist = + let rec loop acc = function + | [] -> acc + | L (_, S (_, head) :: rest) :: l when key = head -> + loop (acc @ rest) l + | _ :: l -> loop acc l in + loop [] alist + +let rec has_key key = function + | [] -> false + | L (_, S (_, head) :: _) :: _ when key = head -> true + | _ :: l -> has_key key l + +let rem_keys keys xs = + let f xs x = + match x with + | L (_, S (_, head) :: _) when List.mem head keys -> xs + | _ -> x :: xs in + List.rev (List.fold_left f [] xs) diff --git a/src/ocaml/sexpr.mli b/src/ocaml/sexpr.mli new file mode 100644 --- /dev/null +++ b/src/ocaml/sexpr.mli @@ -0,0 +1,109 @@ +(** S-expressions + +This module provides a data structure for S-expressions, and a reader. +The reader records the position in the file at which items that make +up the list are located. + +The S-expressions used are restricted so that most dialects of Lisp +can read them, and characters within symbols and strings never need +quoting. Every list is proper. An atom is either a symbol, an integer, +or a string. The characters that make up a symbol are the letters, the +digits, and these special characters. + +{[ +-*\/\<=>!?:$%_&~^]} + +A symbol may not begin with a digit or a sign followed by a digit. The +characters that make up a string are the printing characters omitting +double quote and backslash. Double quotes delimit a string. A comment +begins with a semicolon and continues to the end of the current line. + + *) + +open Lexing +open Format + +(** S-expression datatype *) +type 'a sexpr = + | S of 'a * string (** Symbol *) + | Q of 'a * string (** String *) + | N of 'a * int (** Number (integer) *) + | L of 'a * 'a sexpr list (** Proper list *) + +(** Extract the annotation associated with an S-expression. *) +val annotation : 'a sexpr -> 'a + +(** {1 Input} *) + +(** Given a file name and its channel, return a {!val:Lexer.lexbuf} + for use by the reader. Use the empty string as the file name for + {!val:Sys.stdin}. *) +val read_lexbuf : string -> in_channel -> lexbuf + +(** Read an S-expression from a file annotated with the position of + the datum in the file. See module {!module:Reader} for functions + that use positions to construct informative error messages. + + @raise End_of_file on end of file + @raise Failure on malformed input *) +val read_sexpr : lexbuf -> position sexpr + +(** Read an S-expression from a string annotated with the position of + the datum in the string. *) +val read_sexpr_from_string : string -> position sexpr + +(** {1 Output} *) + +(** Pretty print an S-expression *) +val print_sexpr : out_channel -> 'a sexpr -> unit + +(** An S-expression printer that can be installed as a printer in a + toplevel system using + +{[ install_printer Sexpr.sexpr_printer]} + *) +val sexpr_printer : formatter -> 'a sexpr -> unit + +(** {1 List Builders} *) + +(** Construct a symbol *) +val sym : string -> unit sexpr + +(** Construct a string *) +val quo : string -> unit sexpr + +(** Construct an integer *) +val num : int -> unit sexpr + +(** Construct a list *) +val lst : unit sexpr list -> unit sexpr + +(** {1 List Operations} *) + +(** Replace all annotations in a list with the unit value. *) +val strip : 'a sexpr -> unit sexpr + +(** {2 Association Lists} + + An association list is a list of lists, in which the first element + of each interior list is a symbol. The symbol is call a key. The + list of values associated with a key is the result of appending + all interior lists that are headed by the key after removing the + key. Thus, the list of values [(a b c d)] is associated with key + [k] in the following association list + +{[ ((k a b) + (x y z) + (k c d))]} + + An interior list that does not begin with a symbol is silently + ignored. *) + +(** Return the values associated with a key. *) +val assoc : string -> 'a sexpr list -> 'a sexpr list + +(** Does an association list have an interior list headed with the + given key? *) +val has_key : string -> 'a sexpr list -> bool + +(** Remove interior lists if their key is in a given list. *) +val rem_keys : string list -> 'a sexpr list -> 'a sexpr list diff --git a/src/ocaml/sexpr_type.ml b/src/ocaml/sexpr_type.ml new file mode 100644 --- /dev/null +++ b/src/ocaml/sexpr_type.ml @@ -0,0 +1,5 @@ +type 'a sexpr = + | S of 'a * string + | Q of 'a * string + | N of 'a * int + | L of 'a * 'a sexpr list 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 3.6.1") +(comment "CPSA 3.6.2") (comment "All input read from aik.scm") (defprotocol aikprot basic diff --git a/tst/axiom2.tst b/tst/axiom2.tst --- a/tst/axiom2.tst +++ b/tst/axiom2.tst @@ -1,6 +1,6 @@ (herald "Axiom 2 Protocol" (bound 20)) -(comment "CPSA 3.6.1") +(comment "CPSA 3.6.2") (comment "All input read from axiom2.scm") (comment "Strand count bounded at 20") @@ -112,6 +112,7 @@ (label 6) (parent 5) (unrealized (0 1)) + (dead) (comment "empty cohort")) (comment "Nothing left to do") @@ -229,6 +230,7 @@ (label 13) (parent 12) (unrealized (0 1)) + (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 3.6.1") +(comment "CPSA 3.6.2") (comment "All input read from blanchet.scm") (defprotocol blanchet basic @@ -55,6 +55,7 @@ (label 2) (parent 0) (unrealized (1 0)) + (dead) (comment "empty cohort")) (defskeleton blanchet @@ -176,6 +177,7 @@ (label 8) (parent 6) (unrealized (2 0)) + (dead) (comment "empty cohort")) (defskeleton blanchet @@ -214,6 +216,7 @@ (label 10) (parent 9) (unrealized (3 0)) + (dead) (comment "empty cohort")) (comment "Nothing left to do") @@ -241,6 +244,7 @@ (label 11) (unrealized (0 0) (1 0)) (preskeleton) + (origs (d (0 1))) (comment "Not a skeleton")) (defskeleton blanchet @@ -331,6 +335,7 @@ (label 16) (parent 14) (unrealized (1 0)) + (dead) (comment "empty cohort")) (defskeleton blanchet-corrected @@ -409,6 +414,7 @@ (label 20) (parent 18) (unrealized (2 0)) + (dead) (comment "empty cohort")) (defskeleton blanchet-corrected @@ -447,6 +453,7 @@ (label 22) (parent 21) (unrealized (3 0)) + (dead) (comment "empty cohort")) (comment "Nothing left to do") @@ -517,6 +524,7 @@ (label 25) (unrealized (0 0) (1 0)) (preskeleton) + (origs (d (0 1))) (comment "Not a skeleton")) (defskeleton blanchet-corrected @@ -568,6 +576,7 @@ (label 28) (parent 27) (unrealized (3 0)) + (dead) (comment "empty cohort")) (comment "Nothing left to do") diff --git a/tst/bltk_test.tst b/tst/bltk_test.tst --- a/tst/bltk_test.tst +++ b/tst/bltk_test.tst @@ -1,6 +1,6 @@ (herald "bltk Test File" (algebra diffie-hellman) (bound 12)) -(comment "CPSA 3.6.1") +(comment "CPSA 3.6.2") (comment "All input read from bltk_test.scm") (defprotocol test diffie-hellman @@ -40,6 +40,7 @@ (label 1) (unrealized (1 0)) (preskeleton) + (origs (n (0 0))) (comment "Not a skeleton")) (defskeleton test @@ -54,6 +55,7 @@ (label 2) (parent 1) (unrealized (1 0)) + (dead) (origs (n (0 0))) (comment "empty cohort")) @@ -76,6 +78,7 @@ (label 3) (unrealized (1 0)) (preskeleton) + (origs (n (0 0))) (comment "Not a skeleton")) (defskeleton test @@ -90,6 +93,7 @@ (label 4) (parent 3) (unrealized (1 0)) + (dead) (origs (n (0 0))) (comment "empty cohort")) diff --git a/tst/dh-ca.tst b/tst/dh-ca.tst --- a/tst/dh-ca.tst +++ b/tst/dh-ca.tst @@ -1,6 +1,6 @@ (herald dhca (algebra diffie-hellman)) -(comment "CPSA 3.6.1") +(comment "CPSA 3.6.2") (comment "All input read from dh-ca.scm") (defprotocol dhca diffie-hellman @@ -528,6 +528,7 @@ (label 15) (parent 8) (unrealized (4 0)) + (dead) (comment "empty cohort")) (defskeleton dhca @@ -586,6 +587,7 @@ (label 17) (parent 9) (unrealized (3 0)) + (dead) (comment "empty cohort")) (defskeleton dhca @@ -618,6 +620,7 @@ (label 18) (parent 9) (unrealized (2 0) (3 0)) + (dead) (comment "empty cohort")) (defskeleton dhca @@ -879,6 +882,7 @@ (label 25) (parent 16) (unrealized (4 0)) + (dead) (comment "empty cohort")) (defskeleton dhca @@ -924,6 +928,7 @@ (label 26) (parent 19) (unrealized (5 0)) + (dead) (comment "empty cohort")) (defskeleton dhca @@ -988,6 +993,7 @@ (label 28) (parent 20) (unrealized (4 0)) + (dead) (comment "empty cohort")) (defskeleton dhca @@ -1023,6 +1029,7 @@ (label 29) (parent 20) (unrealized (3 0) (4 0)) + (dead) (comment "empty cohort")) (defskeleton dhca @@ -1227,6 +1234,7 @@ (label 34) (parent 23) (unrealized (6 0)) + (dead) (comment "empty cohort")) (defskeleton dhca @@ -1262,6 +1270,7 @@ (label 35) (parent 24) (unrealized (4 0) (5 0)) + (dead) (comment "empty cohort")) (defskeleton dhca @@ -1296,6 +1305,7 @@ (label 36) (parent 24) (unrealized (5 0)) + (dead) (comment "empty cohort")) (defskeleton dhca @@ -1330,6 +1340,7 @@ (label 37) (parent 24) (unrealized (5 0)) + (dead) (comment "empty cohort")) (defskeleton dhca @@ -1368,6 +1379,7 @@ (label 38) (parent 24) (unrealized (4 0) (5 0)) + (dead) (comment "empty cohort")) (defskeleton dhca @@ -1402,6 +1414,7 @@ (label 39) (parent 27) (unrealized (5 0)) + (dead) (comment "empty cohort")) (defskeleton dhca @@ -2033,6 +2046,7 @@ (label 57) (parent 50) (unrealized (4 0)) + (dead) (comment "empty cohort")) (defskeleton dhca @@ -2093,6 +2107,7 @@ (label 59) (parent 51) (unrealized (3 0)) + (dead) (comment "empty cohort")) (defskeleton dhca @@ -2126,6 +2141,7 @@ (label 60) (parent 51) (unrealized (2 0) (3 0)) + (dead) (comment "empty cohort")) (defskeleton dhca @@ -2395,6 +2411,7 @@ (label 67) (parent 58) (unrealized (4 0)) + (dead) (comment "empty cohort")) (defskeleton dhca @@ -2441,6 +2458,7 @@ (label 68) (parent 61) (unrealized (5 0)) + (dead) (comment "empty cohort")) (defskeleton dhca @@ -2507,6 +2525,7 @@ (label 70) (parent 62) (unrealized (4 0)) + (dead) (comment "empty cohort")) (defskeleton dhca @@ -2543,6 +2562,7 @@ (label 71) (parent 62) (unrealized (3 0) (4 0)) + (dead) (comment "empty cohort")) (defskeleton dhca @@ -2758,6 +2778,7 @@ (label 76) (parent 65) (unrealized (6 0)) + (dead) (comment "empty cohort")) (defskeleton dhca @@ -2794,6 +2815,7 @@ (label 77) (parent 66) (unrealized (4 0) (5 0)) + (dead) (comment "empty cohort")) (defskeleton dhca @@ -2829,6 +2851,7 @@ (label 78) (parent 66) (unrealized (5 0)) + (dead) (comment "empty cohort")) (defskeleton dhca @@ -2864,6 +2887,7 @@ (label 79) (parent 66) (unrealized (5 0)) + (dead) (comment "empty cohort")) (defskeleton dhca @@ -2903,6 +2927,7 @@ (label 80) (parent 66) (unrealized (4 0) (5 0)) + (dead) (comment "empty cohort")) (defskeleton dhca @@ -2938,6 +2963,7 @@ (label 81) (parent 69) (unrealized (5 0)) + (dead) (comment "empty cohort")) (defskeleton dhca @@ -3088,6 +3114,7 @@ (label 84) (unrealized (0 1) (0 3) (1 1) (1 2) (1 4)) (preskeleton) + (origs (n (1 3))) (comment "Not a skeleton")) (defskeleton dhca @@ -3548,6 +3575,7 @@ (label 95) (parent 93) (unrealized (0 1) (6 0)) + (dead) (comment "empty cohort")) (defskeleton dhca @@ -3591,6 +3619,7 @@ (label 96) (parent 94) (unrealized (0 1) (4 0) (5 0)) + (dead) (comment "empty cohort")) (defskeleton dhca @@ -3633,6 +3662,7 @@ (label 97) (parent 94) (unrealized (0 1) (5 0)) + (dead) (comment "empty cohort")) (defskeleton dhca @@ -3675,6 +3705,7 @@ (label 98) (parent 94) (unrealized (0 1) (5 0)) + (dead) (comment "empty cohort")) (defskeleton dhca @@ -3720,6 +3751,7 @@ (label 99) (parent 94) (unrealized (0 1) (4 0) (5 0)) + (dead) (comment "empty cohort")) (comment "Nothing left to do") diff --git a/tst/dh_mim.tst b/tst/dh_mim.tst --- a/tst/dh_mim.tst +++ b/tst/dh_mim.tst @@ -1,7 +1,7 @@ (herald "Diffie-Hellman protocol, man-in-the-middle attack" (algebra diffie-hellman)) -(comment "CPSA 3.6.1") +(comment "CPSA 3.6.2") (comment "All input read from dh_mim.scm") (defprotocol dh_mim diffie-hellman diff --git a/tst/dh_mim2.tst b/tst/dh_mim2.tst --- a/tst/dh_mim2.tst +++ b/tst/dh_mim2.tst @@ -1,7 +1,7 @@ (herald "Diffie-Hellman protocol, man-in-the-middle attack" (algebra diffie-hellman)) -(comment "CPSA 3.6.1") +(comment "CPSA 3.6.2") (comment "All input read from dh_mim2.scm") (defprotocol dh_mim diffie-hellman diff --git a/tst/dh_sig.tst b/tst/dh_sig.tst --- a/tst/dh_sig.tst +++ b/tst/dh_sig.tst @@ -1,6 +1,6 @@ (herald "Signed DH exchange" (algebra diffie-hellman)) -(comment "CPSA 3.6.1") +(comment "CPSA 3.6.2") (comment "All input read from dh_sig.scm") (defprotocol dh_sig diffie-hellman diff --git a/tst/dh_test.tst b/tst/dh_test.tst --- a/tst/dh_test.tst +++ b/tst/dh_test.tst @@ -1,7 +1,7 @@ (herald "Diffie-Hellman protocol, man-in-the-middle attack" (algebra diffie-hellman) (bound 20)) -(comment "CPSA 3.6.1") +(comment "CPSA 3.6.2") (comment "All input read from dh_test.scm") (comment "Strand count bounded at 20") diff --git a/tst/dhnsl_basic.tst b/tst/dhnsl_basic.tst --- a/tst/dhnsl_basic.tst +++ b/tst/dhnsl_basic.tst @@ -1,7 +1,7 @@ (herald "Diffie-Hellman enhanced Needham-Schroeder-Lowe Protocol" (algebra diffie-hellman)) -(comment "CPSA 3.6.1") +(comment "CPSA 3.6.2") (comment "All input read from dhnsl_basic.scm") (defprotocol dhnsl diffie-hellman @@ -147,6 +147,7 @@ (label 5) (parent 2) (unrealized (1 0)) + (dead) (comment "empty cohort")) (defskeleton dhnsl @@ -235,6 +236,7 @@ (label 9) (parent 4) (unrealized (2 0)) + (dead) (comment "empty cohort")) (defskeleton dhnsl @@ -364,6 +366,7 @@ (label 14) (parent 6) (unrealized (3 0)) + (dead) (comment "empty cohort")) (defskeleton dhnsl @@ -388,6 +391,7 @@ (label 15) (parent 7) (unrealized (1 0)) + (dead) (comment "empty cohort")) (defskeleton dhnsl @@ -411,6 +415,7 @@ (label 16) (parent 8) (unrealized (3 0)) + (dead) (comment "empty cohort")) (defskeleton dhnsl @@ -438,6 +443,7 @@ (label 17) (parent 10) (unrealized (3 0)) + (dead) (comment "empty cohort")) (defskeleton dhnsl @@ -468,6 +474,7 @@ (label 18) (parent 11) (unrealized (4 0)) + (dead) (comment "empty cohort")) (defskeleton dhnsl @@ -525,6 +532,7 @@ (label 20) (parent 13) (unrealized (4 0)) + (dead) (comment "empty cohort")) (comment "Nothing left to do") @@ -627,6 +635,7 @@ (label 24) (parent 23) (unrealized (1 0)) + (dead) (comment "empty cohort")) (defskeleton dhnsl @@ -746,6 +755,7 @@ (label 29) (parent 26) (unrealized (3 0)) + (dead) (comment "empty cohort")) (defskeleton dhnsl @@ -770,6 +780,7 @@ (label 30) (parent 27) (unrealized (3 0)) + (dead) (comment "empty cohort")) (comment "Nothing left to do") diff --git a/tst/dhnsl_use.tst b/tst/dhnsl_use.tst --- a/tst/dhnsl_use.tst +++ b/tst/dhnsl_use.tst @@ -1,7 +1,7 @@ (herald "Diffie-Hellman enhanced Needham-Schroeder-Lowe Protocol" (algebra diffie-hellman)) -(comment "CPSA 3.6.1") +(comment "CPSA 3.6.2") (comment "All input read from dhnsl_use.scm") (defprotocol dhnsl diffie-hellman @@ -156,6 +156,7 @@ (label 5) (parent 2) (unrealized (1 0)) + (dead) (comment "empty cohort")) (defskeleton dhnsl @@ -181,6 +182,7 @@ (label 6) (parent 2) (unrealized (0 1) (0 3) (1 0)) + (dead) (comment "empty cohort")) (defskeleton dhnsl @@ -224,6 +226,7 @@ (label 8) (parent 2) (unrealized (0 1) (0 3) (1 0)) + (dead) (comment "empty cohort")) (defskeleton dhnsl @@ -297,6 +300,7 @@ (label 11) (parent 4) (unrealized (2 0)) + (dead) (comment "empty cohort")) (defskeleton dhnsl @@ -322,6 +326,7 @@ (label 12) (parent 4) (unrealized (0 1) (0 3) (2 0)) + (dead) (comment "empty cohort")) (defskeleton dhnsl @@ -352,6 +357,7 @@ (label 13) (parent 4) (unrealized (0 1) (0 3) (2 0)) + (dead) (comment "empty cohort")) (defskeleton dhnsl @@ -405,6 +411,7 @@ (label 15) (parent 4) (unrealized (0 1) (0 3) (2 0)) + (dead) (comment "empty cohort")) (defskeleton dhnsl @@ -430,6 +437,7 @@ (label 16) (parent 7) (unrealized (1 0)) + (dead) (comment "empty cohort")) (defskeleton dhnsl @@ -576,6 +584,7 @@ (label 21) (parent 18) (unrealized (2 0)) + (dead) (comment "empty cohort")) (defskeleton dhnsl @@ -636,6 +645,7 @@ (label 23) (parent 18) (unrealized (1 2) (2 0)) + (dead) (comment "empty cohort")) (defskeleton dhnsl @@ -696,6 +706,7 @@ (label 25) (parent 18) (unrealized (1 2) (2 0)) + (dead) (comment "empty cohort")) (defskeleton dhnsl @@ -724,6 +735,7 @@ (label 26) (parent 19) (unrealized (2 0) (3 0)) + (dead) (comment "empty cohort")) (defskeleton dhnsl @@ -751,6 +763,7 @@ (label 27) (parent 19) (unrealized (3 0)) + (dead) (comment "empty cohort")) (defskeleton dhnsl @@ -782,6 +795,7 @@ (label 28) (parent 19) (unrealized (2 0) (3 0)) + (dead) (comment "empty cohort")) (defskeleton dhnsl @@ -809,6 +823,7 @@ (label 29) (parent 19) (unrealized (3 0)) + (dead) (comment "empty cohort")) (defskeleton dhnsl @@ -839,6 +854,7 @@ (label 30) (parent 19) (unrealized (2 0) (3 0)) + (dead) (comment "empty cohort")) (defskeleton dhnsl @@ -868,6 +884,7 @@ (label 31) (parent 22) (unrealized (2 0)) + (dead) (comment "empty cohort")) (defskeleton dhnsl @@ -902,6 +919,7 @@ (label 32) (parent 24) (unrealized (1 2) (2 0)) + (dead) (comment "empty cohort")) (comment "Nothing left to do") @@ -1103,6 +1121,7 @@ (label 39) (parent 35) (unrealized (1 0)) + (dead) (comment "empty cohort")) (defskeleton dhnsl @@ -1151,6 +1170,7 @@ (label 41) (parent 35) (unrealized (0 2) (0 4) (1 0)) + (dead) (comment "empty cohort")) (defskeleton dhnsl @@ -1176,6 +1196,7 @@ (label 42) (parent 35) (unrealized (0 2) (0 4) (1 0)) + (dead) (comment "empty cohort")) (defskeleton dhnsl @@ -1273,6 +1294,7 @@ (label 45) (parent 40) (unrealized (0 4) (1 0)) + (dead) (comment "empty cohort")) (defskeleton dhnsl @@ -1311,6 +1333,7 @@ (label 46) (parent 43) (unrealized (2 1) (3 0)) + (dead) (comment "empty cohort")) (defskeleton dhnsl @@ -1387,6 +1410,7 @@ (label 48) (parent 43) (unrealized (2 1) (3 0)) + (dead) (comment "empty cohort")) (defskeleton dhnsl @@ -1458,6 +1482,7 @@ (label 50) (parent 43) (unrealized (2 1) (3 0)) + (dead) (comment "empty cohort")) (defskeleton dhnsl @@ -1497,6 +1522,7 @@ (label 51) (parent 43) (unrealized (2 1) (3 0)) + (dead) (comment "empty cohort")) (defskeleton dhnsl @@ -1527,6 +1553,7 @@ (label 52) (parent 44) (unrealized (2 0) (3 0)) + (dead) (comment "empty cohort")) (defskeleton dhnsl @@ -1556,6 +1583,7 @@ (label 53) (parent 44) (unrealized (3 0)) + (dead) (comment "empty cohort")) (defskeleton dhnsl @@ -1589,6 +1617,7 @@ (label 54) (parent 44) (unrealized (2 0) (3 0)) + (dead) (comment "empty cohort")) (defskeleton dhnsl @@ -1618,6 +1647,7 @@ (label 55) (parent 44) (unrealized (3 0)) + (dead) (comment "empty cohort")) (defskeleton dhnsl @@ -1650,6 +1680,7 @@ (label 56) (parent 44) (unrealized (2 0) (3 0)) + (dead) (comment "empty cohort")) (defskeleton dhnsl @@ -1686,6 +1717,7 @@ (label 57) (parent 47) (unrealized (2 1) (3 0)) + (dead) (comment "empty cohort")) (defskeleton dhnsl @@ -1727,6 +1759,7 @@ (label 58) (parent 49) (unrealized (2 1) (3 0)) + (dead) (comment "empty cohort")) (comment "Nothing left to do") @@ -1883,6 +1916,7 @@ (label 64) (parent 61) (unrealized (1 0)) + (dead) (comment "empty cohort")) (defskeleton dhns @@ -1908,6 +1942,7 @@ (label 65) (parent 61) (unrealized (0 1) (0 3) (1 0)) + (dead) (comment "empty cohort")) (defskeleton dhns @@ -1951,6 +1986,7 @@ (label 67) (parent 61) (unrealized (0 1) (0 3) (1 0)) + (dead) (comment "empty cohort")) (defskeleton dhns @@ -2024,6 +2060,7 @@ (label 70) (parent 63) (unrealized (2 0)) + (dead) (comment "empty cohort")) (defskeleton dhns @@ -2049,6 +2086,7 @@ (label 71) (parent 63) (unrealized (0 1) (0 3) (2 0)) + (dead) (comment "empty cohort")) (defskeleton dhns @@ -2079,6 +2117,7 @@ (label 72) (parent 63) (unrealized (0 1) (0 3) (2 0)) + (dead) (comment "empty cohort")) (defskeleton dhns @@ -2132,6 +2171,7 @@ (label 74) (parent 63) (unrealized (0 1) (0 3) (2 0)) + (dead) (comment "empty cohort")) (defskeleton dhns @@ -2157,6 +2197,7 @@ (label 75) (parent 66) (unrealized (1 0)) + (dead) (comment "empty cohort")) (defskeleton dhns @@ -2303,6 +2344,7 @@ (label 80) (parent 77) (unrealized (2 0)) + (dead) (comment "empty cohort")) (defskeleton dhns @@ -2363,6 +2405,7 @@ (label 82) (parent 77) (unrealized (1 2) (2 0)) + (dead) (comment "empty cohort")) (defskeleton dhns @@ -2423,6 +2466,7 @@ (label 84) (parent 77) (unrealized (1 2) (2 0)) + (dead) (comment "empty cohort")) (defskeleton dhns @@ -2451,6 +2495,7 @@ (label 85) (parent 78) (unrealized (2 0) (3 0)) + (dead) (comment "empty cohort")) (defskeleton dhns @@ -2478,6 +2523,7 @@ (label 86) (parent 78) (unrealized (3 0)) + (dead) (comment "empty cohort")) (defskeleton dhns @@ -2509,6 +2555,7 @@ (label 87) (parent 78) (unrealized (2 0) (3 0)) + (dead) (comment "empty cohort")) (defskeleton dhns @@ -2536,6 +2583,7 @@ (label 88) (parent 78) (unrealized (3 0)) + (dead) (comment "empty cohort")) (defskeleton dhns @@ -2566,6 +2614,7 @@ (label 89) (parent 78) (unrealized (2 0) (3 0)) + (dead) (comment "empty cohort")) (defskeleton dhns @@ -2595,6 +2644,7 @@ (label 90) (parent 81) (unrealized (2 0)) + (dead) (comment "empty cohort")) (defskeleton dhns @@ -2629,6 +2679,7 @@ (label 91) (parent 83) (unrealized (1 2) (2 0)) + (dead) (comment "empty cohort")) (comment "Nothing left to do") @@ -2830,6 +2881,7 @@ (label 98) (parent 94) (unrealized (1 0)) + (dead) (comment "empty cohort")) (defskeleton dhns @@ -2878,6 +2930,7 @@ (label 100) (parent 94) (unrealized (0 2) (0 4) (1 0)) + (dead) (comment "empty cohort")) (defskeleton dhns @@ -2903,6 +2956,7 @@ (label 101) (parent 94) (unrealized (0 2) (0 4) (1 0)) + (dead) (comment "empty cohort")) (defskeleton dhns @@ -3038,6 +3092,7 @@ (label 105) (parent 102) (unrealized (2 1) (3 0)) + (dead) (comment "empty cohort")) (defskeleton dhns @@ -3113,6 +3168,7 @@ (label 107) (parent 102) (unrealized (2 1) (3 0)) + (dead) (comment "empty cohort")) (defskeleton dhns @@ -3147,6 +3203,7 @@ (label 108) (parent 102) (unrealized (2 1) (3 0)) + (dead) (comment "empty cohort")) (defskeleton dhns @@ -3183,6 +3240,7 @@ (label 109) (parent 102) (unrealized (2 1) (3 0)) + (dead) (comment "empty cohort")) (defskeleton dhns @@ -3222,6 +3280,7 @@ (label 110) (parent 102) (unrealized (2 1) (3 0)) + (dead) (comment "empty cohort")) (defskeleton dhns @@ -3252,6 +3311,7 @@ (label 111) (parent 103) (unrealized (2 0) (3 0)) + (dead) (comment "empty cohort")) (defskeleton dhns @@ -3281,6 +3341,7 @@ (label 112) (parent 103) (unrealized (3 0)) + (dead) (comment "empty cohort")) (defskeleton dhns @@ -3314,6 +3375,7 @@ (label 113) (parent 103) (unrealized (2 0) (3 0)) + (dead) (comment "empty cohort")) (defskeleton dhns @@ -3343,6 +3405,7 @@ (label 114) (parent 103) (unrealized (3 0)) + (dead) (comment "empty cohort")) (defskeleton dhns @@ -3375,6 +3438,7 @@ (label 115) (parent 103) (unrealized (2 0) (3 0)) + (dead) (comment "empty cohort")) (defskeleton dhns @@ -3506,6 +3570,7 @@ (label 119) (parent 106) (unrealized (2 1) (3 0)) + (dead) (comment "empty cohort")) (defskeleton dhns @@ -3622,6 +3687,7 @@ (label 122) (parent 120) (unrealized (3 1) (4 0)) + (dead) (comment "empty cohort")) (defskeleton dhns @@ -3702,6 +3768,7 @@ (label 124) (parent 120) (unrealized (3 1) (4 0)) + (dead) (comment "empty cohort")) (defskeleton dhns @@ -3739,6 +3806,7 @@ (label 125) (parent 120) (unrealized (3 1) (4 0)) + (dead) (comment "empty cohort")) (defskeleton dhns @@ -3778,6 +3846,7 @@ (label 126) (parent 120) (unrealized (3 1) (4 0)) + (dead) (comment "empty cohort")) (defskeleton dhns @@ -3819,6 +3888,7 @@ (label 127) (parent 120) (unrealized (3 1) (4 0)) + (dead) (comment "empty cohort")) (defskeleton dhns @@ -3851,6 +3921,7 @@ (label 128) (parent 121) (unrealized (3 0) (4 0)) + (dead) (comment "empty cohort")) (defskeleton dhns @@ -3882,6 +3953,7 @@ (label 129) (parent 121) (unrealized (4 0)) + (dead) (comment "empty cohort")) (defskeleton dhns @@ -3917,6 +3989,7 @@ (label 130) (parent 121) (unrealized (3 0) (4 0)) + (dead) (comment "empty cohort")) (defskeleton dhns @@ -3948,6 +4021,7 @@ (label 131) (parent 121) (unrealized (4 0)) + (dead) (comment "empty cohort")) (defskeleton dhns @@ -3982,6 +4056,7 @@ (label 132) (parent 121) (unrealized (3 0) (4 0)) + (dead) (comment "empty cohort")) (defskeleton dhns @@ -4020,6 +4095,7 @@ (label 133) (parent 123) (unrealized (3 1) (4 0)) + (dead) (comment "empty cohort")) (comment "Nothing left to do") diff --git a/tst/enrich.tst b/tst/enrich.tst --- a/tst/enrich.tst +++ b/tst/enrich.tst @@ -1,6 +1,6 @@ (herald enrich) -(comment "CPSA 3.6.1") +(comment "CPSA 3.6.2") (comment "All input read from enrich.scm") (defprotocol enrich 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 20)) -(comment "CPSA 3.6.1") +(comment "CPSA 3.6.2") (comment "All input read from envelope.scm") (comment "Strand count bounded at 20") @@ -78,6 +78,7 @@ (label 0) (unrealized (0 0) (1 0) (2 5)) (preskeleton) + (origs (esk (2 0)) (n (2 2)) (tno (2 2)) (v (2 6))) (comment "Not a skeleton")) (defskeleton envelope @@ -149,6 +150,7 @@ (label 2) (parent 1) (unrealized (0 0) (3 1)) + (dead) (comment "empty cohort")) (defskeleton envelope @@ -230,6 +232,7 @@ (label 4) (parent 3) (unrealized (0 0) (1 0) (4 1)) + (dead) (comment "empty cohort")) (defskeleton envelope @@ -305,6 +308,7 @@ (label 6) (parent 5) (unrealized (0 0) (4 1)) + (dead) (comment "empty cohort")) (defskeleton envelope @@ -388,6 +392,7 @@ (label 8) (parent 7) (unrealized (0 0) (5 1)) + (dead) (comment "empty cohort")) (defskeleton envelope @@ -894,6 +899,7 @@ (label 15) (parent 12) (unrealized (0 0) (6 2) (8 3)) + (dead) (comment "empty cohort")) (defskeleton envelope @@ -1030,6 +1036,7 @@ (label 17) (parent 13) (unrealized (0 0) (7 1)) + (dead) (comment "empty cohort")) (defskeleton envelope @@ -1420,6 +1427,7 @@ (label 22) (parent 16) (unrealized (7 1)) + (dead) (comment "empty cohort")) (defskeleton envelope @@ -1496,6 +1504,7 @@ (label 23) (parent 18) (unrealized (0 0) (8 1)) + (dead) (comment "empty cohort")) (defskeleton envelope @@ -1974,6 +1983,7 @@ (label 28) (parent 24) (unrealized (0 0) (6 2) (10 3)) + (dead) (comment "empty cohort")) (defskeleton envelope @@ -2075,6 +2085,7 @@ (label 29) (parent 25) (unrealized (0 0) (6 2) (10 3)) + (dead) (comment "empty cohort")) (defskeleton envelope @@ -2247,6 +2258,7 @@ (label 31) (parent 26) (unrealized (0 0) (10 1)) + (dead) (comment "empty cohort")) (defskeleton envelope @@ -2517,6 +2529,7 @@ (label 34) (parent 30) (unrealized (0 0) (6 0) (10 1)) + (dead) (comment "empty cohort")) (defskeleton envelope @@ -2695,6 +2708,7 @@ (label 36) (parent 32) (unrealized (0 0) (11 1)) + (dead) (comment "empty cohort")) (defskeleton envelope @@ -3105,6 +3119,7 @@ (label 40) (parent 35) (unrealized (0 0) (6 0) (11 1)) + (dead) (comment "empty cohort")) (defskeleton envelope @@ -3202,6 +3217,7 @@ (label 41) (parent 37) (unrealized (0 0) (12 1)) + (dead) (comment "empty cohort")) (defskeleton envelope @@ -3336,6 +3352,7 @@ (label 42) (parent 38) (unrealized (9 2) (11 3)) + (dead) (comment "empty cohort")) (defskeleton envelope @@ -4079,6 +4096,7 @@ (label 48) (parent 45) (unrealized (9 2) (13 3)) + (dead) (comment "empty cohort")) (defskeleton envelope @@ -4208,6 +4226,7 @@ (label 49) (parent 46) (unrealized (9 2) (13 3)) + (dead) (comment "empty cohort")) (defskeleton envelope @@ -4437,6 +4456,7 @@ (label 51) (parent 47) (unrealized (13 1)) + (dead) (comment "empty cohort")) (defskeleton envelope @@ -4669,6 +4689,7 @@ (label 53) (parent 50) (unrealized (9 0) (13 1)) + (dead) (comment "empty cohort")) (defskeleton envelope @@ -4906,6 +4927,7 @@ (label 55) (parent 52) (unrealized (14 1)) + (dead) (comment "empty cohort")) (defskeleton envelope @@ -5148,6 +5170,7 @@ (label 57) (parent 54) (unrealized (9 0) (14 1)) + (dead) (comment "empty cohort")) (defskeleton envelope @@ -5273,6 +5296,7 @@ (label 58) (parent 56) (unrealized (15 1)) + (dead) (comment "empty cohort")) (comment "Nothing left to do") @@ -5347,6 +5371,7 @@ (label 59) (unrealized (0 0) (1 5)) (preskeleton) + (origs (esk (1 0)) (n (1 2)) (tno (1 2)) (v (1 6))) (comment "Not a skeleton")) (defskeleton envelope @@ -5410,6 +5435,7 @@ (label 61) (parent 60) (unrealized (2 1)) + (dead) (comment "empty cohort")) (defskeleton envelope @@ -5483,6 +5509,7 @@ (label 63) (parent 62) (unrealized (0 0) (3 1)) + (dead) (comment "empty cohort")) (defskeleton envelope @@ -5549,6 +5576,7 @@ (label 65) (parent 64) (unrealized (3 1)) + (dead) (comment "empty cohort")) (defskeleton envelope @@ -5623,6 +5651,7 @@ (label 67) (parent 66) (unrealized (4 1)) + (dead) (comment "empty cohort")) (defskeleton envelope @@ -6094,6 +6123,7 @@ (label 74) (parent 71) (unrealized (5 2) (7 3)) + (dead) (comment "empty cohort")) (defskeleton envelope @@ -6226,6 +6256,7 @@ (label 76) (parent 72) (unrealized (6 1)) + (dead) (comment "empty cohort")) (defskeleton envelope @@ -6525,6 +6556,7 @@ (label 80) (parent 77) (unrealized (7 1)) + (dead) (comment "empty cohort")) (defskeleton envelope @@ -6898,6 +6930,7 @@ (label 84) (parent 81) (unrealized (5 2) (9 3)) + (dead) (comment "empty cohort")) (defskeleton envelope @@ -6993,6 +7026,7 @@ (label 85) (parent 82) (unrealized (5 2) (9 3)) + (dead) (comment "empty cohort")) (defskeleton envelope @@ -7153,6 +7187,7 @@ (label 87) (parent 83) (unrealized (9 1)) + (dead) (comment "empty cohort")) (defskeleton envelope @@ -7316,6 +7351,7 @@ (label 89) (parent 86) (unrealized (5 0) (9 1)) + (dead) (comment "empty cohort")) (defskeleton envelope @@ -7484,6 +7520,7 @@ (label 91) (parent 88) (unrealized (10 1)) + (dead) (comment "empty cohort")) (defskeleton envelope @@ -7658,6 +7695,7 @@ (label 93) (parent 90) (unrealized (5 0) (10 1)) + (dead) (comment "empty cohort")) (defskeleton envelope @@ -7750,6 +7788,7 @@ (label 94) (parent 92) (unrealized (11 1)) + (dead) (comment "empty cohort")) (comment "Nothing left to do") 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 3.6.1") +(comment "CPSA 3.6.2") (comment "All input read from ffgg.scm") (defprotocol ffgg basic @@ -29,6 +29,7 @@ (label 0) (unrealized (1 0)) (preskeleton) + (origs (m (0 2))) (comment "Not a skeleton")) (defskeleton ffgg diff --git a/tst/fnof_or.tst b/tst/fnof_or.tst --- a/tst/fnof_or.tst +++ b/tst/fnof_or.tst @@ -2,7 +2,7 @@ (comment "Version using variables of sort mesg, with ltk function emulated.")) -(comment "CPSA 3.6.1") +(comment "CPSA 3.6.2") (comment "All input read from fnof_or.scm") (defprotocol or basic diff --git a/tst/fnof_test.tst b/tst/fnof_test.tst --- a/tst/fnof_test.tst +++ b/tst/fnof_test.tst @@ -1,7 +1,7 @@ (herald "Function constraint test protocol" (comment "Skeletons 2, 4, and 7 should have no shapes.")) -(comment "CPSA 3.6.1") +(comment "CPSA 3.6.2") (comment "All input read from fnof_test.scm") (defprotocol fnoftest basic @@ -56,6 +56,7 @@ (traces ((send (cat n0 (enc an0 an1 n0 n1 k))) (recv n1))) (label 2) (unrealized (0 1)) + (dead) (origs (n0 (0 0)) (n1 (0 0))) (comment "empty cohort")) @@ -78,6 +79,7 @@ (label 3) (unrealized) (preskeleton) + (origs (n1 (0 0))) (comment "Not a skeleton")) (defskeleton fnoftest @@ -113,6 +115,7 @@ (traces ((send (cat n1 (enc an0 an1 n1 n1 k))) (recv n1))) (label 5) (unrealized) + (origs (n1 (0 0))) (comment "Input cannot be made into a skeleton--nothing to do")) (defprotocol fnoftest2 basic @@ -221,6 +224,7 @@ (traces ((send (cat n0 (enc bn0 bn1 an0 an1 n0 n1 k))) (recv n1))) (label 10) (unrealized (0 1)) + (dead) (origs (n0 (0 0)) (n1 (0 0))) (comment "empty cohort")) diff --git a/tst/fnof_woolam.tst b/tst/fnof_woolam.tst --- a/tst/fnof_woolam.tst +++ b/tst/fnof_woolam.tst @@ -1,6 +1,6 @@ (herald "Woo-Lam Protocol, using fnof to emulate ltk function") -(comment "CPSA 3.6.1") +(comment "CPSA 3.6.2") (comment "All input read from fnof_woolam.scm") (defprotocol woolam basic diff --git a/tst/fnof_yahalom.tst b/tst/fnof_yahalom.tst --- a/tst/fnof_yahalom.tst +++ b/tst/fnof_yahalom.tst @@ -2,7 +2,7 @@ "Yahalom Protocol with Forwarding Removed, using fnof to emulate ltk function" (bound 12)) -(comment "CPSA 3.6.1") +(comment "CPSA 3.6.2") (comment "All input read from fnof_yahalom.scm") (defprotocol yahalom basic @@ -268,6 +268,7 @@ (label 8) (parent 6) (unrealized (1 0)) + (dead) (comment "empty cohort")) (defskeleton yahalom @@ -297,6 +298,7 @@ (label 9) (parent 7) (unrealized (1 0)) + (dead) (comment "empty cohort")) (comment "Nothing left to do") diff --git a/tst/goals.scm b/tst/goals.scm --- a/tst/goals.scm +++ b/tst/goals.scm @@ -214,6 +214,20 @@ (= z z-0)))) (comment "Double initiator point of view")) +;;; Double initiator point of view +(defskeleton ns + (vars (a b name) (n1 n1-0 text)) + (defstrand init 3 (a a) (b b) (n1 n1)) + (defstrand init 3 (a a) (b b) (n1 n1-0)) + (non-orig (privk b) (privk a)) + (uniq-orig n1 n1-0) + (goals + (forall ((z z-0 strd)) + (implies + (and (p "init" z 3) (p "init" z-0 3)) + (= z z-0)))) + (comment "Double initiator point of view 2")) + (defprotocol nsl-typeless basic (defrole init (vars (a b name) (n1 text) (n2 mesg)) 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 3.6.1") +(comment "CPSA 3.6.2") (comment "All input read from goals.scm") (defprotocol ns basic @@ -260,6 +260,7 @@ (label 8) (unrealized (0 0) (1 1)) (preskeleton) + (origs (n1 (1 0))) (comment "Not a skeleton")) (defskeleton ns @@ -427,6 +428,7 @@ (label 16) (parent 14) (unrealized (0 0)) + (dead) (comment "empty cohort")) (comment "Nothing left to do") @@ -754,6 +756,7 @@ (label 28) (unrealized (0 0) (1 2)) (preskeleton) + (origs (n2 (1 1))) (comment "Not a skeleton")) (defskeleton ns @@ -1037,6 +1040,184 @@ (comment "Nothing left to do") +(defprotocol ns basic + (defrole init + (vars (a b name) (n1 n2 text)) + (trace (send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a))) + (send (enc n2 (pubk b))))) + (defrole resp + (vars (b a name) (n2 n1 text)) + (trace (recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a))) + (recv (enc n2 (pubk b))))) + (comment "Needham-Schroeder with no role origination assumptions")) + +(defskeleton ns + (vars (n1 n1-0 n2 n2-0 text) (a b name)) + (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b)) + (defstrand init 3 (n1 n1-0) (n2 n2-0) (a a) (b b)) + (non-orig (privk a) (privk b)) + (uniq-orig n1 n1-0) + (subgoals + (forall ((z z-0 strd)) + (implies (and (p "init" z 3) (p "init" z-0 3)) (= z z-0)))) + (comment "Double initiator point of view 2") + (traces + ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a))) + (send (enc n2 (pubk b)))) + ((send (enc n1-0 a (pubk b))) (recv (enc n1-0 n2-0 (pubk a))) + (send (enc n2-0 (pubk b))))) + (label 41) + (unrealized (0 1) (1 1)) + (origs (n1 (0 0)) (n1-0 (1 0))) + (comment "1 in cohort - 1 not yet seen")) + +(defskeleton ns + (vars (n1 n2 text) (a b name)) + (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b)) + (non-orig (privk a) (privk b)) + (uniq-orig n1) + (operation collapsed 1 0) + (traces + ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a))) + (send (enc n2 (pubk b))))) + (label 42) + (parent 41) + (unrealized (0 1)) + (comment "1 in cohort - 1 not yet seen")) + +(defskeleton ns + (vars (n1 n1-0 n2 n2-0 n2-1 text) (a b name)) + (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b)) + (defstrand init 3 (n1 n1-0) (n2 n2-0) (a a) (b b)) + (defstrand resp 2 (n2 n2-1) (n1 n1-0) (b b) (a a)) + (precedes ((1 0) (2 0)) ((2 1) (1 1))) + (non-orig (privk a) (privk b)) + (uniq-orig n1 n1-0) + (operation nonce-test (added-strand resp 2) n1-0 (1 1) + (enc n1-0 a (pubk b))) + (traces + ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a))) + (send (enc n2 (pubk b)))) + ((send (enc n1-0 a (pubk b))) (recv (enc n1-0 n2-0 (pubk a))) + (send (enc n2-0 (pubk b)))) + ((recv (enc n1-0 a (pubk b))) (send (enc n1-0 n2-1 (pubk a))))) + (label 43) + (parent 41) + (unrealized (0 1) (1 1)) + (comment "1 in cohort - 1 not yet seen")) + +(defskeleton ns + (vars (n1 n2 n2-0 text) (a b name)) + (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b)) + (defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a)) + (precedes ((0 0) (1 0)) ((1 1) (0 1))) + (non-orig (privk a) (privk b)) + (uniq-orig n1) + (operation nonce-test (added-strand resp 2) n1 (0 1) + (enc n1 a (pubk b))) + (traces + ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a))) + (send (enc n2 (pubk b)))) + ((recv (enc n1 a (pubk b))) (send (enc n1 n2-0 (pubk a))))) + (label 44) + (parent 42) + (unrealized (0 1)) + (origs (n1 (0 0))) + (comment "1 in cohort - 1 not yet seen")) + +(defskeleton ns + (vars (n1 n1-0 n2 n2-0 text) (a b name)) + (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b)) + (defstrand init 3 (n1 n1-0) (n2 n2-0) (a a) (b b)) + (defstrand resp 2 (n2 n2-0) (n1 n1-0) (b b) (a a)) + (precedes ((1 0) (2 0)) ((2 1) (1 1))) + (non-orig (privk a) (privk b)) + (uniq-orig n1 n1-0) + (operation nonce-test (contracted (n2-1 n2-0)) n1-0 (1 1) + (enc n1-0 n2-0 (pubk a)) (enc n1-0 a (pubk b))) + (traces + ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a))) + (send (enc n2 (pubk b)))) + ((send (enc n1-0 a (pubk b))) (recv (enc n1-0 n2-0 (pubk a))) + (send (enc n2-0 (pubk b)))) + ((recv (enc n1-0 a (pubk b))) (send (enc n1-0 n2-0 (pubk a))))) + (label 45) + (parent 43) + (unrealized (0 1)) + (comment "1 in cohort - 1 not yet seen")) + +(defskeleton ns + (vars (n1 n2 text) (a b name)) + (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b)) + (defstrand resp 2 (n2 n2) (n1 n1) (b b) (a a)) + (precedes ((0 0) (1 0)) ((1 1) (0 1))) + (non-orig (privk a) (privk b)) + (uniq-orig n1) + (operation nonce-test (contracted (n2-0 n2)) n1 (0 1) + (enc n1 n2 (pubk a)) (enc n1 a (pubk b))) + (traces + ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a))) + (send (enc n2 (pubk b)))) + ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a))))) + (label 46) + (parent 44) + (unrealized) + (shape) + (satisfies yes) + (maps ((0 0) ((a a) (b b) (n1 n1) (n1-0 n1) (n2 n2) (n2-0 n2)))) + (origs (n1 (0 0)))) + +(defskeleton ns + (vars (n1 n1-0 n2 n2-0 n2-1 text) (a b name)) + (defstrand init 3 (n1 n1) (n2 n2) (a a) (b b)) + (defstrand init 3 (n1 n1-0) (n2 n2-0) (a a) (b b)) + (defstrand resp 2 (n2 n2-0) (n1 n1-0) (b b) (a a)) + (defstrand resp 2 (n2 n2-1) (n1 n1) (b b) (a a)) + (precedes ((0 0) (3 0)) ((1 0) (2 0)) ((2 1) (1 1)) ((3 1) (0 1))) + (non-orig (privk a) (privk b)) + (uniq-orig n1 n1-0) + (operation nonce-test (added-strand resp 2) n1 (0 1) + (enc n1 a (pubk b))) + (traces + ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a))) + (send (enc n2 (pubk b)))) + ((send (enc n1-0 a (pubk b))) (recv (enc n1-0 n2-0 (pubk a))) + (send (enc n2-0 (pubk b)))) + ((recv (enc n1-0 a (pubk b))) (send (enc n1-0 n2-0 (pubk a)))) + ((recv (enc n1 a (pubk b))) (send (enc n1 n2-1 (pubk a))))) + (label 47) + (parent 45) + (unrealized (0 1)) + (comment "1 in cohort - 1 not yet seen")) + +(defskeleton ns + (vars (n1 n1-0 n2 n2-0 text) (a b name)) + (defstrand init 3 (n1 n1) (n2 n2-0) (a a) (b b)) + (defstrand init 3 (n1 n1-0) (n2 n2) (a a) (b b)) + (defstrand resp 2 (n2 n2) (n1 n1-0) (b b) (a a)) + (defstrand resp 2 (n2 n2-0) (n1 n1) (b b) (a a)) + (precedes ((0 0) (3 0)) ((1 0) (2 0)) ((2 1) (1 1)) ((3 1) (0 1))) + (non-orig (privk a) (privk b)) + (uniq-orig n1 n1-0) + (operation nonce-test (contracted (n2-1 n2-0)) n1 (0 1) + (enc n1 n2-0 (pubk a)) (enc n1 a (pubk b))) + (traces + ((send (enc n1 a (pubk b))) (recv (enc n1 n2-0 (pubk a))) + (send (enc n2-0 (pubk b)))) + ((send (enc n1-0 a (pubk b))) (recv (enc n1-0 n2 (pubk a))) + (send (enc n2 (pubk b)))) + ((recv (enc n1-0 a (pubk b))) (send (enc n1-0 n2 (pubk a)))) + ((recv (enc n1 a (pubk b))) (send (enc n1 n2-0 (pubk a))))) + (label 48) + (parent 47) + (unrealized) + (shape) + (satisfies (no (z 0) (z-0 1))) + (maps ((0 1) ((a a) (b b) (n1 n1) (n1-0 n1-0) (n2 n2-0) (n2-0 n2)))) + (origs (n1 (0 0)) (n1-0 (1 0)))) + +(comment "Nothing left to do") + (defprotocol nsl-typeless basic (defrole init (vars (a b name) (n1 text) (n2 mesg)) @@ -1063,9 +1244,10 @@ (comment "Shows typeflaw in typeless NSL") (traces ((recv n2)) ((recv (enc a n1 (pubk b))) (send (enc n1 n2 b (pubk a))))) - (label 41) + (label 49) (unrealized (0 0)) (preskeleton) + (origs (n2 (1 1))) (comment "Not a skeleton")) (defskeleton nsl-typeless @@ -1084,8 +1266,8 @@ (comment "Shows typeflaw in typeless NSL") (traces ((recv n2)) ((recv (enc a n1 (pubk b))) (send (enc n1 n2 b (pubk a))))) - (label 42) - (parent 41) + (label 50) + (parent 49) (unrealized (0 0)) (origs (n2 (1 1))) (comment "2 in cohort - 2 not yet seen")) @@ -1104,9 +1286,10 @@ ((recv (enc a n1 (pubk b))) (send (enc n1 n2 b (pubk a)))) ((send (enc a n1 (pubk b))) (recv (enc n1 n2 b (pubk a))) (send (enc n2 (pubk b))))) - (label 43) - (parent 42) + (label 51) + (parent 50) (unrealized (0 0)) + (dead) (comment "empty cohort")) (defskeleton nsl-typeless @@ -1123,8 +1306,8 @@ ((recv (enc a a-0 (pubk b))) (send (enc a-0 n2 b (pubk a)))) ((recv (enc a-0 n2 b (pubk a))) (send (enc (cat n2 b) n2-0 a (pubk a-0))))) - (label 44) - (parent 42) + (label 52) + (parent 50) (unrealized) (shape) (satisfies (no (n2 n2) (a a) (b b) (z 1) (z-0 0))) diff --git a/tst/iadh_um.tst b/tst/iadh_um.tst # file too large to diff: tst/iadh_um.tst diff --git a/tst/injection.tst b/tst/injection.tst --- a/tst/injection.tst +++ b/tst/injection.tst @@ -2,7 +2,7 @@ (comment "This protocol contains a man-in-the-middle" "attack discovered by Galvin Lowe.")) -(comment "CPSA 3.6.1") +(comment "CPSA 3.6.2") (comment "All input read from injection.scm") (defprotocol ns diffie-hellman diff --git a/tst/kerb.tst b/tst/kerb.tst --- a/tst/kerb.tst +++ b/tst/kerb.tst @@ -1,4 +1,4 @@ -(comment "CPSA 3.6.1") +(comment "CPSA 3.6.2") (comment "All input read from kerb.scm") (defprotocol kerb-flawed basic @@ -30,6 +30,7 @@ (label 0) (unrealized (0 1) (1 0)) (preskeleton) + (origs (n (0 0)) (m (0 2))) (comment "Not a skeleton")) (defskeleton kerb-flawed @@ -112,6 +113,7 @@ (label 4) (parent 3) (unrealized (3 0)) + (dead) (comment "empty cohort")) (comment "Nothing left to do") @@ -143,6 +145,7 @@ (label 5) (unrealized (0 1) (1 0)) (preskeleton) + (origs (n (0 0)) (m (0 2))) (comment "Not a skeleton")) (defskeleton kerb-flawed2 diff --git a/tst/kerberos++.tst b/tst/kerberos++.tst --- a/tst/kerberos++.tst +++ b/tst/kerberos++.tst @@ -1,4 +1,4 @@ -(comment "CPSA 3.6.1") +(comment "CPSA 3.6.2") (comment "All input read from kerberos++.scm") (defprotocol kerberos basic @@ -150,6 +150,7 @@ (label 3) (parent 1) (unrealized (2 0)) + (dead) (comment "empty cohort")) (defskeleton kerberos @@ -201,6 +202,7 @@ (label 4) (parent 2) (unrealized (2 0) (3 3)) + (dead) (comment "empty cohort")) (defskeleton kerberos @@ -286,6 +288,7 @@ (label 6) (parent 2) (unrealized (2 0) (3 1)) + (dead) (comment "empty cohort")) (defskeleton kerberos @@ -327,6 +330,7 @@ (label 7) (parent 2) (unrealized (3 0)) + (dead) (comment "empty cohort")) (defskeleton kerberos @@ -690,6 +694,7 @@ (label 15) (parent 10) (unrealized (4 0)) + (dead) (comment "empty cohort")) (defskeleton kerberos @@ -787,6 +792,7 @@ (label 17) (parent 11) (unrealized (4 0)) + (dead) (comment "empty cohort")) (defskeleton kerberos @@ -846,6 +852,7 @@ (label 18) (parent 12) (unrealized (3 0) (4 1)) + (dead) (comment "empty cohort")) (defskeleton kerberos @@ -906,6 +913,7 @@ (label 19) (parent 12) (unrealized (5 0)) + (dead) (comment "empty cohort")) (defskeleton kerberos @@ -963,6 +971,7 @@ (label 20) (parent 13) (unrealized (5 0)) + (dead) (comment "empty cohort")) (defskeleton kerberos @@ -1013,6 +1022,7 @@ (label 21) (parent 14) (unrealized (5 0)) + (dead) (comment "empty cohort")) (comment "Nothing left to do") @@ -1138,6 +1148,7 @@ (label 24) (parent 23) (unrealized (2 3)) + (dead) (comment "empty cohort")) (defskeleton kerberos @@ -1203,6 +1214,7 @@ (label 26) (parent 23) (unrealized (2 0)) + (dead) (comment "empty cohort")) (defskeleton kerberos diff --git a/tst/lt_test.tst b/tst/lt_test.tst --- a/tst/lt_test.tst +++ b/tst/lt_test.tst @@ -2,7 +2,7 @@ (comment "First and third skeletons should have a shape," "second and fourth should be dead.")) -(comment "CPSA 3.6.1") +(comment "CPSA 3.6.2") (comment "All input read from lt_test.scm") (defprotocol lttest basic @@ -55,6 +55,7 @@ (traces ((send (cat n1 (enc n1 n2 k))) (recv n2))) (label 2) (unrealized (0 1)) + (dead) (origs (n1 (0 0)) (n2 (0 0))) (comment "empty cohort")) @@ -114,6 +115,7 @@ (traces ((send n) (send (cat n1 (enc n1 n2 k))) (recv n2))) (label 5) (unrealized (0 2)) + (dead) (origs (n1 (0 1)) (n2 (0 1))) (comment "empty cohort")) 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, and hird should be dead.")) -(comment "CPSA 3.6.1") +(comment "CPSA 3.6.2") (comment "All input read from neq_test.scm") (defprotocol neqtest basic @@ -55,6 +55,7 @@ (traces ((send (cat n1 (enc n1 n2 k))) (recv n2))) (label 2) (unrealized (0 1)) + (dead) (origs (n1 (0 0)) (n2 (0 0))) (comment "empty cohort")) @@ -76,6 +77,7 @@ (traces ((send (cat n1 (enc n1 n2 n3 k))) (recv n2))) (label 3) (unrealized (0 1)) + (dead) (origs (n1 (0 0)) (n2 (0 0))) (comment "empty cohort")) diff --git a/tst/ns.tst b/tst/ns.tst --- a/tst/ns.tst +++ b/tst/ns.tst @@ -2,7 +2,7 @@ (comment "This protocol contains a man-in-the-middle" "attack discovered by Galvin Lowe.")) -(comment "CPSA 3.6.1") +(comment "CPSA 3.6.2") (comment "All input read from ns.scm") (defprotocol ns basic 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 3.6.1") +(comment "CPSA 3.6.2") (comment "All input read from or.scm") (defprotocol or basic diff --git a/tst/owang.tst b/tst/owang.tst --- a/tst/owang.tst +++ b/tst/owang.tst @@ -1,4 +1,4 @@ -(comment "CPSA 3.6.1") +(comment "CPSA 3.6.2") (comment "All input read from owang.scm") (defprotocol wang basic @@ -294,6 +294,7 @@ (label 0) (unrealized (1 0)) (preskeleton) + (origs (m (0 0)) (k (0 0))) (comment "Not a skeleton")) (defskeleton wang @@ -795,6 +796,7 @@ (label 7) (unrealized (1 0)) (preskeleton) + (origs (m (0 0)) (k (0 0))) (comment "Not a skeleton")) (defskeleton wang diff --git a/tst/owat.tst b/tst/owat.tst --- a/tst/owat.tst +++ b/tst/owat.tst @@ -1,7 +1,7 @@ (herald "One-way Authentication Test with bltk keys" (algebra diffie-hellman) (bound 12)) -(comment "CPSA 3.6.1") +(comment "CPSA 3.6.2") (comment "All input read from owat.scm") (defprotocol owa diffie-hellman diff --git a/tst/pkinit.tst b/tst/pkinit.tst --- a/tst/pkinit.tst +++ b/tst/pkinit.tst @@ -1,6 +1,6 @@ (herald "Kerberos PKINIT") -(comment "CPSA 3.6.1") +(comment "CPSA 3.6.2") (comment "All input read from pkinit.scm") (defprotocol pkinit-flawed basic @@ -254,6 +254,7 @@ (label 7) (parent 6) (unrealized (2 0)) + (dead) (comment "empty cohort")) (comment "Nothing left to do") @@ -422,6 +423,7 @@ (label 12) (parent 11) (unrealized (2 0)) + (dead) (comment "empty cohort")) (comment "Nothing left to do") @@ -470,6 +472,7 @@ (label 13) (unrealized (1 1)) (preskeleton) + (origs (n1-0 (1 0)) (n2-0 (1 0)) (k (0 1)) (ak (0 1))) (comment "Not a skeleton")) (defskeleton pkinit-flawed @@ -583,6 +586,7 @@ (label 16) (unrealized (1 1)) (preskeleton) + (origs (n1-0 (1 0)) (n2-0 (1 0)) (k (0 1)) (ak (0 1))) (comment "Not a skeleton")) (defskeleton pkinit-fix1 @@ -755,6 +759,7 @@ (label 22) (parent 20) (unrealized (0 0) (2 0)) + (dead) (comment "empty cohort")) (comment "Nothing left to do") @@ -810,6 +815,7 @@ (label 23) (unrealized (1 1)) (preskeleton) + (origs (n1-0 (1 0)) (n2-0 (1 0)) (k (0 1)) (ak (0 1))) (comment "Not a skeleton")) (defskeleton pkinit-fix2 @@ -972,6 +978,7 @@ (label 28) (parent 27) (unrealized (2 0)) + (dead) (comment "empty cohort")) (comment "Nothing left to do") diff --git a/tst/plaindh.tst b/tst/plaindh.tst --- a/tst/plaindh.tst +++ b/tst/plaindh.tst @@ -1,7 +1,7 @@ (herald "Plain diffie-hellman protocol with challenge-response" (algebra diffie-hellman)) -(comment "CPSA 3.6.1") +(comment "CPSA 3.6.2") (comment "All input read from plaindh.scm") (defprotocol plaindh diffie-hellman diff --git a/tst/priority_test.tst b/tst/priority_test.tst --- a/tst/priority_test.tst +++ b/tst/priority_test.tst @@ -1,6 +1,6 @@ (herald "Receive priority test protocol") -(comment "CPSA 3.6.1") +(comment "CPSA 3.6.2") (comment "All input read from priority_test.scm") (defprotocol priority_test 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 3.6.1") +(comment "CPSA 3.6.2") (comment "All input read from reflect.scm") (defprotocol reflect basic diff --git a/tst/staticdh.tst b/tst/staticdh.tst --- a/tst/staticdh.tst +++ b/tst/staticdh.tst @@ -1,6 +1,6 @@ (herald "Static DH key exchange" (algebra diffie-hellman)) -(comment "CPSA 3.6.1") +(comment "CPSA 3.6.2") (comment "All input read from staticdh.scm") (defprotocol staticdh1 diffie-hellman @@ -569,6 +569,7 @@ (label 18) (parent 9) (unrealized (3 0) (4 0)) + (dead) (comment "empty cohort")) (defskeleton staticdh1 @@ -600,6 +601,7 @@ (label 19) (parent 9) (unrealized (3 0) (4 0)) + (dead) (comment "empty cohort")) (comment "Nothing left to do") diff --git a/tst/station.tst b/tst/station.tst --- a/tst/station.tst +++ b/tst/station.tst @@ -1,6 +1,6 @@ (herald "Station-to-station protocol" (algebra diffie-hellman)) -(comment "CPSA 3.6.1") +(comment "CPSA 3.6.2") (comment "All input read from station.scm") (defprotocol station-to-station diffie-hellman @@ -217,6 +217,7 @@ (label 5) (parent 4) (unrealized (2 0) (3 0)) + (dead) (comment "empty cohort")) (defskeleton station-to-station @@ -253,6 +254,7 @@ (label 6) (parent 4) (unrealized (3 0)) + (dead) (comment "empty cohort")) (defskeleton station-to-station @@ -289,6 +291,7 @@ (label 7) (parent 4) (unrealized (3 0)) + (dead) (comment "empty cohort")) (defskeleton station-to-station @@ -328,6 +331,7 @@ (label 8) (parent 4) (unrealized (2 0) (3 0)) + (dead) (comment "empty cohort")) (defskeleton station-to-station @@ -372,6 +376,7 @@ (label 9) (parent 4) (unrealized (2 0) (3 0)) + (dead) (comment "empty cohort")) (comment "Nothing left to do") @@ -599,6 +604,7 @@ (label 15) (parent 14) (unrealized (2 0) (3 0)) + (dead) (comment "empty cohort")) (defskeleton station-to-station @@ -636,6 +642,7 @@ (label 16) (parent 14) (unrealized (3 0)) + (dead) (comment "empty cohort")) (defskeleton station-to-station @@ -676,6 +683,7 @@ (label 17) (parent 14) (unrealized (2 0) (3 0)) + (dead) (comment "empty cohort")) (defskeleton station-to-station @@ -713,6 +721,7 @@ (label 18) (parent 14) (unrealized (3 0)) + (dead) (comment "empty cohort")) (defskeleton station-to-station @@ -757,6 +766,7 @@ (label 19) (parent 14) (unrealized (2 0) (3 0)) + (dead) (comment "empty cohort")) (comment "Nothing left to do") diff --git a/tst/station2.tst b/tst/station2.tst --- a/tst/station2.tst +++ b/tst/station2.tst @@ -1,6 +1,6 @@ (herald "Station-to-station protocol" (algebra diffie-hellman)) -(comment "CPSA 3.6.1") +(comment "CPSA 3.6.2") (comment "All input read from station2.scm") (defprotocol station-to-station diffie-hellman diff --git a/tst/subsort_test.tst b/tst/subsort_test.tst --- a/tst/subsort_test.tst +++ b/tst/subsort_test.tst @@ -2,7 +2,7 @@ (comment "First, third, and fourth skeletons should have a shape," "second should be dead.")) -(comment "CPSA 3.6.1") +(comment "CPSA 3.6.2") (comment "All input read from subsort_test.scm") (defprotocol subsorttest basic @@ -55,6 +55,7 @@ (traces ((send (cat n1 (enc n1 n2 k))) (recv n2))) (label 2) (unrealized (0 1)) + (dead) (origs (n1 (0 0)) (n2 (0 0))) (comment "empty cohort")) diff --git a/tst/test_small.tst b/tst/test_small.tst --- a/tst/test_small.tst +++ b/tst/test_small.tst @@ -1,6 +1,6 @@ (herald "small test" (algebra diffie-hellman)) -(comment "CPSA 3.6.1") +(comment "CPSA 3.6.2") (comment "All input read from test_small.scm") (defprotocol test diffie-hellman 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 3.6.1") +(comment "CPSA 3.6.2") (comment "All input read from 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 3.6.1") +(comment "CPSA 3.6.2") (comment "All input read from uniq-gen-test.scm") (defprotocol uniqgentest basic @@ -133,6 +133,7 @@ (label 7) (parent 5) (unrealized (1 0)) + (dead) (comment "empty cohort")) (comment "Nothing left to do") 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 3.6.1") +(comment "CPSA 3.6.2") (comment "All input read from woolam.scm") (defprotocol woolam basic diff --git a/tst/wrap_decrypt.tst b/tst/wrap_decrypt.tst --- a/tst/wrap_decrypt.tst +++ b/tst/wrap_decrypt.tst @@ -1,6 +1,6 @@ (herald wrap-decrypt (bound 10)) -(comment "CPSA 3.6.1") +(comment "CPSA 3.6.2") (comment "All input read from wrap_decrypt.lsp") (comment "Strand count bounded at 10") @@ -51,6 +51,7 @@ (label 0) (unrealized (1 2) (3 0) (4 0) (5 2) (5 3)) (preskeleton) + (origs) (comment "Not a skeleton")) (defskeleton wrap-decrypt @@ -345,6 +346,7 @@ (label 10) (parent 6) (unrealized (1 2) (3 0) (4 0)) + (dead) (comment "empty cohort")) (defskeleton wrap-decrypt @@ -470,6 +472,7 @@ (label 14) (parent 8) (unrealized (1 2) (3 0) (4 0)) + (dead) (origs) (comment "empty cohort")) @@ -664,6 +667,7 @@ (label 20) (parent 12) (unrealized (1 2) (3 0) (4 0)) + (dead) (comment "empty cohort")) (defskeleton wrap-decrypt @@ -821,6 +825,7 @@ (label 26) (parent 16) (unrealized (1 2) (3 0) (4 0)) + (dead) (comment "empty cohort")) (defskeleton wrap-decrypt @@ -1059,6 +1064,7 @@ (label 33) (parent 19) (unrealized (1 2) (8 0)) + (dead) (comment "empty cohort")) (defskeleton wrap-decrypt @@ -1257,6 +1263,7 @@ (label 39) (parent 25) (unrealized (1 2) (7 0)) + (dead) (comment "empty cohort")) (defskeleton wrap-decrypt @@ -1326,6 +1333,7 @@ (label 41) (parent 28) (unrealized (1 2) (3 0) (4 0)) + (dead) (comment "empty cohort")) (defskeleton wrap-decrypt @@ -1433,6 +1441,7 @@ (label 45) (parent 32) (unrealized (8 0)) + (dead) (comment "empty cohort")) (defskeleton wrap-decrypt @@ -1606,6 +1615,7 @@ (label 51) (parent 38) (unrealized (7 0)) + (dead) (comment "empty cohort")) (defskeleton wrap-decrypt @@ -1713,6 +1723,7 @@ (label 57) (parent 48) (unrealized (8 0)) + (dead) (comment "empty cohort")) (defskeleton wrap-decrypt @@ -1750,6 +1761,7 @@ (label 58) (parent 49) (unrealized (8 0)) + (dead) (comment "empty cohort")) (defskeleton wrap-decrypt @@ -1787,6 +1799,7 @@ (label 60) (parent 52) (unrealized (8 0)) + (dead) (comment "empty cohort")) (comment "Strand bound exceeded--aborting run") @@ -1827,6 +1840,7 @@ (label 22) (parent 12) (unrealized (1 2) (3 0) (4 0) (9 0)) + (aborted) (comment "aborted")) (defskeleton wrap-decrypt @@ -1866,6 +1880,7 @@ (label 44) (parent 31) (unrealized (1 2) (9 0)) + (aborted) (comment "aborted")) (defskeleton wrap-decrypt @@ -1905,6 +1920,7 @@ (label 47) (parent 34) (unrealized (1 2) (9 0)) + (aborted) (comment "aborted")) (defskeleton wrap-decrypt @@ -1944,6 +1960,7 @@ (label 54) (parent 42) (unrealized (9 0)) + (aborted) (comment "aborted")) (defskeleton wrap-decrypt @@ -1983,6 +2000,7 @@ (label 55) (parent 43) (unrealized (9 0)) + (aborted) (comment "aborted")) (defskeleton wrap-decrypt @@ -2022,6 +2040,7 @@ (label 56) (parent 46) (unrealized (9 0)) + (aborted) (comment "aborted")) (defskeleton wrap-decrypt @@ -2061,6 +2080,7 @@ (label 59) (parent 50) (unrealized (1 2) (9 0)) + (aborted) (comment "aborted")) (defskeleton wrap-decrypt @@ -2100,4 +2120,5 @@ (label 61) (parent 53) (unrealized (1 2) (9 0)) + (aborted) (comment "aborted")) diff --git a/tst/yahalom.tst b/tst/yahalom.tst --- a/tst/yahalom.tst +++ b/tst/yahalom.tst @@ -1,7 +1,7 @@ (herald "Yahalom Protocol with Forwarding Removed" (algebra diffie-hellman) (bound 12)) -(comment "CPSA 3.6.1") +(comment "CPSA 3.6.2") (comment "All input read from yahalom.scm") (defprotocol yahalom diffie-hellman @@ -277,6 +277,7 @@ (label 11) (parent 5) (unrealized (0 3) (2 0)) + (dead) (comment "empty cohort")) (defskeleton yahalom @@ -329,6 +330,7 @@ (label 13) (parent 7) (unrealized (0 3) (3 0)) + (dead) (comment "empty cohort")) (defskeleton yahalom @@ -598,6 +600,7 @@ (label 22) (parent 15) (unrealized (4 0)) + (dead) (comment "empty cohort")) (defskeleton yahalom @@ -963,6 +966,7 @@ (label 33) (parent 21) (unrealized (5 0)) + (dead) (comment "empty cohort")) (defskeleton yahalom @@ -1065,6 +1069,7 @@ (label 36) (parent 25) (unrealized (2 1) (4 0)) + (dead) (comment "empty cohort")) (defskeleton yahalom @@ -1138,6 +1143,7 @@ (label 38) (parent 27) (unrealized (3 1) (5 0)) + (dead) (comment "empty cohort")) (defskeleton yahalom @@ -1315,6 +1321,7 @@ (label 43) (parent 31) (unrealized (6 0)) + (dead) (comment "empty cohort")) (defskeleton yahalom @@ -1350,6 +1357,7 @@ (label 44) (parent 32) (unrealized (2 1) (5 0)) + (dead) (comment "empty cohort")) (defskeleton yahalom @@ -1414,6 +1422,7 @@ (label 46) (parent 35) (unrealized (2 1) (5 0)) + (dead) (comment "empty cohort")) (defskeleton yahalom @@ -1452,6 +1461,7 @@ (label 47) (parent 37) (unrealized (3 1) (6 0)) + (dead) (comment "empty cohort")) (defskeleton yahalom @@ -1521,6 +1531,7 @@ (label 49) (parent 41) (unrealized (7 0)) + (dead) (comment "empty cohort")) (defskeleton yahalom @@ -1559,6 +1570,7 @@ (label 50) (parent 42) (unrealized (2 1) (6 0)) + (dead) (comment "empty cohort")) (defskeleton yahalom @@ -1703,6 +1715,7 @@ (label 56) (parent 54) (unrealized (0 3) (1 0)) + (dead) (comment "empty cohort")) (defskeleton yahalom @@ -1725,6 +1738,7 @@ (label 57) (parent 55) (unrealized (0 3) (1 0)) + (dead) (comment "empty cohort")) (comment "Nothing left to do")