Sapic fixes diverse (tamarin-prover#540)

* Fix overly strong error in Sapic translation

Multiset can only be used for the specific integer modeling, we
thuse raise a warning when multiset is translated, not an error.
This should disappear once builtin natural numbers are included
in Tamarin and translated in Sapic.

* Example fix due to event renaming

Events are now renamed to correclty export msr to proverif,
manulaly specified queries thus need to be updated.

* Fix newly raised multiple definition error

* Fix non exported exist trace

examples/sapic/export/ExistingSapicModels/AC_counter_with_attack.spthy

@@ -53,8 +53,8 @@ lemma can_run_v: //for sanity
 	"Ex #t h .Voutput(h)@t"
 */
 
+/* attack  expected to be found */
 lemma attested_comput_second_step:
-    exists-trace
-	"not(All #t1 o2 i2 o i.  Voutput(<o2,i2,<o,list(i,'init')>>)@t1 ==> (Ex #t2 . Poutput(<o2,i2,<o,list(i,'init')>>)@t2 & t2<t1))"
+	"All #t1 o2 i2 o i.  Voutput(<o2,i2,<o,list(i,'init')>>)@t1 ==> (Ex #t2 . Poutput(<o2,i2,<o,list(i,'init')>>)@t2 & t2<t1)"
 
 end

examples/sapic/export/SSH/ssh-with-forwarding-bounded.spthy

@@ -118,12 +118,12 @@ let remoteP(pkS,~remote:channel) =
 		let <lvl,ms,'sign_req'> = sdec(signreq,kSP) in
                 out(senc(<nest(lvl),ms,'sign_req'>,kSP2));
 		in(signans2);
-		let <sig3,lvl,'sign_ans'> = sdec(signans2,kPS2) in
+		let <sig3,lvlr,'sign_ans'> = sdec(signans2,kPS2) in
                 // let <lvlf3,dump3>= getMess(sig3) in
 //     	        if issign(sig3,pkP)=true then
 //		if isnest(lvl) = true then
 		event Test(sig3);
-		out(senc( <sig3,lvl,'sign_ans'>,kPS))
+		out(senc( <sig3,lvlr,'sign_ans'>,kPS))
 
 		)
 		)

examples/sapic/export/ex1.spthy

@@ -20,7 +20,7 @@ equations: bij(unbij(x))=x
 export queries :
  "
  (* This query was added manualy, and the other one automatically from the lemmas. *)
- query x:bitstring; event(Secret(x)) && (attacker(x)).
+ query x:bitstring; event(eSecret(x)) && (attacker(x)).
  "
 
 let P = new a; event Secret(a); out (senc(<a,'test'>,sk))

lib/export/src/Export.hs

@@ -1077,7 +1077,8 @@ loadHeaders tc thy typeEnv = do
       foldl
         ( \y x -> case List.lookup x builtins of
             Nothing -> case x of
-              "multiset"         -> throw UnsupportedBuiltinMS
+              "multiset"         -> -- on the long run, this should throw UnsupportedBuiltinMS, but we currently allow to use multiset in a restricted fashion
+                translationWarning "you are using in the Sapic model the multiset builtin. Unless you are only using it to model natural numbers, this may result in a failure of the translation." y
               "bilinear-pairing" -> throw UnsupportedBuiltinBP
               _                  -> y
             Just t -> y `S.union` t