fix issue 519

Makefile

@@ -398,7 +398,7 @@ auto-sources-case-studies:	$(AUTO_SOURCES_CS_TARGETS)
 ## Regression (old issues)
 ##########################
 
-REGRESSION_CASE_STUDIES=issue216.spthy issue193.spthy issue310.spthy
+REGRESSION_CASE_STUDIES=issue216.spthy issue193.spthy issue310.spthy issue519.spthy
 
 REGRESSION_TARGETS=$(subst .spthy,_analyzed.spthy,$(addprefix case-studies$(SUBDIR)regression/trace/,$(REGRESSION_CASE_STUDIES)))
 

case-studies-regression/regression/trace/issue519_analyzed.spthy

@@ -0,0 +1,86 @@
+theory issue519 begin
+
+// Function signature and definition of the equational theory E
+
+builtins: multiset
+functions: fst/1[destructor], pair/2, snd/1[destructor]
+equations: fst(<x.1, x.2>) = x.1, snd(<x.1, x.2>) = x.2
+
+
+
+
+
+rule (modulo E) CreateAndStoreFresh:
+   [ Fr( ~x ) ] --> [ St( ~x ) ]
+
+  /* has exactly the trivial AC variant */
+
+rule (modulo E) Send_multiset_msgVar:
+   [ St( x ), In( y ) ] --[ Secret_MsgVar( x ) ]-> [ Out( (x+y) ) ]
+
+  /* has exactly the trivial AC variant */
+
+rule (modulo E) Send_multiset_freshVar:
+   [ St( ~x ), In( y ) ] --[ Secret_FreshVar( ~x ) ]-> [ Out( (~x+y) ) ]
+
+  /* has exactly the trivial AC variant */
+
+lemma secret_msgVar:
+  all-traces "∀ #i x. (Secret_MsgVar( x ) @ #i) ⇒ (¬(∃ #j. K( x ) @ #j))"
+/*
+guarded formula characterizing all counter-examples:
+"∃ #i x. (Secret_MsgVar( x ) @ #i) ∧ ∃ #j. (K( x ) @ #j)"
+*/
+simplify
+solve( St( x ) ▶₀ #i )
+  case CreateAndStoreFresh
+  solve( !KU( ~x ) @ #vk.1 )
+    case Send_multiset_msgVar
+    SOLVED // trace found
+  qed
+qed
+
+lemma secret_freshVar:
+  all-traces "∀ #i x. (Secret_FreshVar( x ) @ #i) ⇒ (¬(∃ #j. K( x ) @ #j))"
+/*
+guarded formula characterizing all counter-examples:
+"∃ #i x. (Secret_FreshVar( x ) @ #i) ∧ ∃ #j. (K( x ) @ #j)"
+*/
+simplify
+solve( St( ~x ) ▶₀ #i )
+  case CreateAndStoreFresh
+  solve( !KU( ~x ) @ #vk.1 )
+    case Send_multiset_freshVar
+    SOLVED // trace found
+  qed
+qed
+
+/* All wellformedness checks were successful. */
+
+/*
+Generated from:
+Tamarin version 1.7.1
+Maude version 3.2.1
+Git revision: 3063551fa783622802bf38bdec715c58f70eefd2 (with uncommited changes), branch: fix-dh-neutral
+Compiled at: 2022-09-23 14:03:06.880236851 UTC
+*/
+
+end
+/* Output
+maude tool: 'maude'
+ checking version: 3.2.1. OK.
+ checking installation: OK.
+
+==============================================================================
+summary of summaries:
+
+analyzed: examples/regression/trace/issue519.spthy
+
+  output:          examples/regression/trace/issue519.spthy.tmp
+  processing time: 0.03603801s
+
+  secret_msgVar (all-traces): falsified - found trace (4 steps)
+  secret_freshVar (all-traces): falsified - found trace (4 steps)
+
+==============================================================================
+*/

examples/regression/trace/issue519.spthy

@@ -0,0 +1,36 @@
+theory issue519
+begin
+
+/* Minimal working example for incorrect source computation bug where the source is a MsgVar part of a multiset.
+ *
+ * Expectation: Both lemmas should be false, because St(x) can only occur for x a fresh value.
+ * However, in Tamarin 1.6.1, the first is verified (MsgVar, incorrectly), and the second falsified (FreshVar, correctly).
+ *
+ * This seems to be caused by an incorrect source computation for the fresh value, which does not consider Send_multiset_msgVar as a source.
+ *
+ * By Cas Cremers
+ */
+builtins: multiset
+
+rule CreateAndStoreFresh:
+  [Fr(~x)]-->[St(~x)]
+
+rule Send_multiset_msgVar:
+  [St(x), In(y)]
+  --[ Secret_MsgVar(x) ]->
+  [ Out(x+y) ]
+
+rule Send_multiset_freshVar:
+  [St(~x), In(y)]
+  --[ Secret_FreshVar(~x) ]->
+  [ Out(~x+y) ]
+
+lemma secret_msgVar:
+  // Tamarin 1.6.1 falsely yields verified
+  "All #i x. Secret_MsgVar(x)@i   ==> not Ex #j. K(x)@j"
+
+lemma secret_freshVar:
+  // Tamarin 1.6.1 correctly yields falsified
+  "All #i x. Secret_FreshVar(x)@i ==> not Ex #j. K(x)@j"
+
+end

lib/theory/src/Theory/Constraint/Solver/Goals.hs

@@ -305,15 +305,15 @@ solveChain :: [RuleAC]              -- ^ All destruction rules.
            -> Reduction String      -- ^ Case name to use.
 solveChain rules (c, p) = do
     faConc  <- gets $ nodeConcFact c
-    (do -- solve it by a direct edge
+    do -- solve it by a direct edge
         cRule <- gets $ nodeRule (nodeConcNode c)
         pRule <- gets $ nodeRule (nodePremNode p)
         faPrem <- gets $ nodePremFact p
         contradictoryIf (forbiddenEdge cRule pRule)
         insertEdges [(c, faConc, faPrem, p)]
         let mPrem = case kFactView faConc of
                       Just (DnK, m') -> m'
-                      _              -> error $ "solveChain: impossible"
+                      _              -> error "solveChain: impossible"
             caseName (viewTerm -> FApp o _)    = showFunSymName o
             caseName (viewTerm -> Lit l)       = showLitName l
         contradictoryIf (illegalCoerce pRule mPrem)
@@ -326,7 +326,7 @@ solveChain rules (c, p) = do
                 -- compute the applicable destruction rules directly.
                 i <- freshLVar "vr" LSortNode
                 let rus = map (ruleACIntrToRuleACInst . mkDUnionRule args)
-                              (filter (not . isMsgVar) args)
+                              args
                 -- NOTE: We rely on the check that the chain is open here.
                 ru <- disjunctionOfList rus
                 modM sNodes (M.insert i ru)
@@ -349,7 +349,6 @@ solveChain rules (c, p) = do
                 (v, faPrem) <- disjunctionOfList $ take 1 $ enumPrems ru
                 extendAndMark i ru v faPrem faConc
          _ -> error "solveChain: not a down fact"
-     )
   where
     extendAndMark :: NodeId -> RuleACInst -> PremIdx -> LNFact -> LNFact
       -> Control.Monad.Trans.State.Lazy.StateT System