tamarin-prover 0.8.0.0 → 0.8.1.0
raw patch · 23 files changed
+480/−208 lines, 23 filesdep +dlistdep ~tamarin-prover-termdep ~tamarin-prover-utils
Dependencies added: dlist
Dependency ranges changed: tamarin-prover-term, tamarin-prover-utils
Files
- .ghci +1/−1
- data/CHANGES +18/−0
- data/examples/loops/TESLA_Scheme1.spthy +49/−58
- data/examples/loops/Typing_and_Destructors.spthy +122/−0
- data/js/tamarin-prover-ui.js +32/−22
- interactive-only-src/Paths_tamarin_prover.hs +1/−1
- src/Main/Mode/Batch.hs +4/−1
- src/Main/TheoryLoader.hs +15/−8
- src/Theory.hs +32/−20
- src/Theory/Constraint/Solver/CaseDistinctions.hs +25/−28
- src/Theory/Constraint/Solver/Goals.hs +28/−12
- src/Theory/Constraint/Solver/ProofMethod.hs +18/−12
- src/Theory/Constraint/Solver/Reduction.hs +10/−6
- src/Theory/Constraint/System.hs +29/−13
- src/Theory/Constraint/System/Guarded.hs +41/−4
- src/Theory/Text/Parser/Token.hs +1/−1
- src/Theory/Tools/EquationStore.hs +2/−1
- src/Theory/Tools/Wellformedness.hs +12/−0
- src/Web/Dispatch.hs +2/−1
- src/Web/Handler.hs +11/−6
- src/Web/Theory.hs +14/−9
- src/Web/Types.hs +1/−1
- tamarin-prover.cabal +12/−3
.ghci view
@@ -2,4 +2,4 @@ -- :set -ilib/term/src -- :set -ilib/utils/src :set -isrc-:set -Wall+:set -Wall -fwarn-tabs
data/CHANGES view
@@ -1,3 +1,21 @@+* 0.8.1.0+ - enabled parallelization by default when compiling `tamarin-prover` with+ GHC 7.4 and higher. It uses as many threads as there are CPU cores on+ the system. Use `tamarin-prover +RTS -N1 -RTS` to use only one thread.++ - fixed: lemmas proven for some trace ('exists-trace') and marked with+ the [reuse] attribute were wrongly used in the proof of other lemmas.+ - fixed: axioms that are not safety formulas were not transformed+ properly when applying induction.+ - fixed: fresh name generation was not always handled properly when+ applying a precomputed case distinction to a goal that uses+ DH-exponentiation. Security protocol models that use DH-exponentiation+ should be checked again. Some of our case studies were indeed missing+ a few cases, but no property changed its validity.+ - fixed: no more case names containing spaces,+ when solving deconstruction chains.+ - fixed: avoid solving KU-goals for nullary function symbols+ * 0.8.0.0 - new homepage: http://www.infsec.ethz.ch/research/software/tamarin - mailing list: https://groups.google.com/group/tamarin-prover
data/examples/loops/TESLA_Scheme1.spthy view
@@ -60,17 +60,18 @@ // Setup phase ////////////// -// We choose a fresh start key and provide facts for sending and answering-// receiver connection requests.+// A sender knows is own identity $S. He chooses a fresh key to start sending+// a new authenticated stream. We provide facts for sending the stream and for+// answering receiver connection requests. rule Sender_Setup: [ Fr(~k1) ] -->- [ Sender1(~k1), !Sender0a(~k1) ]+ [ Sender1($S, ~k1), !Sender0a($S, ~k1) ] // Everybody can listen in by sending a request for the commitment to the // first key. rule Sender0a:- [ !Sender0a(k1)+ [ !Sender0a(S, k1) , In( < R, S, nR> ) , !Ltk(S, ltkS) ]@@ -78,73 +79,64 @@ [ Out( <S, R, f(k1), sign{ f(k1), nR}ltkS> ) ] // Receivers start by requesting the commitment to the first key and verifying-// the signature on this commitment.+// the signature on this commitment. We use the receiver nonce to identify+// receivers. rule Receiver0a:- [ Fr( ~nR ) ]+ [ Fr( ~rid ) ] -->- [ Out( < $R, $S, ~nR > )- , Receiver0b( $R, $S, ~nR ) ]+ [ Out( < $R, $S, ~rid > )+ , Receiver0b( ~rid, $R, $S ) ] rule Receiver0b:- [ Receiver0b ( R, S, nR )+ [ Receiver0b ( rid, R, S ) , !Pk( S, pkS)- , In( <S, R, k2, signature> )+ , In( <S, R, commit_k1, signature> ) ] -->- [ Receiver0b_check(S, k2, verify(signature, <k2, nR>, pkS)) ]+ [ Receiver0b_check( rid, S, commit_k1+ , verify(signature, <commit_k1, rid>, pkS)) ] rule Receiver0b_check:- [ Receiver0b_check(S, k2, true) ]+ [ Receiver0b_check(rid, S, commit_k1, true) ] -->- [ Receiver1( S, k2 ) ]+ [ Receiver1( rid, S, commit_k1 ) ] -/* The following setup-phase allows for a simpler proof.--rule Setup:- [ Fr(~k1) ]- -->- [ Sender1(~k1)- , Receiver1(f(~k1))- ]--*/- // Authenticated broadcasting rule Send1: let data1 = <'1', ~m1, f(~k2)> in- [ Sender1(~k1)+ [ Sender1(S, ~k1) , Fr(~m1) , Fr(~k2) ]- --[ Sent(data1)+ --[ Sent(S, data1) ]->- [ Sender(~k1, ~k2)+ [ Sender(S, ~k1, ~k2) , Out( < data1, MAC{data1}~k1 > ) ] rule Recv1: let data1 = <'1', m1, commit_k2> in- [ Receiver1(S, commit_k1)+ [ Receiver1(rid, S, commit_k1) , In( <data1, mac1> ) ]- --[ AssumeCommitNotExpired(commit_k1)+ --[ AssumeCommitNotExpired(rid, commit_k1) ]->- [ Receiver(S, data1, mac1, commit_k1, commit_k2) ]+ [ Receiver(rid, S, data1, mac1, commit_k1, commit_k2) ] rule SendN: let data = <'N', ~m, f(~kNew), ~kOld> in- [ Sender(~kOld, ~k)+ [ Sender(S, ~kOld, ~k) , Fr(~m) , Fr(~kNew) ]- --[ Sent(data)+ --[ Sent(S, data) , CommitExpired(f(~kOld)) ]->- [ Sender(~k, ~kNew)+ [ Sender(S, ~k, ~kNew) , Out( <data, MAC{data}~k> ) ] @@ -152,31 +144,32 @@ let data = <'N', m, commit_kNew, kOld> in [ In(< data, mac >)- , Receiver(S, dataOld, MAC{dataOld}kOld, f(kOld), commit_k)+ , Receiver(rid, S, dataOld, MAC{dataOld}kOld, f(kOld), commit_k) ]- --[ FromSender(S, dataOld)- , AssumeCommitNotExpired(commit_k)+ --[ FromSender(rid, S, dataOld)+ , AssumeCommitNotExpired(rid, commit_k) ]->- [ Receiver(S, data, mac, commit_k, commit_kNew) ]+ [ Receiver(rid, S, data, mac, commit_k, commit_kNew) ] -// The desired security property: if all commits expired after all asumptions-// that they are not expired, then we have message authentication provided the-// long-term key of the server was not revealed.-//-// Note that we could strengthen this property such that only expiredness of-// commits in this broadcasting session before the 'FromSender'-claim is-// required.+/*+The desired security property: if all expiredness assumptions of the test+thread are given and the server that is sending was not compromised before,+then received data was sent by the server.+*/ lemma authentic [use_induction]:- "(All commit #i #j .- AssumeCommitNotExpired(commit) @ i- & CommitExpired(commit) @ j- ==> i < j- )- ==>- (All S m #i. FromSender(S, m) @ i ==>- ( (Ex #j. Sent(m) @ j & j < i)+ /* For every reciever claiming that it received data 'm' from the server, */+ "(All rid S m #i. FromSender(rid, S, m) @ i ==>+ /* the server actually sent that data */+ ( (Ex #j. Sent(S, m) @ j & j < i)+ /* or the server's longterm key was compromised before the claim */ | (Ex #j. RevealLtk(S) @ j & j < i)+ /* or one of the receivers expiredness assumptions before the claim+ was not met. */+ | (Ex commit #ne #e. AssumeCommitNotExpired(rid, commit) @ ne+ & CommitExpired(commit) @ e+ & e < ne+ & ne < i) ) ) "@@ -184,14 +177,12 @@ // Ensure that the above lemma is not vacuous due to the filtering condition. lemma authentic_reachable [use_induction]: exists-trace- "(All commit #i #j .- AssumeCommitNotExpired(commit) @ i+ "(All rid commit #i #j .+ AssumeCommitNotExpired(rid, commit) @ i & CommitExpired(commit) @ j ==> i < j- )- &- (Ex S m #i. FromSender(S, m) @ i)- "+ ) &+ (Ex rid S m #i. FromSender(rid, S, m) @ i) " end
+ data/examples/loops/Typing_and_Destructors.spthy view
@@ -0,0 +1,122 @@+theory Typing_and_Destructors+begin++/*+ Protocol: Demonstration of the interaction between typing and+ destructors+ Modeler: Simon Meier+ Date: July 2012++ Status: working / misses theory extension (see issue #104)++ This protocol is a variant of 'Minimal_Typing_Example' that uses explicit+ destructors. Its verification does not yet work out of the box, as the+ implemented definition of guarded trace properties is too restrictive to+ allow formalizing the required type invariant.++ NOTE that it seems that the best option is to explicitly state in a rule+ that it does not continue in case the application of a deconstructor was+ not successful using an axiom like 'No_failure_terms'. This considerably+ simplifies the verification.+*/+++builtins: symmetric-encryption, hashing++// Shared keys that can be compromised.+rule Setup_Key:+ [ Fr(~k) ] --[ IsKey(~k) ]-> [ !Key(~k) ]++rule Reveal_Key:+ [ !Key(k) ] --[ Rev(k) ]-> [ Out(k) ]++rule Initiator:+ let msg = senc{~sec,~pub}k+ in+ [ !Key(k), Fr(~sec), Fr(~pub) ]+ --[ Out_Initiator(msg)+ , Public(~pub)+ ]->+ [ Out( msg ) ]++rule Responder:+ // We use explicit destructors instead of the pattern matching+ //+ // msg = senc{sec,pub}key+ //+ // This explicit use of destructors is more permissive (i.e., allows more+ // traces), as it allows the rule to fire even if an failure term is sent.+ //+ let body = sdec{msg}key+ sec = fst(body)+ pub = snd(body)+ in+ [ !Key(key), In( msg )+ ]+ --[ In_Responder(msg, pub)+ , Secret(sec, key)+ // We can simulate pattern matching by logging that the 'pub' term must+ // not be an failure term.+ , NoFailureTerm(pub)+ ]->+ [ Out( pub ) ]++// Commented out to test the type assertion.+//+// // This axiom then filters all traces with disallowed failure terms.+// // Note that we interpret its formula modulo AC.+// axiom No_failure_terms:+// "(All x #i. NoFailureTerm(snd(x)) @ i ==> F)"+// // Here we should also exclude all other possible shapes of failure terms.++// This type assertion does not hold, as 'pub' could be an failure term. See the+// case marked below for the missing piece of the puzzle.+// Note that we interpret its formula modulo AC.+lemma type_assertion [typing]:+ /* For all messages received by the responder */+ "(All m pub #i. In_Responder(m, pub) @ i ==>+ /* they either came from the adversary and he therefore knows the+ * contained 'k' variable before it was instantiated */+ ( (Ex #j. KU(pub) @ j & j < i)+ /* or there is an initiator that sent 'm'. */+ | (Ex #j. Out_Initiator(m) @ j)+ // These two cases cover the failure cases and make the type assertion+ // valid. They are also sufficient to prove the statements below.+ // They are currently not wellformed because 'snd' and 'sdec' are not+ // allowed in formulas.+ | (Ex body #j. KU(body) @ j+ & pub = snd(body) & j < i)+ | (Ex body key #j #k. IsKey(key)@k & KU(body) @ j+ & pub = snd(sdec{body}key) & j < i)+ // Note that I thinkg that these two cases might be sufficient. They+ // would however require that equalities can also be guarding.+ // | (Ex body. pub = snd(body))+ // | (Ex body key. pub = snd(sdec{body}key))+ )+ )+ "++/* The secret part of the message received by Responder is secret provided the+ * key has not been compromised.+ */+lemma Responder_secrecy:+ " All sec key #i #j.+ Secret(sec, key) @ #i+ & K(sec) @ #j+ ==>+ (Ex #r. Rev(key) @ r)+ "++/* Sanity check: the public part is accessible to the adversary without+ * performing a key reveal.+ */+lemma Public_part_public:+ exists-trace+ " /* No key reveal has been performed */+ not (Ex k #i. Rev(k) @ i)+ /* and the public part of a message is known to the adversary. */+ & (Ex pub #i #j. Public(pub) @ i & K(pub) @ j )+ "+++end
data/js/tamarin-prover-ui.js view
@@ -186,15 +186,15 @@ }); // Enable context menu- $("#proof a.proof-step").contextMenu(- { menu: "contextMenu" },- function(action, el, pos) {- var theoryPath = theory.extractTheoryPath($(el).attr("href"));- mainDisplay.loadTarget(- theory.absolutePath(action,theoryPath),- null- );- });+ // $("#proof a.proof-step").contextMenu(+ // { menu: "contextMenu" },+ // function(action, el, pos) {+ // var theoryPath = theory.extractTheoryPath($(el).attr("href"));+ // mainDisplay.loadTarget(+ // theory.absolutePath(action,theoryPath),+ // null+ // );+ // }); // Click handler for save link events.installAbsoluteClickHandler("a.save-link", server.handleJson);@@ -249,26 +249,27 @@ // Install handlers on plain internal links events.installRelativeClickHandler( "div#proof a.internal-link",- "main",+ null, null); + // FIXME: delete is disabled // Install handlers on delete links- events.installRelativeClickHandler(- "div#proof a.internal-link.delete-link",- "del/path",- null);+ // events.installRelativeClickHandler(+ // "div#proof a.internal-link.delete-link",+ // "del/path",+ // null); // Install handlers on proof-step links events.installRelativeClickHandler( "div#proof a.internal-link.proof-step",- "main",+ null, null ); // Install click handlers on main events.installRelativeClickHandler( "div#ui-main-display a.internal-link",- "main",+ null, null); // Install handlers on removal links@@ -335,7 +336,7 @@ // callback function and pass keycode if(map[key]) { // Hide context menu- $("ul#contextMenu").hide();+ // $("ul#contextMenu").hide(); // Call callback var callback = map[key]; callback(key);@@ -379,7 +380,7 @@ installScrollHandler: function(name, selector) { $(selector).scroll(function(ev) { // Hide context menu- $("ul#contextMenu").hide();+ // $("ul#contextMenu").hide(); // Record position in cookie var pos = $(this).scrollTop(); $.cookie(name + "-position", pos, { path: "/" });@@ -419,10 +420,19 @@ // Add new click handler $(selector).click(function(ev) { ev.preventDefault();- var element = $(this);++ // FIXME: always set the right link on the Haskell side+ // and get rid of section+ path = $(this).attr("href");+ if(section) {+ // replace section in path+ elementPath = $(this).attr("href").split("/");+ elementPath[3] = section;+ path = elementPath.join("/");+ }+ mainDisplay.loadTarget(- // section,- element.attr("href"),+ path, function() { if(callback) callback(element); });@@ -665,7 +675,7 @@ // Re-install click handlers on main events.installRelativeClickHandler( "div#ui-main-display a.internal-link",- "main",+ null, null); },
interactive-only-src/Paths_tamarin_prover.hs view
@@ -12,7 +12,7 @@ version :: Version-version = Version {versionBranch = [0,8,0,0], versionTags = []}+version = Version {versionBranch = [0,8,1,0], versionTags = []} bindir, libdir, datadir, libexecdir :: FilePath bindir = "./"
src/Main/Mode/Batch.hs view
@@ -12,6 +12,8 @@ ) where import Control.Basics+import Control.DeepSeq (force)+import Control.Exception (evaluate) import Data.List import Data.Maybe import System.Console.CmdArgs.Explicit as CmdArgs@@ -142,7 +144,8 @@ (thySummary, t) <- timed $ do thy <- load writeFileWithDirs outFile $ renderDoc $ fullDoc thy- return $ summaryDoc thy+ -- ensure that the summary is in normal form+ evaluate $ force $ summaryDoc thy let summary = Pretty.vcat [ ppAnalyzed , Pretty.text $ ""
src/Main/TheoryLoader.hs view
@@ -105,30 +105,37 @@ where (loadOpen, close) = loadThy as -loadClosedThyString :: Arguments -> String -> IO ClosedTheory-loadClosedThyString = uncurry (>=>) . loadThyString+loadClosedThyString :: Arguments -> String -> IO (Either String ClosedTheory)+loadClosedThyString as file = do+ let (loader, closer) = loadThyString as+ openThy <- loader file+ case openThy of+ Right thy -> Right <$> closer thy+ Left err -> return $ Left err -- | Load an open/closed theory from a file. loadThy :: Arguments -> (FilePath -> IO OpenTheory, OpenTheory -> IO ClosedTheory) loadThy as = loadGenericThy (parseOpenTheory (defines as)) as -- | Load an open/closed theory from a string.-loadThyString :: Arguments -> (String -> IO OpenTheory, OpenTheory -> IO ClosedTheory)+loadThyString :: Arguments -> ( String -> IO (Either String OpenTheory)+ , OpenTheory -> IO ClosedTheory) loadThyString as = loadGenericThy loader as where loader str = case parseOpenTheoryString (defines as) str of- Right thy -> return thy- Left err -> error $ show err+ Right thy -> return $ Right thy+ Left err -> return $ Left $ "parse error: " ++ show err -- | The defined pre-processor flags in the argument. defines :: Arguments -> [String] defines = findArg "defines" +-- FIXME: SM: This naming, tupling, blah is a mess and can be done more+-- cleanly. DO IT!+ -- | Load an open/closed theory given a loader function.-loadGenericThy :: (a -> IO OpenTheory)- -> Arguments- -> (a -> IO OpenTheory, OpenTheory -> IO ClosedTheory)+loadGenericThy :: a -> Arguments -> (a, OpenTheory -> IO ClosedTheory) loadGenericThy loader as = (loader, (closeThy as) <=< addMessageDeductionRuleVariants)
src/Theory.hs view
@@ -38,6 +38,7 @@ , thyCache , thyItems , theoryRules+ , theoryLemmas , theoryAxioms , addAxiom , addLemma@@ -201,11 +202,10 @@ -- soundness sequent, if required. closeProtoRule :: MaudeHandle -> OpenProtoRule -> ClosedProtoRule closeProtoRule hnd ruE = ClosedProtoRule ruE (variantsProtoRule hnd ruE)- -- | Close a rule cache. Hower, note that the -- requires case distinctions are not computed here.-closeRuleCache :: [LNFormula] -- ^ Axioms to use.- -> [LNFormula] -- ^ Typing lemmas to use.+closeRuleCache :: [LNGuarded] -- ^ Axioms to use.+ -> [LNGuarded] -- ^ Typing lemmas to use. -> SignatureWithMaude -- ^ Signature of theory. -> [ClosedProtoRule] -- ^ Protocol rules with variants. -> OpenRuleCache -- ^ Intruder rules modulo AC.@@ -222,8 +222,11 @@ injFactInstances = simpleInjectiveFactInstances $ L.get cprRuleE <$> protoRules - -- precomputing the case distinctions- untypedCaseDists = precomputeCaseDistinctions ctxt0 axioms+ -- precomputing the case distinctions: we make sure to only add safety+ -- axioms. Otherwise, it wouldn't be sound to use the precomputed case+ -- distinctions for properties proven using induction.+ safetyAxioms = filter isSafetyFormula axioms+ untypedCaseDists = precomputeCaseDistinctions ctxt0 safetyAxioms typedCaseDists = refineWithTypingAsms typAsms ctxt0 untypedCaseDists -- classifying the rules@@ -608,10 +611,11 @@ TextItem -- extract typing axioms and lemmas- axioms = [ L.get axFormula ax | AxiomItem ax <- items ]+ axioms = do AxiomItem ax <- items+ return $ formulaToGuarded_ $ L.get axFormula ax typAsms = do LemmaItem lem <- items guard (isTypingLemma lem)- return $ L.get lFormula lem+ return $ formulaToGuarded_ $ L.get lFormula lem -- extract protocol rules rules = theoryRules (Theory errClose errClose errClose items)@@ -689,21 +693,26 @@ add prf = fromMaybe prf $ runProver prover ctxt 0 sys prf -- | Construct a constraint system for verifying the given formula.-mkSystem :: ProofContext -> [Axiom] -> [TheoryItem r p] -> LNFormula -> System-mkSystem ctxt axioms preItems =- addAxiomsAndLemmasToSystem- . formulaToSystem (L.get pcCaseDistKind ctxt) (L.get pcTraceQuantifier ctxt)+mkSystem :: ProofContext -> [Axiom] -> [TheoryItem r p]+ -> LNFormula -> System+mkSystem ctxt axioms previousItems =+ -- Note that it is OK to add reusable lemmas directly to the system, as+ -- they do not change the considered set of traces. This is the key+ -- difference between lemmas and axioms.+ addLemmas+ . formulaToSystem (map (formulaToGuarded_ . L.get axFormula) axioms)+ (L.get pcCaseDistKind ctxt)+ (L.get pcTraceQuantifier ctxt) where- addAxiomsAndLemmasToSystem sys =- (`insertLemmas` sys) $- map (L.get axFormula) axioms ++- gatherReusableLemmas (L.get sCaseDistKind sys)+ addLemmas sys =+ insertLemmas (gatherReusableLemmas $ L.get sCaseDistKind sys) sys gatherReusableLemmas kind = do- LemmaItem lem <- preItems- guard $ lemmaCaseDistKind lem <= kind &&- ReuseLemma `elem` L.get lAttributes lem- return $ L.get lFormula lem+ LemmaItem lem <- previousItems+ guard $ lemmaCaseDistKind lem <= kind+ && ReuseLemma `elem` L.get lAttributes lem+ && AllTraces == L.get lTraceQuantifier lem+ return $ formulaToGuarded_ $ L.get lFormula lem ------------------------------------------------------------------------------@@ -780,7 +789,10 @@ prettyAxiom :: HighlightDocument d => Axiom -> d prettyAxiom ax = kwAxiom <-> text (L.get axName ax) <> colon $-$- (nest 2 $ doubleQuotes $ prettyLNFormula $ L.get axFormula ax)+ (nest 2 $ doubleQuotes $ prettyLNFormula $ L.get axFormula ax) $-$+ (nest 2 $ if safety then lineComment_ "safety formula" else emptyDoc)+ where+ safety = isSafetyFormula $ formulaToGuarded_ $ L.get axFormula ax -- | Pretty print a lemma. prettyLemma :: HighlightDocument d => (p -> d) -> Lemma p -> d
src/Theory/Constraint/Solver/CaseDistinctions.hs view
@@ -67,7 +67,7 @@ -- given typing assumptions are justified. initialCaseDistinction :: ProofContext- -> [LNFormula] -- ^ Axioms.+ -> [LNGuarded] -- ^ Axioms. -> Goal -> CaseDistinction initialCaseDistinction ctxt axioms goal =@@ -111,9 +111,8 @@ solveAllSafeGoals ths = solve [] where- -- safeGoal _ _ = False- safeGoal _ (_, (_, Useless)) = False- safeGoal doSplit (goal, _ ) =+ safeGoal _ (_, (_, LoopBreaker)) = False+ safeGoal doSplit (goal, _ ) = case goal of ChainG _ _ -> True ActionG _ fa -> not (isKUFact fa)@@ -158,9 +157,13 @@ :: ProofContext -- ^ Proof context used for refining the case distinction. -> CaseDistinction -- ^ Case distinction to use. -> Goal -- ^ Goal to match- -> Maybe CaseDistinction- -- ^ An adapted version of the case distinction and a matcher of the case- -- distinction goal to the substitution goal.+ -> Maybe (Reduction [String])+ -- ^ A constraint reduction step to apply the resulting case distinction.+ -- Note that this step assumes that the theorem has been imported using+ -- 'someInst' into the context that this reduction is executed in.+ --+ -- FIXME: This is a mess. Factor code such that this inter-dependency+ -- between 'applyCaseDistinction' and 'matchToGoal' goes away. matchToGoal ctxt th goalTerm = case (goalTerm, get cdGoal th) of ( PremiseG (iTerm, premIdxTerm) faTerm@@ -168,27 +171,26 @@ let match = faTerm `matchFact` faPat <> iTerm `matchLVar` iPat in case runReader (solveMatchLNTerm match) (get pcMaudeHandle ctxt) of [] -> Nothing- subst:_ ->- let refine = do- modM sEdges (substNodePrem pPat (iPat, premIdxTerm))- void (solveSubstEqs SplitNow subst)- return ((), [])- in Just $ snd $ refineCaseDistinction ctxt refine th+ subst:_ -> Just $ genericApply subst $+ -- add the missing edge to each case of the theorem+ modify sEdges (substNodePrem pPat (iPat, premIdxTerm)) (ActionG iTerm faTerm, ActionG iPat faPat) -> let match = faTerm `matchFact` faPat <> iTerm `matchLVar` iPat in case runReader (solveMatchLNTerm match) (get pcMaudeHandle ctxt) of [] -> Nothing- subst:_ ->- let refine = do- void (solveSubstEqs SplitNow subst)- return ((), [])- in Just $ snd $ refineCaseDistinction ctxt refine th+ subst:_ -> Just $ genericApply subst id -- No other matches possible, as we only precompute case distinctions for -- premises and KU-actions. _ -> Nothing where+ genericApply subst systemModifier = do+ void (solveSubstEqs SplitNow subst)+ (names, sysTh) <- disjunctionOfList $ getDisj $ get cdCases th+ conjoinSystem (systemModifier sysTh)+ return names+ substNodePrem from to = S.map (\ e@(Edge c p) -> if p == from then Edge c to else e) @@ -211,11 +213,8 @@ | isJust $ matchToGoal ctxt th goal = Just $ do markGoalAsSolved "precomputed" goal thRenamed <- rename th- let thInst = fromJustNote "applyCaseDistinction: impossible" $- matchToGoal ctxt thRenamed goal- (names, sysTh) <- disjunctionOfList $ getDisj $ get cdCases thInst- conjoinSystem sysTh- return names+ fromJustNote "applyCaseDistinction: impossible" $+ matchToGoal ctxt thRenamed goal | otherwise = Nothing @@ -240,7 +239,7 @@ -- | Precompute a saturated set of case distinctions. precomputeCaseDistinctions :: ProofContext- -> [LNFormula] -- ^ Axioms.+ -> [LNGuarded] -- ^ Axioms. -> [CaseDistinction] precomputeCaseDistinctions ctxt axioms = map cleanupCaseNames $ saturateCaseDistinctions ctxt rawCaseDists@@ -294,17 +293,15 @@ -- | Refine a set of case distinction by exploiting additional typing -- assumptions. refineWithTypingAsms- :: [LNFormula] -- ^ Typing assumptions to use.+ :: [LNGuarded] -- ^ Typing assumptions to use. -> ProofContext -- ^ Proof context to use. -> [CaseDistinction] -- ^ Original, untyped case distinctions. -> [CaseDistinction] -- ^ Refined, typed case distinctions.-refineWithTypingAsms assumptions0 ctxt cases0 =+refineWithTypingAsms assumptions ctxt cases0 = fmap (modifySystems removeFormulas) $ saturateCaseDistinctions ctxt $ modifySystems updateSystem <$> cases0 where- assumptions =- map (either (error . render) id . formulaToGuarded) assumptions0 modifySystems = modify cdCases . fmap . second updateSystem se = modify sFormulas (S.union (S.fromList assumptions)) $
src/Theory/Constraint/Solver/Goals.hs view
@@ -26,6 +26,7 @@ import qualified Data.DAG.Simple as D (cyclic) import qualified Data.Map as M+import qualified Data.Set as S import Control.Basics import Control.Category@@ -45,7 +46,15 @@ -- Extracting Goals ------------------------------------------------------------------------------ -data Usefulness = Useful | Useless+data Usefulness =+ Useful+ -- ^ A goal that is likely to result in progress.+ | LoopBreaker+ -- ^ A goal that is delayed to avoid immediate termination. Needs to be+ -- handled fairly.+ | ProbablySolvable+ -- ^ A goal that is very likely to be solvable without introducing further+ -- interesting constraints. These goals are delayed until the very end. deriving (Show, Eq) -- | Goals annotated with their number and usefulness.@@ -60,13 +69,16 @@ compare a b = check a b where- check Useful Useful = EQ- check Useless Useless = EQ- check x y = compare (tag x) (tag y)- tag (Useful) = 0 :: Int- tag (Useless) = 1 :: Int+ check Useful Useful = EQ+ check LoopBreaker LoopBreaker = EQ+ check ProbablySolvable ProbablySolvable = EQ+ check x y = compare (tag x) (tag y) + tag (Useful) = 0 :: Int+ tag (LoopBreaker) = 1+ tag (ProbablySolvable) = 2 + -- | The list of goals that must be solved before a solution can be extracted. -- Each goal is annotated with its age and an indicator for its usefulness. openGoals :: System -> [AnnotatedGoal]@@ -80,6 +92,7 @@ || isMsgVar m || sortOfLNTerm m == LSortPub -- handled by 'insertAction' || isPair m || isInverse m || isProduct m+ || isNullaryFunction m ActionG _ _ -> not solved PremiseG _ _ -> not solved -- Technically the 'False' disj would be a solvable goal. However, we@@ -97,17 +110,20 @@ -- explicitly if they still exist. SplitG idx -> splitExists (get sEqStore sys) idx - let useful = case goal of- -- Note that 'solveAllSafeGoals' in "CaseDistinctions" relies on- -- looping goals being classified as 'Useless'.- _ | get gsLoopBreaker status -> Useless+ let+ useful = case goal of+ _ | get gsLoopBreaker status -> LoopBreaker ActionG i (kFactView -> Just (UpK, m))- | isSimpleTerm m || deducible i m -> Useless+ -- if there are KU-guards then all knowledge goals are useful+ | hasKUGuards -> Useful+ | isSimpleTerm m || deducible i m -> ProbablySolvable _ -> Useful return (goal, (get gsNr status, useful)) where existingDeps = rawLessRel sys+ hasKUGuards =+ any ((KUFact `elem`) . guardFactTags) $ S.toList $ get sFormulas sys -- We use the following heuristic for marking KU-actions as useful (worth -- solving now) or useless (to be delayed until no more useful goals@@ -216,7 +232,7 @@ let m = case kFactView faConc of Just (DnK, m') -> m' _ -> error $ "solveChain: impossible"- caseName (viewTerm -> FApp o _) = show o+ caseName (viewTerm -> FApp o _) = showFunSymName o caseName t = show t return $ caseName m `disjunction`
src/Theory/Constraint/Solver/ProofMethod.hs view
@@ -258,8 +258,9 @@ solveGoalMethod (goal, (nr, usefulness)) = ( SolveGoal goal , "nr. " ++ show nr ++ case usefulness of- Useful -> ""- Useless -> " (marked useless)"+ Useful -> ""+ LoopBreaker -> " (loop breaker)"+ ProbablySolvable -> " (probably solvable)" ) newtype Heuristic = Heuristic [GoalRanking]@@ -320,9 +321,9 @@ -> System -> [AnnotatedGoal] -> [AnnotatedGoal] smartRanking allowPremiseGLoopBreakers sys =- delayUseless . unmark . sortDecisionTree solveFirst . goalNrRanking+ sortOnUsefulness . unmark . sortDecisionTree solveFirst . goalNrRanking where- delayUseless = sortOn (snd . snd)+ sortOnUsefulness = sortOn (snd . snd) unmark | allowPremiseGLoopBreakers = map unmarkPremiseG | otherwise = id@@ -338,10 +339,16 @@ , isFreshKnowsGoal . fst , isSplitGoalSmall . fst , isDoubleExpGoal . fst- , isLoopBreakerGoal ]- -- prefer knowledge goals and loop-breaker premises- -- before expensive equation splits+ , isNoLargeSplitGoal . fst ]+ -- move the rest (mostly more expensive KU-goals) before expensive+ -- equation splits + -- FIXME: This small split goal preferral is quite hacky when using+ -- induction. The problem is that we may end up solving message premise+ -- goals all the time instead performing a necessary split. We should make+ -- sure that a split does not get too old.+ smallSplitGoalSize = 3+ isNonLoopBreakerProtoFactGoal (PremiseG _ fa, (_, Useful)) = not $ isKFact fa isNonLoopBreakerProtoFactGoal _ = False @@ -356,14 +363,13 @@ Just (viewTerm2 -> FExp _ (viewTerm2 -> FMult _)) -> True _ -> False - isLoopBreakerGoal (ActionG _ fa, _ ) = isKUFact fa- isLoopBreakerGoal (PremiseG _ _, (_, Useless)) = True- isLoopBreakerGoal _ = False- -- Be conservative on splits that don't exist. isSplitGoalSmall (SplitG sid) =- maybe False (< 3) $ splitSize (L.get sEqStore sys) sid+ maybe False (<= smallSplitGoalSize) $ splitSize (L.get sEqStore sys) sid isSplitGoalSmall _ = False++ isNoLargeSplitGoal goal@(SplitG _) = isSplitGoalSmall goal+ isNoLargeSplitGoal _ = True -- | @sortDecisionTree xs ps@ returns a reordering of @xs@ -- such that the sublist satisfying @ps!!0@ occurs first,
src/Theory/Constraint/Solver/Reduction.hs view
@@ -76,6 +76,7 @@ import qualified Data.Foldable as F import qualified Data.Map as M import qualified Data.Set as S+import Data.List (mapAccumL) import Safe import Control.Basics@@ -266,7 +267,7 @@ modM sEdges (\es -> foldr S.insert es [ Edge c p | (c,_,_,p) <- edges]) -- | Insert an 'Action' atom. Ensures that (almost all) trivial *KU* actions--- are solved immediatly using rule *S_{at,u,triv}*. We currently avoid+-- are solved immediately using rule *S_{at,u,triv}*. We currently avoid -- adding intermediate products. Indicates whether nodes other than the given -- action have been added to the constraint system. --@@ -292,7 +293,7 @@ where goal = ActionG i fa -- Here we rely on the fact that the action is new. Otherwise, we might- -- loop due to generating new KU-nodes that are merged immediatly.+ -- loop due to generating new KU-nodes that are merged immediately. requiresKU t = do j <- freshLVar "vk" LSortNode let faKU = kuFact t@@ -558,12 +559,17 @@ joinSets sEdges F.mapM_ insertLast $ get sLastAtom sys F.mapM_ (uncurry insertLess) $ get sLessAtoms sys- mapM_ (uncurry insertGoalStatus) $ M.toList $ get sGoals sys+ -- split-goals are not valid anymore+ mapM_ (uncurry insertGoalStatus) $ filter (not . isSplitGoal . fst) $ M.toList $ get sGoals sys F.mapM_ insertFormula $ get sFormulas sys -- update nodes _ <- (setNodes . (M.toList (get sNodes sys) ++) . M.toList) =<< getM sNodes -- conjoin equation store- modM sConjDisjEqs (`mappend` get sConjDisjEqs sys)+ eqs <- getM sEqStore+ let (eqs',splitIds) = (mapAccumL addDisj eqs (map snd . getConj $ get sConjDisjEqs sys))+ setM sEqStore eqs'+ -- add split-goals for all disjunctions of sys+ mapM_ (`insertGoal` False) $ SplitG <$> splitIds void (solveSubstEqs SplitNow $ get sSubst sys) -- Propagate substitution changes. Ignore change indicator, as it is -- assumed to be 'Changed' by default.@@ -571,8 +577,6 @@ where joinSets :: Ord a => (System :-> S.Set a) -> Reduction () joinSets proj = modM proj (`S.union` get proj sys)-- -- Unification via the equation store -------------------------------------
src/Theory/Constraint/System.hs view
@@ -100,7 +100,7 @@ import Data.Binary import qualified Data.DAG.Simple as D import Data.DeriveTH-import Data.List (foldl')+import Data.List (foldl', partition) import qualified Data.Map as M import Data.Maybe (fromMaybe) import Data.Monoid (Monoid(..))@@ -134,12 +134,18 @@ -- | Case dinstinction kind that are allowed. The order of the kinds -- corresponds to the subkinding relation: untyped < typed. data CaseDistKind = UntypedCaseDist | TypedCaseDist- deriving( Eq, Ord )+ deriving( Eq ) instance Show CaseDistKind where show UntypedCaseDist = "untyped" show TypedCaseDist = "typed" +instance Ord CaseDistKind where+ compare UntypedCaseDist UntypedCaseDist = EQ+ compare UntypedCaseDist TypedCaseDist = LT+ compare TypedCaseDist UntypedCaseDist = GT+ compare TypedCaseDist TypedCaseDist = EQ+ -- | The status of a 'Goal'. Use its 'Semigroup' instance to combine the -- status info of goals that collapse. data GoalStatus = GoalStatus@@ -203,25 +209,35 @@ -- | Returns the constraint system that has to be proven to show that given -- formula holds in the context of the given theory.-formulaToSystem :: CaseDistKind -> SystemTraceQuantifier -> LNFormula -> System-formulaToSystem kind traceQuantifier fm =- L.set sFormulas (S.singleton gf) (emptySystem kind)+formulaToSystem :: [LNGuarded] -- ^ Axioms to add+ -> CaseDistKind -- ^ Case distinction kind+ -> SystemTraceQuantifier -- ^ Trace quantifier+ -> LNFormula+ -> System+formulaToSystem axioms kind traceQuantifier fm =+ insertLemmas safetyAxioms+ $ L.set sFormulas (S.singleton gf2)+ $ (emptySystem kind) where- adapt = case traceQuantifier of- ExistsSomeTrace -> id- ExistsNoTrace -> gnot- gf = either (error . render) id (adapt <$> formulaToGuarded fm)+ (safetyAxioms, otherAxioms) = partition isSafetyFormula axioms+ gf0 = formulaToGuarded_ fm+ gf1 = case traceQuantifier of+ ExistsSomeTrace -> gf0+ ExistsNoTrace -> gnot gf0+ -- Non-safety axioms must be added to the formula, as they render the set+ -- of traces non-prefix-closed, which makes the use of induction unsound.+ gf2 = gconj $ gf1 : otherAxioms -- | Add a lemma / additional assumption to a constraint system.-insertLemma :: LNFormula -> System -> System-insertLemma fm0 =- go (either (error . render) id $ formulaToGuarded fm0)+insertLemma :: LNGuarded -> System -> System+insertLemma =+ go where go (GConj conj) = foldr (.) id $ map go $ getConj conj go fm = L.modify sLemmas (S.insert fm) -- | Add lemmas / additional assumptions to a constraint system.-insertLemmas :: [LNFormula] -> System -> System+insertLemmas :: [LNGuarded] -> System -> System insertLemmas fms sys = foldl' (flip insertLemma) sys fms ------------------------------------------------------------------------------
src/Theory/Constraint/System/Guarded.hs view
@@ -1,5 +1,6 @@ {-# LANGUAGE BangPatterns #-} {-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeSynonymInstances #-}@@ -29,6 +30,7 @@ , ginduct , formulaToGuarded+ , formulaToGuarded_ -- ** Transformation , simplifyGuarded@@ -40,7 +42,10 @@ , isDisjunction , isAllGuarded , isExGuarded+ , isSafetyFormula + , guardFactTags+ -- ** Conversions to non-bound representations , bvarToLVar , openGuarded@@ -70,6 +75,7 @@ import Data.Either (partitionEithers) import Data.Foldable (Foldable(..), foldMap) import Data.List+import qualified Data.DList as D import Data.Monoid (Monoid(..)) import Data.Traversable hiding (mapM, sequence) @@ -94,26 +100,50 @@ -- f@i atoms in as. deriving (Eq, Ord, Show) -isConjunction :: Guarded t t1 t2 -> Bool+isConjunction :: Guarded s c v -> Bool isConjunction (GConj _) = True isConjunction _ = False -isDisjunction :: Guarded t t1 t2 -> Bool+isDisjunction :: Guarded s c v -> Bool isDisjunction (GDisj _) = True isDisjunction _ = False -isExGuarded :: Guarded t t1 t2 -> Bool+isExGuarded :: Guarded s c v -> Bool isExGuarded (GGuarded Ex _ _ _) = True isExGuarded _ = False -isAllGuarded :: Guarded t t1 t2 -> Bool+isAllGuarded :: Guarded s c v -> Bool isAllGuarded (GGuarded All _ _ _) = True isAllGuarded _ = False +-- | Check whether the guarded formula is closed and does not contain an+-- existential quantifier. This under-approximates the question whether the+-- formula is a safety formula. A safety formula @phi@ has the property that a+-- trace violating it can never be extended to a trace satisfying it.+isSafetyFormula :: HasFrees (Guarded s c v) => Guarded s c v -> Bool+isSafetyFormula gf0 =+ null (frees [gf0]) && noExistential gf0+ where+ noExistential (GAto _ ) = True+ noExistential (GGuarded Ex _ _ _) = False+ noExistential (GGuarded All _ _ gf) = noExistential gf+ noExistential (GDisj disj) = all noExistential $ getDisj disj+ noExistential (GConj conj) = all noExistential $ getConj conj++-- | All 'FactTag's that are used in guards.+guardFactTags :: Guarded s c v -> [FactTag]+guardFactTags =+ D.toList .+ foldGuarded mempty (mconcat . getDisj) (mconcat . getConj) getTags+ where+ getTags _qua _ss atos inner =+ mconcat [ D.singleton tag | Action _ (Fact tag _) <- atos ] <> inner+ ------------------------------------------------------------------------------ -- Folding ------------------------------------------------------------------------------ + -- | Fold a guarded formula. foldGuarded :: (Atom (VTerm c (BVar v)) -> b) -> (Disj b -> b)@@ -355,6 +385,13 @@ instance Document d => Error (ErrorDoc d) where noMsg = emptyDoc strMsg = text+++-- | @formulaToGuarded fm@ returns a guarded formula @gf@ that is+-- equivalent to @fm@ under the assumption that this is possible.+-- If not, then 'error' is called.+formulaToGuarded_ :: LNFormula -> LNGuarded+formulaToGuarded_ = either (error . render) id . formulaToGuarded -- | @formulaToGuarded fm@ returns a guarded formula @gf@ that is -- equivalent to @fm@ if possible.
src/Theory/Text/Parser/Token.hs view
@@ -149,7 +149,7 @@ -- | Parse a symbol. symbol :: String -> Parser String-symbol = try . T.symbol spthy+symbol sym = try (T.symbol spthy sym) <?> ("\"" ++ sym ++ "\"") -- | Parse a symbol without returning the parsed string. symbol_ :: String -> Parser ()
src/Theory/Tools/EquationStore.hs view
@@ -32,6 +32,7 @@ -- ** Adding equalities , addEqs , addRuleVariants+ , addDisj -- ** Case splitting , performSplit@@ -157,7 +158,7 @@ splits eqs = map fst $ nub $ sortOn snd [ (idx, S.size conj) | (idx, conj) <- getConj $ L.get eqsConj eqs ] --- | Returns the number of cases for a given 'SplitId'.+-- | Returns 'True' if the 'SplitId' is valid. splitExists :: EqStore -> SplitId -> Bool splitExists eqs = isJust . splitSize eqs
src/Theory/Tools/Wellformedness.hs view
@@ -341,6 +341,17 @@ atomTerms (Less i j) = [i, j] atomTerms (Last i) = [i] +-- TODO: Perhaps a lot of errors would be captured when making the signature+-- of facts, term, and atom constructors explicit.+lemmaAttributeReport :: OpenTheory -> WfErrorReport+lemmaAttributeReport thy = do+ lem <- theoryLemmas thy+ guard $ get lTraceQuantifier lem == ExistsTrace+ && ReuseLemma `elem` get lAttributes lem+ return ( "attributes"+ , text "lemma" <-> (text $ quote $ get lName lem) <> colon <->+ text "cannot reuse 'exists-trace' lemmas"+ ) -- | Check for mistakes in lemmas. --@@ -490,6 +501,7 @@ , ruleSortsReport , factReports , formulaReports+ , lemmaAttributeReport , multRestrictedReport ]
src/Web/Dispatch.hs view
@@ -70,7 +70,8 @@ -> Bool -- ^ Load last proof state if present -> Bool -- ^ Automatically save proof state -> (FilePath -> IO ClosedTheory) -- ^ Theory loader (from file).- -> (String -> IO ClosedTheory) -- ^ Theory loader (from string).+ -> (String -> IO (Either String ClosedTheory))+ -- ^ Theory loader (from string). -> (OpenTheory -> IO ClosedTheory) -- ^ Theory closer. -> Bool -- ^ Show debugging messages? -> FilePath -- ^ Path to static content directory
src/Web/Handler.hs view
@@ -337,12 +337,17 @@ case result of Nothing -> setMessage "Post request failed."- Just fileinfo -> do- yesod <- getYesod- closedThy <- liftIO $ parseThy yesod (BS.unpack $ fileContent fileinfo)- void $ putTheory Nothing- (Just $ Upload $ T.unpack $ fileName fileinfo) closedThy- setMessage "Loaded new theory!"+ Just fileinfo+ | BS.null $ fileContent fileinfo -> setMessage "No theory file given."+ | otherwise -> do+ yesod <- getYesod+ closedThy <- liftIO $ parseThy yesod (BS.unpack $ fileContent fileinfo)+ case closedThy of+ Left err -> setMessage $ "Theory loading failed:\n" <> toHtml err+ Right thy -> do+ void $ putTheory Nothing+ (Just $ Upload $ T.unpack $ fileName fileinfo) thy+ setMessage "Loaded new theory!" theories <- getTheories defaultLayout $ do setTitle "Welcome to the Tamarin prover"
src/Web/Theory.hs view
@@ -133,14 +133,15 @@ where ppCase step = markStatus (fst $ psInfo step) - ppStep step = case fst $ psInfo step of- (Nothing, _) -> superfluousStep- (_, Nothing) -> stepLink ["sorry-step"] <>- case psMethod step of- Sorry _ -> emptyDoc- _ -> removeStep- (_, Just True) -> stepLink ["hl_good"]- (_, Just False) -> stepLink ["hl_bad"]+ ppStep step =+ case fst $ psInfo step of+ (Nothing, _) -> superfluousStep+ (_, Nothing) -> stepLink ["sorry-step"]+ (_, Just True) -> stepLink ["hl_good"]+ (_, Just False) -> stepLink ["hl_bad"]+ <> case psMethod step of+ Sorry _ -> emptyDoc+ _ -> removeStep where ppMethod = prettyProofMethod $ psMethod step stepLink cls = linkToPath renderUrl@@ -218,8 +219,12 @@ bold = withTag "strong" [] . text overview n info p = linkToPath renderUrl (TheoryPathMR tidx p) [] (bold n <-> info) messageLink = overview "Message theory" (text "") TheoryMessage- ruleLink = overview "Multiset rewriting rules and axioms" rulesInfo TheoryRules+ ruleLink = overview ruleLinkMsg rulesInfo TheoryRules+ ruleLinkMsg = "Multiset rewriting rules" +++ if null(theoryAxioms thy) then "" else " and axioms"+ reqCasesLink name k = overview name (casesInfo k) (TheoryCaseDist k 0 0)+ {- -- | A snippet that explains a sequent using a rendered graph and the pretty
src/Web/Types.hs view
@@ -101,7 +101,7 @@ , workDir :: FilePath -- ^ The working directory (for storing/loading theories). -- , parseThy :: MonadIO m => String -> GenericHandler m ClosedTheory- , parseThy :: String -> IO ClosedTheory+ , parseThy :: String -> IO (Either String ClosedTheory) -- ^ Parse a closed theory according to command-line arguments. , closeThy :: OpenTheory -> IO ClosedTheory -- ^ Close an open theory according to command-line arguments.
tamarin-prover.cabal view
@@ -1,7 +1,7 @@ cabal-version: >= 1.8 build-type: Simple name: tamarin-prover-version: 0.8.0.0+version: 0.8.1.0 license: GPL license-file: LICENSE category: Theorem Provers@@ -80,6 +80,7 @@ examples/loops/Minimal_Create_Use_Destroy.spthy examples/loops/Minimal_Typing_Example.spthy examples/loops/Minimal_Loop_Example.spthy+ examples/loops/Typing_and_Destructors.spthy examples/loops/JCS12_Typing_Example.spthy examples/loops/TESLA_Scheme1.spthy @@ -165,6 +166,13 @@ ghc-options: -Wall -fwarn-tabs -rtsopts ghc-prof-options: -auto-all++ -- Parallelize by default. Only activated for GHC 7.4, as this flag was+ -- unstable in earlier -- versions; i.e., it resulted in command-line+ -- parsing errors.+ if impl(ghc >= 7.4)+ ghc-options: -with-rtsopts=-N+ hs-source-dirs: src main-is: Main.hs @@ -204,6 +212,7 @@ , deepseq == 1.3.* , array >= 0.3 && < 0.5 , containers >= 0.4.2 && < 0.5+ , dlist == 0.5.* , mtl == 2.0.* , cmdargs == 0.9.* , filepath >= 1.1 && < 1.4@@ -221,8 +230,8 @@ , parallel == 3.2.* , HUnit == 1.2.* - , tamarin-prover-utils == 0.8.*- , tamarin-prover-term == 0.8.*+ , tamarin-prover-utils >= 0.8.1 && < 0.9+ , tamarin-prover-term >= 0.8.1 && < 0.9 other-modules: