packages feed

cpsa 3.6.3 → 3.6.4

raw patch · 83 files changed

+3246/−377 lines, 83 filesdep ~base

Dependency ranges changed: base

Files

ChangeLog view
@@ -1,3 +1,23 @@+2019-10-21  John D. Ramsdell  <ramsdell@gootoo.mitre.org>++	* cpsa.cabal (Version): Tagged as 3.6.4++2019-10-21  John D. Ramsdell  <ramsdell@mitre.org>++	* src/CPSA/Lib/Utilities.hs: Used the C preprocessor to allow+	compilation using older versions of GHC.++2019-10-15  John D. Ramsdell  <ramsdell@mitre.org>++	* src/CPSA/Lib/Utilities.hs: Updated code to support the removal+	of fail from Monad as implemented in base-4.13.0.0.++2019-09-16  John D. Ramsdell  <ramsdell@mitre.org>++	* src/CPSA/Lib/Strand.hs (thinManyStrands):  Replaced isomorphic+	check with probIsomorphic check so that strands in the+	point-of-view remain unmodified.+ 2019-08-26  John D. Ramsdell  <ramsdell@mitre.org>  	* cpsa.cabal (Version): Tagged as 3.6.3
NEWS view
@@ -1,5 +1,14 @@ CPSA NEWS +  October 2019:++* Release 3.6.4 adds support for the latest version of the GHC+  compiler.  As of version 8.8, the Monad type class no longer+  contains the fail method, and that method is now provided by the+  MonadFail type class.  This version of CPSA makes use of the C+  preprocessor to handle this incompatible change.  The release also+  fixes a bug in thinning.+   August 2019:  * Release 3.6.3 adds the cpsainit program and fixes bugs.  The
cpsa.cabal view
@@ -1,10 +1,10 @@-Name:			cpsa-Version:		3.6.3-Maintainer:		mliskov@mitre.org-Cabal-Version:		>= 1.6-License:		BSD3-License-File:		license.txt-Synopsis:		Symbolic cryptographic protocol analyzer+Name:                   cpsa+Version:                3.6.4+Maintainer:             mliskov@mitre.org+Cabal-Version:          >= 1.6+License:                BSD3+License-File:           license.txt+Synopsis:               Symbolic cryptographic protocol analyzer Description:   The Cryptographic Protocol Shapes Analyzer (CPSA) attempts to   enumerate all essentially different executions possibe for a@@ -46,8 +46,8 @@   F. Doghmi, F. Javier Thayer, Paul D. Rowe, and Moses D. Liskov.   John D. Ramsdell and Moses D. Liskov implemented the algorithm in   Haskell.  CPSA was designed and implemented at The MITRE Corporation.-Category:		Cryptography-Build-Type:		Simple+Category:               Cryptography+Build-Type:             Simple Data-Files:   Make.hs cpsa.mk cpsamanual.pdf examples/blanchet.scm   examples/blanchet.xhtml examples/bltk_or.scm examples/bltk_or.xhtml@@ -73,7 +73,7 @@   examples/fluffy_draft03_pske.scm examples/eq_test.scm   init/Makefile init/template.lisp   examples/eq_test.xhtml-Data-Dir:	    	doc+Data-Dir:               doc Extra-Source-Files:   Makefile ChangeLog README.txt NEWS ghci cpsatst setup.bat   src/cpsa.el src/cpsaops.scm src/cpsa.pl src/pp.pl@@ -112,17 +112,22 @@   tst/wrap_decrypt.tst tst/yahalom.scm tst/yahalom.tst   tst/aik.scm tst/aik.tst tst/reflect.scm tst/reflect.tst   tst/station.scm tst/station.tst tst/kerb.scm tst/kerb.tst+  tst/attest.scm tst/attest.tst tst/comp_test.scm tst/comp_test.tst+  tst/fluffy_draft03_gske.scm tst/fluffy_draft03_gske.tst+  tst/ordered.scm tst/ordered.tst tst/prottrans.scm tst/prottrans.tst+  tst/role_uniq.scm tst/role_uniq.tst tst/rule-order.scm+  tst/rule-order.tst tst/trust-anchor.scm tst/trust-anchor.tst    Source-Repository head   Type:     git   Location: git://github.com/mitre/cpsa.git  Executable cpsa-  Main-Is:		CPSA/Lib/Main.hs-  Build-Depends:	base >= 3 && < 5, containers, parallel+  Main-Is:              CPSA/Lib/Main.hs+  Build-Depends:        base >= 4 && < 5, containers, parallel   GHC-Options:     -Wall -fno-warn-name-shadowing -fwarn-unused-imports -threaded -rtsopts-  Hs-Source-Dirs:	src+  Hs-Source-Dirs:       src   Other-Modules:     Paths_cpsa CPSA.Lib.Utilities     CPSA.Lib.Pretty CPSA.Lib.SExpr CPSA.Lib.Printer CPSA.Lib.Entry@@ -133,11 +138,11 @@     CPSA.Basic.Algebra CPSA.DiffieHellman.Algebra CPSA.Lib.Declaration  Executable cpsagraph-  Main-Is:		CPSA/Graph/Main.hs-  Build-Depends:	base >= 3 && < 5, containers+  Main-Is:              CPSA/Graph/Main.hs+  Build-Depends:        base >= 4 && < 5, containers   GHC-Options:     -Wall -fno-warn-name-shadowing -fwarn-unused-imports-  Hs-Source-Dirs:	src+  Hs-Source-Dirs:       src   Other-Modules:     Paths_cpsa CPSA.Lib.Utilities CPSA.Lib.Pretty CPSA.Lib.SExpr     CPSA.Lib.Printer CPSA.Lib.Notation CPSA.Lib.Entry CPSA.Lib.Algebra@@ -147,22 +152,22 @@     CPSA.Graph.ExpandedView CPSA.Graph.LaTeXView CPSA.Basic.Algebra  Executable cpsashapes-  Main-Is:		CPSA/Shapes/Main.hs-  Build-Depends:	base >= 3 && < 5, containers+  Main-Is:              CPSA/Shapes/Main.hs+  Build-Depends:        base >= 4 && < 5, containers   GHC-Options:     -Wall -fno-warn-name-shadowing -fwarn-unused-imports-  Hs-Source-Dirs:	src+  Hs-Source-Dirs:       src   Other-Modules:     Paths_cpsa CPSA.Lib.Utilities CPSA.Lib.Pretty CPSA.Lib.SExpr     CPSA.Lib.Printer CPSA.Lib.Entry CPSA.Lib.Algebra     CPSA.Shapes.Shapes CPSA.Basic.Algebra  Executable cpsaannotations-  Main-Is:		CPSA/Annotations/Main.hs-  Build-Depends:	base >= 3 && < 5, containers+  Main-Is:              CPSA/Annotations/Main.hs+  Build-Depends:        base >= 4 && < 5, containers   GHC-Options:     -Wall -fno-warn-name-shadowing -fwarn-unused-imports-  Hs-Source-Dirs:	src+  Hs-Source-Dirs:       src   Other-Modules:     Paths_cpsa CPSA.Lib.Utilities CPSA.Lib.Pretty CPSA.Lib.SExpr     CPSA.Lib.Printer CPSA.Lib.Entry CPSA.Lib.Algebra@@ -170,76 +175,76 @@     CPSA.Basic.Algebra CPSA.DiffieHellman.Algebra      Executable cpsadiff-  Main-Is:		CPSA/Diff/Main.hs-  Build-Depends:	base >= 3 && < 5, containers+  Main-Is:              CPSA/Diff/Main.hs+  Build-Depends:        base >= 3 && < 5, containers   GHC-Options:     -Wall -fno-warn-name-shadowing -fwarn-unused-imports-  Hs-Source-Dirs:	src+  Hs-Source-Dirs:       src   Other-Modules:     Paths_cpsa CPSA.Lib.Utilities CPSA.Lib.Pretty CPSA.Lib.SExpr     CPSA.Lib.Printer CPSA.Lib.Entry CPSA.Lib.Algebra     CPSA.Basic.Algebra  Executable cpsasas-  Main-Is:		CPSA/SAS/Main.hs-  Build-Depends:	base >= 3 && < 5, containers+  Main-Is:              CPSA/SAS/Main.hs+  Build-Depends:        base >= 4 && < 5, containers   GHC-Options:     -Wall -fno-warn-name-shadowing -fwarn-unused-imports-  Hs-Source-Dirs:	src+  Hs-Source-Dirs:       src   Other-Modules:     Paths_cpsa CPSA.Lib.Utilities CPSA.Lib.Pretty CPSA.Lib.SExpr     CPSA.Lib.Printer CPSA.Lib.Entry CPSA.Lib.Algebra CPSA.SAS.SAS     CPSA.Basic.Algebra CPSA.DiffieHellman.Algebra  Executable cpsapp-  Main-Is:		CPSA/Pretty/Main.hs-  Build-Depends:	base >= 3 && < 5, containers+  Main-Is:              CPSA/Pretty/Main.hs+  Build-Depends:        base >= 3 && < 5, containers   GHC-Options:     -Wall -fno-warn-name-shadowing -fwarn-unused-imports-  Hs-Source-Dirs:	src+  Hs-Source-Dirs:       src   Other-Modules:     Paths_cpsa CPSA.Lib.Utilities CPSA.Lib.Pretty CPSA.Lib.SExpr     CPSA.Lib.Printer CPSA.Lib.Entry CPSA.Lib.Algebra     CPSA.Basic.Algebra  Executable cpsajson-  Main-Is:		CPSA/JSON/Main.hs-  Build-Depends:	base >= 3 && < 5, containers+  Main-Is:              CPSA/JSON/Main.hs+  Build-Depends:        base >= 3 && < 5, containers   GHC-Options:     -Wall -fno-warn-name-shadowing -fwarn-unused-imports-  Hs-Source-Dirs:	src+  Hs-Source-Dirs:       src   Other-Modules:     Paths_cpsa CPSA.Lib.Utilities CPSA.Lib.Pretty CPSA.Lib.SExpr     CPSA.Lib.Printer CPSA.Lib.Entry CPSA.Lib.Algebra     CPSA.Basic.Algebra  Executable cpsadebase-  Main-Is:		CPSA/Debase/Main.hs-  Build-Depends:	base >= 3 && < 5, containers+  Main-Is:              CPSA/Debase/Main.hs+  Build-Depends:        base >= 3 && < 5, containers   GHC-Options:     -Wall -fno-warn-name-shadowing -fwarn-unused-imports-  Hs-Source-Dirs:	src+  Hs-Source-Dirs:       src   Other-Modules:     Paths_cpsa CPSA.Lib.Utilities CPSA.Lib.Pretty CPSA.Lib.SExpr     CPSA.Lib.Printer CPSA.Lib.Entry CPSA.Lib.Algebra     CPSA.Basic.Algebra  Executable cpsamatch-  Main-Is:		CPSA/Match/Main.hs-  Build-Depends:	base >= 3 && < 5, containers+  Main-Is:              CPSA/Match/Main.hs+  Build-Depends:        base >= 4 && < 5, containers   GHC-Options:     -Wall -fno-warn-name-shadowing -fwarn-unused-imports-  Hs-Source-Dirs:	src+  Hs-Source-Dirs:       src   Other-Modules:     Paths_cpsa CPSA.Lib.Utilities CPSA.Lib.Pretty CPSA.Lib.SExpr     CPSA.Lib.Printer CPSA.Lib.Entry CPSA.Lib.Algebra CPSA.Match.Match     CPSA.Basic.Algebra CPSA.DiffieHellman.Algebra  Executable cpsainit-  Main-Is:		CPSA/Init/Main.hs-  Build-Depends:	base, directory+  Main-Is:              CPSA/Init/Main.hs+  Build-Depends:        base, directory   GHC-Options:     -Wall -fno-warn-name-shadowing -fwarn-unused-imports-  Hs-Source-Dirs:	src+  Hs-Source-Dirs:       src   Other-Modules:     Paths_cpsa
src/CPSA/Annotations/Annotations.hs view
@@ -6,6 +6,12 @@ -- modify it under the terms of the BSD License as published by the -- University of California. +{-# LANGUAGE CPP #-}++#if !(MIN_VERSION_base(4,13,0))+#define MonadFail Monad+#endif+ module CPSA.Annotations.Annotations (Prot, annotations) where  import Control.Monad@@ -28,7 +34,7 @@ -- generator.  The third argument is the protocol information required -- for processing preskeletons. -annotations :: (Algebra t p g s e c, Monad m) => String -> g ->+annotations :: (Algebra t p g s e c, MonadFail m) => String -> g ->          [Prot t g] -> SExpr Pos -> m ([Prot t g], SExpr Pos) annotations name origin ps x@(L pos (S _ "defprotocol" : xs)) =     do@@ -61,7 +67,7 @@  -- Load a protocol.  On success, returns a Prot record. -loadProt :: (Algebra t p g s e c, Monad m) => String -> g ->+loadProt :: (Algebra t p g s e c, MonadFail m) => String -> g ->             Pos -> [SExpr Pos] -> m (Prot t g) loadProt nom origin pos (S _ name : S _ alg : x : xs)     | alg /= nom =@@ -78,12 +84,12 @@ -- every variable that occurs in a preskeleton never occurs in one of -- its roles. -loadRoles :: (Algebra t p g s e c, Monad m) => g ->+loadRoles :: (Algebra t p g s e c, MonadFail m) => g ->              [SExpr Pos] -> m (g, [Role t]) loadRoles origin xs =     mapAccumLM loadRole origin xs -loadRole :: (Algebra t p g s e c, Monad m) => g ->+loadRole :: (Algebra t p g s e c, MonadFail m) => g ->             SExpr Pos -> m (g, Role t) loadRole gen (L pos (S _ "defrole" :                      S _ name :@@ -100,7 +106,7 @@ loadRole _ x =     fail (shows (annotation x) "Malformed role") -loadFormulas :: (Algebra t p g s e c, Monad m) => Pos -> [t] -> Int ->+loadFormulas :: (Algebra t p g s e c, MonadFail m) => Pos -> [t] -> Int ->                 g -> [SExpr Pos] -> m (g, t, [Formula t]) loadFormulas pos vars len gen (x : xs) =     do@@ -116,7 +122,7 @@ loadFormulas pos _ _ _ [] =     fail (shows pos "Role missing annotations") -loadIndexedFormula :: (Algebra t p g s e c, Monad m) => [t] -> Int ->+loadIndexedFormula :: (Algebra t p g s e c, MonadFail m) => [t] -> Int ->                       g -> SExpr Pos -> m (g, (Int, Formula t)) loadIndexedFormula _ len _ (L _ [N pos i, _])     | i < 0 || i >= len = fail (shows pos "Bad index for formula")@@ -128,7 +134,7 @@     fail (shows (annotation x) "Malformed indexed formula")  -- Ensure there are no formulas with the same index-checkIndices :: (Algebra t p g s e c, Monad m) => Pos ->+checkIndices :: (Algebra t p g s e c, MonadFail m) => Pos ->                 [(Int, Formula t)] -> m () checkIndices _ [] = return () checkIndices pos ((i, _) : alist)@@ -167,7 +173,7 @@  -- Find protocol and then load preskeleton. -- Remove any old annotations, and add new ones.-findPreskel :: (Algebra t p g s e c, Monad m) => Pos ->+findPreskel :: (Algebra t p g s e c, MonadFail m) => Pos ->                [Prot t g] -> [SExpr Pos] -> m (SExpr Pos) findPreskel pos ps (S _ name : xs) =     case L.find (\p -> name == pname p) ps of@@ -178,7 +184,7 @@             return (L pos (S pos "defskeleton" : S pos name : xs)) findPreskel pos _ _ = fail (shows pos "Malformed skeleton") -updatePreskel :: (Algebra t p g s e c, Monad m) => Pos ->+updatePreskel :: (Algebra t p g s e c, MonadFail m) => Pos ->                  Prot t g -> [SExpr Pos] -> m [SExpr Pos] updatePreskel pos prot (vs@(L _ (S _ "vars" : vars)) : xs)     | not (realized xs) || not (hasKey tracesKey xs) =@@ -199,7 +205,7 @@ realized xs =     null (assoc "unrealized" xs) && hasKey "unrealized" xs -loadPreskel :: (Algebra t p g s e c, Monad m) => Prot t g ->+loadPreskel :: (Algebra t p g s e c, MonadFail m) => Prot t g ->                g -> [t] -> [SExpr Pos] -> m (Preskel t g e) loadPreskel prot gen kvars xs =     do@@ -212,7 +218,7 @@                         traces = traces,                         orderings = orderings }) -loadInsts :: (Algebra t p g s e c, Monad m) => Prot t g ->+loadInsts :: (Algebra t p g s e c, MonadFail m) => Prot t g ->              g -> [t] -> [Instance t e] -> [SExpr Pos] ->              m [Instance t e] loadInsts prot gen kvars insts (L pos (S _ "defstrand" : x) : xs) =@@ -235,7 +241,7 @@ loadInsts _ _ _ insts _ =     return (reverse insts) -loadInst :: (Algebra t p g s e c, Monad m) => Pos -> Prot t g ->+loadInst :: (Algebra t p g s e c, MonadFail m) => Pos -> Prot t g ->             g -> [t] -> String -> Int -> [SExpr Pos] ->             m (g, Instance t e) loadInst pos prot gen kvars role height env =@@ -248,14 +254,14 @@       return (gen', Instance { pos = pos, role = Just r,                                env = env, height = height }) -lookupRole :: Monad m => Pos -> Prot t g -> String -> m (Role t)+lookupRole :: MonadFail m => Pos -> Prot t g -> String -> m (Role t) lookupRole pos prot role =     case L.find (\r -> role == rname r) (roles prot) of       Nothing ->           fail (shows pos $ "Role " ++ role ++ " not found in " ++ pname prot)       Just r -> return r -loadMaplet :: (Algebra t p g s e c, Monad m) =>+loadMaplet :: (Algebra t p g s e c, MonadFail m) =>               [t] -> [t] -> (g, e) -> SExpr Pos -> m (g, e) loadMaplet kvars vars env (L pos [domain, range]) =     do@@ -268,11 +274,11 @@  -- Load a trace -loadTrace :: Monad m => SExpr Pos -> m Trace+loadTrace :: MonadFail m => SExpr Pos -> m Trace loadTrace (L _ xs) = mapM loadDt xs loadTrace x = fail (shows (annotation x) "Malformed trace") -loadDt :: Monad m => SExpr Pos -> m Dir+loadDt :: MonadFail m => SExpr Pos -> m Dir loadDt (L _ [S _ "recv", _]) = return InDir loadDt (L _ [S _ "send", _]) = return OutDir loadDt (L _ [S _ "sync", _]) = return SyncDir@@ -282,7 +288,7 @@  -- Load the node orderings -loadOrderings :: Monad m => Strands -> [SExpr Pos] -> m [Pair]+loadOrderings :: MonadFail m => Strands -> [SExpr Pos] -> m [Pair] loadOrderings _ [] = return [] loadOrderings strands (x : xs) =     do@@ -290,7 +296,7 @@       nps <- loadOrderings strands xs       return (adjoin np nps) -loadPair :: Monad m => [Int] -> SExpr Pos -> m Pair+loadPair :: MonadFail m => [Int] -> SExpr Pos -> m Pair loadPair heights (L pos [x0, x1]) =     do       n0 <- loadNode heights x0@@ -302,7 +308,7 @@       sameStrands (s0, _) (s1, _) = s0 == s1 loadPair _ x = fail (shows (annotation x) "Malformed pair") -loadNode :: Monad m => [Int] -> SExpr Pos -> m Node+loadNode :: MonadFail m => [Int] -> SExpr Pos -> m Node loadNode heights (L pos [N _ s, N _ p])     | s < 0 = fail (shows pos "Negative strand in node")     | p < 0 = fail (shows pos "Negative position in node")@@ -323,7 +329,7 @@ type Annotations t = Maybe (t, [Formula t])  -- Construct the annotations for an instance-instAnnos :: (Algebra t p g s e c, Monad m) =>+instAnnos :: (Algebra t p g s e c, MonadFail m) =>              Instance t e -> m (Annotations t) -- A listener has no annotations instAnnos (Instance { role = Nothing }) = return Nothing@@ -344,7 +350,7 @@     addToContext emptyContext vars  -- Instantiate term and ensure all the free variables have been mapped.-transTerm :: (Algebra t p g s e c, Monad m) => Pos -> [t] -> e -> t -> m t+transTerm :: (Algebra t p g s e c, MonadFail m) => Pos -> [t] -> e -> t -> m t transTerm pos vars env t =     let t' = instantiate env t in     case L.find (flip S.member (fv t')) vars of@@ -356,7 +362,7 @@       fv t = foldVars (flip S.insert) S.empty t  -- Instantiate formula and ensure all the free variables have been mapped.-transForm :: (Algebra t p g s e c, Monad m) => Pos -> [t] -> e ->+transForm :: (Algebra t p g s e c, MonadFail m) => Pos -> [t] -> e ->              Formula t -> m (Formula t) transForm pos vars env f =     let f' = finstantiate env f in@@ -427,7 +433,7 @@ successors strands =     [((s, p), (s, p + 1)) | (s, n) <- zip [0..] strands, p <- nats (n - 1)] -before :: Monad m => Pos -> Preskel t g e -> m [(Node, [Node])]+before :: MonadFail m => Pos -> Preskel t g e -> m [(Node, [Node])] before pos k =     case isAcyclic graph nodes of       False -> fail (shows pos "Cycle found")@@ -450,7 +456,7 @@  type Obligation t = (Node, t, Formula t) -obligations :: (Algebra t p g s e c, Monad m) => Pos ->+obligations :: (Algebra t p g s e c, MonadFail m) => Pos ->                Preskel t g e -> [Annotations t] -> m [Obligation t] obligations pos k annos =     do
src/CPSA/Annotations/Formulas.hs view
@@ -6,12 +6,19 @@ -- modify it under the terms of the BSD License as published by the -- University of California. +{-# LANGUAGE CPP #-}++#if !(MIN_VERSION_base(4,13,0))+#define MonadFail Monad+#endif+ module CPSA.Annotations.Formulas (Formula, truth, true, says, implies,     freeVars, finstantiate, mapAccumLM, loadDecls, loadFormula,     displayFormula) where  import Control.Monad import qualified Data.Set as S+import CPSA.Lib.Utilities import CPSA.Lib.SExpr import CPSA.Lib.Algebra @@ -136,7 +143,7 @@ -- the loading process so that every bound variable is quantified -- once, and no free variable is bound within a formula.  Use -- loadDecls to ensure vars are not keywords.-loadFormula :: (Algebra t p g s e c, Monad m) => [t] -> g ->+loadFormula :: (Algebra t p g s e c, MonadFail m) => [t] -> g ->                SExpr Pos -> m (g, Formula t) loadFormula vars gen (L _ (S _ pred : xs)) -- Atomic formula     | notElem pred keywords =@@ -175,77 +182,33 @@ loadFormula _ _ x =     fail (shows (annotation x) "Malformed formula") -data EitherS a-    = RightS a-    | LeftS String--instance Functor (EitherS) where-    fmap _ (LeftS x) = LeftS x-    fmap f (RightS y) = RightS (f y)--instance Applicative (EitherS) where-    pure          = RightS-    LeftS e <*> _ = LeftS e-    RightS f <*> r = fmap f r--instance Monad EitherS where-    return = RightS-    LeftS l >>= _ = LeftS l-    RightS r >>= k = k r-    fail s = LeftS s--{- Monad laws--1. return a >>= k          <==> k a--RightS r >>= k ==> k r--2. m >>= return            <==> m--  Cases on m-  a. m is RightS r-     RightS r >>= RightS ==> RightS r ==> m-  b. m is LeftS l-     LeftS l >>= RightS ==> LeftS l ==> m--3. m >>= (\x -> k x >>= h) <===> (m >>= k) >>= h--  Cases on m-  a. m is RightS r-     1. RightS r >>= (\x -> k x >>= h) ==> k r >>= h-     2. (RightS r >> k) >>= h ==> k r >>= h-  b. m is LeftS l ==>-     1. LeftS l >>= (\x -> k x >>= h) ==> LeftS l-     2. (LeftS l >>= k) >>= h ==> LeftS l >>= h ==> LeftS l--}--loadFTerms :: (Algebra t p g s e c, Monad m) => [t] ->+loadFTerms :: (Algebra t p g s e c, MonadFail m) => [t] ->               [SExpr Pos] -> m [FTerm t] loadFTerms vars xs =     foldM f [] (reverse xs)     where       f acc x =           case loadFTerm vars x of-            RightS t -> return (t : acc)-            LeftS msg -> fail msg+            Return t -> return (t : acc)+            Fail msg -> fail msg  -- Load a formula term loadFTerm :: Algebra t p g s e c => [t] -> SExpr Pos ->-             EitherS (FTerm t)+             ReturnFail (FTerm t) loadFTerm vars x =     case loadTerm vars False x of-      RightS t -> return (AlgTerm t)-      LeftS msg ->              -- If x is not an algebra term+      Return t -> return (AlgTerm t)+      Fail msg ->               -- If x is not an algebra term           case x of             -- see if it's an application             L _ (S pos fun : xs)                 | elem fun keywords ->-                    LeftS (shows pos $+                    Fail (shows pos $                            "Keyword " ++ fun ++ " used as a function")                 | otherwise ->                  case mapM (loadFTerm vars) xs of-                   RightS ts -> RightS (Application fun ts)-                   LeftS _ -> LeftS msg-            _ -> LeftS msg+                   Return ts -> Return (Application fun ts)+                   Fail _ -> Fail msg+            _ -> Fail msg  -- A monad version of map accumulation from the left mapAccumLM :: Monad m => (a -> b -> m (a, c)) -> a -> [b] -> m (a, [c])@@ -260,7 +223,7 @@ -- Load a quantified formula.  Note that loadVars returns variables in -- reverse order, so list append is the correct way to extend the list -- of variables that are in scope.-loadQuantified :: (Algebra t p g s e c, Monad m) =>+loadQuantified :: (Algebra t p g s e c, MonadFail m) =>                   ([t] -> Formula t -> Formula t) ->                   [t] -> g -> [SExpr Pos] -> SExpr Pos ->                   m (g, Formula t)@@ -270,7 +233,7 @@       (gen'', f) <- loadFormula (vars' ++ vars) gen' body       return (gen'', build (reverse vars') f) -loadDecls :: (Algebra t p g s e c, Monad m) => g ->+loadDecls :: (Algebra t p g s e c, MonadFail m) => g ->              [SExpr Pos] -> m (g, [t]) loadDecls gen decls =     do@@ -278,7 +241,7 @@       loadVars gen decls  -- Fail if a variable is used as a keyword-checkDecl :: Monad m => SExpr Pos -> m ()+checkDecl :: MonadFail m => SExpr Pos -> m () checkDecl (L _ (S pos sym : _))     | elem sym keywords =         fail (shows pos "Keyword " ++ sym ++ " used as a variable")
src/CPSA/Basic/Algebra.hs view
@@ -14,8 +14,12 @@ -- modify it under the terms of the BSD License as published by the -- University of California. -{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE MultiParamTypeClasses, CPP #-} +#if !(MIN_VERSION_base(4,13,0))+#define MonadFail Monad+#endif+ module CPSA.Basic.Algebra (name, origin) where  import Control.Monad (foldM)@@ -937,20 +941,20 @@  -- Term specific loading functions -loadVars :: Monad m => Gen -> [SExpr Pos] -> m (Gen, [Term])+loadVars :: MonadFail m => Gen -> [SExpr Pos] -> m (Gen, [Term]) loadVars gen sexprs =     do       pairs <- mapM loadVarPair sexprs       (g, vars) <- foldM loadVar (gen, []) (concat pairs)       return (g, reverse vars) -loadVarPair :: Monad m => SExpr Pos -> m [(SExpr Pos, SExpr Pos)]+loadVarPair :: MonadFail m => SExpr Pos -> m [(SExpr Pos, SExpr Pos)] loadVarPair (L _ (x:y:xs)) =     let (t:vs) = reverse (x:y:xs) in     return [(v,t) | v <- reverse vs] loadVarPair x = fail (shows (annotation x) "Bad variable declaration") -loadVar :: Monad m => (Gen, [Term]) -> (SExpr Pos, SExpr Pos) ->+loadVar :: MonadFail m => (Gen, [Term]) -> (SExpr Pos, SExpr Pos) ->            m (Gen, [Term]) loadVar (gen, vars) (S pos name, S pos' sort) =     case loadLookup pos vars name of@@ -981,25 +985,25 @@     let name' = idName (varId t) in     if name' == name then Right t else loadLookup pos u name -loadLookupName :: Monad m => Pos -> [Term] -> String -> m Term+loadLookupName :: MonadFail m => Pos -> [Term] -> String -> m Term loadLookupName pos vars name =     either fail f (loadLookup pos vars name)     where       f t@(F Name [I _]) = return t       f _ = fail (shows pos $ "Expecting " ++ name ++ " to be a name") -loadLookupAkey :: Monad m => Pos -> [Term] -> String -> m Term+loadLookupAkey :: MonadFail m => Pos -> [Term] -> String -> m Term loadLookupAkey pos vars name =     either fail f (loadLookup pos vars name)     where       f t@(F Akey [I _]) = return t       f _ = fail (shows pos $ "Expecting " ++ name ++ " to be an akey") -loadTerm2 :: Monad m => [Term] -> Bool -> SExpr Pos -> m Term+loadTerm2 :: MonadFail m => [Term] -> Bool -> SExpr Pos -> m Term loadTerm2 vars _ pos = loadTerm vars pos  -- Load term and check that it is well-formed.-loadTerm :: Monad m => [Term] -> SExpr Pos -> m Term+loadTerm :: MonadFail m => [Term] -> SExpr Pos -> m Term loadTerm vars (S pos s) =     either fail return (loadLookup pos vars s) loadTerm _ (Q _ t) =@@ -1012,7 +1016,7 @@  type LoadFunction m = Pos -> [Term] -> [SExpr Pos] -> m Term -loadDispatch :: Monad m => [(String, LoadFunction m)]+loadDispatch :: MonadFail m => [(String, LoadFunction m)] loadDispatch =     [("pubk", loadPubk)     ,("privk", loadPrivk)@@ -1025,7 +1029,7 @@  -- Atom constructors: pubk privk invk ltk -loadPubk :: Monad m => LoadFunction m+loadPubk :: MonadFail m => LoadFunction m loadPubk _ vars [S pos s] =     do       t <- loadLookupName pos vars s@@ -1036,7 +1040,7 @@       return $ F Akey [F Pubk [C c, I $ varId t]] loadPubk pos _ _ = fail (shows pos "Malformed pubk") -loadPrivk :: Monad m => LoadFunction m+loadPrivk :: MonadFail m => LoadFunction m loadPrivk _ vars [S pos s] =     do       t <- loadLookupName pos vars s@@ -1047,7 +1051,7 @@       return $ F Akey [F Invk [F Pubk [C c, I $ varId t]]] loadPrivk pos _ _ = fail (shows pos "Malformed privk") -loadInvk :: Monad m => LoadFunction m+loadInvk :: MonadFail m => LoadFunction m loadInvk _ vars [S pos s] =     do       t <- loadLookupAkey pos vars s@@ -1081,7 +1085,7 @@         _ -> fail (shows (annotation t) "Expecting an akey") loadInvk pos _ _ = fail (shows pos "Malformed invk") -loadLtk :: Monad m => LoadFunction m+loadLtk :: MonadFail m => LoadFunction m loadLtk _ vars [S pos s, S pos' s'] =     do       t <- loadLookupName pos vars s@@ -1091,14 +1095,14 @@  -- Term constructors: cat enc -loadCat :: Monad m => LoadFunction m+loadCat :: MonadFail m => LoadFunction m loadCat _ vars (l : ls) =     do       ts <- mapM (loadTerm vars) (l : ls)       return $ foldr1 (\a b -> F Cat [a, b]) ts loadCat pos _ _ = fail (shows pos "Malformed cat") -loadEnc :: Monad m => LoadFunction m+loadEnc :: MonadFail m => LoadFunction m loadEnc pos vars (l : l' : ls) =     do       let (butLast, last) = splitLast l (l' : ls)@@ -1114,7 +1118,7 @@       loop z x [] = (reverse z, x)       loop z x (y : ys) = loop (x : z) y ys -loadHash :: Monad m => LoadFunction m+loadHash :: MonadFail m => LoadFunction m loadHash _ vars (l : ls) =    do      ts <- mapM (loadTerm vars) (l : ls)
src/CPSA/DiffieHellman/Algebra.hs view
@@ -98,6 +98,10 @@  {-# LANGUAGE MultiParamTypeClasses, CPP #-} +#if !(MIN_VERSION_base(4,13,0))+#define MonadFail Monad+#endif+ -- Fail on non-canonical terms with this is defined -- #define CANONICAL @@ -2416,20 +2420,20 @@  -- Term specific loading functions -loadVars :: Monad m => Gen -> [SExpr Pos] -> m (Gen, [Term])+loadVars :: MonadFail m => Gen -> [SExpr Pos] -> m (Gen, [Term]) loadVars gen sexprs =     do       pairs <- mapM loadVarPair sexprs       (g, vars) <- foldM loadVar (gen, []) (concat pairs)       return (g, reverse vars) -loadVarPair :: Monad m => SExpr Pos -> m [(SExpr Pos, SExpr Pos)]+loadVarPair :: MonadFail m => SExpr Pos -> m [(SExpr Pos, SExpr Pos)] loadVarPair (L _ (x:y:xs)) =     let (t:vs) = reverse (x:y:xs) in     return [(v,t) | v <- reverse vs] loadVarPair x = fail (shows (annotation x) "Malformed vars declaration") -loadVar :: Monad m => (Gen, [Term]) -> (SExpr Pos, SExpr Pos) ->+loadVar :: MonadFail m => (Gen, [Term]) -> (SExpr Pos, SExpr Pos) ->            m (Gen, [Term]) loadVar (gen, vars) (S pos name, S pos' sort) =     case loadLookup pos vars name of@@ -2442,7 +2446,7 @@             return (gen', p : vars) loadVar _ (x,_) = fail (shows (annotation x) "Bad variable syntax") -mkVar :: Monad m => Pos -> String -> Id -> m Term+mkVar :: MonadFail m => Pos -> String -> Id -> m Term mkVar pos sort x   | sort == "mesg" = return $ I x   | sort == "text" = return $ F Text [I x]@@ -2467,14 +2471,14 @@     let name' = idName (varId t) in     if name' == name then Right t else loadLookup pos u name -loadLookupName :: Monad m => Pos -> [Term] -> String -> m Term+loadLookupName :: MonadFail m => Pos -> [Term] -> String -> m Term loadLookupName pos vars name =     either fail f (loadLookup pos vars name)     where       f t@(F Name [I _]) = return t       f _ = fail (shows pos $ "Expecting " ++ name ++ " to be a name") -loadLookupAkey :: Monad m => Pos -> [Term] -> String -> m Term+loadLookupAkey :: MonadFail m => Pos -> [Term] -> String -> m Term loadLookupAkey pos vars name =     either fail f (loadLookup pos vars name)     where@@ -2482,7 +2486,7 @@       f _ = fail (shows pos $ "Expecting " ++ name ++ " to be an akey")  -- Load term and check that it is well-formed.-loadTerm :: Monad m => [Term] -> Bool -> SExpr Pos -> m Term+loadTerm :: MonadFail m => [Term] -> Bool -> SExpr Pos -> m Term loadTerm vars _ (S pos s) =     either fail return (loadLookup pos vars s) loadTerm _ _ (Q _ t) =@@ -2495,7 +2499,7 @@  type LoadFunction m = Pos -> Bool -> [Term] -> [SExpr Pos] -> m Term -loadDispatch :: Monad m => [(String, LoadFunction m)]+loadDispatch :: MonadFail m => [(String, LoadFunction m)] loadDispatch =     [("pubk", loadPubk)     ,("privk", loadPrivk)@@ -2514,7 +2518,7 @@  -- Atom constructors: pubk privk invk ltk -loadPubk :: Monad m => LoadFunction m+loadPubk :: MonadFail m => LoadFunction m loadPubk _ _ vars [S pos s] =     do       t <- loadLookupName pos vars s@@ -2525,7 +2529,7 @@       return $ F Akey [F Pubk [C c, I $ varId t]] loadPubk pos _ _ _ = fail (shows pos "Malformed pubk") -loadPrivk :: Monad m => LoadFunction m+loadPrivk :: MonadFail m => LoadFunction m loadPrivk _ _ vars [S pos s] =     do       t <- loadLookupName pos vars s@@ -2536,7 +2540,7 @@       return $ F Akey [F Invk [F Pubk [C c, I $ varId t]]] loadPrivk pos _ _ _ = fail (shows pos "Malformed privk") -loadInvk :: Monad m => LoadFunction m+loadInvk :: MonadFail m => LoadFunction m loadInvk _ _ vars [S pos s] =     do       t <- loadLookupAkey pos vars s@@ -2553,7 +2557,7 @@       return $ F Akey [F Invk [F Pubk [C c, I $ varId t]]] loadInvk pos _ _ _ = fail (shows pos "Malformed invk") -loadLtk :: Monad m => LoadFunction m+loadLtk :: MonadFail m => LoadFunction m loadLtk _ _ vars [S pos s, S pos' s'] =     do       t <- loadLookupName pos vars s@@ -2561,7 +2565,7 @@       return $ F Skey [F Ltk [I $ varId t, I $ varId t']] loadLtk pos _ _ _ = fail (shows pos "Malformed ltk") -loadBltk :: Monad m => LoadFunction m+loadBltk :: MonadFail m => LoadFunction m loadBltk _ _ vars [S pos s, S pos' s'] =     do       t <- loadLookupName pos vars s@@ -2571,12 +2575,12 @@  -- Base and exponents -loadGen :: Monad m => LoadFunction m+loadGen :: MonadFail m => LoadFunction m loadGen _ _ _ [] =     return $ F Base [F Genr []] loadGen pos _ _ _ = fail (shows pos "Malformed gen") -loadExp :: Monad m => LoadFunction m+loadExp :: MonadFail m => LoadFunction m loadExp _ _ vars [x, x'] =     do       t <- loadBase vars x@@ -2584,7 +2588,7 @@       return $ F Base [idSubst emptyIdMap $ F Exp [t, G t']] loadExp pos _ _ _ = fail (shows pos "Malformed exp") -loadBase :: Monad m => [Term] -> SExpr Pos -> m Term+loadBase :: MonadFail m => [Term] -> SExpr Pos -> m Term loadBase vars x =     do       t <- loadTerm vars False x@@ -2592,7 +2596,7 @@         F Base [t] -> return t         _ -> fail (shows (annotation x) "Malformed base") -loadExpr :: Monad m => [Term] -> Bool -> SExpr Pos -> m Group+loadExpr :: MonadFail m => [Term] -> Bool -> SExpr Pos -> m Group loadExpr vars False x =     do       t <- loadTerm vars False x@@ -2604,13 +2608,13 @@ --    do --      fail (shows (annotation x) "Disallowed bare exponent") -loadOne :: Monad m => LoadFunction m+loadOne :: MonadFail m => LoadFunction m loadOne _ False _ [] =     return $ G M.empty loadOne pos True _ _ = fail (shows pos "Disallowed bare exponent") loadOne pos _ _ _ = fail (shows pos "Malformed one") -loadRec :: Monad m => LoadFunction m+loadRec :: MonadFail m => LoadFunction m loadRec _ False vars [x] =     do       t <- loadExpr vars False x@@ -2618,7 +2622,7 @@ loadRec pos True _ _ = fail (shows pos "Disallowed bare exponent") loadRec pos _ _ _ = fail (shows pos "Malformed rec") -loadMul :: Monad m => LoadFunction m+loadMul :: MonadFail m => LoadFunction m loadMul _ False vars xs =     do       t <- foldM f M.empty xs@@ -2632,14 +2636,14 @@  -- Term constructors: cat enc -loadCat :: Monad m => LoadFunction m+loadCat :: MonadFail m => LoadFunction m loadCat _ strict vars (l : ls) =     do       ts <- mapM (loadTerm vars strict) (l : ls)       return $ foldr1 (\a b -> F Cat [a, b]) ts loadCat pos _ _ _ = fail (shows pos "Malformed cat") -loadEnc :: Monad m => LoadFunction m+loadEnc :: MonadFail m => LoadFunction m loadEnc pos strict vars (l : l' : ls) =     do       let (butLast, last) = splitLast l (l' : ls)@@ -2655,7 +2659,7 @@       loop z x [] = (reverse z, x)       loop z x (y : ys) = loop (x : z) y ys -loadHash :: Monad m => LoadFunction m+loadHash :: MonadFail m => LoadFunction m loadHash _ strict vars (l : ls) =    do      ts <- mapM (loadTerm vars strict) (l : ls)
src/CPSA/Graph/Loader.hs view
@@ -11,6 +11,12 @@ -- modify it under the terms of the BSD License as published by the -- University of California. +{-# LANGUAGE CPP #-}++#if !(MIN_VERSION_base(4,13,0))+#define MonadFail Monad+#endif+ module CPSA.Graph.Loader (Preskel, Dir (..), Vertex, protocol, role, env, inst,                           part, lastVertex, vertices, Node, vnode, aborted,                           strands, label, parent, seen, unrealized, shape,@@ -185,7 +191,7 @@  -- Protocols -loadProt :: Monad m => SExpr Pos -> Pos -> [SExpr Pos] ->+loadProt :: MonadFail m => SExpr Pos -> Pos -> [SExpr Pos] ->             m (String, Protocol) loadProt x _ (S _ name : S _ _ : xs) =     do@@ -193,7 +199,7 @@       return (name, Protocol { name = name, roles = roles, src = x }) loadProt _ pos _ = fail (shows pos "Malformed protocol") -loadRoles :: Monad m => [SExpr Pos] -> m [(String, Trace)]+loadRoles :: MonadFail m => [SExpr Pos] -> m [(String, Trace)] loadRoles (L pos (S _ "defrole" : x) : xs) =     do       r <- loadRole pos x@@ -201,7 +207,7 @@       return (r : rs) loadRoles _ = return [] -loadRole :: Monad m => Pos -> [SExpr Pos] -> m (String, Trace)+loadRole :: MonadFail m => Pos -> [SExpr Pos] -> m (String, Trace) loadRole _ (S _ name :             L _ (S _ "vars" : _) :             L _ (S _ "trace" : trace) : _) = return (name, trace)@@ -209,7 +215,7 @@  -- Preskeletons -loadPreskel :: Monad m => SExpr Pos -> Pos -> [(String, Protocol)] ->+loadPreskel :: MonadFail m => SExpr Pos -> Pos -> [(String, Protocol)] ->                Int -> [SExpr Pos] -> m Preskel loadPreskel s pos ps tag (S _ name : (L _ (S _ "vars" : _)) : xs) =     case lookup name ps of@@ -223,7 +229,7 @@             loadInsts s pos p tag [] cs xs loadPreskel _ pos _ _ _ = fail (shows pos "Malformed skeleton") -loadInsts :: Monad m => SExpr Pos -> Pos -> Protocol -> Int ->+loadInsts :: MonadFail m => SExpr Pos -> Pos -> Protocol -> Int ->              [Inst] -> [SExpr Pos] -> [SExpr Pos] -> m Preskel loadInsts s top p tag insts cs (L pos (S _ "defstrand" : x) : xs) =     case x of@@ -358,7 +364,7 @@  -- Instances -loadInst :: Monad m => Pos -> Protocol -> [SExpr Pos] -> String ->+loadInst :: MonadFail m => Pos -> Protocol -> [SExpr Pos] -> String ->             Int -> [SExpr Pos] -> m Inst loadInst pos p c role ht env =     case lookup role (roles p) of@@ -384,7 +390,7 @@ itrace env [] (r : rs) =     subst env r : itrace env [] rs -loadMaplet :: Monad m => [SExpr Pos] -> m [(String, SExpr Pos)]+loadMaplet :: MonadFail m => [SExpr Pos] -> m [(String, SExpr Pos)] loadMaplet (L _ [S _ name, x] : xs) =     do       env <- loadMaplet xs@@ -401,7 +407,7 @@ subst _ x = x  -- Ensure alist has the proper form-alist :: Monad m => [SExpr Pos] -> m ()+alist :: MonadFail m => [SExpr Pos] -> m () alist [] = return () alist ((L _ (S _ _ : _)) : xs) = alist xs alist xs = fail (shows (annotation $ head xs) "Malformed association list")@@ -432,7 +438,7 @@ -- assoc key alist = --    concat [ rest | L _ (S _ head : rest) <- alist, key == head ] -nassoc :: Monad m => String -> [SExpr Pos] -> m (Maybe Int)+nassoc :: MonadFail m => String -> [SExpr Pos] -> m (Maybe Int) nassoc key xs =     case assoc key xs of       Nothing -> return Nothing@@ -443,11 +449,11 @@       Just (x:_) -> fail (shows (annotation x) "Expecting one number")       Just [] -> fail (shows (annotation (head xs)) "Expecting one number") -num :: Monad m => SExpr Pos -> m Int+num :: MonadFail m => SExpr Pos -> m Int num (N _ n) = return n num x = fail (shows (annotation x) "Expecting a number") -nsassoc :: Monad m => String -> [SExpr Pos] -> m (Maybe [Int])+nsassoc :: MonadFail m => String -> [SExpr Pos] -> m (Maybe [Int]) nsassoc key xs =     case assoc key xs of       Nothing -> return Nothing@@ -456,7 +462,7 @@             ns <- mapM num val             return (Just ns) -loadOrderings :: Monad m => [Int] -> [SExpr Pos] -> Bool -> m [Pair]+loadOrderings :: MonadFail m => [Int] -> [SExpr Pos] -> Bool -> m [Pair] loadOrderings heights x strict =     foldM f [] x     where@@ -465,7 +471,7 @@             np <- loadPair heights x strict             return (adjoin np ns) -loadPair :: Monad m => [Int] -> SExpr Pos -> Bool -> m Pair+loadPair :: MonadFail m => [Int] -> SExpr Pos -> Bool -> m Pair loadPair heights (L pos [x0, x1]) strict =     do       n0 <- loadNode heights x0@@ -477,7 +483,7 @@       sameStrands (s0, _) (s1, _) = s0 == s1 loadPair _ x _ = fail (shows (annotation x) "Malformed pair") -loadNode :: Monad m => [Int] -> SExpr Pos -> m Node+loadNode :: MonadFail m => [Int] -> SExpr Pos -> m Node loadNode heights (L pos [N _ s, N _ p])     | s < 0 = fail (shows pos "Negative strand in node")     | p < 0 = fail (shows pos "Negative position in node")@@ -493,7 +499,7 @@           | otherwise = height xs (s - 1) loadNode _ x = fail (shows (annotation x) "Malformed node") -loadNodes :: Monad m => [Int] -> Maybe [SExpr Pos] -> m (Maybe [Node])+loadNodes :: MonadFail m => [Int] -> Maybe [SExpr Pos] -> m (Maybe [Node]) loadNodes _ Nothing = return Nothing loadNodes heights (Just xs) =     do
src/CPSA/Lib/Algebra.hs view
@@ -8,6 +8,12 @@  {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-} +{-# LANGUAGE CPP #-}++#if !(MIN_VERSION_base(4,13,0))+#define MonadFail Monad+#endif+ module CPSA.Lib.Algebra where  import Data.Set (Set)@@ -90,7 +96,7 @@     escapeSet :: Set t -> Set t -> t -> Maybe (Set t)      -- Given a list of variables, load a term from an S-expression.-    loadTerm :: Monad m => [t] -> Bool -> SExpr Pos -> m t+    loadTerm :: MonadFail m => [t] -> Bool -> SExpr Pos -> m t      -- Determines if an element is "numeric", meaning that it is     -- part of a numeric sort.@@ -162,7 +168,7 @@     -- Given a generator, load a list of variables or return an error     -- message.  Each element of the list is an identifier and a sort.     -- The varibles are returned in the reverse order.-    loadVars :: Monad m => g -> [SExpr Pos] -> m (g, [t])+    loadVars :: MonadFail m => g -> [SExpr Pos] -> m (g, [t])      -- For DH
src/CPSA/Lib/Characteristic.hs view
@@ -6,10 +6,17 @@ -- modify it under the terms of the BSD License as published by the -- University of California. +{-# LANGUAGE CPP #-}++#if !(MIN_VERSION_base(4,13,0))+#define MonadFail Monad+#endif+ module CPSA.Lib.Characteristic (Conj, characteristic) where  import Control.Monad import qualified Data.List as L+import CPSA.Lib.Utilities import CPSA.Lib.SExpr import CPSA.Lib.Algebra import CPSA.Lib.Declaration@@ -27,7 +34,7 @@ -- Entry point.  Takes a position, a protocol, a variable generator, a -- goal, and a skeleton comment and makes a skeleton or fails.  This -- function extracts the anecedent and univesally quantified variable.-characteristic :: (Algebra t p g s e c, Monad m) => Pos -> Prot t g ->+characteristic :: (Algebra t p g s e c, MonadFail m) => Pos -> Prot t g ->                   [Goal t] -> g -> Conj t -> [SExpr ()] -> m (Preskel t g s e) characteristic pos prot goals g antec comment =   equalsForm pos prot goals g antec comment@@ -35,7 +42,7 @@ -- Checks for equals in an antecedent and fails if it finds one.  One -- could use unification to solve the equality, and then apply the -- result to the remaining parts of the formula.-equalsForm :: (Algebra t p g s e c, Monad m) => Pos -> Prot t g ->+equalsForm :: (Algebra t p g s e c, MonadFail m) => Pos -> Prot t g ->               [Goal t] -> g -> Conj t -> [SExpr ()] -> m (Preskel t g s e) equalsForm pos _ _ _ as _ | any isEquals as =   fail (shows pos "Equals not allowed in antecedent")@@ -50,7 +57,7 @@ -- The instance formulas are used to generate the skeleton's -- instances, and the skeleton formulas generate the rest.  Make the -- instances, and then make the rest.-splitForm :: (Algebra t p g s e c, Monad m) => Pos -> Prot t g ->+splitForm :: (Algebra t p g s e c, MonadFail m) => Pos -> Prot t g ->              [Goal t] -> g -> Conj t -> [SExpr ()] -> m (Preskel t g s e) splitForm pos prot goals g as comment =   do@@ -67,7 +74,7 @@  -- Make the instances from the instance predicates -mkInsts :: (Algebra t p g s e c, Monad m) => g -> Conj t ->+mkInsts :: (Algebra t p g s e c, MonadFail m) => g -> Conj t ->            m ([(t, Sid)], g, [Instance t e]) mkInsts g as =   do@@ -77,7 +84,7 @@     return (strdMap, g, insts) -- Construct node map for later use  -- Computes a map from strands to roles and lengths-strdRoleLength :: (Algebra t p g s e c, Monad m) =>+strdRoleLength :: (Algebra t p g s e c, MonadFail m) =>                   Conj t -> m [(t, (Role t, Int))] strdRoleLength as =   foldM f [] as@@ -94,7 +101,7 @@     f srl _ = return srl  -- Construct instances-foldInsts :: (Algebra t p g s e c, Monad m) =>+foldInsts :: (Algebra t p g s e c, MonadFail m) =>              g -> Conj t -> [(t, (Role t, Int))] ->              m (g, [Instance t e]) foldInsts g _ [] = return (g, [])@@ -106,7 +113,7 @@  -- Construct an instance by extracting maplets from the parameter -- predicates associated with the strand.-mkInst :: (Algebra t p g s e c, Monad m) =>+mkInst :: (Algebra t p g s e c, MonadFail m) =>           g -> Conj t -> t -> Role t -> Int -> m (g, Instance t e) mkInst g as z r h =   do@@ -114,7 +121,7 @@     return (mkInstance g r env h)  -- Add match from a maplet-mkMaplet :: (Algebra t p g s e c, Monad m) =>+mkMaplet :: (Algebra t p g s e c, MonadFail m) =>             Role t -> t -> (g, e) ->             (Pos, AForm t) -> m (g, e) mkMaplet role z env (pos, Param r v _ z' t)@@ -138,7 +145,7 @@  -- Create a skeleton given a list of instances -mkSkel :: (Algebra t p g s e c, Monad m) => Pos -> Prot t g ->+mkSkel :: (Algebra t p g s e c, MonadFail m) => Pos -> Prot t g ->           [Goal t] -> [(t, Sid)] -> g -> [Instance t e] ->           Conj t -> [SExpr ()] -> m (Preskel t g s e) mkSkel pos p goals nmap g insts as comment =@@ -158,8 +165,8 @@       False -> fail (shows pos "Terms in skeleton not well formed")       True -> return ()     case verbosePreskelWellFormed k of-      Right () -> return k-      Left msg -> fail $ shows pos+      Return () -> return k+      Fail msg -> fail $ shows pos                   $ showString "Skeleton not well formed: " msg   where     termsInDlist olist = concat $ map dterms (concatMap snd olist)@@ -211,7 +218,7 @@         Nothing -> FTerm t mkFact _ _ ts = ts -checkUniqAt :: (Algebra t p g s e c, Monad m) => [(t, Sid)] ->+checkUniqAt :: (Algebra t p g s e c, MonadFail m) => [(t, Sid)] ->                Preskel t g s e -> (Pos, AForm t) -> m () checkUniqAt nmap k (pos, UniqAt t n) =   case lookup t $ korig k of
src/CPSA/Lib/Expand.hs view
@@ -6,6 +6,12 @@ -- modify it under the terms of the BSD License as published by the -- University of California. +{-# LANGUAGE CPP #-}++#if !(MIN_VERSION_base(4,13,0))+#define MonadFail Monad+#endif+ module CPSA.Lib.Expand (expand, readSExprs) where  import Control.Monad@@ -82,7 +88,7 @@       args :: [String],       body :: SExpr Pos } -defmacro :: Monad m => Pos -> [SExpr Pos] -> m Macro+defmacro :: MonadFail m => Pos -> [SExpr Pos] -> m Macro defmacro _ [L _ (name : args), body] =     do       name <- symbol name@@ -92,13 +98,13 @@                        body = body} defmacro pos _ = fail (shows pos "Malformed macro") -symbol :: Monad m => SExpr Pos -> m String+symbol :: MonadFail m => SExpr Pos -> m String symbol (S _ string) = return string symbol x = fail (shows (annotation x) "Malformed macro: Expecting a symbol")  -- Expand an S-expression using a given set of macros -expandAll :: Monad m => [Macro] -> SExpr Pos -> m (SExpr Pos)+expandAll :: MonadFail m => [Macro] -> SExpr Pos -> m (SExpr Pos) expandAll macs sexpr =     do       sexpr <- macroExpand macs (annotation sexpr) limit sexpr@@ -111,7 +117,7 @@  -- Expand one S-expression limiting the number of expansions. -macroExpand :: Monad m => [Macro] -> Pos ->  Int ->+macroExpand :: MonadFail m => [Macro] -> Pos ->  Int ->                SExpr Pos -> m (SExpr Pos) macroExpand _ pos limit _     | limit <= 0 = fail (shows pos "Expansion limit exceeded")
src/CPSA/Lib/Loader.hs view
@@ -6,6 +6,12 @@ -- modify it under the terms of the BSD License as published by the -- University of California. +{-# LANGUAGE CPP #-}++#if !(MIN_VERSION_base(4,13,0))+#define MonadFail Monad+#endif+ module CPSA.Lib.Loader (loadSExprs) where  import Control.Monad@@ -28,14 +34,14 @@ -- then return a list of preskeletons.  The name of the algebra is -- nom, and its variable generator is provided. -loadSExprs :: (Algebra t p g s e c, Monad m) => String -> g ->+loadSExprs :: (Algebra t p g s e c, MonadFail m) => String -> g ->               [SExpr Pos] -> m [Preskel t g s e] loadSExprs nom origin xs =     do       (_, ks) <- foldM (loadSExpr nom origin) ([], []) xs       return (reverse ks) -loadSExpr :: (Algebra t p g s e c, Monad m) => String -> g ->+loadSExpr :: (Algebra t p g s e c, MonadFail m) => String -> g ->              ([Prot t g], [Preskel t g s e]) -> SExpr Pos ->              m ([Prot t g], [Preskel t g s e]) loadSExpr nom origin (ps, ks) (L pos (S _ "defprotocol" : xs)) =@@ -58,7 +64,7 @@  -- load a protocol -loadProt :: (Algebra t p g s e c, Monad m) => String -> g ->+loadProt :: (Algebra t p g s e c, MonadFail m) => String -> g ->             Pos -> [SExpr Pos] -> m (Prot t g) loadProt nom origin pos (S _ name : S _ alg : x : xs)     | alg /= nom =@@ -83,7 +89,7 @@                 fail (shows pos msg) loadProt _ _ pos _ = fail (shows pos "Malformed protocol") -loadRoles :: (Algebra t p g s e c, Monad m) => g -> [SExpr Pos] ->+loadRoles :: (Algebra t p g s e c, MonadFail m) => g -> [SExpr Pos] ->              m (g, [Role t], [SExpr Pos]) loadRoles gen (L pos (S _ "defrole" : x) : xs) =     do@@ -93,7 +99,7 @@ loadRoles gen xs =   return (gen, [], xs) -loadRole :: (Algebra t p g s e c, Monad m) => g -> Pos ->+loadRole :: (Algebra t p g s e c, MonadFail m) => g -> Pos ->             [SExpr Pos] -> m (g, Role t) loadRole gen pos (S _ name :                   L _ (S _ "vars" : vars) :@@ -129,7 +135,7 @@  loadRole _ pos _ = fail (shows pos "Malformed role") -loadAllPredefRoleDecls :: (Algebra t p g s e c, Monad m) => Int -> [t] ->+loadAllPredefRoleDecls :: (Algebra t p g s e c, MonadFail m) => Int -> [t] ->                           [SExpr Pos] -> m [RoleDeclaration t] loadAllPredefRoleDecls height vars exprs =     do@@ -140,7 +146,7 @@                 (nats (length formats))       return result -loadAllPredefSkelDecls :: (Algebra t p g s e c, Monad m) => [Int] -> [t] ->+loadAllPredefSkelDecls :: (Algebra t p g s e c, MonadFail m) => [Int] -> [t] ->                           [SExpr Pos] -> m ([SkelDeclaration t]) loadAllPredefSkelDecls heights vars exprs =     do@@ -152,9 +158,10 @@                 (nats (length formats))       return result -loadPredefRoleDeclsAux :: (Algebra t p g s e c, Monad m) => Int -> [t] -> String ->-                       (DeclInFormat, Bool, Bool) ->-                       [SExpr Pos] -> m [(RoleDeclaration t)]+loadPredefRoleDeclsAux :: (Algebra t p g s e c, MonadFail m) => Int ->+                          [t] -> String ->+                          (DeclInFormat, Bool, Bool) ->+                          [SExpr Pos] -> m [(RoleDeclaration t)] loadPredefRoleDeclsAux _ _ _ _ [] = do return [] loadPredefRoleDeclsAux height vars tag (fmt,areq,False) exprs =     do (tg,insts) <- loadPredefRoleDecls height vars tag "" fmt areq exprs@@ -178,9 +185,10 @@ loadPredefRoleDeclsAux _ _ tag _ (x:_) =     fail (shows (annotation x) ("Malformed declaration: subtag required " ++ tag)) -loadPredefSkelDeclsAux :: (Algebra t p g s e c, Monad m) => [Int] -> [t] -> String ->-                       (DeclInFormat, Bool, Bool) ->-                       [SExpr Pos] -> m [(SkelDeclaration t)]+loadPredefSkelDeclsAux :: (Algebra t p g s e c, MonadFail m) => [Int] ->+                          [t] -> String ->+                          (DeclInFormat, Bool, Bool) ->+                          [SExpr Pos] -> m [(SkelDeclaration t)] loadPredefSkelDeclsAux _ _ _ _ [] = do return [] loadPredefSkelDeclsAux height vars tag (fmt,areq,False) exprs =     do (tg,insts) <- loadPredefSkelDecls height vars tag "" fmt areq exprs@@ -204,7 +212,7 @@      fail (shows (annotation x) ("Malformed declaration: subtag required " ++ tag)) -- loadPredefSkelDeclsAux _ _ _ (_,_,True) _ = do return [] -loadPredefRoleDecls :: (Algebra t p g s e c, Monad m) => Int -> [t] -> String ->+loadPredefRoleDecls :: (Algebra t p g s e c, MonadFail m) => Int -> [t] -> String ->                        String -> DeclInFormat -> Bool ->                        [SExpr Pos] -> m (RoleDeclaration t) -- Anything with no expressions: not present, return an empty list of instances.@@ -252,7 +260,7 @@        then fail ("[ASSERT FAILED] Input format not supported")        else fail (shows (annotation (head xs)) "[ASSERT FAILED] Input format not supported") -loadPredefSkelDecls :: (Algebra t p g s e c, Monad m) => [Int] -> [t] -> String ->+loadPredefSkelDecls :: (Algebra t p g s e c, MonadFail m) => [Int] -> [t] -> String ->                        String -> DeclInFormat -> Bool ->                        [SExpr Pos] -> m (SkelDeclaration t) -- Anything with no expressions: not present, return an empty list of instances.@@ -297,7 +305,7 @@        then fail ("[ASSERT FAILED] Input format not supported")        else fail (shows (annotation (head xs)) "[ASSERT FAILED] Input format not supported") -loadRoleTermPairPlusMaybeOneLoc :: (Algebra t p g s e c, Monad m) => Int ->+loadRoleTermPairPlusMaybeOneLoc :: (Algebra t p g s e c, MonadFail m) => Int ->                                    [t] -> String ->                                    SExpr Pos -> m (RoleDeclInst t) loadRoleTermPairPlusMaybeOneLoc _ vars stag (L _ [x1, x2]) =@@ -314,7 +322,7 @@ loadRoleTermPairPlusMaybeOneLoc _ _ _ x = fail                         (shows (annotation x) "Malformed pair of terms") -loadSkelTermPair :: (Algebra t p g s e c, Monad m) => [t] -> String ->+loadSkelTermPair :: (Algebra t p g s e c, MonadFail m) => [t] -> String ->                                    SExpr Pos -> m (SkelDeclInst t) loadSkelTermPair vars stag (L _ [x1, x2]) =     do@@ -324,7 +332,7 @@ loadSkelTermPair _ _ x = fail                         (shows (annotation x) "Malformed pair of terms") -loadRolePriority :: Monad m => Int -> SExpr Pos -> m (Int, Int)+loadRolePriority :: MonadFail m => Int -> SExpr Pos -> m (Int, Int) loadRolePriority n (L _ [N _ i, N _ p])     | 0 <= i && i < n = return (i, p) loadRolePriority _ x = fail (shows (annotation x) "Malformed priority")@@ -340,7 +348,8 @@  -- This is the only place a role is generated with an empty name. -- This is what marks a strand as a listener.-mkListenerRole :: (Algebra t p g s e c, Monad m) => Pos -> g -> m (g, Role t)+mkListenerRole :: (Algebra t p g s e c, MonadFail m) => Pos -> g ->+                  m (g, Role t) mkListenerRole pos g =   do     (g, xs) <- loadVars g [L pos [S pos "x", S pos "mesg"]]@@ -350,7 +359,7 @@  -- Protocol Rules -loadRules :: (Algebra t p g s e c, Monad m) => Prot t g -> g ->+loadRules :: (Algebra t p g s e c, MonadFail m) => Prot t g -> g ->              [SExpr Pos] -> m (g, [Rule t], [SExpr ()]) loadRules prot g (L pos (S _ "defrule" : x) : xs) =     do@@ -365,7 +374,7 @@       comment <- alist [] xs    -- Ensure remaining is an alist       return (g, [], comment) -loadRule :: (Algebra t p g s e c, Monad m) => Prot t g -> g ->+loadRule :: (Algebra t p g s e c, MonadFail m) => Prot t g -> g ->             Pos -> [SExpr Pos] -> m (g, Rule t) loadRule prot g pos (S _ name : x : xs) =   do@@ -381,7 +390,7 @@ -- Make an association list into a comment.  The first argument is the -- set of keys of key-value pairs to be dropped from the comment. -alist :: Monad m => [String] -> [SExpr Pos] -> m [SExpr ()]+alist :: MonadFail m => [String] -> [SExpr Pos] -> m [SExpr ()] alist _ [] = return [] alist keys (a@(L _ (S _ key : _)) : xs)     | elem key keys = alist keys xs@@ -418,18 +427,18 @@       f _ = False  -- Complain if alist has a bad key-badKey :: Monad m => [String] -> [SExpr Pos] -> m ()+badKey :: MonadFail 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] ->+loadTrace :: (Algebra t p g s e c, MonadFail m) => [t] ->              [SExpr Pos] -> m [Event t] loadTrace vars xs = mapM (loadEvt vars) xs -loadEvt :: (Algebra t p g s e c, Monad m) => [t] ->+loadEvt :: (Algebra t p g s e c, MonadFail m) => [t] ->           SExpr Pos -> m (Event t) loadEvt vars (L _ [S _ "recv", t]) =     do@@ -456,7 +465,7 @@     fail (shows pos $ "Malformed direction: " ++ dir) loadEvt _ x = fail (shows (annotation x) "Malformed event") -loadBaseTerms :: (Algebra t p g s e c, Monad m) => [t] -> [SExpr Pos] -> m [t]+loadBaseTerms :: (Algebra t p g s e c, MonadFail m) => [t] -> [SExpr Pos] -> m [t] loadBaseTerms _ [] = return [] loadBaseTerms vars (x : xs) =     do@@ -464,7 +473,8 @@       ts <- loadBaseTerms vars xs       return (adjoin t ts) -maybeLoadBaseTerm :: (Algebra t p g s e c, Monad m) => [t] -> SExpr Pos -> m (Maybe t)+maybeLoadBaseTerm :: (Algebra t p g s e c, MonadFail m) => [t] ->+                     SExpr Pos -> m (Maybe t) maybeLoadBaseTerm vars x =     do       t <- loadTerm vars False x@@ -472,7 +482,7 @@          True -> return (Just t)          False -> return Nothing -loadBaseTerm :: (Algebra t p g s e c, Monad m) => [t] -> SExpr Pos -> m t+loadBaseTerm :: (Algebra t p g s e c, MonadFail m) => [t] -> SExpr Pos -> m t loadBaseTerm vars x =     do       mt <- maybeLoadBaseTerm vars x@@ -480,7 +490,7 @@         Just t -> return t         Nothing -> fail (shows (annotation x) "Expecting an atom") -loadPosBaseTerms :: (Algebra t p g s e c, Monad m) => [t] ->+loadPosBaseTerms :: (Algebra t p g s e c, MonadFail m) => [t] ->                     [SExpr Pos] -> m [(Maybe Int, t)] loadPosBaseTerms _ [] = return [] loadPosBaseTerms vars (x : xs) =@@ -489,7 +499,7 @@       ts <- loadPosBaseTerms vars xs       return (t:ts) -loadPosBaseTerm :: (Algebra t p g s e c, Monad m) => [t] ->+loadPosBaseTerm :: (Algebra t p g s e c, MonadFail m) => [t] ->                    SExpr Pos -> m (Maybe Int, t) loadPosBaseTerm vars x'@(L _ [x, N _ opos])     | opos < 0 =@@ -506,7 +516,7 @@         True -> return (Nothing, t)         False -> fail (shows (annotation x) "Expecting an atom") -loadPositions :: Monad m => Int -> [SExpr Pos] -> m [Int]+loadPositions :: MonadFail m => Int -> [SExpr Pos] -> m [Int] loadPositions _ [] = return [] loadPositions height (x : xs) =     do@@ -514,7 +524,7 @@       ps <- loadPositions height xs       return (p:ps) -loadPosition :: Monad m => Int -> SExpr Pos -> m Int+loadPosition :: MonadFail m => Int -> SExpr Pos -> m Int loadPosition height x@(N _ pos)     | pos < 0 = fail (shows (annotation x) "Expecting a non-negative height")     | pos >= height = fail (shows (annotation x) "Height out of range")@@ -523,7 +533,7 @@  -- Find protocol and then load a preskeleton. -findPreskel :: (Algebra t p g s e c, Monad m) => Pos ->+findPreskel :: (Algebra t p g s e c, MonadFail m) => Pos ->                [Prot t g] -> [SExpr Pos] ->                m (Preskel t g s e) findPreskel pos ps (S _ name : xs) =@@ -532,7 +542,7 @@       Just p -> loadPreskel pos p xs findPreskel pos _ _ = fail (shows pos "Malformed skeleton") -loadPreskel :: (Algebra t p g s e c, Monad m) => Pos ->+loadPreskel :: (Algebra t p g s e c, MonadFail m) => Pos ->                Prot t g -> [SExpr Pos] ->                m (Preskel t g s e) loadPreskel pos p (L _ (S _ "vars" : vars) : xs) =@@ -541,7 +551,7 @@       loadInsts pos p kvars gen [] xs loadPreskel pos _ _ = fail (shows pos "Malformed skeleton") -loadInsts :: (Algebra t p g s e c, Monad m) => Pos ->+loadInsts :: (Algebra t p g s e c, MonadFail m) => Pos ->              Prot t g -> [t] -> g -> [Instance t e] ->              [SExpr Pos] -> m (Preskel t g s e) loadInsts top p kvars gen insts (L pos (S _ "defstrand" : x) : xs) =@@ -587,7 +597,7 @@ loadComment key comment =   [L () (S () key : map strip comment)] -loadPriorities :: (Algebra t p g s e c, Monad m) => [SExpr Pos] ->+loadPriorities :: (Algebra t p g s e c, MonadFail m) => [SExpr Pos] ->                   [Instance t e] -> m [((Int,Int),Int)] loadPriorities [] _ = return [] loadPriorities ((L pos [L _ [N _ s, N _ i], N _ p]) : rest) insts@@ -612,7 +622,7 @@     where       keys = [ key | L _ (S _ head : (S _ key : _)) <- alist, head=="decl" ] -loadInst :: (Algebra t p g s e c, Monad m) => Pos ->+loadInst :: (Algebra t p g s e c, MonadFail m) => Pos ->             Prot t g -> [t] -> g -> String -> Int ->             [SExpr Pos] -> m (g, Instance t e) loadInst pos p kvars gen role height env =@@ -626,7 +636,7 @@               (gen', env') <- foldM (loadMaplet kvars vars) (gen, emptyEnv) env               return (mkInstance gen' r env' height) -lookupRole :: Monad m => Pos -> Prot t g -> String -> m (Role t)+lookupRole :: MonadFail m => Pos -> Prot t g -> String -> m (Role t) lookupRole _ p role  | role == "" =     return $ listenerRole p lookupRole pos p role =@@ -635,7 +645,7 @@           fail (shows pos $ "Role " ++ role ++ " not found in " ++ pname p)       Just r -> return r -loadMaplet :: (Algebra t p g s e c, Monad m) => [t] -> [t] ->+loadMaplet :: (Algebra t p g s e c, MonadFail m) => [t] -> [t] ->               (g, e) -> SExpr Pos -> m (g, e) loadMaplet kvars vars env (L pos [domain, range]) =     do@@ -646,14 +656,14 @@         [] -> fail (shows pos "Domain does not match range") loadMaplet _ _ _ x = fail (shows (annotation x) "Malformed maplet") -loadListener :: (Algebra t p g s e c, Monad m) => Prot t g ->+loadListener :: (Algebra t p g s e c, MonadFail m) => Prot t g ->                 [t] -> g -> SExpr Pos -> m (g, Instance t e) loadListener p kvars gen x =     do       t <- loadTerm kvars False x       return $ mkListener p gen t -loadRest :: (Algebra t p g s e c, Monad m) => Pos -> [t] ->+loadRest :: (Algebra t p g s e c, MonadFail m) => Pos -> [t] ->             Prot t g -> [Goal t] -> g -> [Instance t e] ->             [SExpr Pos] -> [SExpr Pos] -> SkelDeclList t ->             [SExpr Pos] -> [SExpr ()] -> [((Int,Int),Int)] ->@@ -682,7 +692,7 @@       where         termsInDlist olist = concat $ map dterms (concatMap snd olist) -loadGenSkelDecls :: (Algebra t p g s e c, Monad m) => [Int] -> [t] ->+loadGenSkelDecls :: (Algebra t p g s e c, MonadFail m) => [Int] -> [t] ->                     [(String,[SExpr Pos])] -> m [SkelDeclaration t] loadGenSkelDecls _ _ [] = return [] loadGenSkelDecls heights vars ((name,rawds):b) =@@ -691,7 +701,8 @@       b' <- loadGenSkelDecls heights vars b       return ((name,a'):b') -loadGenSkelDeclList :: (Algebra t p g s e c, Monad m) => [Int] -> [t] -> [SExpr Pos] ->+loadGenSkelDeclList :: (Algebra t p g s e c, MonadFail m) => [Int] ->+                       [t] -> [SExpr Pos] ->                        m (SkelDeclInstList t) loadGenSkelDeclList _ _ [] = return [] loadGenSkelDeclList heights vars (a:b) =@@ -700,7 +711,8 @@       b' <- loadGenSkelDeclList heights vars b       return (a':b') -loadGenSkelDecl :: (Algebra t p g s e c, Monad m) => [Int] -> [t] -> String ->+loadGenSkelDecl :: (Algebra t p g s e c, MonadFail m) => [Int] ->+                   [t] -> String ->                    SExpr Pos -> m (SkelDeclInst t) loadGenSkelDecl heights vars stag (L _ (tlist:llist)) =     do@@ -712,7 +724,7 @@ loadGenSkelDecl _ _ _ x =     fail (shows (annotation x) "Malformed declaration: expecting a list") -loadGenRoleDecls :: (Algebra t p g s e c, Monad m) => Int -> [t] ->+loadGenRoleDecls :: (Algebra t p g s e c, MonadFail m) => Int -> [t] ->                     [(String,[SExpr Pos])] -> m [RoleDeclaration t] loadGenRoleDecls _ _ [] = return [] loadGenRoleDecls height vars ((name,rawds):b) =@@ -721,7 +733,8 @@       b' <- loadGenRoleDecls height vars b       return ((name,a'):b') -loadGenRoleDeclList :: (Algebra t p g s e c, Monad m) => Int -> [t] -> [SExpr Pos] ->+loadGenRoleDeclList :: (Algebra t p g s e c, MonadFail m) => Int ->+                       [t] -> [SExpr Pos] ->                        m (RoleDeclInstList t) loadGenRoleDeclList _ _ [] = return [] loadGenRoleDeclList height vars (a:b) =@@ -730,7 +743,7 @@       b' <- loadGenRoleDeclList height vars b       return (a':b') -loadGenRoleDecl :: (Algebra t p g s e c, Monad m) => Int -> [t] -> String ->+loadGenRoleDecl :: (Algebra t p g s e c, MonadFail m) => Int -> [t] -> String ->                    SExpr Pos -> m (RoleDeclInst t) loadGenRoleDecl height vars stag (L _ (tlist:llist)) =     do@@ -742,7 +755,7 @@ loadGenRoleDecl _ _ _ x =     fail (shows (annotation x) "Malformed declaration: expecting a list") -loadOrderings :: Monad m => [Int] -> [SExpr Pos] -> Bool -> m [Pair]+loadOrderings :: MonadFail m => [Int] -> [SExpr Pos] -> Bool -> m [Pair] loadOrderings heights x strict =     foldM f [] x     where@@ -751,7 +764,7 @@             np <- loadPair heights x strict             return (adjoin np ns) -loadPair :: Monad m => [Int] -> SExpr Pos -> Bool -> m Pair+loadPair :: MonadFail m => [Int] -> SExpr Pos -> Bool -> m Pair loadPair heights (L pos [x0, x1]) strict =     do       n0 <- loadNode heights x0@@ -761,7 +774,7 @@         False -> return (n0, n1) loadPair _ x _ = fail (shows (annotation x) "Malformed pair") -loadTerms :: (Algebra t p g s e c, Monad m) => [t] -> SExpr Pos -> m [t]+loadTerms :: (Algebra t p g s e c, MonadFail m) => [t] -> SExpr Pos -> m [t] loadTerms _ (L _ []) = return [] loadTerms vars (L pos (head:rest)) =     do@@ -770,7 +783,7 @@       return (a:b) loadTerms _ x = fail (shows (annotation x) "Malformed list of terms") -loadNodes :: Monad m => [Int] -> [SExpr Pos] -> m [Node]+loadNodes :: MonadFail m => [Int] -> [SExpr Pos] -> m [Node] loadNodes _ [] = return [] loadNodes heights (head:rest) =     do@@ -778,7 +791,7 @@       a <- loadNode heights head       return (a:b) -loadIntsMax :: Monad m => Int -> [SExpr Pos] -> m [Int]+loadIntsMax :: MonadFail m => Int -> [SExpr Pos] -> m [Int] loadIntsMax _ [] = return [] loadIntsMax max (a:b) =     do@@ -786,14 +799,14 @@       b <- loadIntsMax max b       return (a:b) -loadIntMax :: Monad m => Int -> SExpr Pos -> m Int+loadIntMax :: MonadFail m => Int -> SExpr Pos -> m Int loadIntMax max (N pos x)     | x < 0 = fail (shows pos "Malformed declaration: Negative position in role")     | x >= max = fail (shows pos "Malformed declaration: Bad position in role")     | otherwise = return x loadIntMax _ x = fail (shows (annotation x) "Malformed declaration: position") -loadNode :: Monad m => [Int] -> SExpr Pos -> m Node+loadNode :: MonadFail m => [Int] -> SExpr Pos -> m Node loadNode heights (L pos [N _ s, N _ p])     | s < 0 = fail (shows pos "Malformed node: Negative strand in node")     | p < 0 = fail (shows pos "Malformed node: Negative position in node")@@ -809,7 +822,7 @@           | otherwise = height xs (s - 1) loadNode _ x = fail (shows (annotation x) "Malformed node") -loadFact :: (Algebra t p g s e c, Monad m) =>+loadFact :: (Algebra t p g s e c, MonadFail m) =>             [Int] -> [t] -> SExpr Pos -> m (Fact t) loadFact heights vars (L _ (S _ name : fs)) =   do@@ -818,7 +831,7 @@ loadFact _ _ x =   fail (shows (annotation x) "Malformed fact") -loadFterm :: (Algebra t p g s e c, Monad m) =>+loadFterm :: (Algebra t p g s e c, MonadFail m) =>              [Int] -> [t] -> SExpr Pos -> m (FTerm t) loadFterm heights _ (N pos s)   | 0 <= s && s < length heights = return $ FSid s@@ -828,7 +841,7 @@     t <- loadTerm vars False x     return $ FTerm t -loadPov :: (Algebra t p g s e c, Monad m) => Pos -> Prot t g ->+loadPov :: (Algebra t p g s e c, MonadFail m) => Pos -> Prot t g ->            [SExpr Pos] -> m (Maybe (Preskel t g s e), [Sid]) loadPov _ _ [] = return (Nothing, []) loadPov pos p [L _ xs, x] =@@ -838,18 +851,18 @@     return (Just k, prob) loadPov pos _ _ = fail (shows pos "Bad POV within a skeleton") -loadInt :: Monad m => SExpr Pos -> m Int+loadInt :: MonadFail m => SExpr Pos -> m Int loadInt (N _ n) = return n loadInt x = fail (shows (annotation x) "Expecting an integer") -loadPovPreskel :: (Algebra t p g s e c, Monad m) => Pos -> Prot t g ->+loadPovPreskel :: (Algebra t p g s e c, MonadFail m) => Pos -> Prot t g ->                   SExpr Pos -> m (Preskel t g s e) loadPovPreskel _ p (L pos (S _ "defskeleton" : S _ name : xs))   | pname p == name = loadPreskel pos p xs   | otherwise = fail (shows pos $ "Protocol " ++ name ++ " mismatch") loadPovPreskel pos _ _ = fail (shows pos "Malformed defskeleton") -checkProb :: Monad m => Pos -> Int -> [Sid] -> m ()+checkProb :: MonadFail m => Pos -> Int -> [Sid] -> m () checkProb pos nstrands prob =   mapM_ f prob   where@@ -859,7 +872,7 @@ -- Security Goals  -- Load a defgoal form-findGoal :: (Algebra t p g s e c, Monad m) => Pos ->+findGoal :: (Algebra t p g s e c, MonadFail m) => Pos ->             [Prot t g] -> [SExpr Pos] -> m (Preskel t g s e) findGoal pos ps (S _ name : x : xs) =     case L.find (\p -> name == pname p) ps of@@ -889,7 +902,7 @@  --- Load a sequence of security goals -loadGoals :: (Algebra t p g s e c, Monad m) => Pos -> Prot t g ->+loadGoals :: (Algebra t p g s e c, MonadFail m) => Pos -> Prot t g ->              g -> [SExpr Pos] -> m (g, [Goal t]) loadGoals _ _ g [] = return (g, []) loadGoals pos prot g (x : xs) =@@ -905,7 +918,7 @@ -- Load a single security goal, a universally quantified formula -- Returns the goal and the antecedent with position information. -loadSentence :: (Algebra t p g s e c, Monad m) => Mode -> Pos ->+loadSentence :: (Algebra t p g s e c, MonadFail m) => Mode -> Pos ->                 Prot t g -> g -> SExpr Pos -> m (g, Goal t, Conj t) loadSentence md _ prot g (L pos [S _ "forall", L _ vs, x]) =   do@@ -915,7 +928,8 @@  -- Load the top-level implication of a security goal -loadImplication :: (Algebra t p g s e c, Monad m) => Mode -> Pos -> Prot t g ->+loadImplication :: (Algebra t p g s e c, MonadFail m) => Mode ->+                   Pos -> Prot t g ->                    g -> [t] -> SExpr Pos -> m (g, Goal t, Conj t) loadImplication md _ prot g vars (L pos [S _ "implies", a, c]) =   do@@ -934,7 +948,7 @@ -- The conclusion must be a disjunction.  Each disjunct may introduce -- existentially quantified variables. -loadConclusion :: (Algebra t p g s e c, Monad m) => Pos -> Prot t g ->+loadConclusion :: (Algebra t p g s e c, MonadFail m) => Pos -> Prot t g ->                   g -> [t] -> SExpr Pos -> m (g, [([t], Conj t)]) loadConclusion _ _ g _ (L _ [S _ "false"]) = return (g, []) loadConclusion _ prot g vars (L pos (S _ "or" : xs)) =@@ -944,7 +958,7 @@     (g, a) <- loadExistential pos prot g vars x     return (g, [a]) -loadDisjuncts :: (Algebra t p g s e c, Monad m) => Pos ->+loadDisjuncts :: (Algebra t p g s e c, MonadFail m) => Pos ->                  Prot t g -> g -> [t] -> [SExpr Pos] ->                  [([t], Conj t)] -> m (g, [([t], Conj t)]) loadDisjuncts _ _ g _ [] rest = return (g, reverse rest)@@ -953,7 +967,7 @@     (g, a) <- loadExistential pos prot g vars x     loadDisjuncts pos prot g vars xs (a : rest) -loadExistential :: (Algebra t p g s e c, Monad m) => Pos -> Prot t g ->+loadExistential :: (Algebra t p g s e c, MonadFail m) => Pos -> Prot t g ->                    g -> [t] -> SExpr Pos -> m (g, ([t], Conj t)) loadExistential _ prot g vars (L pos [S _ "exists", L _ vs, x]) =   do@@ -968,7 +982,7 @@ -- Load a conjunction and check the result as determined by the mode -- md. -loadCheckedConj :: (Algebra t p g s e c, Monad m) => Mode -> Pos ->+loadCheckedConj :: (Algebra t p g s e c, MonadFail m) => Mode -> Pos ->                    Prot t g -> [t] -> [t] -> SExpr Pos -> m (Conj t) loadCheckedConj RoleSpec pos prot vars unbound x =   loadRoleSpecific pos prot vars unbound x@@ -978,7 +992,7 @@ --- Load a conjunction of atomic formulas and ensure the formula is --- role specific. -loadRoleSpecific :: (Algebra t p g s e c, Monad m) => Pos -> Prot t g ->+loadRoleSpecific :: (Algebra t p g s e c, MonadFail m) => Pos -> Prot t g ->                     [t] -> [t] -> SExpr Pos -> m (Conj t) loadRoleSpecific pos prot vars unbound x =   do@@ -996,7 +1010,7 @@ -- Load a conjuction of atomic formulas and ensure that all declared -- variables are used. -loadUsedVars :: (Algebra t p g s e c, Monad m) => Pos -> Prot t g ->+loadUsedVars :: (Algebra t p g s e c, MonadFail m) => Pos -> Prot t g ->                 [t] -> [t] -> SExpr Pos -> m (Conj t) loadUsedVars pos prot vars unbound x =   do@@ -1009,7 +1023,7 @@  -- Load a conjunction of atomic formulas -loadConjunction :: (Algebra t p g s e c, Monad m) => Pos -> Prot t g ->+loadConjunction :: (Algebra t p g s e c, MonadFail m) => Pos -> Prot t g ->                    [t] -> SExpr Pos -> m (Conj t) loadConjunction _ p kvars (L pos (S _ "and" : xs)) =   loadConjuncts pos p kvars xs []@@ -1018,7 +1032,7 @@     (pos, a) <- loadPrimary top p kvars x     return [(pos, a)] -loadConjuncts :: (Algebra t p g s e c, Monad m) => Pos -> Prot t g ->+loadConjuncts :: (Algebra t p g s e c, MonadFail m) => Pos -> Prot t g ->                  [t] -> [SExpr Pos] -> Conj t -> m (Conj t) loadConjuncts _ _ _ [] rest = return (reverse rest) loadConjuncts top p kvars (x : xs) rest =@@ -1028,7 +1042,7 @@  -- Load the atomic formulas -loadPrimary :: (Algebra t p g s e c, Monad m) => Pos -> Prot t g ->+loadPrimary :: (Algebra t p g s e c, MonadFail m) => Pos -> Prot t g ->                [t] -> SExpr Pos -> m (Pos, AForm t) loadPrimary _ _ kvars (L pos [S _ "=", x, y]) =   do@@ -1105,7 +1119,7 @@  -- Load a term and make sure it has sort strd -loadStrdTerm :: (Algebra t p g s e c, Monad m) =>+loadStrdTerm :: (Algebra t p g s e c, MonadFail  m) =>                 [t] -> SExpr Pos -> m t loadStrdTerm ts x =   do@@ -1116,7 +1130,7 @@  -- Load a term and make sure it describes a node -loadNodeTerm :: (Algebra t p g s e c, Monad m) =>+loadNodeTerm :: (Algebra t p g s e c, MonadFail m) =>                 [t] -> SExpr Pos -> SExpr Pos -> m (NodeTerm t) loadNodeTerm ts x (N _ i) | i >= 0 =   do@@ -1127,7 +1141,7 @@  -- Load a term and make sure it does not have sort node -loadAlgTerm :: (Algebra t p g s e c, Monad m) => [t] -> SExpr Pos -> m t+loadAlgTerm :: (Algebra t p g s e c, MonadFail m) => [t] -> SExpr Pos -> m t loadAlgTerm _ x@(L _ [N _ _, N _ _]) =   fail (shows (annotation x) "Expecting an algebra term") loadAlgTerm ts x =@@ -1148,7 +1162,7 @@  -- Returns variables in unbound that are not role specific -roleSpecific :: (Algebra t p g s e c, Monad m) =>+roleSpecific :: (Algebra t p g s e c, MonadFail m) =>                 [t] -> (Pos, AForm t) -> m [t] roleSpecific unbound (_, Length _ z _) =   return $ L.delete z unbound
src/CPSA/Lib/Protocol.hs view
@@ -6,6 +6,12 @@ -- modify it under the terms of the BSD License as published by the -- University of California. +{-# LANGUAGE CPP #-}++#if !(MIN_VERSION_base(4,13,0))+#define MonadFail Monad+#endif+ module CPSA.Lib.Protocol (Event (..), evtTerms, evtMesgTerms, evtMap, evt,     recvTerm, Trace, stripSync, tterms, originates,     originationPos, gainedPos, genGainedPos, firstOccurs,@@ -344,7 +350,7 @@ -- the trace, and every variable that occurs in each atom -- declared to be non-originating occurs in some term in the trace, -- and the atom must never be carried by any term in the trace.-roleWellFormed :: (Monad m, Algebra t p g s e c) => Role t -> m ()+roleWellFormed :: (MonadFail m, Algebra t p g s e c) => Role t -> m () roleWellFormed role =     do       failwith "[ASSERT FAILED] invalid declaration"
src/CPSA/Lib/Strand.hs view
@@ -6,6 +6,12 @@ -- modify it under the terms of the BSD License as published by the -- University of California. +{-# LANGUAGE CPP #-}++#if !(MIN_VERSION_base(4,13,0))+#define MonadFail Monad+#endif+ module CPSA.Lib.Strand (Instance, mkInstance, bldInstance, mkListener,     role, env, trace, height, listenerTerm, Sid, Node, mkPreskel,     firstSkeleton, Pair, Preskel, gen, protocol, kgoals, insts,@@ -1250,7 +1256,7 @@ thinManyStrands prs ps =   [ prs' | prs' <- compressMany prs ps,            prs'' <- compressMany prs (swap ps),-           isomorphic (gist (skel prs')) (gist (skel prs''))]+           probIsomorphic (skel prs') (skel prs'')]  compressMany :: Algebra t p g s e c => PRS t p g s e c ->                 [(Sid, Sid)] -> [PRS t p g s e c]@@ -2136,7 +2142,7 @@                             (filter (\(t, _) -> not (isNum t)) (kugen k)))  -- Do notation friendly preskeleton well formed check.-wellFormedPreskel :: (Monad m, Algebra t p g s e c) =>+wellFormedPreskel :: (MonadFail m, Algebra t p g s e c) =>                      Preskel t g s e -> m (Preskel t g s e) wellFormedPreskel k     | preskelWellFormed k = return k@@ -2145,7 +2151,7 @@ -- Exported -- A version of preskelWellFormed that explains why a preskeleton is -- not well formed.-verbosePreskelWellFormed :: (Monad m, Algebra t p g s e c) =>+verbosePreskelWellFormed :: (MonadFail m, Algebra t p g s e c) =>                             Preskel t g s e -> m () verbosePreskelWellFormed k =     do@@ -2189,14 +2195,14 @@           (null ts)  -- Do notation friendly preskeleton well formed check.-reducedWellFormed :: Monad m => Preskel t g s e -> m ()+reducedWellFormed :: MonadFail m => Preskel t g s e -> m () reducedWellFormed k   | reducedWellOrdered k = return ()   | otherwise = fail "reduced preskeleton not well formed"  -- A transition or an observer node should have at most one transition -- node immediately after it.-noStateSplit :: Monad m => Preskel t g s e -> m ()+noStateSplit :: MonadFail m => Preskel t g s e -> m () noStateSplit k   | loop (leadsto k) S.empty = return ()   | otherwise = fail "reduced preskeleton has a state split"
src/CPSA/Lib/Utilities.hs view
@@ -7,6 +7,8 @@ -- modify it under the terms of the BSD License as published by the -- University of California. +{-# LANGUAGE CPP #-}+ module CPSA.Lib.Utilities where  import qualified Data.Set as S@@ -30,8 +32,14 @@ instance Monad ReturnFail where     Fail l >>= _   = Fail l     Return r >>= k = k r-    fail s = Fail s             -- This must be moved to MonadFail +#if (MIN_VERSION_base(4,13,0))+instance MonadFail ReturnFail where+#else+#define MonadFail Monad+#endif+    fail s         = Fail s+ adjoin :: Eq a => a -> [a] -> [a] adjoin x xs     | x `elem` xs = xs@@ -62,7 +70,7 @@ nats n = [0..(n - 1)]  {-# INLINE assert #-}-assert :: Monad m => (a -> Bool) -> a -> m a+assert :: MonadFail m => (a -> Bool) -> a -> m a assert pred x     | pred x = return x     | otherwise = fail "assertion failed"@@ -114,7 +122,7 @@       (Just n, Just n') -> n >= n'       _ -> True -failwith :: Monad m => String -> Bool -> m ()+failwith :: MonadFail m => String -> Bool -> m () failwith msg test =     case test of       True -> return ()
src/CPSA/Match/Match.hs view
@@ -4,6 +4,12 @@ -- modify it under the terms of the BSD License as published by the -- University of California. +{-# LANGUAGE CPP #-}++#if !(MIN_VERSION_base(4,13,0))+#define MonadFail Monad+#endif+ module CPSA.Match.Match (testMatcher) where  import CPSA.Lib.SExpr@@ -31,7 +37,7 @@     return $ L () $ map (showSubst vs) (absenceSubst g a) go _ x = fail (shows (annotation x) "Malformed input!") -loadMatch :: (Algebra t p g s e c, Monad m) =>+loadMatch :: (Algebra t p g s e c, MonadFail m) =>               [t] -> SExpr Pos -> m (t, t) loadMatch vs (L _ [r, n]) =   do
src/CPSA/SAS/SAS.hs view
@@ -6,6 +6,12 @@ -- modify it under the terms of the BSD License as published by the -- University of California. +{-# LANGUAGE CPP #-}++#if !(MIN_VERSION_base(4,13,0))+#define MonadFail Monad+#endif+ module CPSA.SAS.SAS (State, sas) where  import Control.Monad (foldM)@@ -31,7 +37,7 @@  type State t g c = ([Prot t g c], [Preskel t g c]) -sas :: (Algebra t p g s e c, Monad m) => String -> g ->+sas :: (Algebra t p g s e c, MonadFail m) => String -> g ->          State t g c -> Maybe (SExpr Pos) ->          m (State t g c, Maybe (SExpr ())) sas _ _ (ps, ks) Nothing =    -- Nothing signifies end-of-file@@ -41,7 +47,7 @@ sas name gen (ps, ks) (Just sexpr) = -- Looking for shapes     loadOtherPreskel name gen ps ks sexpr -loadPOV :: (Algebra t p g s e c, Monad m) => String -> g ->+loadPOV :: (Algebra t p g s e c, MonadFail m) => String -> g ->            [Prot t g c] -> SExpr Pos ->            m (State t g c, Maybe (SExpr ())) loadPOV name origin ps (L pos (S _ "defprotocol" : xs)) =@@ -60,7 +66,7 @@         _ -> return ((ps, []), Nothing) -- Not POV loadPOV _ _ ps _ = return ((ps, []), Nothing) -loadOtherPreskel :: (Algebra t p g s e c, Monad m) => String -> g ->+loadOtherPreskel :: (Algebra t p g s e c, MonadFail m) => String -> g ->                     [Prot t g c] -> [Preskel t g c] ->                     SExpr Pos -> m (State t g c, Maybe (SExpr ())) loadOtherPreskel name origin ps ks (L pos (S _ "defprotocol" : xs)) =@@ -81,7 +87,7 @@ loadOtherPreskel _ _ ps ks _ = return ((ps, ks), Nothing)  -- Ensure every uniq originates-origCheck :: (Algebra t p g s e c, Monad m) =>+origCheck :: (Algebra t p g s e c, MonadFail m) =>              Pos -> Preskel t g c -> m () origCheck pos k =   mapM_ f (uniqs k)@@ -114,7 +120,7 @@  -- Load a protocol.  On success, returns a Prot record. -loadProt :: (Algebra t p g s e c, Monad m) => String -> g ->+loadProt :: (Algebra t p g s e c, MonadFail m) => String -> g ->             Pos -> [SExpr Pos] -> m (Prot t g c) loadProt nom origin pos (S _ name : S _ alg : x : xs)     | alg /= nom =@@ -132,7 +138,7 @@ -- every variable that occurs in a preskeleton never occurs in one of -- its roles. -loadRoles :: (Algebra t p g s e c, Monad m) => g ->+loadRoles :: (Algebra t p g s e c, MonadFail m) => g ->              [SExpr Pos] -> m (g, [Role t c]) loadRoles origin xs =     mapAccumLM loadRole origin $ stripComments xs@@ -154,7 +160,7 @@       (z'', ys) <- mapAccumLM f z' xs       return (z'', y : ys) -loadRole :: (Algebra t p g s e c, Monad m) => g ->+loadRole :: (Algebra t p g s e c, MonadFail m) => g ->             SExpr Pos -> m (g, Role t c) loadRole gen (L _ (S _ "defrole" :                      S _ name :@@ -174,7 +180,7 @@ listenerName :: String listenerName = "" -makeListenerRole :: (Algebra t p g s e c, Monad m) => Pos -> g ->+makeListenerRole :: (Algebra t p g s e c, MonadFail m) => Pos -> g ->                     m (g, Role t c) makeListenerRole pos gen =     do@@ -184,7 +190,7 @@       let r = Role { rname = listenerName, vars = vars, ctx = ctx }       return (gen', r) -makeVar :: (Algebra t p g s e c, Monad m) => Pos -> g -> String -> m (g, t)+makeVar :: (Algebra t p g s e c, MonadFail m) => Pos -> g -> String -> m (g, t) makeVar pos gen name =     do       (gen', ts) <- loadVars gen [L pos [S pos name, S pos "mesg"]]@@ -202,7 +208,7 @@ type GVM g t = (g, VM t)  -- Add a variable for a node if the mapping does not already exist.-addVar :: (Algebra t p g s e c, Monad m) =>+addVar :: (Algebra t p g s e c, MonadFail m) =>           Pos -> GVM g t -> Strand -> m (GVM g t) addVar pos (gen, vm) z =   case M.lookup z vm of@@ -224,7 +230,7 @@  -- Find a protocol -findProt :: Monad m => Pos -> [Prot t g c] -> [SExpr Pos] -> m (Prot t g c)+findProt :: MonadFail m => Pos -> [Prot t g c] -> [SExpr Pos] -> m (Prot t g c) findProt pos ps (S _ name : _) =     case L.find (\p -> name == pname p) ps of       Nothing -> fail (shows pos $ "Protocol " ++ name ++ " unknown")@@ -269,7 +275,7 @@       homomorphisms :: [SExpr Pos], -- Loaded later       varmap :: VM t } -loadPreskel :: (Algebra t p g s e c, Monad m) => Pos -> Prot t g c ->+loadPreskel :: (Algebra t p g s e c, MonadFail m) => Pos -> Prot t g c ->                g -> [SExpr Pos] -> m (Preskel t g c) loadPreskel pos prot gen (S _ _ : L _ (S _ "vars" : vars) : xs) =     do@@ -304,7 +310,7 @@                         varmap = varmap}) loadPreskel pos _ _ _ = fail (shows pos "Malformed skeleton") -loadInsts :: (Algebra t p g s e c, Monad m) => Prot t g c ->+loadInsts :: (Algebra t p g s e c, MonadFail m) => Prot t g c ->              [t] -> [Instance t c] -> [SExpr Pos] -> m [Instance t c] loadInsts prot kvars insts (L pos (S _ "defstrand" : x) : xs) =     case x of@@ -325,7 +331,7 @@ loadInsts _ _ insts _ =     return (reverse insts) -loadInst :: (Algebra t p g s e c, Monad m) => Pos -> Prot t g c ->+loadInst :: (Algebra t p g s e c, MonadFail m) => Pos -> Prot t g c ->             [t] -> String -> Int -> [SExpr Pos] -> m (Instance t c) loadInst pos prot kvars role height env =     do@@ -334,14 +340,14 @@       return (Instance { pos = pos, role = r,                          env = env, height = height }) -lookupRole :: Monad m => Pos -> Prot t g c -> String -> m (Role t c)+lookupRole :: MonadFail m => Pos -> Prot t g c -> String -> m (Role t c) lookupRole pos prot role =     case L.find (\r -> role == rname r) (roles prot) of       Nothing ->           fail (shows pos $ "Role " ++ role ++ " not found in " ++ pname prot)       Just r -> return r -loadMaplet :: (Algebra t p g s e c, Monad m) =>+loadMaplet :: (Algebra t p g s e c, MonadFail m) =>               [t] -> [t] -> SExpr Pos -> m (t, t) loadMaplet kvars vars (L _ [domain, range]) =     do@@ -350,7 +356,7 @@       return (t, t') loadMaplet _ _ x = fail (shows (annotation x) "Malformed maplet") -loadListener :: (Algebra t p g s e c, Monad m) => Pos ->+loadListener :: (Algebra t p g s e c, MonadFail m) => Pos ->                 Prot t g c -> [t] -> SExpr Pos -> m (Instance t c) loadListener pos prot kvars x =     do@@ -361,7 +367,7 @@  -- Load the node orderings -loadOrderings :: Monad m => Strands -> [SExpr Pos] -> m [Pair]+loadOrderings :: MonadFail m => Strands -> [SExpr Pos] -> m [Pair] loadOrderings _ [] = return [] loadOrderings strands (x : xs) =     do@@ -369,7 +375,7 @@       nps <- loadOrderings strands xs       return (adjoin np nps) -loadPair :: Monad m => [Int] -> SExpr Pos -> m Pair+loadPair :: MonadFail m => [Int] -> SExpr Pos -> m Pair loadPair heights (L pos [x0, x1]) =     do       n0 <- loadNode heights x0@@ -381,7 +387,7 @@       sameStrands (s0, _) (s1, _) = s0 == s1 loadPair _ x = fail (shows (annotation x) "Malformed pair") -loadNode :: Monad m => [Int] -> SExpr Pos -> m Node+loadNode :: MonadFail m => [Int] -> SExpr Pos -> m Node loadNode heights (L pos [N _ s, N _ p])     | s < 0 = fail (shows pos "Negative strand in node")     | p < 0 = fail (shows pos "Negative position in node")@@ -397,7 +403,8 @@           | otherwise = height xs (s - 1) loadNode _ x = fail (shows (annotation x) "Malformed node") -loadBaseTerms :: (Algebra t p g s e c, Monad m) => [t] -> [SExpr Pos] -> m [t]+loadBaseTerms :: (Algebra t p g s e c, MonadFail m) => [t] ->+                 [SExpr Pos] -> m [t] loadBaseTerms _ [] = return [] loadBaseTerms vars (x : xs) =     do@@ -405,7 +412,7 @@       ts <- loadBaseTerms vars xs       return (adjoin t ts) -loadBaseTerm :: (Algebra t p g s e c, Monad m) => [t] -> SExpr Pos -> m t+loadBaseTerm :: (Algebra t p g s e c, MonadFail m) => [t] -> SExpr Pos -> m t loadBaseTerm vars x =     do       t <- loadTerm vars False x@@ -413,7 +420,7 @@         True -> return t         False -> fail (shows (annotation x) "Expecting an atom") -loadOrigs :: (Algebra t p g s e c, Monad m) => [t] -> Strands ->+loadOrigs :: (Algebra t p g s e c, MonadFail m) => [t] -> Strands ->              [SExpr Pos] -> m [(t, Node)] loadOrigs _ _ [] = return [] loadOrigs vars heights (x : xs) =@@ -422,7 +429,7 @@       os <- loadOrigs vars heights xs       return (adjoin o os) -loadOrig :: (Algebra t p g s e c, Monad m) => [t] -> Strands ->+loadOrig :: (Algebra t p g s e c, MonadFail m) => [t] -> Strands ->             SExpr Pos -> m (t, Node) loadOrig vars heights (L _ [x, y]) =     do@@ -433,12 +440,12 @@     fail (shows (annotation x) "Malformed origination")  -- Make a variable for each strand-makeVarmap :: (Algebra t p g s e c, Monad m) =>+makeVarmap :: (Algebra t p g s e c, MonadFail m) =>               Pos -> g -> [Strand] -> m (GVM g t) makeVarmap pos g strands =   foldM (addVar pos) (g, M.empty) strands -loadFact :: (Algebra t p g s e c, Monad m) => [t] ->+loadFact :: (Algebra t p g s e c, MonadFail m) => [t] ->             VM t -> SExpr Pos -> m (Fact t) loadFact vars varmap (L _ (S _ name : ft)) =   do@@ -447,7 +454,7 @@ loadFact _ _ x =   fail (shows (annotation x) "Malformed fact") -loadFactTerm :: (Algebra t p g s e c, Monad m) =>+loadFactTerm :: (Algebra t p g s e c, MonadFail m) =>                 [t] -> VM t -> SExpr Pos -> m t loadFactTerm _ varmap (N pos z) =   case M.lookup z varmap of@@ -464,12 +471,12 @@  type Homo t = ([(t, t)], [(t, t)]) -loadMaps :: (Algebra t p g s e c, Monad m) => Preskel t g c ->+loadMaps :: (Algebra t p g s e c, MonadFail m) => Preskel t g c ->             Preskel t g c -> [SExpr Pos] -> m [Homo t] loadMaps pov k maps =     mapM (loadMap pov k) maps -loadMap :: (Algebra t p g s e c, Monad m) => Preskel t g c ->+loadMap :: (Algebra t p g s e c, MonadFail m) => Preskel t g c ->             Preskel t g c -> SExpr Pos -> m (Homo t) loadMap pov k (L _ [L _ strandMap, L _ algebraMap]) =     do@@ -480,18 +487,19 @@       return (nh, ah) loadMap _ _ x = fail (shows (annotation x) "Malformed map") -loadPerm :: Monad m => SExpr Pos -> m Int+loadPerm :: MonadFail m => SExpr Pos -> m Int loadPerm (N _ n) | n >= 0 = return n loadPerm x = fail (shows (annotation x) "Expecting a natural number")  -- Applies a strand permutation to a strand.-loadStrandEq :: Monad m => Preskel t g c -> [Int] -> (Strand, t) -> m (t, t)+loadStrandEq :: MonadFail m => Preskel t g c -> [Int] ->+                (Strand, t) -> m (t, t) loadStrandEq k perm (z, v) =   do     z <- index perm z     return (v, slookup z (varmap k)) -index :: Monad m => [a] -> Int -> m a+index :: MonadFail m => [a] -> Int -> m a index (x : _) 0 = return x index (_ : xs) i | i > 0 = index xs (i - 1) index _ _ = fail "Bad strand map"@@ -552,7 +560,7 @@  type Analysis t g c = (Preskel t g c, [(Homo t, Preskel t g c)]) -loadAnalysis :: (Algebra t p g s e c, Monad m) => Preskel t g c ->+loadAnalysis :: (Algebra t p g s e c, MonadFail m) => Preskel t g c ->                 [Preskel t g c] -> m (Analysis t g c) loadAnalysis pov ks =   do@@ -642,7 +650,7 @@  -- Formula printing -displayFormula :: (Algebra t p g s e c, Monad m) =>+displayFormula :: (Algebra t p g s e c, MonadFail m) =>                   [Prot t g c] -> [Preskel t g c] ->                   m (State t g c, Maybe (SExpr ())) displayFormula ps [] =
src/CPSA/Shapes/Shapes.hs view
@@ -6,6 +6,12 @@ -- modify it under the terms of the BSD License as published by the -- University of California. +{-# LANGUAGE CPP #-}++#if !(MIN_VERSION_base(4,13,0))+#define MonadFail Monad+#endif+ module CPSA.Shapes.Shapes (Map, empty, shape) where  import qualified Data.IntMap as I@@ -24,7 +30,7 @@ -- skeleton is changed to reflect omitted skeletons, and its seen -- children are deleted. -shape :: Monad m => Map -> SExpr Pos -> m (Map, Maybe (SExpr Pos))+shape :: MonadFail m => Map -> SExpr Pos -> m (Map, Maybe (SExpr Pos)) shape map x@(L _ (S _ "defskeleton" : _ : _ : strands)) =     do       label <- nassoc "label" xs@@ -71,7 +77,7 @@       extend x (Just y) = Just (x ++ y)  -- Look up a value known to be an Int-nassoc :: Monad m => String -> [SExpr Pos] -> m (Maybe Int)+nassoc :: MonadFail m => String -> [SExpr Pos] -> m (Maybe Int) nassoc key xs =     case assoc key xs of       Nothing -> return Nothing@@ -82,7 +88,7 @@       Just (x:_) -> fail (shows (annotation x) "Expecting one number")       Just [] -> fail (shows (annotation (head xs)) "Expecting one number") -num :: Monad m => SExpr Pos -> m Int+num :: MonadFail m => SExpr Pos -> m Int num (N _ n) = return n num x = fail (shows (annotation x) "Expecting a number")
tst/aik.scm view
@@ -28,4 +28,3 @@   (vars (i x mf pc name) (ek k akey) (srk skey))   (deflistener (enc "aic" i k x (privk pc)))   (non-orig (privk pc)))-
tst/aik.tst view
@@ -1,6 +1,6 @@ (herald "Anonymous identity protocol from TCG") -(comment "CPSA 3.6.3")+(comment "CPSA 3.6.4") (comment "All input read from aik.scm")  (defprotocol aikprot basic
+ tst/attest.scm view
@@ -0,0 +1,106 @@+(herald attest-door)++(defprotocol attest-door basic+  (defrole appraise+    (vars (d p a akey) (n text))+    (trace+     (recv (enc (enc d n (invk p)) a))+     (send (enc n a p)))+    (comment "The appraiser for the door"))+  (defrole person+    (vars (d p a akey) (k skey) (n t text))+    (trace+     (send (enc (enc d n (invk p)) a))+     (recv (enc n a p))+     (send (enc (enc k (invk p)) d))+     (recv (enc t k))+     (send t))+    (uniq-orig n k)+    (comment "Person requesting door entry"))+  (defrole door+    (vars (d p akey) (k skey) (t text))+    (trace+     (recv (enc (enc k (invk p)) d))+     (send (enc t k))+     (recv t))+    (uniq-orig t))+  (defrole squealer+    (vars (d p akey) (k skey) (t text))+    (trace+     (recv (enc (enc k (invk p)) d))+     (send k))+    (comment "Fake door"))+  (defrule yes+    (forall ((z strd) (a akey))+	    (implies+	     (and (p "appraise" z 2)+		  (p "appraise" "a" z a)+		  (non (invk a)))+	     (exists ((d akey))+		     (and (p "appraise" "d" z d)+			  (non (invk d))))))+    (comment "Appraisal succeeded"))+  (comment "Door attestations protocol"))++(defskeleton attest-door+  (vars (p a akey))+  (defstrand person 5 (p p) (a a))+  (non-orig (invk p) (invk a))+  (comment "Analyze from the person's perspective"))++(defprotocol attest-door-trust basic+  (defrole appraise+    (vars (d p a akey) (n text))+    (trace+     (recv (enc (enc d n (invk p)) a))+     (send (enc n a p)))+    (comment "The appraiser for the door"))+  (defrole person+    (vars (d p a akey) (k skey) (n t text))+    (trace+     (send (enc (enc d n (invk p)) a))+     (recv (enc n a p))+     (send (enc (enc k (invk p)) d))+     (recv (enc t k))+     (send t))+    (uniq-orig n k)+    (comment "Person requesting door entry"))+  (defrole door+    (vars (d p akey) (k skey) (t text))+    (trace+     (recv (enc (enc k (invk p)) d))+     (send (enc t k))+     (recv t))+    (uniq-orig t))+  (defrole squealer+    (vars (d p akey) (k skey) (t text))+    (trace+     (recv (enc (enc k (invk p)) d))+     (send k))+    (comment "Fake door"))+  (defrule yes+    (forall ((z strd) (a akey))+	    (implies+	     (and (p "appraise" z 2)+		  (p "appraise" "a" z a)+		  (non (invk a)))+	     (exists ((d akey))+		     (and (p "appraise" "d" z d)+			  (non (invk d))))))+    (comment "Appraisal succeeded"))+  (defrule trust+    (forall ((z w strd) (d akey))+	    (implies+	     (and (p "appraise" z 2)+		  (p "appraise" "d" z d)+		  (p "squealer" w 2)+		  (p "squealer" "d" w d))+	     (false)))+    (comment "Squealer prohibited due to attestation"))+  (comment "Door attestations protocol with attestation"))++(defskeleton attest-door-trust+  (vars (p a akey))+  (defstrand person 5 (p p) (a a))+  (non-orig (invk p) (invk a))+  (comment "Analyze from the person's perspective"))
+ tst/attest.tst view
@@ -0,0 +1,325 @@+(herald attest-door)++(comment "CPSA 3.6.4")+(comment "All input read from attest.scm")++(defprotocol attest-door basic+  (defrole appraise+    (vars (d p a akey) (n text))+    (trace (recv (enc (enc d n (invk p)) a)) (send (enc n a p)))+    (comment "The appraiser for the door"))+  (defrole person+    (vars (d p a akey) (k skey) (n t text))+    (trace (send (enc (enc d n (invk p)) a)) (recv (enc n a p))+      (send (enc (enc k (invk p)) d)) (recv (enc t k)) (send t))+    (uniq-orig n k)+    (comment "Person requesting door entry"))+  (defrole door+    (vars (d p akey) (k skey) (t text))+    (trace (recv (enc (enc k (invk p)) d)) (send (enc t k)) (recv t))+    (uniq-orig t))+  (defrole squealer+    (vars (d p akey) (k skey))+    (trace (recv (enc (enc k (invk p)) d)) (send k))+    (comment "Fake door"))+  (defrule yes+    (forall ((z strd) (a akey))+      (implies+        (and (p "appraise" z 2) (p "appraise" "a" z a) (non (invk a)))+        (exists ((d akey))+          (and (p "appraise" "d" z d) (non (invk d))))))+    (comment "Appraisal succeeded"))+  (comment "Door attestations protocol"))++(defskeleton attest-door+  (vars (n t text) (k skey) (p a d akey))+  (defstrand person 5 (n n) (t t) (k k) (d d) (p p) (a a))+  (non-orig (invk p) (invk a))+  (uniq-orig n k)+  (comment "Analyze from the person's perspective")+  (traces+    ((send (enc (enc d n (invk p)) a)) (recv (enc n a p))+      (send (enc (enc k (invk p)) d)) (recv (enc t k)) (send t)))+  (label 0)+  (unrealized (0 1))+  (origs (n (0 0)) (k (0 2)))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton attest-door+  (vars (n t text) (k skey) (p a d akey))+  (defstrand person 5 (n n) (t t) (k k) (d d) (p p) (a a))+  (defstrand appraise 2 (n n) (d d) (p p) (a a))+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (invk p) (invk a) (invk d))+  (uniq-orig n k)+  (rule yes)+  (operation nonce-test (added-strand appraise 2) n (0 1)+    (enc (enc d n (invk p)) a))+  (traces+    ((send (enc (enc d n (invk p)) a)) (recv (enc n a p))+      (send (enc (enc k (invk p)) d)) (recv (enc t k)) (send t))+    ((recv (enc (enc d n (invk p)) a)) (send (enc n a p))))+  (label 1)+  (parent 0)+  (unrealized (0 3))+  (comment "2 in cohort - 2 not yet seen"))++(defskeleton attest-door+  (vars (n t text) (k skey) (p a d d-0 p-0 akey))+  (defstrand person 5 (n n) (t t) (k k) (d d) (p p) (a a))+  (defstrand appraise 2 (n n) (d d) (p p) (a a))+  (defstrand door 2 (t t) (k k) (d d-0) (p p-0))+  (precedes ((0 0) (1 0)) ((0 2) (2 0)) ((1 1) (0 1)) ((2 1) (0 3)))+  (non-orig (invk p) (invk a) (invk d))+  (uniq-orig n t k)+  (operation encryption-test (added-strand door 2) (enc t k) (0 3))+  (traces+    ((send (enc (enc d n (invk p)) a)) (recv (enc n a p))+      (send (enc (enc k (invk p)) d)) (recv (enc t k)) (send t))+    ((recv (enc (enc d n (invk p)) a)) (send (enc n a p)))+    ((recv (enc (enc k (invk p-0)) d-0)) (send (enc t k))))+  (label 2)+  (parent 1)+  (unrealized (2 0))+  (comment "2 in cohort - 2 not yet seen"))++(defskeleton attest-door+  (vars (n t text) (k skey) (p a d akey))+  (defstrand person 5 (n n) (t t) (k k) (d d) (p p) (a a))+  (defstrand appraise 2 (n n) (d d) (p p) (a a))+  (deflistener k)+  (precedes ((0 0) (1 0)) ((0 2) (2 0)) ((1 1) (0 1)) ((2 1) (0 3)))+  (non-orig (invk p) (invk a) (invk d))+  (uniq-orig n k)+  (operation encryption-test (added-listener k) (enc t k) (0 3))+  (traces+    ((send (enc (enc d n (invk p)) a)) (recv (enc n a p))+      (send (enc (enc k (invk p)) d)) (recv (enc t k)) (send t))+    ((recv (enc (enc d n (invk p)) a)) (send (enc n a p)))+    ((recv k) (send k)))+  (label 3)+  (parent 1)+  (unrealized (2 0))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton attest-door+  (vars (n t text) (k skey) (p a d akey))+  (defstrand person 5 (n n) (t t) (k k) (d d) (p p) (a a))+  (defstrand appraise 2 (n n) (d d) (p p) (a a))+  (defstrand door 2 (t t) (k k) (d d) (p p))+  (precedes ((0 0) (1 0)) ((0 2) (2 0)) ((1 1) (0 1)) ((2 1) (0 3)))+  (non-orig (invk p) (invk a) (invk d))+  (uniq-orig n t k)+  (operation nonce-test (contracted (d-0 d) (p-0 p)) k (2 0)+    (enc (enc k (invk p)) d))+  (traces+    ((send (enc (enc d n (invk p)) a)) (recv (enc n a p))+      (send (enc (enc k (invk p)) d)) (recv (enc t k)) (send t))+    ((recv (enc (enc d n (invk p)) a)) (send (enc n a p)))+    ((recv (enc (enc k (invk p)) d)) (send (enc t k))))+  (label 4)+  (parent 2)+  (unrealized)+  (shape)+  (maps ((0) ((p p) (a a) (d d) (k k) (n n) (t t))))+  (origs (t (2 1)) (n (0 0)) (k (0 2))))++(defskeleton attest-door+  (vars (n t text) (k skey) (p a d d-0 p-0 akey))+  (defstrand person 5 (n n) (t t) (k k) (d d) (p p) (a a))+  (defstrand appraise 2 (n n) (d d) (p p) (a a))+  (defstrand door 2 (t t) (k k) (d d-0) (p p-0))+  (defstrand squealer 2 (k k) (d d) (p p))+  (precedes ((0 0) (1 0)) ((0 2) (3 0)) ((1 1) (0 1)) ((2 1) (0 3))+    ((3 1) (2 0)))+  (non-orig (invk p) (invk a) (invk d))+  (uniq-orig n t k)+  (operation nonce-test (added-strand squealer 2) k (2 0)+    (enc (enc k (invk p)) d))+  (traces+    ((send (enc (enc d n (invk p)) a)) (recv (enc n a p))+      (send (enc (enc k (invk p)) d)) (recv (enc t k)) (send t))+    ((recv (enc (enc d n (invk p)) a)) (send (enc n a p)))+    ((recv (enc (enc k (invk p-0)) d-0)) (send (enc t k)))+    ((recv (enc (enc k (invk p)) d)) (send k)))+  (label 5)+  (parent 2)+  (unrealized)+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton attest-door+  (vars (n t text) (k skey) (p a d akey))+  (defstrand person 5 (n n) (t t) (k k) (d d) (p p) (a a))+  (defstrand appraise 2 (n n) (d d) (p p) (a a))+  (deflistener k)+  (defstrand squealer 2 (k k) (d d) (p p))+  (precedes ((0 0) (1 0)) ((0 2) (3 0)) ((1 1) (0 1)) ((2 1) (0 3))+    ((3 1) (2 0)))+  (non-orig (invk p) (invk a) (invk d))+  (uniq-orig n k)+  (operation nonce-test (added-strand squealer 2) k (2 0)+    (enc (enc k (invk p)) d))+  (traces+    ((send (enc (enc d n (invk p)) a)) (recv (enc n a p))+      (send (enc (enc k (invk p)) d)) (recv (enc t k)) (send t))+    ((recv (enc (enc d n (invk p)) a)) (send (enc n a p)))+    ((recv k) (send k)) ((recv (enc (enc k (invk p)) d)) (send k)))+  (label 6)+  (parent 3)+  (seen 7)+  (unrealized)+  (comment "1 in cohort - 0 not yet seen"))++(defskeleton attest-door+  (vars (n t text) (k skey) (p a d akey))+  (defstrand person 5 (n n) (t t) (k k) (d d) (p p) (a a))+  (defstrand appraise 2 (n n) (d d) (p p) (a a))+  (defstrand squealer 2 (k k) (d d) (p p))+  (precedes ((0 0) (1 0)) ((0 2) (2 0)) ((1 1) (0 1)) ((2 1) (0 3)))+  (non-orig (invk p) (invk a) (invk d))+  (uniq-orig n k)+  (operation generalization deleted (2 0))+  (traces+    ((send (enc (enc d n (invk p)) a)) (recv (enc n a p))+      (send (enc (enc k (invk p)) d)) (recv (enc t k)) (send t))+    ((recv (enc (enc d n (invk p)) a)) (send (enc n a p)))+    ((recv (enc (enc k (invk p)) d)) (send k)))+  (label 7)+  (parent 5)+  (unrealized)+  (shape)+  (maps ((0) ((p p) (a a) (d d) (k k) (n n) (t t))))+  (origs (n (0 0)) (k (0 2))))++(comment "Nothing left to do")++(defprotocol attest-door-trust basic+  (defrole appraise+    (vars (d p a akey) (n text))+    (trace (recv (enc (enc d n (invk p)) a)) (send (enc n a p)))+    (comment "The appraiser for the door"))+  (defrole person+    (vars (d p a akey) (k skey) (n t text))+    (trace (send (enc (enc d n (invk p)) a)) (recv (enc n a p))+      (send (enc (enc k (invk p)) d)) (recv (enc t k)) (send t))+    (uniq-orig n k)+    (comment "Person requesting door entry"))+  (defrole door+    (vars (d p akey) (k skey) (t text))+    (trace (recv (enc (enc k (invk p)) d)) (send (enc t k)) (recv t))+    (uniq-orig t))+  (defrole squealer+    (vars (d p akey) (k skey))+    (trace (recv (enc (enc k (invk p)) d)) (send k))+    (comment "Fake door"))+  (defrule yes+    (forall ((z strd) (a akey))+      (implies+        (and (p "appraise" z 2) (p "appraise" "a" z a) (non (invk a)))+        (exists ((d akey))+          (and (p "appraise" "d" z d) (non (invk d))))))+    (comment "Appraisal succeeded"))+  (defrule trust+    (forall ((z w strd) (d akey))+      (implies+        (and (p "appraise" z 2) (p "appraise" "d" z d)+          (p "squealer" w 2) (p "squealer" "d" w d))+        (false)))+    (comment "Squealer prohibited due to attestation"))+  (comment "Door attestations protocol with attestation"))++(defskeleton attest-door-trust+  (vars (n t text) (k skey) (p a d akey))+  (defstrand person 5 (n n) (t t) (k k) (d d) (p p) (a a))+  (non-orig (invk p) (invk a))+  (uniq-orig n k)+  (comment "Analyze from the person's perspective")+  (traces+    ((send (enc (enc d n (invk p)) a)) (recv (enc n a p))+      (send (enc (enc k (invk p)) d)) (recv (enc t k)) (send t)))+  (label 8)+  (unrealized (0 1))+  (origs (n (0 0)) (k (0 2)))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton attest-door-trust+  (vars (n t text) (k skey) (p a d akey))+  (defstrand person 5 (n n) (t t) (k k) (d d) (p p) (a a))+  (defstrand appraise 2 (n n) (d d) (p p) (a a))+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (invk p) (invk a) (invk d))+  (uniq-orig n k)+  (rule yes)+  (operation nonce-test (added-strand appraise 2) n (0 1)+    (enc (enc d n (invk p)) a))+  (traces+    ((send (enc (enc d n (invk p)) a)) (recv (enc n a p))+      (send (enc (enc k (invk p)) d)) (recv (enc t k)) (send t))+    ((recv (enc (enc d n (invk p)) a)) (send (enc n a p))))+  (label 9)+  (parent 8)+  (unrealized (0 3))+  (comment "2 in cohort - 2 not yet seen"))++(defskeleton attest-door-trust+  (vars (n t text) (k skey) (p a d d-0 p-0 akey))+  (defstrand person 5 (n n) (t t) (k k) (d d) (p p) (a a))+  (defstrand appraise 2 (n n) (d d) (p p) (a a))+  (defstrand door 2 (t t) (k k) (d d-0) (p p-0))+  (precedes ((0 0) (1 0)) ((0 2) (2 0)) ((1 1) (0 1)) ((2 1) (0 3)))+  (non-orig (invk p) (invk a) (invk d))+  (uniq-orig n t k)+  (operation encryption-test (added-strand door 2) (enc t k) (0 3))+  (traces+    ((send (enc (enc d n (invk p)) a)) (recv (enc n a p))+      (send (enc (enc k (invk p)) d)) (recv (enc t k)) (send t))+    ((recv (enc (enc d n (invk p)) a)) (send (enc n a p)))+    ((recv (enc (enc k (invk p-0)) d-0)) (send (enc t k))))+  (label 10)+  (parent 9)+  (unrealized (2 0))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton attest-door-trust+  (vars (n t text) (k skey) (p a d akey))+  (defstrand person 5 (n n) (t t) (k k) (d d) (p p) (a a))+  (defstrand appraise 2 (n n) (d d) (p p) (a a))+  (deflistener k)+  (precedes ((0 0) (1 0)) ((0 2) (2 0)) ((1 1) (0 1)) ((2 1) (0 3)))+  (non-orig (invk p) (invk a) (invk d))+  (uniq-orig n k)+  (operation encryption-test (added-listener k) (enc t k) (0 3))+  (traces+    ((send (enc (enc d n (invk p)) a)) (recv (enc n a p))+      (send (enc (enc k (invk p)) d)) (recv (enc t k)) (send t))+    ((recv (enc (enc d n (invk p)) a)) (send (enc n a p)))+    ((recv k) (send k)))+  (label 11)+  (parent 9)+  (unrealized (2 0))+  (dead)+  (comment "empty cohort"))++(defskeleton attest-door-trust+  (vars (n t text) (k skey) (p a d akey))+  (defstrand person 5 (n n) (t t) (k k) (d d) (p p) (a a))+  (defstrand appraise 2 (n n) (d d) (p p) (a a))+  (defstrand door 2 (t t) (k k) (d d) (p p))+  (precedes ((0 0) (1 0)) ((0 2) (2 0)) ((1 1) (0 1)) ((2 1) (0 3)))+  (non-orig (invk p) (invk a) (invk d))+  (uniq-orig n t k)+  (operation nonce-test (contracted (d-0 d) (p-0 p)) k (2 0)+    (enc (enc k (invk p)) d))+  (traces+    ((send (enc (enc d n (invk p)) a)) (recv (enc n a p))+      (send (enc (enc k (invk p)) d)) (recv (enc t k)) (send t))+    ((recv (enc (enc d n (invk p)) a)) (send (enc n a p)))+    ((recv (enc (enc k (invk p)) d)) (send (enc t k))))+  (label 12)+  (parent 10)+  (unrealized)+  (shape)+  (maps ((0) ((p p) (a a) (d d) (k k) (n n) (t t))))+  (origs (t (2 1)) (n (0 0)) (k (0 2))))++(comment "Nothing left to do")
tst/axiom2.tst view
@@ -1,6 +1,6 @@ (herald "Axiom 2 Protocol" (bound 20)) -(comment "CPSA 3.6.3")+(comment "CPSA 3.6.4") (comment "All input read from axiom2.scm") (comment "Strand count bounded at 20")
tst/blanchet.tst view
@@ -1,7 +1,7 @@ (herald "Blanchet's Simple Example Protocol"   (comment "There is a flaw in this protocol by design")) -(comment "CPSA 3.6.3")+(comment "CPSA 3.6.4") (comment "All input read from blanchet.scm")  (defprotocol blanchet basic
tst/bltk_test.scm view
@@ -71,5 +71,3 @@   (vars (a b name))   (defstrand recvr 2 (a a) (b b))   (non-orig (bltk a b)))--
tst/bltk_test.tst view
@@ -1,6 +1,6 @@ (herald "bltk Test File" (algebra diffie-hellman) (bound 12)) -(comment "CPSA 3.6.3")+(comment "CPSA 3.6.4") (comment "All input read from bltk_test.scm")  (defprotocol test diffie-hellman
+ tst/comp_test.scm view
@@ -0,0 +1,156 @@+(herald "Main Example")++(defprotocol main-ex-src basic+  (defrole qn+    (vars (a b c akey) (i ssn text) (k skey))+    (trace+     (send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))+     (recv (enc "sorry" a b k)))+    (uniq-orig k))+  (defrole qy+    (vars (a b c akey) (i ssn d text) (k skey))+    (trace+     (send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))+     (recv (enc "data" d k)))+    (uniq-orig k))+  (defrole an+    (vars (a b c akey) (i text) (k skey) (x mesg))+    (trace+     (recv (cat i a (enc (enc k b c i (invk a)) b) x))+     (send (enc "sorry" a b k))))+  (defrole ay+    (vars (a b c akey) (i d text) (k skey) (x mesg))+    (trace+     (recv (cat i a (enc (enc k b c i (invk a)) b) x))+     (send (enc "data" d k)))+    (uniq-orig d)))++(defprotocol main-ex-tgt basic+  (defrole qn+    (vars (a b c akey) (i ssn text) (k skey))+    (trace+     (send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))+     (recv (enc "sorry" a b k)))+    (uniq-orig k))+  (defrole qy+    (vars (a b c akey) (i ssn d text) (k skey))+    (trace+     (send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))+     (recv (enc "data" d k)))+    (uniq-orig k))+  (defrole an+    (vars (a b c akey) (i y n text) (k skey) (x mesg))+    (trace+     (recv (cat i a (enc (enc k b c i (invk a)) b) x))+     (send (enc y n i a x c))+     (recv n)+     (send (enc "sorry" a b k)))+    (uniq-orig y n))+  (defrole ay+    (vars (a b c akey) (i y n d text) (k skey) (x mesg))+    (trace+     (recv (cat i a (enc (enc k b c i (invk a)) b) x))+     (send (enc y n i a x c))+     (recv y)+     (send (enc "data" d k)))+    (uniq-orig d y n))+  (defrole sn+    (vars (a b c akey) (i ssn y n text))+    (trace+     (recv (enc y n i a (enc a b i ssn c) c))+     (send n)))+  (defrole sy+    (vars (a b c akey) (i ssn y n text))+    (trace+     (recv (enc y n i a (enc a b i ssn c) c))+     (send y))))++(defprotocol main-ex-tgt-rule basic+  (defrole qn+    (vars (a b c akey) (i ssn text) (k skey))+    (trace+     (send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))+     (recv (enc "sorry" a b k)))+    (uniq-orig k))+  (defrole qy+    (vars (a b c akey) (i ssn d text) (k skey))+    (trace+     (send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))+     (recv (enc "data" d k)))+    (uniq-orig k))+  (defrole an+    (vars (a b c akey) (i y n text) (k skey) (x mesg))+    (trace+     (recv (cat i a (enc (enc k b c i (invk a)) b) x))+     (send (enc y n i a x c))+     (recv n)+     (send (enc "sorry" a b k)))+    (uniq-orig y n))+  (defrole ay+    (vars (a b c akey) (i y n d text) (k skey) (x mesg))+    (trace+     (recv (cat i a (enc (enc k b c i (invk a)) b) x))+     (send (enc y n i a x c))+     (recv y)+     (send (enc "data" d k)))+    (uniq-orig d y n))+  (defrole sn+    (vars (a b c akey) (i ssn y n text))+    (trace+     (recv (enc y n i a (enc a b i ssn c) c))+     (send n)))+  (defrole sy+    (vars (a b c akey) (i ssn y n text))+    (trace+     (recv (enc y n i a (enc a b i ssn c) c))+     (send y)))+  (defrule src+    (forall ((z strd) (i ssn text) (k skey) (a b c akey))+	    (implies+	     (and (p "qn" z 2) (p "qn" "i" z i) (p "qn" "ssn" z ssn)+		  (p "qn" "k" z k) (p "qn" "a" z a) (p "qn" "b" z b)+		  (p "qn" "c" z c) (non (invk a)) (non (invk b)) (non (invk c))+		  (uniq k))+	     (exists ((z-0 strd) (x mesg))+		     (and (p "an" z-0 4) (p "an" "x" z-0 x)+			  (p "an" "i" z-0 i) (p "an" "k" z-0 k)+			  (p "an" "a" z-0 a) (p "an" "b" z-0 b)+			  (p "an" "c" z-0 c) (prec z 0 z-0 0)+			  (prec z-0 3 z 1)))))))++(defskeleton main-ex-src+  (vars (a b c akey))+  (defstrand qn 2 (a a) (b b) (c c))+  (non-orig (invk a) (invk b) (invk c))+  (comment+   (defgoal main-ex-src+     (forall ((i ssn text) (k skey) (a b c akey) (z strd))+	     (implies+	      (and (p "qn" z 2) (p "qn" "i" z i) (p "qn" "ssn" z ssn)+		   (p "qn" "k" z k) (p "qn" "a" z a) (p "qn" "b" z b)+		   (p "qn" "c" z c) (non (invk a)) (non (invk b)) (non (invk c))+		   (uniq-at k z 0))+	      (exists ((x mesg) (z-0 strd))+		      (and (p "an" z-0 2) (p "an" "x" z-0 x) (p "an" "i" z-0 i)+			   (p "an" "k" z-0 k) (p "an" "a" z-0 a) (p "an" "b" z-0 b)+			   (p "an" "c" z-0 c) (prec z 0 z-0 0) (prec z-0 1 z 1))))))))++(defskeleton main-ex-src+  (vars (a b c akey))+  (defstrand qy 2 (a a) (b b) (c c))+  (non-orig (invk a) (invk b) (invk c)))++(defskeleton main-ex-tgt+  (vars (a b c akey))+  (defstrand qn 2 (a a) (b b) (c c))+  (non-orig (invk a) (invk b) (invk c)))++(defskeleton main-ex-tgt+  (vars (a b c akey))+  (defstrand qy 2 (a a) (b b) (c c))+  (non-orig (invk a) (invk b) (invk c)))++(defskeleton main-ex-tgt-rule+  (vars (a b c akey))+  (defstrand qn 2 (a a) (b b) (c c))+  (non-orig (invk a) (invk b) (invk c)))
+ tst/comp_test.tst view
@@ -0,0 +1,604 @@+(herald "Main Example")++(comment "CPSA 3.6.4")+(comment "All input read from comp_test.scm")++(defprotocol main-ex-src basic+  (defrole qn+    (vars (a b c akey) (i ssn text) (k skey))+    (trace+      (send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))+      (recv (enc "sorry" a b k)))+    (uniq-orig k))+  (defrole qy+    (vars (a b c akey) (i ssn d text) (k skey))+    (trace+      (send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))+      (recv (enc "data" d k)))+    (uniq-orig k))+  (defrole an+    (vars (a b c akey) (i text) (k skey) (x mesg))+    (trace (recv (cat i a (enc (enc k b c i (invk a)) b) x))+      (send (enc "sorry" a b k))))+  (defrole ay+    (vars (a b c akey) (i d text) (k skey) (x mesg))+    (trace (recv (cat i a (enc (enc k b c i (invk a)) b) x))+      (send (enc "data" d k)))+    (uniq-orig d)))++(defskeleton main-ex-src+  (vars (i ssn text) (k skey) (a b c akey))+  (defstrand qn 2 (i i) (ssn ssn) (k k) (a a) (b b) (c c))+  (non-orig (invk a) (invk b) (invk c))+  (uniq-orig k)+  (comment+    (defgoal main-ex-src+      (forall ((i ssn text) (k skey) (a b c akey) (z strd))+        (implies+          (and (p "qn" z 2) (p "qn" "i" z i) (p "qn" "ssn" z ssn)+            (p "qn" "k" z k) (p "qn" "a" z a) (p "qn" "b" z b)+            (p "qn" "c" z c) (non (invk a)) (non (invk b))+            (non (invk c)) (uniq-at k z 0))+          (exists ((x mesg) (z-0 strd))+            (and (p "an" z-0 2) (p "an" "x" z-0 x) (p "an" "i" z-0 i)+              (p "an" "k" z-0 k) (p "an" "a" z-0 a) (p "an" "b" z-0 b)+              (p "an" "c" z-0 c) (prec z 0 z-0 0) (prec z-0 1 z 1)))))))+  (traces+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))+      (recv (enc "sorry" a b k))))+  (label 0)+  (unrealized (0 1))+  (origs (k (0 0)))+  (comment "2 in cohort - 2 not yet seen"))++(defskeleton main-ex-src+  (vars (x mesg) (i ssn i-0 text) (k skey) (a b c c-0 akey))+  (defstrand qn 2 (i i) (ssn ssn) (k k) (a a) (b b) (c c))+  (defstrand an 2 (x x) (i i-0) (k k) (a a) (b b) (c c-0))+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (invk a) (invk b) (invk c))+  (uniq-orig k)+  (operation encryption-test (added-strand an 2) (enc "sorry" a b k)+    (0 1))+  (traces+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))+      (recv (enc "sorry" a b k)))+    ((recv (cat i-0 a (enc (enc k b c-0 i-0 (invk a)) b) x))+      (send (enc "sorry" a b k))))+  (label 1)+  (parent 0)+  (unrealized (1 0))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton main-ex-src+  (vars (i ssn text) (k skey) (a b c akey))+  (defstrand qn 2 (i i) (ssn ssn) (k k) (a a) (b b) (c c))+  (deflistener k)+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (invk a) (invk b) (invk c))+  (uniq-orig k)+  (operation encryption-test (added-listener k) (enc "sorry" a b k)+    (0 1))+  (traces+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))+      (recv (enc "sorry" a b k))) ((recv k) (send k)))+  (label 2)+  (parent 0)+  (unrealized (1 0))+  (dead)+  (comment "empty cohort"))++(defskeleton main-ex-src+  (vars (x mesg) (i ssn text) (k skey) (a b c akey))+  (defstrand qn 2 (i i) (ssn ssn) (k k) (a a) (b b) (c c))+  (defstrand an 2 (x x) (i i) (k k) (a a) (b b) (c c))+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (invk a) (invk b) (invk c))+  (uniq-orig k)+  (operation encryption-test (displaced 2 0 qy 1)+    (enc k b c-0 i-0 (invk a)) (1 0))+  (traces+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))+      (recv (enc "sorry" a b k)))+    ((recv (cat i a (enc (enc k b c i (invk a)) b) x))+      (send (enc "sorry" a b k))))+  (label 3)+  (parent 1)+  (unrealized)+  (shape)+  (maps ((0) ((a a) (b b) (c c) (i i) (ssn ssn) (k k))))+  (origs (k (0 0))))++(comment "Nothing left to do")++(defprotocol main-ex-src basic+  (defrole qn+    (vars (a b c akey) (i ssn text) (k skey))+    (trace+      (send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))+      (recv (enc "sorry" a b k)))+    (uniq-orig k))+  (defrole qy+    (vars (a b c akey) (i ssn d text) (k skey))+    (trace+      (send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))+      (recv (enc "data" d k)))+    (uniq-orig k))+  (defrole an+    (vars (a b c akey) (i text) (k skey) (x mesg))+    (trace (recv (cat i a (enc (enc k b c i (invk a)) b) x))+      (send (enc "sorry" a b k))))+  (defrole ay+    (vars (a b c akey) (i d text) (k skey) (x mesg))+    (trace (recv (cat i a (enc (enc k b c i (invk a)) b) x))+      (send (enc "data" d k)))+    (uniq-orig d)))++(defskeleton main-ex-src+  (vars (i ssn d text) (k skey) (a b c akey))+  (defstrand qy 2 (i i) (ssn ssn) (d d) (k k) (a a) (b b) (c c))+  (non-orig (invk a) (invk b) (invk c))+  (uniq-orig k)+  (traces+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))+      (recv (enc "data" d k))))+  (label 4)+  (unrealized (0 1))+  (origs (k (0 0)))+  (comment "2 in cohort - 2 not yet seen"))++(defskeleton main-ex-src+  (vars (x mesg) (i ssn d i-0 text) (k skey) (a b c a-0 b-0 c-0 akey))+  (defstrand qy 2 (i i) (ssn ssn) (d d) (k k) (a a) (b b) (c c))+  (defstrand ay 2 (x x) (i i-0) (d d) (k k) (a a-0) (b b-0) (c c-0))+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (invk a) (invk b) (invk c))+  (uniq-orig d k)+  (operation encryption-test (added-strand ay 2) (enc "data" d k) (0 1))+  (traces+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))+      (recv (enc "data" d k)))+    ((recv (cat i-0 a-0 (enc (enc k b-0 c-0 i-0 (invk a-0)) b-0) x))+      (send (enc "data" d k))))+  (label 5)+  (parent 4)+  (unrealized (1 0))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton main-ex-src+  (vars (i ssn d text) (k skey) (a b c akey))+  (defstrand qy 2 (i i) (ssn ssn) (d d) (k k) (a a) (b b) (c c))+  (deflistener k)+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (invk a) (invk b) (invk c))+  (uniq-orig k)+  (operation encryption-test (added-listener k) (enc "data" d k) (0 1))+  (traces+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))+      (recv (enc "data" d k))) ((recv k) (send k)))+  (label 6)+  (parent 4)+  (unrealized (1 0))+  (dead)+  (comment "empty cohort"))++(defskeleton main-ex-src+  (vars (x mesg) (i ssn d text) (k skey) (a b c akey))+  (defstrand qy 2 (i i) (ssn ssn) (d d) (k k) (a a) (b b) (c c))+  (defstrand ay 2 (x x) (i i) (d d) (k k) (a a) (b b) (c c))+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (invk a) (invk b) (invk c))+  (uniq-orig d k)+  (operation nonce-test (contracted (a-0 a) (b-0 b) (c-0 c) (i-0 i)) k+    (1 0) (enc (enc k b c i (invk a)) b))+  (traces+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))+      (recv (enc "data" d k)))+    ((recv (cat i a (enc (enc k b c i (invk a)) b) x))+      (send (enc "data" d k))))+  (label 7)+  (parent 5)+  (unrealized)+  (shape)+  (maps ((0) ((a a) (b b) (c c) (i i) (ssn ssn) (d d) (k k))))+  (origs (d (1 1)) (k (0 0))))++(comment "Nothing left to do")++(defprotocol main-ex-tgt basic+  (defrole qn+    (vars (a b c akey) (i ssn text) (k skey))+    (trace+      (send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))+      (recv (enc "sorry" a b k)))+    (uniq-orig k))+  (defrole qy+    (vars (a b c akey) (i ssn d text) (k skey))+    (trace+      (send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))+      (recv (enc "data" d k)))+    (uniq-orig k))+  (defrole an+    (vars (a b c akey) (i y n text) (k skey) (x mesg))+    (trace (recv (cat i a (enc (enc k b c i (invk a)) b) x))+      (send (enc y n i a x c)) (recv n) (send (enc "sorry" a b k)))+    (uniq-orig y n))+  (defrole ay+    (vars (a b c akey) (i y n d text) (k skey) (x mesg))+    (trace (recv (cat i a (enc (enc k b c i (invk a)) b) x))+      (send (enc y n i a x c)) (recv y) (send (enc "data" d k)))+    (uniq-orig y n d))+  (defrole sn+    (vars (a b c akey) (i ssn y n text))+    (trace (recv (enc y n i a (enc a b i ssn c) c)) (send n)))+  (defrole sy+    (vars (a b c akey) (i ssn y n text))+    (trace (recv (enc y n i a (enc a b i ssn c) c)) (send y))))++(defskeleton main-ex-tgt+  (vars (i ssn text) (k skey) (a b c akey))+  (defstrand qn 2 (i i) (ssn ssn) (k k) (a a) (b b) (c c))+  (non-orig (invk a) (invk b) (invk c))+  (uniq-orig k)+  (traces+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))+      (recv (enc "sorry" a b k))))+  (label 8)+  (unrealized (0 1))+  (origs (k (0 0)))+  (comment "2 in cohort - 2 not yet seen"))++(defskeleton main-ex-tgt+  (vars (x mesg) (i ssn i-0 y n text) (k skey) (a b c c-0 akey))+  (defstrand qn 2 (i i) (ssn ssn) (k k) (a a) (b b) (c c))+  (defstrand an 4 (x x) (i i-0) (y y) (n n) (k k) (a a) (b b) (c c-0))+  (precedes ((0 0) (1 0)) ((1 3) (0 1)))+  (non-orig (invk a) (invk b) (invk c))+  (uniq-orig y n k)+  (operation encryption-test (added-strand an 4) (enc "sorry" a b k)+    (0 1))+  (traces+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))+      (recv (enc "sorry" a b k)))+    ((recv (cat i-0 a (enc (enc k b c-0 i-0 (invk a)) b) x))+      (send (enc y n i-0 a x c-0)) (recv n) (send (enc "sorry" a b k))))+  (label 9)+  (parent 8)+  (unrealized (1 0))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton main-ex-tgt+  (vars (i ssn text) (k skey) (a b c akey))+  (defstrand qn 2 (i i) (ssn ssn) (k k) (a a) (b b) (c c))+  (deflistener k)+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (invk a) (invk b) (invk c))+  (uniq-orig k)+  (operation encryption-test (added-listener k) (enc "sorry" a b k)+    (0 1))+  (traces+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))+      (recv (enc "sorry" a b k))) ((recv k) (send k)))+  (label 10)+  (parent 8)+  (unrealized (1 0))+  (dead)+  (comment "empty cohort"))++(defskeleton main-ex-tgt+  (vars (x mesg) (i ssn y n text) (k skey) (a b c akey))+  (defstrand qn 2 (i i) (ssn ssn) (k k) (a a) (b b) (c c))+  (defstrand an 4 (x x) (i i) (y y) (n n) (k k) (a a) (b b) (c c))+  (precedes ((0 0) (1 0)) ((1 3) (0 1)))+  (non-orig (invk a) (invk b) (invk c))+  (uniq-orig y n k)+  (operation encryption-test (displaced 2 0 qy 1)+    (enc k b c-0 i-0 (invk a)) (1 0))+  (traces+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))+      (recv (enc "sorry" a b k)))+    ((recv (cat i a (enc (enc k b c i (invk a)) b) x))+      (send (enc y n i a x c)) (recv n) (send (enc "sorry" a b k))))+  (label 11)+  (parent 9)+  (unrealized (1 2))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton main-ex-tgt+  (vars (i ssn y n ssn-0 text) (k skey) (a b c b-0 akey))+  (defstrand qn 2 (i i) (ssn ssn) (k k) (a a) (b b) (c c))+  (defstrand an 4 (x (enc a b-0 i ssn-0 c)) (i i) (y y) (n n) (k k)+    (a a) (b b) (c c))+  (defstrand sn 2 (i i) (ssn ssn-0) (y y) (n n) (a a) (b b-0) (c c))+  (precedes ((0 0) (1 0)) ((1 1) (2 0)) ((1 3) (0 1)) ((2 1) (1 2)))+  (non-orig (invk a) (invk b) (invk c))+  (uniq-orig y n k)+  (operation nonce-test (added-strand sn 2) n (1 2)+    (enc y n i a (enc a b-0 i ssn-0 c) c))+  (traces+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))+      (recv (enc "sorry" a b k)))+    ((recv+       (cat i a (enc (enc k b c i (invk a)) b) (enc a b-0 i ssn-0 c)))+      (send (enc y n i a (enc a b-0 i ssn-0 c) c)) (recv n)+      (send (enc "sorry" a b k)))+    ((recv (enc y n i a (enc a b-0 i ssn-0 c) c)) (send n)))+  (label 12)+  (parent 11)+  (unrealized)+  (shape)+  (maps ((0) ((a a) (b b) (c c) (i i) (ssn ssn) (k k))))+  (origs (k (0 0)) (y (1 1)) (n (1 1))))++(comment "Nothing left to do")++(defprotocol main-ex-tgt basic+  (defrole qn+    (vars (a b c akey) (i ssn text) (k skey))+    (trace+      (send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))+      (recv (enc "sorry" a b k)))+    (uniq-orig k))+  (defrole qy+    (vars (a b c akey) (i ssn d text) (k skey))+    (trace+      (send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))+      (recv (enc "data" d k)))+    (uniq-orig k))+  (defrole an+    (vars (a b c akey) (i y n text) (k skey) (x mesg))+    (trace (recv (cat i a (enc (enc k b c i (invk a)) b) x))+      (send (enc y n i a x c)) (recv n) (send (enc "sorry" a b k)))+    (uniq-orig y n))+  (defrole ay+    (vars (a b c akey) (i y n d text) (k skey) (x mesg))+    (trace (recv (cat i a (enc (enc k b c i (invk a)) b) x))+      (send (enc y n i a x c)) (recv y) (send (enc "data" d k)))+    (uniq-orig y n d))+  (defrole sn+    (vars (a b c akey) (i ssn y n text))+    (trace (recv (enc y n i a (enc a b i ssn c) c)) (send n)))+  (defrole sy+    (vars (a b c akey) (i ssn y n text))+    (trace (recv (enc y n i a (enc a b i ssn c) c)) (send y))))++(defskeleton main-ex-tgt+  (vars (i ssn d text) (k skey) (a b c akey))+  (defstrand qy 2 (i i) (ssn ssn) (d d) (k k) (a a) (b b) (c c))+  (non-orig (invk a) (invk b) (invk c))+  (uniq-orig k)+  (traces+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))+      (recv (enc "data" d k))))+  (label 13)+  (unrealized (0 1))+  (origs (k (0 0)))+  (comment "2 in cohort - 2 not yet seen"))++(defskeleton main-ex-tgt+  (vars (x mesg) (i ssn d i-0 y n text) (k skey)+    (a b c a-0 b-0 c-0 akey))+  (defstrand qy 2 (i i) (ssn ssn) (d d) (k k) (a a) (b b) (c c))+  (defstrand ay 4 (x x) (i i-0) (y y) (n n) (d d) (k k) (a a-0) (b b-0)+    (c c-0))+  (precedes ((0 0) (1 0)) ((1 3) (0 1)))+  (non-orig (invk a) (invk b) (invk c))+  (uniq-orig d y n k)+  (operation encryption-test (added-strand ay 4) (enc "data" d k) (0 1))+  (traces+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))+      (recv (enc "data" d k)))+    ((recv (cat i-0 a-0 (enc (enc k b-0 c-0 i-0 (invk a-0)) b-0) x))+      (send (enc y n i-0 a-0 x c-0)) (recv y) (send (enc "data" d k))))+  (label 14)+  (parent 13)+  (unrealized (1 0))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton main-ex-tgt+  (vars (i ssn d text) (k skey) (a b c akey))+  (defstrand qy 2 (i i) (ssn ssn) (d d) (k k) (a a) (b b) (c c))+  (deflistener k)+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (invk a) (invk b) (invk c))+  (uniq-orig k)+  (operation encryption-test (added-listener k) (enc "data" d k) (0 1))+  (traces+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))+      (recv (enc "data" d k))) ((recv k) (send k)))+  (label 15)+  (parent 13)+  (unrealized (1 0))+  (dead)+  (comment "empty cohort"))++(defskeleton main-ex-tgt+  (vars (x mesg) (i ssn d y n text) (k skey) (a b c akey))+  (defstrand qy 2 (i i) (ssn ssn) (d d) (k k) (a a) (b b) (c c))+  (defstrand ay 4 (x x) (i i) (y y) (n n) (d d) (k k) (a a) (b b) (c c))+  (precedes ((0 0) (1 0)) ((1 3) (0 1)))+  (non-orig (invk a) (invk b) (invk c))+  (uniq-orig d y n k)+  (operation nonce-test (contracted (a-0 a) (b-0 b) (c-0 c) (i-0 i)) k+    (1 0) (enc (enc k b c i (invk a)) b))+  (traces+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))+      (recv (enc "data" d k)))+    ((recv (cat i a (enc (enc k b c i (invk a)) b) x))+      (send (enc y n i a x c)) (recv y) (send (enc "data" d k))))+  (label 16)+  (parent 14)+  (unrealized (1 2))+  (comment "2 in cohort - 2 not yet seen"))++(defskeleton main-ex-tgt+  (vars (x mesg) (i ssn d n text) (k skey) (a b c akey))+  (defstrand qy 2 (i i) (ssn ssn) (d d) (k k) (a a) (b b) (c c))+  (defstrand ay 4 (x x) (i i) (y n) (n n) (d d) (k k) (a a) (b b) (c c))+  (precedes ((0 0) (1 0)) ((1 3) (0 1)))+  (non-orig (invk a) (invk b) (invk c))+  (uniq-orig d n k)+  (operation nonce-test (displaced 2 1 ay 2) y (1 2) (enc y n i a x c))+  (traces+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))+      (recv (enc "data" d k)))+    ((recv (cat i a (enc (enc k b c i (invk a)) b) x))+      (send (enc n n i a x c)) (recv n) (send (enc "data" d k))))+  (label 17)+  (parent 16)+  (unrealized (1 2))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton main-ex-tgt+  (vars (i ssn d y n ssn-0 text) (k skey) (a b c b-0 akey))+  (defstrand qy 2 (i i) (ssn ssn) (d d) (k k) (a a) (b b) (c c))+  (defstrand ay 4 (x (enc a b-0 i ssn-0 c)) (i i) (y y) (n n) (d d)+    (k k) (a a) (b b) (c c))+  (defstrand sy 2 (i i) (ssn ssn-0) (y y) (n n) (a a) (b b-0) (c c))+  (precedes ((0 0) (1 0)) ((1 1) (2 0)) ((1 3) (0 1)) ((2 1) (1 2)))+  (non-orig (invk a) (invk b) (invk c))+  (uniq-orig d y n k)+  (operation nonce-test (added-strand sy 2) y (1 2)+    (enc y n i a (enc a b-0 i ssn-0 c) c))+  (traces+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))+      (recv (enc "data" d k)))+    ((recv+       (cat i a (enc (enc k b c i (invk a)) b) (enc a b-0 i ssn-0 c)))+      (send (enc y n i a (enc a b-0 i ssn-0 c) c)) (recv y)+      (send (enc "data" d k)))+    ((recv (enc y n i a (enc a b-0 i ssn-0 c) c)) (send y)))+  (label 18)+  (parent 16)+  (unrealized)+  (shape)+  (maps ((0) ((a a) (b b) (c c) (i i) (ssn ssn) (d d) (k k))))+  (origs (y (1 1)) (n (1 1)) (d (1 3)) (k (0 0))))++(defskeleton main-ex-tgt+  (vars (i ssn d n ssn-0 text) (k skey) (a b c b-0 akey))+  (defstrand qy 2 (i i) (ssn ssn) (d d) (k k) (a a) (b b) (c c))+  (defstrand ay 4 (x (enc a b-0 i ssn-0 c)) (i i) (y n) (n n) (d d)+    (k k) (a a) (b b) (c c))+  (defstrand sy 2 (i i) (ssn ssn-0) (y n) (n n) (a a) (b b-0) (c c))+  (precedes ((0 0) (1 0)) ((1 1) (2 0)) ((1 3) (0 1)) ((2 1) (1 2)))+  (non-orig (invk a) (invk b) (invk c))+  (uniq-orig d n k)+  (operation nonce-test (added-strand sy 2) n (1 2)+    (enc n n i a (enc a b-0 i ssn-0 c) c))+  (traces+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))+      (recv (enc "data" d k)))+    ((recv+       (cat i a (enc (enc k b c i (invk a)) b) (enc a b-0 i ssn-0 c)))+      (send (enc n n i a (enc a b-0 i ssn-0 c) c)) (recv n)+      (send (enc "data" d k)))+    ((recv (enc n n i a (enc a b-0 i ssn-0 c) c)) (send n)))+  (label 19)+  (parent 17)+  (unrealized)+  (shape)+  (maps ((0) ((a a) (b b) (c c) (i i) (ssn ssn) (d d) (k k))))+  (origs (n (1 1)) (d (1 3)) (k (0 0))))++(comment "Nothing left to do")++(defprotocol main-ex-tgt-rule basic+  (defrole qn+    (vars (a b c akey) (i ssn text) (k skey))+    (trace+      (send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))+      (recv (enc "sorry" a b k)))+    (uniq-orig k))+  (defrole qy+    (vars (a b c akey) (i ssn d text) (k skey))+    (trace+      (send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))+      (recv (enc "data" d k)))+    (uniq-orig k))+  (defrole an+    (vars (a b c akey) (i y n text) (k skey) (x mesg))+    (trace (recv (cat i a (enc (enc k b c i (invk a)) b) x))+      (send (enc y n i a x c)) (recv n) (send (enc "sorry" a b k)))+    (uniq-orig y n))+  (defrole ay+    (vars (a b c akey) (i y n d text) (k skey) (x mesg))+    (trace (recv (cat i a (enc (enc k b c i (invk a)) b) x))+      (send (enc y n i a x c)) (recv y) (send (enc "data" d k)))+    (uniq-orig y n d))+  (defrole sn+    (vars (a b c akey) (i ssn y n text))+    (trace (recv (enc y n i a (enc a b i ssn c) c)) (send n)))+  (defrole sy+    (vars (a b c akey) (i ssn y n text))+    (trace (recv (enc y n i a (enc a b i ssn c) c)) (send y)))+  (defrule src+    (forall ((z strd) (i ssn text) (k skey) (a b c akey))+      (implies+        (and (p "qn" z 2) (p "qn" "i" z i) (p "qn" "ssn" z ssn)+          (p "qn" "k" z k) (p "qn" "a" z a) (p "qn" "b" z b)+          (p "qn" "c" z c) (non (invk a)) (non (invk b)) (non (invk c))+          (uniq k))+        (exists ((z-0 strd) (x mesg))+          (and (p "an" z-0 4) (p "an" "x" z-0 x) (p "an" "i" z-0 i)+            (p "an" "k" z-0 k) (p "an" "a" z-0 a) (p "an" "b" z-0 b)+            (p "an" "c" z-0 c) (prec z 0 z-0 0) (prec z-0 3 z 1)))))))++(defskeleton main-ex-tgt-rule+  (vars (i ssn text) (k skey) (a b c akey))+  (defstrand qn 2 (i i) (ssn ssn) (k k) (a a) (b b) (c c))+  (non-orig (invk a) (invk b) (invk c))+  (uniq-orig k)+  (traces+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))+      (recv (enc "sorry" a b k))))+  (label 20)+  (unrealized (0 1))+  (origs (k (0 0)))+  (comment "Not closed under rules"))++(defskeleton main-ex-tgt-rule+  (vars (x mesg) (ssn i y n text) (k skey) (a b c akey))+  (defstrand qn 2 (i i) (ssn ssn) (k k) (a a) (b b) (c c))+  (defstrand an 4 (x x) (i i) (y y) (n n) (k k) (a a) (b b) (c c))+  (precedes ((0 0) (1 0)) ((1 3) (0 1)))+  (non-orig (invk a) (invk b) (invk c))+  (uniq-orig y n k)+  (rule src)+  (traces+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))+      (recv (enc "sorry" a b k)))+    ((recv (cat i a (enc (enc k b c i (invk a)) b) x))+      (send (enc y n i a x c)) (recv n) (send (enc "sorry" a b k))))+  (label 21)+  (parent 20)+  (unrealized (1 2))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton main-ex-tgt-rule+  (vars (ssn i y n ssn-0 text) (k skey) (a b c b-0 akey))+  (defstrand qn 2 (i i) (ssn ssn) (k k) (a a) (b b) (c c))+  (defstrand an 4 (x (enc a b-0 i ssn-0 c)) (i i) (y y) (n n) (k k)+    (a a) (b b) (c c))+  (defstrand sn 2 (i i) (ssn ssn-0) (y y) (n n) (a a) (b b-0) (c c))+  (precedes ((0 0) (1 0)) ((1 1) (2 0)) ((1 3) (0 1)) ((2 1) (1 2)))+  (non-orig (invk a) (invk b) (invk c))+  (uniq-orig y n k)+  (operation nonce-test (added-strand sn 2) n (1 2)+    (enc y n i a (enc a b-0 i ssn-0 c) c))+  (traces+    ((send (cat i a (enc (enc k b c i (invk a)) b) (enc a b i ssn c)))+      (recv (enc "sorry" a b k)))+    ((recv+       (cat i a (enc (enc k b c i (invk a)) b) (enc a b-0 i ssn-0 c)))+      (send (enc y n i a (enc a b-0 i ssn-0 c) c)) (recv n)+      (send (enc "sorry" a b k)))+    ((recv (enc y n i a (enc a b-0 i ssn-0 c) c)) (send n)))+  (label 22)+  (parent 21)+  (unrealized)+  (shape)+  (maps ((0) ((a a) (b b) (c c) (i i) (ssn ssn) (k k))))+  (origs (y (1 1)) (n (1 1)) (k (0 0))))++(comment "Nothing left to do")
tst/dh-ca.tst view
@@ -1,6 +1,6 @@ (herald dhca (algebra diffie-hellman)) -(comment "CPSA 3.6.3")+(comment "CPSA 3.6.4") (comment "All input read from dh-ca.scm")  (defprotocol dhca diffie-hellman
tst/dh_mim.scm view
@@ -2,9 +2,9 @@  ; In this example, the initiator and responder roles participate in a ; Diffie-Hellman exchange, and then a nonce is transmitted by the-; initiator and received by the responder.  +; initiator and received by the responder. -; A man-in-the-middle attack is possible, because there is no +; A man-in-the-middle attack is possible, because there is no ; attempt made to authenticate either of the parties.  Therefore, the ; adversary may emulate the responder to the initator and vice versa. @@ -28,7 +28,6 @@     (uniq-gen y))   (comment "Diffie-hellman key exchange followed by an encryption")) - (defskeleton dh_mim   (vars (n text) (x0 y0 expt) (x y rndx))   (defstrand init 3 (n n) (y y0) (x x))@@ -37,4 +36,3 @@   (uniq-orig n)   (pen-non-orig x y)   (comment "Agreement on the encrypted text only"))-
tst/dh_mim.tst view
@@ -1,7 +1,7 @@ (herald "Diffie-Hellman protocol, man-in-the-middle attack"   (algebra diffie-hellman)) -(comment "CPSA 3.6.3")+(comment "CPSA 3.6.4") (comment "All input read from dh_mim.scm")  (defprotocol dh_mim diffie-hellman
tst/dh_mim2.scm view
@@ -32,4 +32,3 @@   (pen-non-orig x y)   (comment "Agreement on the encrypted text only")) ;)-
tst/dh_mim2.tst view
@@ -1,7 +1,7 @@ (herald "Diffie-Hellman protocol, man-in-the-middle attack"   (algebra diffie-hellman)) -(comment "CPSA 3.6.3")+(comment "CPSA 3.6.4") (comment "All input read from dh_mim2.scm")  (defprotocol dh_mim diffie-hellman
tst/dh_sig.tst view
@@ -1,6 +1,6 @@ (herald "Signed DH exchange" (algebra diffie-hellman)) -(comment "CPSA 3.6.3")+(comment "CPSA 3.6.4") (comment "All input read from dh_sig.scm")  (defprotocol dh_sig diffie-hellman
tst/dh_test.tst view
@@ -1,7 +1,7 @@ (herald "Diffie-Hellman protocol, man-in-the-middle attack"   (algebra diffie-hellman) (bound 20)) -(comment "CPSA 3.6.3")+(comment "CPSA 3.6.4") (comment "All input read from dh_test.scm") (comment "Strand count bounded at 20")
tst/dhnsl_basic.scm view
@@ -9,7 +9,7 @@      (recv (enc (exp (gen) x) a (pubk b)))      (send (enc (exp (gen) x) (exp (gen) y) b (pubk a)))      (recv (enc (exp (gen) y) (pubk b)))-     +      )     (absent (y (exp (gen) x))) ;    (uniq-gen y)
tst/dhnsl_basic.tst view
@@ -1,7 +1,7 @@ (herald "Diffie-Hellman enhanced Needham-Schroeder-Lowe Protocol"   (algebra diffie-hellman)) -(comment "CPSA 3.6.3")+(comment "CPSA 3.6.4") (comment "All input read from dhnsl_basic.scm")  (defprotocol dhnsl diffie-hellman
tst/dhnsl_use.tst view
@@ -1,7 +1,7 @@ (herald "Diffie-Hellman enhanced Needham-Schroeder-Lowe Protocol"   (algebra diffie-hellman)) -(comment "CPSA 3.6.3")+(comment "CPSA 3.6.4") (comment "All input read from dhnsl_use.scm")  (defprotocol dhnsl diffie-hellman
tst/enrich.tst view
@@ -1,6 +1,6 @@ (herald enrich) -(comment "CPSA 3.6.3")+(comment "CPSA 3.6.4") (comment "All input read from enrich.scm")  (defprotocol enrich basic
tst/envelope.tst view
@@ -1,6 +1,6 @@ (herald "Envelope Protocol" (bound 20)) -(comment "CPSA 3.6.3")+(comment "CPSA 3.6.4") (comment "All input read from envelope.scm") (comment "Strand count bounded at 20")
tst/ffgg.tst view
@@ -1,7 +1,7 @@ (herald "The ffgg Protocol"   (comment "From A Necessarily Parallel Attack by Jon K. Millen")) -(comment "CPSA 3.6.3")+(comment "CPSA 3.6.4") (comment "All input read from ffgg.scm")  (defprotocol ffgg basic
+ tst/fluffy_draft03_gske.scm view
@@ -0,0 +1,114 @@+(herald "GSKE, part of Fluffy: Simplified Key Exchange for Constrained Environments draft-hardjono-ace-fluffy-03"+ (comment "Based on the Internet-Draft: https://www.ietf.org/archive/id/draft-hardjono-ace-fluffy-03.txt"))++;; This model does not include timestamps or optional fields.+(defprotocol fluffy basic+ (defrole sp+  (vars (b s name) (nb g text) (gk skey))+  (trace+   (send (cat "req" s g (enc b nb (ltk s b))))+   (recv (cat "resp" b (enc s g nb gk (ltk s b))))))+ (defrole keyserv+  (vars (a b s name) (nb na g text) (gk skey))+  (trace+   (recv (cat "req" s g (enc b nb (ltk s b))))+   (send (cat "resp" b (enc s g nb gk (ltk s b))))+   (recv (cat "fetch" s g (enc a na (ltk s a))))+   (send (cat "deliver" a (enc s g na gk (ltk s a)))))+  (uniq-gen gk))+ (defrole client+  (vars (a b s name) (na g text) (gk skey))+  (trace+   (send (cat "fetch" s g (enc a na (ltk s a))))+   (recv (cat "deliver" a (enc s g na gk (ltk s a)))))))++;; Service principal's (sp) point-of-view+(defskeleton fluffy+ (vars (b s name) (nb text) (gk skey))+ (defstrand sp 2 (b b) (s s) (nb nb) (gk gk))+ (non-orig (ltk s b))+ (uniq-orig nb)+ (comment "Service Principal's point-of-view"))++;; Simple key distribution center's (skdc) point-of-view+(defskeleton fluffy+ (vars (a b s name) (nb na text) (gk skey))+ (defstrand keyserv 4 (a a) (b b) (s s) (nb nb) (na na) (gk gk))+ (non-orig (ltk s b) (ltk s a))+ (uniq-gen gk)+ (comment "SKDC's point-of-view"))++;; Client's point-of-view+(defskeleton fluffy+ (vars (a s name) (na text) (gk skey))+ (defstrand client 2 (a a) (s s) (na na) (gk gk))+ (non-orig (ltk s a))+ (uniq-orig na)+ (comment "Clients's point-of-view"))++(defprotocol fluffy-rule basic+  (defrole sp+    (vars (b s name) (nb g text) (gk skey))+    (trace+     (send (cat "req" s g (enc b nb (ltk s b))))+     (recv (cat "resp" b (enc s g nb gk (ltk s b))))))+  (defrole keyserv+    (vars (a b s name) (nb na g text) (gk skey))+    (trace+     (recv (cat "req" s g (enc b nb (ltk s b))))+     (send (cat "resp" b (enc s g nb gk (ltk s b))))+     (recv (cat "fetch" s g (enc a na (ltk s a))))+     (send (cat "deliver" a (enc s g na gk (ltk s a)))))+    (uniq-gen gk))+  (defrole client+    (vars (a b s name) (na g text) (gk skey))+    (trace+     (send (cat "fetch" s g (enc a na (ltk s a))))+     (recv (cat "deliver" a (enc s g na gk (ltk s a))))))+  (defrule client-no-request+    (forall ((a s name) (y z strd))+	    (implies+	     (and+	      (p "client" z 1)+	      (p "client" "s" z s)+	      (p "client" "a" z a)+	      (p "keyserv" y 1)+	      (p "keyserv" "s" y s)+	      (p "keyserv" "b" y a))+	     (false))))+  (defrule sp-no-fetch+    (forall ((b s name) (y z strd))+	    (implies+	     (and+	      (p "sp" z 1)+	      (p "sp" "s" z s)+	      (p "sp" "b" z b)+	      (p "keyserv" y 3)+	      (p "keyserv" "s" y s)+	      (p "keyserv" "a" y b))+	     (false))))+  )++;; Service principal's (sp) point-of-view+(defskeleton fluffy-rule+ (vars (b s name) (nb text) (gk skey))+ (defstrand sp 2 (b b) (s s) (nb nb) (gk gk))+ (non-orig (ltk s b))+ (uniq-orig nb)+ (comment "Service Principal's point-of-view"))++;; Simple key distribution center's (skdc) point-of-view+(defskeleton fluffy-rule+ (vars (a b s name) (nb na text) (gk skey))+ (defstrand keyserv 4 (a a) (b b) (s s) (nb nb) (na na) (gk gk))+ (non-orig (ltk s b) (ltk s a))+ (uniq-gen gk)+ (comment "SKDC's point-of-view"))++;; Client's point-of-view+(defskeleton fluffy-rule+ (vars (a s name) (na text) (gk skey))+ (defstrand client 2 (a a) (s s) (na na) (gk gk))+ (non-orig (ltk s a))+ (uniq-orig na)+ (comment "Clients's point-of-view"))
+ tst/fluffy_draft03_gske.tst view
@@ -0,0 +1,608 @@+(herald+  "GSKE, part of Fluffy: Simplified Key Exchange for Constrained Environments draft-hardjono-ace-fluffy-03"+  (comment+    "Based on the Internet-Draft: https://www.ietf.org/archive/id/draft-hardjono-ace-fluffy-03.txt"))++(comment "CPSA 3.6.4")+(comment "All input read from fluffy_draft03_gske.scm")++(defprotocol fluffy basic+  (defrole sp+    (vars (b s name) (nb g text) (gk skey))+    (trace (send (cat "req" s g (enc b nb (ltk s b))))+      (recv (cat "resp" b (enc s g nb gk (ltk s b))))))+  (defrole keyserv+    (vars (a b s name) (nb na g text) (gk skey))+    (trace (recv (cat "req" s g (enc b nb (ltk s b))))+      (send (cat "resp" b (enc s g nb gk (ltk s b))))+      (recv (cat "fetch" s g (enc a na (ltk s a))))+      (send (cat "deliver" a (enc s g na gk (ltk s a)))))+    (uniq-gen gk))+  (defrole client+    (vars (a s name) (na g text) (gk skey))+    (trace (send (cat "fetch" s g (enc a na (ltk s a))))+      (recv (cat "deliver" a (enc s g na gk (ltk s a)))))))++(defskeleton fluffy+  (vars (nb g text) (b s name) (gk skey))+  (defstrand sp 2 (nb nb) (g g) (b b) (s s) (gk gk))+  (non-orig (ltk s b))+  (uniq-orig nb)+  (comment "Service Principal's point-of-view")+  (traces+    ((send (cat "req" s g (enc b nb (ltk s b))))+      (recv (cat "resp" b (enc s g nb gk (ltk s b))))))+  (label 0)+  (unrealized (0 1))+  (origs (nb (0 0)))+  (comment "2 in cohort - 2 not yet seen"))++(defskeleton fluffy+  (vars (nb g nb-0 text) (b s b-0 name) (gk skey))+  (defstrand sp 2 (nb nb) (g g) (b b) (s s) (gk gk))+  (defstrand keyserv 4 (nb nb-0) (na nb) (g g) (a b) (b b-0) (s s)+    (gk gk))+  (precedes ((0 0) (1 2)) ((1 3) (0 1)))+  (non-orig (ltk s b))+  (uniq-gen gk)+  (uniq-orig nb)+  (operation encryption-test (added-strand keyserv 4)+    (enc s g nb gk (ltk s b)) (0 1))+  (traces+    ((send (cat "req" s g (enc b nb (ltk s b))))+      (recv (cat "resp" b (enc s g nb gk (ltk s b)))))+    ((recv (cat "req" s g (enc b-0 nb-0 (ltk s b-0))))+      (send (cat "resp" b-0 (enc s g nb-0 gk (ltk s b-0))))+      (recv (cat "fetch" s g (enc b nb (ltk s b))))+      (send (cat "deliver" b (enc s g nb gk (ltk s b))))))+  (label 1)+  (parent 0)+  (unrealized)+  (shape)+  (maps ((0) ((b b) (s s) (nb nb) (gk gk) (g g))))+  (origs (nb (0 0))))++(defskeleton fluffy+  (vars (nb g text) (b s name) (gk skey))+  (defstrand sp 2 (nb nb) (g g) (b b) (s s) (gk gk))+  (defstrand keyserv 2 (nb nb) (g g) (b b) (s s) (gk gk))+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (ltk s b))+  (uniq-gen gk)+  (uniq-orig nb)+  (operation encryption-test (added-strand keyserv 2)+    (enc s g nb gk (ltk s b)) (0 1))+  (traces+    ((send (cat "req" s g (enc b nb (ltk s b))))+      (recv (cat "resp" b (enc s g nb gk (ltk s b)))))+    ((recv (cat "req" s g (enc b nb (ltk s b))))+      (send (cat "resp" b (enc s g nb gk (ltk s b))))))+  (label 2)+  (parent 0)+  (unrealized)+  (shape)+  (maps ((0) ((b b) (s s) (nb nb) (gk gk) (g g))))+  (origs (nb (0 0))))++(comment "Nothing left to do")++(defprotocol fluffy basic+  (defrole sp+    (vars (b s name) (nb g text) (gk skey))+    (trace (send (cat "req" s g (enc b nb (ltk s b))))+      (recv (cat "resp" b (enc s g nb gk (ltk s b))))))+  (defrole keyserv+    (vars (a b s name) (nb na g text) (gk skey))+    (trace (recv (cat "req" s g (enc b nb (ltk s b))))+      (send (cat "resp" b (enc s g nb gk (ltk s b))))+      (recv (cat "fetch" s g (enc a na (ltk s a))))+      (send (cat "deliver" a (enc s g na gk (ltk s a)))))+    (uniq-gen gk))+  (defrole client+    (vars (a s name) (na g text) (gk skey))+    (trace (send (cat "fetch" s g (enc a na (ltk s a))))+      (recv (cat "deliver" a (enc s g na gk (ltk s a)))))))++(defskeleton fluffy+  (vars (nb na g text) (a b s name) (gk skey))+  (defstrand keyserv 4 (nb nb) (na na) (g g) (a a) (b b) (s s) (gk gk))+  (non-orig (ltk s a) (ltk s b))+  (uniq-gen gk)+  (comment "SKDC's point-of-view")+  (traces+    ((recv (cat "req" s g (enc b nb (ltk s b))))+      (send (cat "resp" b (enc s g nb gk (ltk s b))))+      (recv (cat "fetch" s g (enc a na (ltk s a))))+      (send (cat "deliver" a (enc s g na gk (ltk s a))))))+  (label 3)+  (unrealized (0 0) (0 2))+  (origs)+  (comment "2 in cohort - 2 not yet seen"))++(defskeleton fluffy+  (vars (nb na g g-0 text) (a b s name) (gk skey))+  (defstrand keyserv 4 (nb nb) (na na) (g g) (a a) (b b) (s s) (gk gk))+  (defstrand sp 1 (nb nb) (g g-0) (b b) (s s))+  (precedes ((1 0) (0 0)))+  (non-orig (ltk s a) (ltk s b))+  (uniq-gen gk)+  (operation encryption-test (added-strand sp 1) (enc b nb (ltk s b))+    (0 0))+  (traces+    ((recv (cat "req" s g (enc b nb (ltk s b))))+      (send (cat "resp" b (enc s g nb gk (ltk s b))))+      (recv (cat "fetch" s g (enc a na (ltk s a))))+      (send (cat "deliver" a (enc s g na gk (ltk s a)))))+    ((send (cat "req" s g-0 (enc b nb (ltk s b))))))+  (label 4)+  (parent 3)+  (unrealized (0 2))+  (comment "3 in cohort - 3 not yet seen"))++(defskeleton fluffy+  (vars (nb na g g-0 text) (a b s name) (gk skey))+  (defstrand keyserv 4 (nb nb) (na na) (g g) (a a) (b b) (s s) (gk gk))+  (defstrand client 1 (na nb) (g g-0) (a b) (s s))+  (precedes ((1 0) (0 0)))+  (non-orig (ltk s a) (ltk s b))+  (uniq-gen gk)+  (operation encryption-test (added-strand client 1)+    (enc b nb (ltk s b)) (0 0))+  (traces+    ((recv (cat "req" s g (enc b nb (ltk s b))))+      (send (cat "resp" b (enc s g nb gk (ltk s b))))+      (recv (cat "fetch" s g (enc a na (ltk s a))))+      (send (cat "deliver" a (enc s g na gk (ltk s a)))))+    ((send (cat "fetch" s g-0 (enc b nb (ltk s b))))))+  (label 5)+  (parent 3)+  (unrealized (0 2))+  (comment "3 in cohort - 3 not yet seen"))++(defskeleton fluffy+  (vars (nb g g-0 text) (b s name) (gk skey))+  (defstrand keyserv 4 (nb nb) (na nb) (g g) (a b) (b b) (s s) (gk gk))+  (defstrand sp 1 (nb nb) (g g-0) (b b) (s s))+  (precedes ((1 0) (0 0)))+  (non-orig (ltk s b))+  (uniq-gen gk)+  (operation encryption-test (displaced 2 1 sp 1) (enc a na (ltk s a))+    (0 2))+  (traces+    ((recv (cat "req" s g (enc b nb (ltk s b))))+      (send (cat "resp" b (enc s g nb gk (ltk s b))))+      (recv (cat "fetch" s g (enc b nb (ltk s b))))+      (send (cat "deliver" b (enc s g nb gk (ltk s b)))))+    ((send (cat "req" s g-0 (enc b nb (ltk s b))))))+  (label 6)+  (parent 4)+  (unrealized)+  (shape)+  (maps ((0) ((a b) (b b) (s s) (nb nb) (na nb) (gk gk) (g g))))+  (origs))++(defskeleton fluffy+  (vars (nb na g g-0 g-1 text) (a b s name) (gk skey))+  (defstrand keyserv 4 (nb nb) (na na) (g g) (a a) (b b) (s s) (gk gk))+  (defstrand sp 1 (nb nb) (g g-0) (b b) (s s))+  (defstrand sp 1 (nb na) (g g-1) (b a) (s s))+  (precedes ((1 0) (0 0)) ((2 0) (0 2)))+  (non-orig (ltk s a) (ltk s b))+  (uniq-gen gk)+  (operation encryption-test (added-strand sp 1) (enc a na (ltk s a))+    (0 2))+  (traces+    ((recv (cat "req" s g (enc b nb (ltk s b))))+      (send (cat "resp" b (enc s g nb gk (ltk s b))))+      (recv (cat "fetch" s g (enc a na (ltk s a))))+      (send (cat "deliver" a (enc s g na gk (ltk s a)))))+    ((send (cat "req" s g-0 (enc b nb (ltk s b)))))+    ((send (cat "req" s g-1 (enc a na (ltk s a))))))+  (label 7)+  (parent 4)+  (unrealized)+  (shape)+  (maps ((0) ((a a) (b b) (s s) (nb nb) (na na) (gk gk) (g g))))+  (origs))++(defskeleton fluffy+  (vars (nb na g g-0 g-1 text) (a b s name) (gk skey))+  (defstrand keyserv 4 (nb nb) (na na) (g g) (a a) (b b) (s s) (gk gk))+  (defstrand sp 1 (nb nb) (g g-0) (b b) (s s))+  (defstrand client 1 (na na) (g g-1) (a a) (s s))+  (precedes ((1 0) (0 0)) ((2 0) (0 2)))+  (non-orig (ltk s a) (ltk s b))+  (uniq-gen gk)+  (operation encryption-test (added-strand client 1)+    (enc a na (ltk s a)) (0 2))+  (traces+    ((recv (cat "req" s g (enc b nb (ltk s b))))+      (send (cat "resp" b (enc s g nb gk (ltk s b))))+      (recv (cat "fetch" s g (enc a na (ltk s a))))+      (send (cat "deliver" a (enc s g na gk (ltk s a)))))+    ((send (cat "req" s g-0 (enc b nb (ltk s b)))))+    ((send (cat "fetch" s g-1 (enc a na (ltk s a))))))+  (label 8)+  (parent 4)+  (unrealized)+  (shape)+  (maps ((0) ((a a) (b b) (s s) (nb nb) (na na) (gk gk) (g g))))+  (origs))++(defskeleton fluffy+  (vars (nb na g g-0 g-1 text) (a b s name) (gk skey))+  (defstrand keyserv 4 (nb nb) (na na) (g g) (a a) (b b) (s s) (gk gk))+  (defstrand client 1 (na nb) (g g-0) (a b) (s s))+  (defstrand sp 1 (nb na) (g g-1) (b a) (s s))+  (precedes ((1 0) (0 0)) ((2 0) (0 2)))+  (non-orig (ltk s a) (ltk s b))+  (uniq-gen gk)+  (operation encryption-test (added-strand sp 1) (enc a na (ltk s a))+    (0 2))+  (traces+    ((recv (cat "req" s g (enc b nb (ltk s b))))+      (send (cat "resp" b (enc s g nb gk (ltk s b))))+      (recv (cat "fetch" s g (enc a na (ltk s a))))+      (send (cat "deliver" a (enc s g na gk (ltk s a)))))+    ((send (cat "fetch" s g-0 (enc b nb (ltk s b)))))+    ((send (cat "req" s g-1 (enc a na (ltk s a))))))+  (label 9)+  (parent 5)+  (unrealized)+  (shape)+  (maps ((0) ((a a) (b b) (s s) (nb nb) (na na) (gk gk) (g g))))+  (origs))++(defskeleton fluffy+  (vars (nb g g-0 text) (b s name) (gk skey))+  (defstrand keyserv 4 (nb nb) (na nb) (g g) (a b) (b b) (s s) (gk gk))+  (defstrand client 1 (na nb) (g g-0) (a b) (s s))+  (precedes ((1 0) (0 0)))+  (non-orig (ltk s b))+  (uniq-gen gk)+  (operation encryption-test (displaced 2 1 client 1)+    (enc a na (ltk s a)) (0 2))+  (traces+    ((recv (cat "req" s g (enc b nb (ltk s b))))+      (send (cat "resp" b (enc s g nb gk (ltk s b))))+      (recv (cat "fetch" s g (enc b nb (ltk s b))))+      (send (cat "deliver" b (enc s g nb gk (ltk s b)))))+    ((send (cat "fetch" s g-0 (enc b nb (ltk s b))))))+  (label 10)+  (parent 5)+  (unrealized)+  (shape)+  (maps ((0) ((a b) (b b) (s s) (nb nb) (na nb) (gk gk) (g g))))+  (origs))++(defskeleton fluffy+  (vars (nb na g g-0 g-1 text) (a b s name) (gk skey))+  (defstrand keyserv 4 (nb nb) (na na) (g g) (a a) (b b) (s s) (gk gk))+  (defstrand client 1 (na nb) (g g-0) (a b) (s s))+  (defstrand client 1 (na na) (g g-1) (a a) (s s))+  (precedes ((1 0) (0 0)) ((2 0) (0 2)))+  (non-orig (ltk s a) (ltk s b))+  (uniq-gen gk)+  (operation encryption-test (added-strand client 1)+    (enc a na (ltk s a)) (0 2))+  (traces+    ((recv (cat "req" s g (enc b nb (ltk s b))))+      (send (cat "resp" b (enc s g nb gk (ltk s b))))+      (recv (cat "fetch" s g (enc a na (ltk s a))))+      (send (cat "deliver" a (enc s g na gk (ltk s a)))))+    ((send (cat "fetch" s g-0 (enc b nb (ltk s b)))))+    ((send (cat "fetch" s g-1 (enc a na (ltk s a))))))+  (label 11)+  (parent 5)+  (unrealized)+  (shape)+  (maps ((0) ((a a) (b b) (s s) (nb nb) (na na) (gk gk) (g g))))+  (origs))++(comment "Nothing left to do")++(defprotocol fluffy basic+  (defrole sp+    (vars (b s name) (nb g text) (gk skey))+    (trace (send (cat "req" s g (enc b nb (ltk s b))))+      (recv (cat "resp" b (enc s g nb gk (ltk s b))))))+  (defrole keyserv+    (vars (a b s name) (nb na g text) (gk skey))+    (trace (recv (cat "req" s g (enc b nb (ltk s b))))+      (send (cat "resp" b (enc s g nb gk (ltk s b))))+      (recv (cat "fetch" s g (enc a na (ltk s a))))+      (send (cat "deliver" a (enc s g na gk (ltk s a)))))+    (uniq-gen gk))+  (defrole client+    (vars (a s name) (na g text) (gk skey))+    (trace (send (cat "fetch" s g (enc a na (ltk s a))))+      (recv (cat "deliver" a (enc s g na gk (ltk s a)))))))++(defskeleton fluffy+  (vars (na g text) (a s name) (gk skey))+  (defstrand client 2 (na na) (g g) (a a) (s s) (gk gk))+  (non-orig (ltk s a))+  (uniq-orig na)+  (comment "Clients's point-of-view")+  (traces+    ((send (cat "fetch" s g (enc a na (ltk s a))))+      (recv (cat "deliver" a (enc s g na gk (ltk s a))))))+  (label 12)+  (unrealized (0 1))+  (origs (na (0 0)))+  (comment "2 in cohort - 2 not yet seen"))++(defskeleton fluffy+  (vars (na g nb text) (a s b name) (gk skey))+  (defstrand client 2 (na na) (g g) (a a) (s s) (gk gk))+  (defstrand keyserv 4 (nb nb) (na na) (g g) (a a) (b b) (s s) (gk gk))+  (precedes ((0 0) (1 2)) ((1 3) (0 1)))+  (non-orig (ltk s a))+  (uniq-gen gk)+  (uniq-orig na)+  (operation encryption-test (added-strand keyserv 4)+    (enc s g na gk (ltk s a)) (0 1))+  (traces+    ((send (cat "fetch" s g (enc a na (ltk s a))))+      (recv (cat "deliver" a (enc s g na gk (ltk s a)))))+    ((recv (cat "req" s g (enc b nb (ltk s b))))+      (send (cat "resp" b (enc s g nb gk (ltk s b))))+      (recv (cat "fetch" s g (enc a na (ltk s a))))+      (send (cat "deliver" a (enc s g na gk (ltk s a))))))+  (label 13)+  (parent 12)+  (unrealized)+  (shape)+  (maps ((0) ((a a) (s s) (na na) (gk gk) (g g))))+  (origs (na (0 0))))++(defskeleton fluffy+  (vars (na g text) (a s name) (gk skey))+  (defstrand client 2 (na na) (g g) (a a) (s s) (gk gk))+  (defstrand keyserv 2 (nb na) (g g) (b a) (s s) (gk gk))+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (ltk s a))+  (uniq-gen gk)+  (uniq-orig na)+  (operation encryption-test (added-strand keyserv 2)+    (enc s g na gk (ltk s a)) (0 1))+  (traces+    ((send (cat "fetch" s g (enc a na (ltk s a))))+      (recv (cat "deliver" a (enc s g na gk (ltk s a)))))+    ((recv (cat "req" s g (enc a na (ltk s a))))+      (send (cat "resp" a (enc s g na gk (ltk s a))))))+  (label 14)+  (parent 12)+  (unrealized)+  (shape)+  (maps ((0) ((a a) (s s) (na na) (gk gk) (g g))))+  (origs (na (0 0))))++(comment "Nothing left to do")++(defprotocol fluffy-rule basic+  (defrole sp+    (vars (b s name) (nb g text) (gk skey))+    (trace (send (cat "req" s g (enc b nb (ltk s b))))+      (recv (cat "resp" b (enc s g nb gk (ltk s b))))))+  (defrole keyserv+    (vars (a b s name) (nb na g text) (gk skey))+    (trace (recv (cat "req" s g (enc b nb (ltk s b))))+      (send (cat "resp" b (enc s g nb gk (ltk s b))))+      (recv (cat "fetch" s g (enc a na (ltk s a))))+      (send (cat "deliver" a (enc s g na gk (ltk s a)))))+    (uniq-gen gk))+  (defrole client+    (vars (a s name) (na g text) (gk skey))+    (trace (send (cat "fetch" s g (enc a na (ltk s a))))+      (recv (cat "deliver" a (enc s g na gk (ltk s a))))))+  (defrule client-no-request+    (forall ((a s name) (y z strd))+      (implies+        (and (p "client" z 1) (p "client" "s" z s) (p "client" "a" z a)+          (p "keyserv" y 1) (p "keyserv" "s" y s) (p "keyserv" "b" y a))+        (false))))+  (defrule sp-no-fetch+    (forall ((b s name) (y z strd))+      (implies+        (and (p "sp" z 1) (p "sp" "s" z s) (p "sp" "b" z b)+          (p "keyserv" y 3) (p "keyserv" "s" y s) (p "keyserv" "a" y b))+        (false)))))++(defskeleton fluffy-rule+  (vars (nb g text) (b s name) (gk skey))+  (defstrand sp 2 (nb nb) (g g) (b b) (s s) (gk gk))+  (non-orig (ltk s b))+  (uniq-orig nb)+  (comment "Service Principal's point-of-view")+  (traces+    ((send (cat "req" s g (enc b nb (ltk s b))))+      (recv (cat "resp" b (enc s g nb gk (ltk s b))))))+  (label 15)+  (unrealized (0 1))+  (origs (nb (0 0)))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton fluffy-rule+  (vars (nb g text) (b s name) (gk skey))+  (defstrand sp 2 (nb nb) (g g) (b b) (s s) (gk gk))+  (defstrand keyserv 2 (nb nb) (g g) (b b) (s s) (gk gk))+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (ltk s b))+  (uniq-gen gk)+  (uniq-orig nb)+  (operation encryption-test (added-strand keyserv 2)+    (enc s g nb gk (ltk s b)) (0 1))+  (traces+    ((send (cat "req" s g (enc b nb (ltk s b))))+      (recv (cat "resp" b (enc s g nb gk (ltk s b)))))+    ((recv (cat "req" s g (enc b nb (ltk s b))))+      (send (cat "resp" b (enc s g nb gk (ltk s b))))))+  (label 16)+  (parent 15)+  (unrealized)+  (shape)+  (maps ((0) ((b b) (s s) (nb nb) (gk gk) (g g))))+  (origs (nb (0 0))))++(comment "Nothing left to do")++(defprotocol fluffy-rule basic+  (defrole sp+    (vars (b s name) (nb g text) (gk skey))+    (trace (send (cat "req" s g (enc b nb (ltk s b))))+      (recv (cat "resp" b (enc s g nb gk (ltk s b))))))+  (defrole keyserv+    (vars (a b s name) (nb na g text) (gk skey))+    (trace (recv (cat "req" s g (enc b nb (ltk s b))))+      (send (cat "resp" b (enc s g nb gk (ltk s b))))+      (recv (cat "fetch" s g (enc a na (ltk s a))))+      (send (cat "deliver" a (enc s g na gk (ltk s a)))))+    (uniq-gen gk))+  (defrole client+    (vars (a s name) (na g text) (gk skey))+    (trace (send (cat "fetch" s g (enc a na (ltk s a))))+      (recv (cat "deliver" a (enc s g na gk (ltk s a))))))+  (defrule client-no-request+    (forall ((a s name) (y z strd))+      (implies+        (and (p "client" z 1) (p "client" "s" z s) (p "client" "a" z a)+          (p "keyserv" y 1) (p "keyserv" "s" y s) (p "keyserv" "b" y a))+        (false))))+  (defrule sp-no-fetch+    (forall ((b s name) (y z strd))+      (implies+        (and (p "sp" z 1) (p "sp" "s" z s) (p "sp" "b" z b)+          (p "keyserv" y 3) (p "keyserv" "s" y s) (p "keyserv" "a" y b))+        (false)))))++(defskeleton fluffy-rule+  (vars (nb na g text) (a b s name) (gk skey))+  (defstrand keyserv 4 (nb nb) (na na) (g g) (a a) (b b) (s s) (gk gk))+  (non-orig (ltk s a) (ltk s b))+  (uniq-gen gk)+  (comment "SKDC's point-of-view")+  (traces+    ((recv (cat "req" s g (enc b nb (ltk s b))))+      (send (cat "resp" b (enc s g nb gk (ltk s b))))+      (recv (cat "fetch" s g (enc a na (ltk s a))))+      (send (cat "deliver" a (enc s g na gk (ltk s a))))))+  (label 17)+  (unrealized (0 0) (0 2))+  (origs)+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton fluffy-rule+  (vars (nb na g g-0 text) (a b s name) (gk skey))+  (defstrand keyserv 4 (nb nb) (na na) (g g) (a a) (b b) (s s) (gk gk))+  (defstrand sp 1 (nb nb) (g g-0) (b b) (s s))+  (precedes ((1 0) (0 0)))+  (non-orig (ltk s a) (ltk s b))+  (uniq-gen gk)+  (operation encryption-test (added-strand sp 1) (enc b nb (ltk s b))+    (0 0))+  (traces+    ((recv (cat "req" s g (enc b nb (ltk s b))))+      (send (cat "resp" b (enc s g nb gk (ltk s b))))+      (recv (cat "fetch" s g (enc a na (ltk s a))))+      (send (cat "deliver" a (enc s g na gk (ltk s a)))))+    ((send (cat "req" s g-0 (enc b nb (ltk s b))))))+  (label 18)+  (parent 17)+  (unrealized (0 2))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton fluffy-rule+  (vars (nb na g g-0 g-1 text) (a b s name) (gk skey))+  (defstrand keyserv 4 (nb nb) (na na) (g g) (a a) (b b) (s s) (gk gk))+  (defstrand sp 1 (nb nb) (g g-0) (b b) (s s))+  (defstrand client 1 (na na) (g g-1) (a a) (s s))+  (precedes ((1 0) (0 0)) ((2 0) (0 2)))+  (non-orig (ltk s a) (ltk s b))+  (uniq-gen gk)+  (operation encryption-test (added-strand client 1)+    (enc a na (ltk s a)) (0 2))+  (traces+    ((recv (cat "req" s g (enc b nb (ltk s b))))+      (send (cat "resp" b (enc s g nb gk (ltk s b))))+      (recv (cat "fetch" s g (enc a na (ltk s a))))+      (send (cat "deliver" a (enc s g na gk (ltk s a)))))+    ((send (cat "req" s g-0 (enc b nb (ltk s b)))))+    ((send (cat "fetch" s g-1 (enc a na (ltk s a))))))+  (label 19)+  (parent 18)+  (unrealized)+  (shape)+  (maps ((0) ((a a) (b b) (s s) (nb nb) (na na) (gk gk) (g g))))+  (origs))++(comment "Nothing left to do")++(defprotocol fluffy-rule basic+  (defrole sp+    (vars (b s name) (nb g text) (gk skey))+    (trace (send (cat "req" s g (enc b nb (ltk s b))))+      (recv (cat "resp" b (enc s g nb gk (ltk s b))))))+  (defrole keyserv+    (vars (a b s name) (nb na g text) (gk skey))+    (trace (recv (cat "req" s g (enc b nb (ltk s b))))+      (send (cat "resp" b (enc s g nb gk (ltk s b))))+      (recv (cat "fetch" s g (enc a na (ltk s a))))+      (send (cat "deliver" a (enc s g na gk (ltk s a)))))+    (uniq-gen gk))+  (defrole client+    (vars (a s name) (na g text) (gk skey))+    (trace (send (cat "fetch" s g (enc a na (ltk s a))))+      (recv (cat "deliver" a (enc s g na gk (ltk s a))))))+  (defrule client-no-request+    (forall ((a s name) (y z strd))+      (implies+        (and (p "client" z 1) (p "client" "s" z s) (p "client" "a" z a)+          (p "keyserv" y 1) (p "keyserv" "s" y s) (p "keyserv" "b" y a))+        (false))))+  (defrule sp-no-fetch+    (forall ((b s name) (y z strd))+      (implies+        (and (p "sp" z 1) (p "sp" "s" z s) (p "sp" "b" z b)+          (p "keyserv" y 3) (p "keyserv" "s" y s) (p "keyserv" "a" y b))+        (false)))))++(defskeleton fluffy-rule+  (vars (na g text) (a s name) (gk skey))+  (defstrand client 2 (na na) (g g) (a a) (s s) (gk gk))+  (non-orig (ltk s a))+  (uniq-orig na)+  (comment "Clients's point-of-view")+  (traces+    ((send (cat "fetch" s g (enc a na (ltk s a))))+      (recv (cat "deliver" a (enc s g na gk (ltk s a))))))+  (label 20)+  (unrealized (0 1))+  (origs (na (0 0)))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton fluffy-rule+  (vars (na g nb text) (a s b name) (gk skey))+  (defstrand client 2 (na na) (g g) (a a) (s s) (gk gk))+  (defstrand keyserv 4 (nb nb) (na na) (g g) (a a) (b b) (s s) (gk gk))+  (precedes ((0 0) (1 2)) ((1 3) (0 1)))+  (non-orig (ltk s a))+  (uniq-gen gk)+  (uniq-orig na)+  (operation encryption-test (added-strand keyserv 4)+    (enc s g na gk (ltk s a)) (0 1))+  (traces+    ((send (cat "fetch" s g (enc a na (ltk s a))))+      (recv (cat "deliver" a (enc s g na gk (ltk s a)))))+    ((recv (cat "req" s g (enc b nb (ltk s b))))+      (send (cat "resp" b (enc s g nb gk (ltk s b))))+      (recv (cat "fetch" s g (enc a na (ltk s a))))+      (send (cat "deliver" a (enc s g na gk (ltk s a))))))+  (label 21)+  (parent 20)+  (unrealized)+  (shape)+  (maps ((0) ((a a) (s s) (na na) (gk gk) (g g))))+  (origs (na (0 0))))++(comment "Nothing left to do")
tst/fnof_or.tst view
@@ -2,7 +2,7 @@   (comment     "Version using variables of sort mesg, with ltk function emulated.")) -(comment "CPSA 3.6.3")+(comment "CPSA 3.6.4") (comment "All input read from fnof_or.scm")  (defprotocol or basic
tst/fnof_test.tst view
@@ -1,7 +1,7 @@ (herald "Function constraint test protocol"   (comment "Skeletons 2, 4, and 7 should have no shapes.")) -(comment "CPSA 3.6.3")+(comment "CPSA 3.6.4") (comment "All input read from fnof_test.scm")  (defprotocol fnoftest basic
tst/fnof_woolam.tst view
@@ -1,6 +1,6 @@ (herald "Woo-Lam Protocol, using fnof to emulate ltk function") -(comment "CPSA 3.6.3")+(comment "CPSA 3.6.4") (comment "All input read from fnof_woolam.scm")  (defprotocol woolam basic
tst/fnof_yahalom.tst view
@@ -2,7 +2,7 @@   "Yahalom Protocol with Forwarding Removed, using fnof to emulate ltk function"   (bound 12)) -(comment "CPSA 3.6.3")+(comment "CPSA 3.6.4") (comment "All input read from fnof_yahalom.scm")  (defprotocol yahalom basic
tst/goals.tst view
@@ -1,6 +1,6 @@ (herald goals) -(comment "CPSA 3.6.3")+(comment "CPSA 3.6.4") (comment "All input read from goals.scm")  (defprotocol ns basic
tst/iadh_um.scm view
@@ -47,7 +47,6 @@     (fn-of ("principal-of" (l self))))   ) - ;; Implicit authentication: participants will agree on the resulting key ;; foo(key).  Therefore they should agree on the names A and B.  (defskeleton iadh-um@@ -60,7 +59,7 @@   (comment "Implicit authentication") ) - ;; Security: + ;; Security: (defskeleton iadh-um   (vars (e1 e2 l rndx) (lp expt) (A B name))   (defstrand participant 5 (e e1) (l l) (ep e2) (lp lp) (self A) (peer B))@@ -68,6 +67,3 @@   (deflistener (hash (exp (gen) (mul l lp)) (exp (gen) (mul e1 e2))))   (non-orig (privk A) (privk B)) )---
tst/iadh_um.tst view

file too large to diff

tst/injection.tst view
@@ -2,7 +2,7 @@   (comment "This protocol contains a man-in-the-middle"     "attack discovered by Galvin Lowe.")) -(comment "CPSA 3.6.3")+(comment "CPSA 3.6.4") (comment "All input read from injection.scm")  (defprotocol ns diffie-hellman
tst/kerb.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 3.6.3")+(comment "CPSA 3.6.4") (comment "All input read from kerb.scm")  (defprotocol kerb-flawed basic
tst/kerberos++.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 3.6.3")+(comment "CPSA 3.6.4") (comment "All input read from kerberos++.scm")  (defprotocol kerberos basic
tst/lt_test.tst view
@@ -2,7 +2,7 @@   (comment "First and third skeletons should have a shape,"     "second and fourth should be dead.")) -(comment "CPSA 3.6.3")+(comment "CPSA 3.6.4") (comment "All input read from lt_test.scm")  (defprotocol lttest basic
tst/neq_test.tst view
@@ -2,7 +2,7 @@   (comment "First skeleton should have a shape,"     "second, and hird should be dead.")) -(comment "CPSA 3.6.3")+(comment "CPSA 3.6.4") (comment "All input read from neq_test.scm")  (defprotocol neqtest basic
tst/ns.tst view
@@ -2,7 +2,7 @@   (comment "This protocol contains a man-in-the-middle"     "attack discovered by Galvin Lowe.")) -(comment "CPSA 3.6.3")+(comment "CPSA 3.6.4") (comment "All input read from ns.scm")  (defprotocol ns basic
tst/or.tst view
@@ -1,7 +1,7 @@ (herald "Otway-Rees Protocol"   (comment "Standard version using variables of sort mesg")) -(comment "CPSA 3.6.3")+(comment "CPSA 3.6.4") (comment "All input read from or.scm")  (defprotocol or basic
+ tst/ordered.scm view
@@ -0,0 +1,26 @@+(herald ordered)++(defprotocol ordered basic++  (defrole dec+    (vars (t text) (k akey))+    (trace (recv (enc t k)) (send t)))++  (defrule neq+    (forall ((x mesg))+	    (implies (fact neq x x) (false))))++  (defrule order+    (forall ((y z strd))+	    (implies+	     (and (p "dec" y 2)+		  (p "dec" z 2))+	     (or (prec y 1 z 0)+		 (prec z 1 y 0)+		 (= y z))))))++(defskeleton ordered+  (vars (a b text))+  (defstrand dec 2 (t a))+  (defstrand dec 2 (t b))+  (facts (neq a b)))
+ tst/ordered.tst view
@@ -0,0 +1,58 @@+(herald ordered)++(comment "CPSA 3.6.4")+(comment "All input read from ordered.scm")++(defprotocol ordered basic+  (defrole dec+    (vars (t text) (k akey))+    (trace (recv (enc t k)) (send t)))+  (defrule neq (forall ((x mesg)) (implies (fact neq x x) (false))))+  (defrule order+    (forall ((y z strd))+      (implies+        (and (p "dec" y 2) (p "dec" z 2))+        (or (prec y 1 z 0) (prec z 1 y 0) (= y z))))))++(defskeleton ordered+  (vars (a b text) (k k-0 akey))+  (defstrand dec 2 (t a) (k k))+  (defstrand dec 2 (t b) (k k-0))+  (facts (neq a b))+  (traces ((recv (enc a k)) (send a)) ((recv (enc b k-0)) (send b)))+  (label 0)+  (unrealized)+  (origs)+  (comment "Not closed under rules"))++(defskeleton ordered+  (vars (a b text) (k k-0 akey))+  (defstrand dec 2 (t a) (k k))+  (defstrand dec 2 (t b) (k k-0))+  (precedes ((0 1) (1 0)))+  (facts (neq a b))+  (rule order)+  (traces ((recv (enc a k)) (send a)) ((recv (enc b k-0)) (send b)))+  (label 1)+  (parent 0)+  (unrealized)+  (shape)+  (maps ((0 1) ((a a) (b b) (k k) (k-0 k-0))))+  (origs))++(defskeleton ordered+  (vars (a b text) (k k-0 akey))+  (defstrand dec 2 (t a) (k k))+  (defstrand dec 2 (t b) (k k-0))+  (precedes ((1 1) (0 0)))+  (facts (neq a b))+  (rule order)+  (traces ((recv (enc a k)) (send a)) ((recv (enc b k-0)) (send b)))+  (label 2)+  (parent 0)+  (unrealized)+  (shape)+  (maps ((0 1) ((a a) (b b) (k k) (k-0 k-0))))+  (origs))++(comment "Nothing left to do")
tst/owang.tst view
@@ -1,4 +1,4 @@-(comment "CPSA 3.6.3")+(comment "CPSA 3.6.4") (comment "All input read from owang.scm")  (defprotocol wang basic
tst/owat.tst view
@@ -1,7 +1,7 @@ (herald "One-way Authentication Test with bltk keys"   (algebra diffie-hellman) (bound 12)) -(comment "CPSA 3.6.3")+(comment "CPSA 3.6.4") (comment "All input read from owat.scm")  (defprotocol owa diffie-hellman
tst/pkinit.tst view
@@ -1,6 +1,6 @@ (herald "Kerberos PKINIT") -(comment "CPSA 3.6.3")+(comment "CPSA 3.6.4") (comment "All input read from pkinit.scm")  (defprotocol pkinit-flawed basic
tst/plaindh.tst view
@@ -1,7 +1,7 @@ (herald "Plain diffie-hellman protocol with challenge-response"   (algebra diffie-hellman)) -(comment "CPSA 3.6.3")+(comment "CPSA 3.6.4") (comment "All input read from plaindh.scm")  (defprotocol plaindh diffie-hellman
tst/priority_test.tst view
@@ -1,6 +1,6 @@ (herald "Receive priority test protocol") -(comment "CPSA 3.6.3")+(comment "CPSA 3.6.4") (comment "All input read from priority_test.scm")  (defprotocol priority_test basic
+ tst/prottrans.scm view
@@ -0,0 +1,107 @@+(herald "Protocol Transformations With Rules")++;; Basic Needham-Schroeder using asymmetric keys++(defprotocol ns basic+  (defrole init+    (vars (a b akey) (na nb text))+    (trace+     (send (enc na a b))+     (recv (enc na nb a))+     (send (enc nb b))))+  (defrole resp+    (vars (b a akey) (nb na text))+    (trace+     (recv (enc na a b))+     (send (enc na nb a))+     (recv (enc nb b))))+  (comment "Needham-Schroeder without rules"))++;;; The initiator point-of-view+(defskeleton ns+  (vars (a b akey) (na text))+  (defstrand init 3 (a a) (b b) (na na))+  (non-orig (invk a) (invk b))+  (uniq-orig na)+  (comment "Initiator point-of-view"))++;;; The responder point-of-view+(defskeleton ns+  (vars (a akey) (nb text))+  (defstrand resp 3 (a a) (nb nb))+  (non-orig (invk a))+  (uniq-orig nb)+  (comment "Responder point-of-view"))++;;; Unilateral protocol+(defprotocol unilateral basic+  (defrole init+     (vars (n text) (k akey))+     (trace+      (send (enc n k))+      (recv n)))+  (defrole resp+     (vars (n text) (k akey))+     (trace+      (recv (enc n k))+      (send n))))++(defskeleton unilateral+  (vars (k akey) (n text))+  (defstrand init 2 (n n) (k k))+  (non-orig (invk k))+  (uniq-orig n)+  (comment "The shape analysis sentence for this problem:"+    (defgoal unilateral+      (forall ((n text) (k akey) (z strd))+        (implies+          (and (p "init" z 2) (p "init" "n" z n) (p "init" "k" z k)+            (non (invk k)) (uniq-at n z 0))+          (exists ((z-0 strd))+            (and (p "resp" z-0 2) (p "resp" "n" z-0 n)+              (p "resp" "k" z-0 k) (prec z 0 z-0 0)+              (prec z-0 1 z 1))))))))++(defprotocol ns-with-rule basic+  (defrole init+    (vars (a b akey) (na nb text))+    (trace+     (send (enc na a b))+     (recv (enc na nb a))+     (send (enc nb b))))+  (defrole resp+    (vars (b a akey) (nb na text))+    (trace+     (recv (enc na a b))+     (send (enc na nb a))+     (recv (enc nb b))))+  (defrule unilateral+    (forall ((r strd) (a akey) (nb text))+	    (implies+	     (and (p "resp" r 3)+		  (p "resp" "a" r a)+		  (p "resp" "nb" r nb)+		  (non (invk a))+		  (uniq nb))+	     (exists ((i strd))+		     (and (p "init" i 3)+			  (p "init" "a" i a)+			  (p "init" "nb" i nb)+			  (prec r 1 i 1)+			  (prec i 2 r 2)))))+    (comment "Unilateral sas under the predicate mapping:")+    (comment (p "init" 2) "->" (p "resp" 3) "and")+    (comment (p "init" "n") "->" (p "resp" "nb") "and")+    (comment (p "init" "k") "->" (p "resp" "a") "and")+    (comment (p "resp" 2) "->" (p "init" 3) "and")+    (comment (p "resp" "n") "->" (p "init" "nb"))+    (comment (p "resp" "k") "->" (p "init" "a")))+  (comment "Needham-Schroeder with rule"))++;;; The responder point-of-view+(defskeleton ns-with-rule+  (vars (a akey) (nb text))+  (defstrand resp 3 (a a) (nb nb))+  (non-orig (invk a))+  (uniq-orig nb)+  (comment "Responder point-of-view"))
+ tst/prottrans.tst view
@@ -0,0 +1,236 @@+(herald "Protocol Transformations With Rules")++(comment "CPSA 3.6.4")+(comment "All input read from prottrans.scm")++(defprotocol ns basic+  (defrole init+    (vars (a b akey) (na nb text))+    (trace (send (enc na a b)) (recv (enc na nb a)) (send (enc nb b))))+  (defrole resp+    (vars (b a akey) (nb na text))+    (trace (recv (enc na a b)) (send (enc na nb a)) (recv (enc nb b))))+  (comment "Needham-Schroeder without rules"))++(defskeleton ns+  (vars (na nb text) (a b akey))+  (defstrand init 3 (na na) (nb nb) (a a) (b b))+  (non-orig (invk a) (invk b))+  (uniq-orig na)+  (comment "Initiator point-of-view")+  (traces ((send (enc na a b)) (recv (enc na nb a)) (send (enc nb b))))+  (label 0)+  (unrealized (0 1))+  (origs (na (0 0)))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton ns+  (vars (na nb nb-0 text) (a b akey))+  (defstrand init 3 (na na) (nb nb) (a a) (b b))+  (defstrand resp 2 (nb nb-0) (na na) (b b) (a a))+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (invk a) (invk b))+  (uniq-orig na)+  (operation nonce-test (added-strand resp 2) na (0 1) (enc na a b))+  (traces ((send (enc na a b)) (recv (enc na nb a)) (send (enc nb b)))+    ((recv (enc na a b)) (send (enc na nb-0 a))))+  (label 1)+  (parent 0)+  (unrealized (0 1))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton ns+  (vars (na nb text) (a b akey))+  (defstrand init 3 (na na) (nb nb) (a a) (b b))+  (defstrand resp 2 (nb nb) (na na) (b b) (a a))+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (invk a) (invk b))+  (uniq-orig na)+  (operation nonce-test (contracted (nb-0 nb)) na (0 1) (enc na nb a)+    (enc na a b))+  (traces ((send (enc na a b)) (recv (enc na nb a)) (send (enc nb b)))+    ((recv (enc na a b)) (send (enc na nb a))))+  (label 2)+  (parent 1)+  (unrealized)+  (shape)+  (maps ((0) ((a a) (b b) (na na) (nb nb))))+  (origs (na (0 0))))++(comment "Nothing left to do")++(defprotocol ns basic+  (defrole init+    (vars (a b akey) (na nb text))+    (trace (send (enc na a b)) (recv (enc na nb a)) (send (enc nb b))))+  (defrole resp+    (vars (b a akey) (nb na text))+    (trace (recv (enc na a b)) (send (enc na nb a)) (recv (enc nb b))))+  (comment "Needham-Schroeder without rules"))++(defskeleton ns+  (vars (nb na text) (a b akey))+  (defstrand resp 3 (nb nb) (na na) (b b) (a a))+  (non-orig (invk a))+  (uniq-orig nb)+  (comment "Responder point-of-view")+  (traces ((recv (enc na a b)) (send (enc na nb a)) (recv (enc nb b))))+  (label 3)+  (unrealized (0 2))+  (origs (nb (0 1)))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton ns+  (vars (nb na text) (a b b-0 akey))+  (defstrand resp 3 (nb nb) (na na) (b b) (a a))+  (defstrand init 3 (na na) (nb nb) (a a) (b b-0))+  (precedes ((0 1) (1 1)) ((1 2) (0 2)))+  (non-orig (invk a))+  (uniq-orig nb)+  (operation nonce-test (added-strand init 3) nb (0 2) (enc na nb a))+  (traces ((recv (enc na a b)) (send (enc na nb a)) (recv (enc nb b)))+    ((send (enc na a b-0)) (recv (enc na nb a)) (send (enc nb b-0))))+  (label 4)+  (parent 3)+  (unrealized)+  (shape)+  (maps ((0) ((a a) (nb nb) (b b) (na na))))+  (origs (nb (0 1))))++(comment "Nothing left to do")++(defprotocol unilateral basic+  (defrole init+    (vars (n text) (k akey))+    (trace (send (enc n k)) (recv n)))+  (defrole resp+    (vars (n text) (k akey))+    (trace (recv (enc n k)) (send n))))++(defskeleton unilateral+  (vars (n text) (k akey))+  (defstrand init 2 (n n) (k k))+  (non-orig (invk k))+  (uniq-orig n)+  (comment "The shape analysis sentence for this problem:"+    (defgoal unilateral+      (forall ((n text) (k akey) (z strd))+        (implies+          (and (p "init" z 2) (p "init" "n" z n) (p "init" "k" z k)+            (non (invk k)) (uniq-at n z 0))+          (exists ((z-0 strd))+            (and (p "resp" z-0 2) (p "resp" "n" z-0 n)+              (p "resp" "k" z-0 k) (prec z 0 z-0 0)+              (prec z-0 1 z 1)))))))+  (traces ((send (enc n k)) (recv n)))+  (label 5)+  (unrealized (0 1))+  (origs (n (0 0)))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton unilateral+  (vars (n text) (k akey))+  (defstrand init 2 (n n) (k k))+  (defstrand resp 2 (n n) (k k))+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (invk k))+  (uniq-orig n)+  (operation nonce-test (added-strand resp 2) n (0 1) (enc n k))+  (traces ((send (enc n k)) (recv n)) ((recv (enc n k)) (send n)))+  (label 6)+  (parent 5)+  (unrealized)+  (shape)+  (maps ((0) ((k k) (n n))))+  (origs (n (0 0))))++(comment "Nothing left to do")++(defprotocol ns-with-rule basic+  (defrole init+    (vars (a b akey) (na nb text))+    (trace (send (enc na a b)) (recv (enc na nb a)) (send (enc nb b))))+  (defrole resp+    (vars (b a akey) (nb na text))+    (trace (recv (enc na a b)) (send (enc na nb a)) (recv (enc nb b))))+  (defrule unilateral+    (forall ((r strd) (a akey) (nb text))+      (implies+        (and (p "resp" r 3) (p "resp" "a" r a) (p "resp" "nb" r nb)+          (non (invk a)) (uniq nb))+        (exists ((i strd))+          (and (p "init" i 3) (p "init" "a" i a) (p "init" "nb" i nb)+            (prec r 1 i 1) (prec i 2 r 2)))))+    (comment "Unilateral sas under the predicate mapping:")+    (comment (p "init" 2) "->" (p "resp" 3) "and")+    (comment (p "init" "n") "->" (p "resp" "nb") "and")+    (comment (p "init" "k") "->" (p "resp" "a") "and")+    (comment (p "resp" 2) "->" (p "init" 3) "and")+    (comment (p "resp" "n") "->" (p "init" "nb"))+    (comment (p "resp" "k") "->" (p "init" "a")))+  (comment "Needham-Schroeder with rule"))++(defskeleton ns-with-rule+  (vars (nb na text) (a b akey))+  (defstrand resp 3 (nb nb) (na na) (b b) (a a))+  (non-orig (invk a))+  (uniq-orig nb)+  (comment "Responder point-of-view")+  (traces ((recv (enc na a b)) (send (enc na nb a)) (recv (enc nb b))))+  (label 7)+  (unrealized (0 2))+  (origs (nb (0 1)))+  (comment "Not closed under rules"))++(defskeleton ns-with-rule+  (vars (na na-0 nb text) (b a b-0 akey))+  (defstrand resp 3 (nb nb) (na na) (b b) (a a))+  (defstrand init 3 (na na-0) (nb nb) (a a) (b b-0))+  (precedes ((0 1) (1 1)) ((1 2) (0 2)))+  (non-orig (invk a))+  (uniq-orig nb)+  (rule unilateral)+  (traces ((recv (enc na a b)) (send (enc na nb a)) (recv (enc nb b)))+    ((send (enc na-0 a b-0)) (recv (enc na-0 nb a))+      (send (enc nb b-0))))+  (label 8)+  (parent 7)+  (unrealized (1 1))+  (comment "2 in cohort - 2 not yet seen"))++(defskeleton ns-with-rule+  (vars (na nb text) (b a b-0 akey))+  (defstrand resp 3 (nb nb) (na na) (b b) (a a))+  (defstrand init 3 (na na) (nb nb) (a a) (b b-0))+  (precedes ((0 1) (1 1)) ((1 2) (0 2)))+  (non-orig (invk a))+  (uniq-orig nb)+  (operation nonce-test (contracted (na-0 na)) nb (1 1) (enc na nb a))+  (traces ((recv (enc na a b)) (send (enc na nb a)) (recv (enc nb b)))+    ((send (enc na a b-0)) (recv (enc na nb a)) (send (enc nb b-0))))+  (label 9)+  (parent 8)+  (unrealized)+  (shape)+  (maps ((0) ((a a) (nb nb) (b b) (na na))))+  (origs (nb (0 1))))++(defskeleton ns-with-rule+  (vars (na na-0 nb text) (b a b-0 b-1 akey))+  (defstrand resp 3 (nb nb) (na na) (b b) (a a))+  (defstrand init 3 (na na-0) (nb nb) (a a) (b b-0))+  (defstrand init 3 (na na) (nb nb) (a a) (b b-1))+  (precedes ((0 1) (2 1)) ((1 2) (0 2)) ((2 2) (1 1)))+  (non-orig (invk a))+  (uniq-orig nb)+  (operation nonce-test (added-strand init 3) nb (1 1) (enc na nb a))+  (traces ((recv (enc na a b)) (send (enc na nb a)) (recv (enc nb b)))+    ((send (enc na-0 a b-0)) (recv (enc na-0 nb a)) (send (enc nb b-0)))+    ((send (enc na a b-1)) (recv (enc na nb a)) (send (enc nb b-1))))+  (label 10)+  (parent 8)+  (seen 9)+  (unrealized)+  (comment "1 in cohort - 0 not yet seen"))++(comment "Nothing left to do")
tst/reflect.tst view
@@ -1,6 +1,6 @@ (herald reflect) -(comment "CPSA 3.6.3")+(comment "CPSA 3.6.4") (comment "All input read from reflect.scm")  (defprotocol reflect basic
+ tst/role_uniq.scm view
@@ -0,0 +1,56 @@+(herald "Role Unique Origination")++(defprotocol blanchet basic+  (defrole init+    (vars (a b akey) (s skey) (d data))+    (trace+     (send (enc (enc s (invk a)) b))+     (recv (enc d s)))+    (uniq-orig s))+  (defrole resp+    (vars (a b akey) (s skey) (d data))+    (trace+     (recv (enc (enc s (invk a)) b))+     (send (enc d s))))+  (comment "Blanchet's protocol using unnamed asymmetric keys"))++(defskeleton blanchet+  (vars (a b akey) (s skey) (d data))+  (defstrand init 2 (a a) (b b) (s s) (d d))+  (non-orig (invk b))+  (comment "Analyze from the initiator's perspective"))++(defskeleton blanchet+  (vars (a b akey) (s skey) (d data))+  (defstrand resp 2 (a a) (b b) (s s) (d d))+  (non-orig (invk a) (invk b))+  (comment "Analyze from the responder's perspective"))++(defprotocol blanchet basic+  (defrole init+    (vars (a b akey) (s skey) (d data))+    (trace+     (send (enc (enc s (invk a)) b))+     (recv (enc d s))))+  (defrole resp+    (vars (a b akey) (s skey) (d data))+    (trace+     (recv (enc (enc s (invk a)) b))+     (send (enc d s))))+  (defrule role-uniq+    (forall ((z strd) (s skey))+	    (implies (p "init" "s" z s)+		     (uniq s))))+  (comment "Blanchet's protocol using unnamed asymmetric keys"))++(defskeleton blanchet+  (vars (a b akey) (s skey) (d data))+  (defstrand init 2 (a a) (b b) (s s) (d d))+  (non-orig (invk b))+  (comment "Analyze from the initiator's perspective"))++(defskeleton blanchet+  (vars (a b akey) (s skey) (d data))+  (defstrand resp 2 (a a) (b b) (s s) (d d))+  (non-orig (invk a) (invk b))+  (comment "Analyze from the responder's perspective"))
+ tst/role_uniq.tst view
@@ -0,0 +1,247 @@+(herald "Role Unique Origination")++(comment "CPSA 3.6.4")+(comment "All input read from role_uniq.scm")++(defprotocol blanchet basic+  (defrole init+    (vars (a b akey) (s skey) (d data))+    (trace (send (enc (enc s (invk a)) b)) (recv (enc d s)))+    (uniq-orig s))+  (defrole resp+    (vars (a b akey) (s skey) (d data))+    (trace (recv (enc (enc s (invk a)) b)) (send (enc d s))))+  (comment "Blanchet's protocol using unnamed asymmetric keys"))++(defskeleton blanchet+  (vars (d data) (s skey) (a b akey))+  (defstrand init 2 (d d) (s s) (a a) (b b))+  (non-orig (invk b))+  (uniq-orig s)+  (comment "Analyze from the initiator's perspective")+  (traces ((send (enc (enc s (invk a)) b)) (recv (enc d s))))+  (label 0)+  (unrealized (0 1))+  (origs (s (0 0)))+  (comment "2 in cohort - 2 not yet seen"))++(defskeleton blanchet+  (vars (d data) (s skey) (a b a-0 b-0 akey))+  (defstrand init 2 (d d) (s s) (a a) (b b))+  (defstrand resp 2 (d d) (s s) (a a-0) (b b-0))+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (invk b))+  (uniq-orig s)+  (operation encryption-test (added-strand resp 2) (enc d s) (0 1))+  (traces ((send (enc (enc s (invk a)) b)) (recv (enc d s)))+    ((recv (enc (enc s (invk a-0)) b-0)) (send (enc d s))))+  (label 1)+  (parent 0)+  (unrealized (1 0))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton blanchet+  (vars (d data) (s skey) (a b akey))+  (defstrand init 2 (d d) (s s) (a a) (b b))+  (deflistener s)+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (invk b))+  (uniq-orig s)+  (operation encryption-test (added-listener s) (enc d s) (0 1))+  (traces ((send (enc (enc s (invk a)) b)) (recv (enc d s)))+    ((recv s) (send s)))+  (label 2)+  (parent 0)+  (unrealized (1 0))+  (dead)+  (comment "empty cohort"))++(defskeleton blanchet+  (vars (d data) (s skey) (a b akey))+  (defstrand init 2 (d d) (s s) (a a) (b b))+  (defstrand resp 2 (d d) (s s) (a a) (b b))+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (invk b))+  (uniq-orig s)+  (operation nonce-test (contracted (a-0 a) (b-0 b)) s (1 0)+    (enc (enc s (invk a)) b))+  (traces ((send (enc (enc s (invk a)) b)) (recv (enc d s)))+    ((recv (enc (enc s (invk a)) b)) (send (enc d s))))+  (label 3)+  (parent 1)+  (unrealized)+  (shape)+  (maps ((0) ((a a) (b b) (s s) (d d))))+  (origs (s (0 0))))++(comment "Nothing left to do")++(defprotocol blanchet basic+  (defrole init+    (vars (a b akey) (s skey) (d data))+    (trace (send (enc (enc s (invk a)) b)) (recv (enc d s)))+    (uniq-orig s))+  (defrole resp+    (vars (a b akey) (s skey) (d data))+    (trace (recv (enc (enc s (invk a)) b)) (send (enc d s))))+  (comment "Blanchet's protocol using unnamed asymmetric keys"))++(defskeleton blanchet+  (vars (d data) (s skey) (a b akey))+  (defstrand resp 2 (d d) (s s) (a a) (b b))+  (non-orig (invk a) (invk b))+  (comment "Analyze from the responder's perspective")+  (traces ((recv (enc (enc s (invk a)) b)) (send (enc d s))))+  (label 4)+  (unrealized (0 0))+  (origs)+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton blanchet+  (vars (d data) (s skey) (a b b-0 akey))+  (defstrand resp 2 (d d) (s s) (a a) (b b))+  (defstrand init 1 (s s) (a a) (b b-0))+  (precedes ((1 0) (0 0)))+  (non-orig (invk a) (invk b))+  (uniq-orig s)+  (operation encryption-test (added-strand init 1) (enc s (invk a))+    (0 0))+  (traces ((recv (enc (enc s (invk a)) b)) (send (enc d s)))+    ((send (enc (enc s (invk a)) b-0))))+  (label 5)+  (parent 4)+  (unrealized)+  (shape)+  (maps ((0) ((a a) (b b) (s s) (d d))))+  (origs (s (1 0))))++(comment "Nothing left to do")++(defprotocol blanchet basic+  (defrole init+    (vars (a b akey) (s skey) (d data))+    (trace (send (enc (enc s (invk a)) b)) (recv (enc d s))))+  (defrole resp+    (vars (a b akey) (s skey) (d data))+    (trace (recv (enc (enc s (invk a)) b)) (send (enc d s))))+  (defrule role-uniq+    (forall ((z strd) (s skey)) (implies (p "init" "s" z s) (uniq s))))+  (comment "Blanchet's protocol using unnamed asymmetric keys"))++(defskeleton blanchet+  (vars (d data) (s skey) (a b akey))+  (defstrand init 2 (d d) (s s) (a a) (b b))+  (non-orig (invk b))+  (comment "Analyze from the initiator's perspective")+  (traces ((send (enc (enc s (invk a)) b)) (recv (enc d s))))+  (label 6)+  (unrealized)+  (origs)+  (comment "Not closed under rules"))++(defskeleton blanchet+  (vars (d data) (s skey) (a b akey))+  (defstrand init 2 (d d) (s s) (a a) (b b))+  (non-orig (invk b))+  (uniq-orig s)+  (rule role-uniq)+  (traces ((send (enc (enc s (invk a)) b)) (recv (enc d s))))+  (label 7)+  (parent 6)+  (unrealized (0 1))+  (origs (s (0 0)))+  (comment "2 in cohort - 2 not yet seen"))++(defskeleton blanchet+  (vars (d data) (s skey) (a b a-0 b-0 akey))+  (defstrand init 2 (d d) (s s) (a a) (b b))+  (defstrand resp 2 (d d) (s s) (a a-0) (b b-0))+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (invk b))+  (uniq-orig s)+  (operation encryption-test (added-strand resp 2) (enc d s) (0 1))+  (traces ((send (enc (enc s (invk a)) b)) (recv (enc d s)))+    ((recv (enc (enc s (invk a-0)) b-0)) (send (enc d s))))+  (label 8)+  (parent 7)+  (unrealized (1 0))+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton blanchet+  (vars (d data) (s skey) (a b akey))+  (defstrand init 2 (d d) (s s) (a a) (b b))+  (deflistener s)+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (invk b))+  (uniq-orig s)+  (operation encryption-test (added-listener s) (enc d s) (0 1))+  (traces ((send (enc (enc s (invk a)) b)) (recv (enc d s)))+    ((recv s) (send s)))+  (label 9)+  (parent 7)+  (unrealized (1 0))+  (dead)+  (comment "empty cohort"))++(defskeleton blanchet+  (vars (d data) (s skey) (a b akey))+  (defstrand init 2 (d d) (s s) (a a) (b b))+  (defstrand resp 2 (d d) (s s) (a a) (b b))+  (precedes ((0 0) (1 0)) ((1 1) (0 1)))+  (non-orig (invk b))+  (uniq-orig s)+  (operation nonce-test (contracted (a-0 a) (b-0 b)) s (1 0)+    (enc (enc s (invk a)) b))+  (traces ((send (enc (enc s (invk a)) b)) (recv (enc d s)))+    ((recv (enc (enc s (invk a)) b)) (send (enc d s))))+  (label 10)+  (parent 8)+  (unrealized)+  (shape)+  (maps ((0) ((a a) (b b) (s s) (d d))))+  (origs (s (0 0))))++(comment "Nothing left to do")++(defprotocol blanchet basic+  (defrole init+    (vars (a b akey) (s skey) (d data))+    (trace (send (enc (enc s (invk a)) b)) (recv (enc d s))))+  (defrole resp+    (vars (a b akey) (s skey) (d data))+    (trace (recv (enc (enc s (invk a)) b)) (send (enc d s))))+  (defrule role-uniq+    (forall ((z strd) (s skey)) (implies (p "init" "s" z s) (uniq s))))+  (comment "Blanchet's protocol using unnamed asymmetric keys"))++(defskeleton blanchet+  (vars (d data) (s skey) (a b akey))+  (defstrand resp 2 (d d) (s s) (a a) (b b))+  (non-orig (invk a) (invk b))+  (comment "Analyze from the responder's perspective")+  (traces ((recv (enc (enc s (invk a)) b)) (send (enc d s))))+  (label 11)+  (unrealized (0 0))+  (origs)+  (comment "1 in cohort - 1 not yet seen"))++(defskeleton blanchet+  (vars (d data) (s skey) (a b b-0 akey))+  (defstrand resp 2 (d d) (s s) (a a) (b b))+  (defstrand init 1 (s s) (a a) (b b-0))+  (precedes ((1 0) (0 0)))+  (non-orig (invk a) (invk b))+  (uniq-orig s)+  (rule role-uniq)+  (operation encryption-test (added-strand init 1) (enc s (invk a))+    (0 0))+  (traces ((recv (enc (enc s (invk a)) b)) (send (enc d s)))+    ((send (enc (enc s (invk a)) b-0))))+  (label 12)+  (parent 11)+  (unrealized)+  (shape)+  (maps ((0) ((a a) (b b) (s s) (d d))))+  (origs (s (1 0))))++(comment "Nothing left to do")
+ tst/rule-order.scm view
@@ -0,0 +1,21 @@+(herald rule-order)++(defprotocol rule-order basic+  (defrole init+    (vars (s t text))+    (trace+     (send (cat s t))))++  (defrule ge+    (forall ((x y text))+	    (implies+	     (fact le x y)+	     (or+	      (= x y)+	      (fact lt x y)))))+  )++(defskeleton rule-order+  (vars (s t text))+  (defstrand init 1 (s s) (t t))+  (facts (le s t)))
+ tst/rule-order.tst view
@@ -0,0 +1,48 @@+(herald rule-order)++(comment "CPSA 3.6.4")+(comment "All input read from rule-order.scm")++(defprotocol rule-order basic+  (defrole init (vars (s t text)) (trace (send (cat s t))))+  (defrule ge+    (forall ((x y text))+      (implies (fact le x y) (or (= x y) (fact lt x y))))))++(defskeleton rule-order+  (vars (s t text))+  (defstrand init 1 (s s) (t t))+  (facts (le s t))+  (traces ((send (cat s t))))+  (label 0)+  (unrealized)+  (origs)+  (comment "Not closed under rules"))++(defskeleton rule-order+  (vars (t text))+  (defstrand init 1 (s t) (t t))+  (facts (le t t))+  (rule ge)+  (traces ((send (cat t t))))+  (label 1)+  (parent 0)+  (unrealized)+  (shape)+  (maps ((0) ((s t) (t t))))+  (origs))++(defskeleton rule-order+  (vars (s t text))+  (defstrand init 1 (s s) (t t))+  (facts (lt s t) (le s t))+  (rule ge)+  (traces ((send (cat s t))))+  (label 2)+  (parent 0)+  (unrealized)+  (shape)+  (maps ((0) ((s s) (t t))))+  (origs))++(comment "Nothing left to do")
tst/staticdh.tst view
@@ -1,6 +1,6 @@ (herald "Static DH key exchange" (algebra diffie-hellman)) -(comment "CPSA 3.6.3")+(comment "CPSA 3.6.4") (comment "All input read from staticdh.scm")  (defprotocol staticdh1 diffie-hellman
tst/station.tst view
@@ -1,6 +1,6 @@ (herald "Station-to-station protocol" (algebra diffie-hellman)) -(comment "CPSA 3.6.3")+(comment "CPSA 3.6.4") (comment "All input read from station.scm")  (defprotocol station-to-station diffie-hellman
tst/station2.tst view
@@ -1,6 +1,6 @@ (herald "Station-to-station protocol" (algebra diffie-hellman)) -(comment "CPSA 3.6.3")+(comment "CPSA 3.6.4") (comment "All input read from station2.scm")  (defprotocol station-to-station diffie-hellman
tst/subsort_test.tst view
@@ -2,7 +2,7 @@   (comment "First, third, and fourth skeletons should have a shape,"     "second should be dead.")) -(comment "CPSA 3.6.3")+(comment "CPSA 3.6.4") (comment "All input read from subsort_test.scm")  (defprotocol subsorttest basic
tst/test_small.tst view
@@ -1,6 +1,6 @@ (herald "small test" (algebra diffie-hellman)) -(comment "CPSA 3.6.3")+(comment "CPSA 3.6.4") (comment "All input read from test_small.scm")  (defprotocol test diffie-hellman
+ tst/trust-anchor.scm view
@@ -0,0 +1,19 @@+(herald trust-anchor+	(comment "Tests rule application on initial skeleton"))++(defprotocol trust-anchor basic+  ;;; trust-anchor property guarantees non+  (defrule trust-anchor-inverse-is-non+    (forall ((k akey))+	    (implies (fact trust-anchor k)+		     (non (invk k))))))++(defskeleton trust-anchor+  (vars (f ca name))+  (deflistener (enc f (pubk f) (privk ca)))+  (non-orig (privk ca)))++(defskeleton trust-anchor+  (vars (f ca name))+  (deflistener (enc f (pubk f) (privk ca)))+  (facts (trust-anchor (pubk ca))))
+ tst/trust-anchor.tst view
@@ -0,0 +1,58 @@+(herald trust-anchor+  (comment "Tests rule application on initial skeleton"))++(comment "CPSA 3.6.4")+(comment "All input read from trust-anchor.scm")++(defprotocol trust-anchor basic+  (defrule trust-anchor-inverse-is-non+    (forall ((k akey)) (implies (fact trust-anchor k) (non (invk k))))))++(defskeleton trust-anchor+  (vars (f ca name))+  (deflistener (enc f (pubk f) (privk ca)))+  (non-orig (privk ca))+  (traces+    ((recv (enc f (pubk f) (privk ca)))+      (send (enc f (pubk f) (privk ca)))))+  (label 0)+  (unrealized (0 0))+  (dead)+  (origs)+  (comment "empty cohort"))++(comment "Nothing left to do")++(defprotocol trust-anchor basic+  (defrule trust-anchor-inverse-is-non+    (forall ((k akey)) (implies (fact trust-anchor k) (non (invk k))))))++(defskeleton trust-anchor+  (vars (f ca name))+  (deflistener (enc f (pubk f) (privk ca)))+  (facts (trust-anchor (pubk ca)))+  (traces+    ((recv (enc f (pubk f) (privk ca)))+      (send (enc f (pubk f) (privk ca)))))+  (label 1)+  (unrealized)+  (origs)+  (comment "Not closed under rules"))++(defskeleton trust-anchor+  (vars (f ca name))+  (deflistener (enc f (pubk f) (privk ca)))+  (non-orig (privk ca))+  (facts (trust-anchor (pubk ca)))+  (rule trust-anchor-inverse-is-non)+  (traces+    ((recv (enc f (pubk f) (privk ca)))+      (send (enc f (pubk f) (privk ca)))))+  (label 2)+  (parent 1)+  (unrealized (0 0))+  (dead)+  (origs)+  (comment "empty cohort"))++(comment "Nothing left to do")
tst/unilateral.tst view
@@ -1,6 +1,6 @@ (herald unilateral) -(comment "CPSA 3.6.3")+(comment "CPSA 3.6.4") (comment "All input read from unilateral.scm")  (defprotocol unilateral basic
tst/uniq-gen-test.tst view
@@ -1,7 +1,7 @@ (herald "Unique generation test protocols."   (comment "Skeletons 2, 4, and 7 should have no shapes.")) -(comment "CPSA 3.6.3")+(comment "CPSA 3.6.4") (comment "All input read from uniq-gen-test.scm")  (defprotocol uniqgentest basic
tst/woolam.tst view
@@ -1,6 +1,6 @@ (herald "Woo-Lam Protocol") -(comment "CPSA 3.6.3")+(comment "CPSA 3.6.4") (comment "All input read from woolam.scm")  (defprotocol woolam basic
tst/wrap_decrypt.tst view
@@ -1,6 +1,6 @@ (herald wrap-decrypt (bound 10)) -(comment "CPSA 3.6.3")+(comment "CPSA 3.6.4") (comment "All input read from wrap_decrypt.lsp") (comment "Strand count bounded at 10")
tst/yahalom.tst view
@@ -1,7 +1,7 @@ (herald "Yahalom Protocol with Forwarding Removed"   (algebra diffie-hellman) (bound 12)) -(comment "CPSA 3.6.3")+(comment "CPSA 3.6.4") (comment "All input read from yahalom.scm")  (defprotocol yahalom diffie-hellman