diff --git a/Makefile b/Makefile
index 62dc40d99316e367be624c7949444b96a7eaba8c..f010dbd61cb44e06c3bc68a0285c14751a5747bd 100755
--- a/Makefile
+++ b/Makefile
@@ -2,6 +2,7 @@
# TTool Makefile
# Tested under Linux *only*
# Meant to work with svn
+export
TARGET_ARCH = linux
@@ -82,10 +83,14 @@ RELEASE_STD_FILES_LIB = TClock1.lib TTimerv01.lib
RELEASE_STD_FILES_BIN = $(LAUNCHER_BINARY) $(TTOOL_BINARY) $(TIFTRANSLATOR_BINARY) $(TMLTRANSLATOR_BINARY) $(REMOTESIMULATOR_BINARY) $(RUNDSE_BINARY)
RELEASE_STD_FILES_LICENSES = LICENSE LICENSE_CECILL_ENG LICENSE_CECILL_FR
-
+TEST_DIR = tests
+TEST_MK = test.mk
+TEST_DIRS = $(shell find $(TEST_DIR)/* -type d)
+TEST_MAKEFILES = $(patsubst %,%/$(TEST_MK),$(TEST_DIRS))
all: basic jar
+.PHONY: svn basicsvnapvrille myrelease basic jar ttooljar launcher tiftranslator tmltranslator rundse remotesimulator documentation stdrelease preinstall preinstall_linux jttooljar updatesimulator test
svn:
date
@@ -285,6 +290,13 @@ updatesimulator:
cd /homes/apvrille/TechTTool/SystemCCode/generated/; make ultraclean
+test: $(TEST_MAKEFILES)
+ $(foreach m,$(TEST_MAKEFILES),$(MAKE) -s -C $(dir $(m)) -f $(TEST_MK);)
+ @echo "Everything went fine"
+
+$(TEST_DIR)/%/$(TEST_MK):
+ @cp $(TEST_DIR)/$(TEST_MK) $@
+
clean:
rm -f $(TTOOL_SRC)/*.dot $(TTOOL_SRC)/*.dta $(TTOOL_SRC)/*.sim $(TTOOL_SRC)/*.lot
rm -f $(TTOOL_SRC)/*.class $(TTOOL_SRC)/*.java~
@@ -299,6 +311,14 @@ clean:
echo rm -f $$p/*.class;\
rm -f $(TTOOL_SRC)/$$p/*.class $(TTOOL_SRC)/$$p/*.java~; \
done
+ @@for t in $(TEST_DIRS); do \
+ if [ -w $$t/$(TEST_MK) ]; \
+ then \
+ $(MAKE) -s -C $$t -f $(TEST_MK) clean; \
+ echo rm -f ./$$t/*.class; \
+ rm -f ./$$t/$(TEST_MK); \
+ fi; \
+ done
ultraclean: clean
@@for p in $(RELEASE_STD_FILES_BIN); do \
diff --git a/src/avatartranslator/toproverif/AVATAR2ProVerif.java b/src/avatartranslator/toproverif/AVATAR2ProVerif.java
index 422b506470f10c37560294cd50b7f0206c3de177..7997b9c233dc7130623c7de0ba6b016f94d205d5 100755
--- a/src/avatartranslator/toproverif/AVATAR2ProVerif.java
+++ b/src/avatartranslator/toproverif/AVATAR2ProVerif.java
@@ -971,7 +971,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
public void translateStopState (AvatarStopState _asme, Object _arg) {
}
- private static String translateTerm (AvatarTerm term, HashMap<AvatarAttribute, Integer> attributeCmp) {
+ protected static String translateTerm (AvatarTerm term, HashMap<AvatarAttribute, Integer> attributeCmp) {
if (term instanceof AvatarAttribute) {
AvatarAttribute attr = (AvatarAttribute) term;
if (attributeCmp != null)
diff --git a/src/proverifspec/ProVerifOutputAnalyzerTest.java b/src/proverifspec/ProVerifOutputAnalyzerTest.java
deleted file mode 100644
index ae9de88d04051a057279c02fa762bde23e1f8131..0000000000000000000000000000000000000000
--- a/src/proverifspec/ProVerifOutputAnalyzerTest.java
+++ /dev/null
@@ -1,174 +0,0 @@
-/**Copyright or (C) or Copr. GET / ENST, Telecom-Paris, Ludovic Apvrille
- *
- * ludovic.apvrille AT enst.fr
- *
- * This software is a computer program whose purpose is to allow the
- * edition of TURTLE analysis, design and deployment diagrams, to
- * allow the generation of RT-LOTOS or Java code from this diagram,
- * and at last to allow the analysis of formal validation traces
- * obtained from external tools, e.g. RTL from LAAS-CNRS and CADP
- * from INRIA Rhone-Alpes.
- *
- * This software is governed by the CeCILL license under French law and
- * abiding by the rules of distribution of free software. You can use,
- * modify and/ or redistribute the software under the terms of the CeCILL
- * license as circulated by CEA, CNRS and INRIA at the following URL
- * "http://www.cecill.info".
- *
- * As a counterpart to the access to the source code and rights to copy,
- * modify and redistribute granted by the license, users are provided only
- * with a limited warranty and the software's author, the holder of the
- * economic rights, and the successive licensors have only limited
- * liability.
- *
- * In this respect, the user's attention is drawn to the risks associated
- * with loading, using, modifying and/or developing or reproducing the
- * software by the user in light of its specific status of free software,
- * that may mean that it is complicated to manipulate, and that also
- * therefore means that it is reserved for developers and experienced
- * professionals having in-depth computer knowledge. Users are therefore
- * encouraged to load and test the software's suitability as regards their
- * requirements in conditions enabling the security of their systems and/or
- * data to be ensured and, more generally, to use and operate it in the
- * same conditions as regards security.
- *
- * The fact that you are presently reading this means that you have had
- * knowledge of the CeCILL license and that you accept its terms.
- *
- * /**
- * Class ProVerifOutputAnalyzer
- * Creation: 16/09/2010
- * @version 1.0 16/09/2010
- * @author Ludovic APVRILLE
- * @see
- */
-
-package proverifspec;
-
-import java.util.*;
-
-import myutil.*;
-import java.io.*;
-
-
-public class ProVerifOutputAnalyzerTest {
- public static void main(String[] args){
- BufferedReader br = null;
- try {
- String s="";
- String sCurrentLine;
- br = new BufferedReader(new FileReader("proverifspec/typed.txt"));
- while ((sCurrentLine = br.readLine()) != null) {
- s= s.concat(sCurrentLine+"\n");
- }
- //System.out.println(s);
-
- System.out.println("__________________________________");
-
- ProVerifOutputAnalyzer poa = new ProVerifOutputAnalyzer();
- poa.analyzeOutput(s,true);
-
-
- //Test for Reachable Events
- System.out.println("Reachable Events " + poa.getReachableEvents().size());
- for (String str: poa.getReachableEvents()){
- System.out.println(str);
- }
- System.out.println("NonReachable Events " + poa.getNonReachableEvents().size());
- for (String str: poa.getNonReachableEvents()){
- System.out.println(str);
- }
- System.out.println("Secret Terms " + poa.getSecretTerms().size());
- for (String str: poa.getSecretTerms()){
- System.out.println(str);
- }
- System.out.println("Non Secret Terms " + poa.getNonSecretTerms().size());
- for (String str: poa.getNonSecretTerms()){
- System.out.println(str);
- }
- System.out.println("Satisfied Authenticity " +poa.getSatisfiedAuthenticity().size());
- for (String str: poa.getSatisfiedAuthenticity()){
- System.out.println(str);
- }
- System.out.println("Satisfied Weak Authenticity " +poa.getSatisfiedWeakAuthenticity().size());
- for (String str: poa.getSatisfiedWeakAuthenticity()){
- System.out.println(str);
- }
- System.out.println("Non Satisfied Authenticity " +poa.getNonSatisfiedAuthenticity().size());
- for (String str: poa.getNonSatisfiedAuthenticity()){
- System.out.println(str);
- }
- System.out.println("Errors " +poa.getErrors().size());
- for (String str: poa.getErrors()){
- System.out.println(str);
- }
- System.out.println("Not proved " +poa.getNotProved().size());
- for (String str: poa.getNotProved()){
- System.out.println(str);
- }
-
- //Untyped Tests
- System.out.println("Untyped Tests");
-
-
- br = new BufferedReader(new FileReader("proverifspec/untyped.txt"));
- while ((sCurrentLine = br.readLine()) != null) {
- s= s.concat(sCurrentLine+"\n");
- }
- //System.out.println(s);
-
- System.out.println("__________________________________");
-
- poa.analyzeOutput(s,false);
-
-
- //Test for Reachable Events
- System.out.println("Reachable Events " + poa.getReachableEvents().size());
- for (String str: poa.getReachableEvents()){
- System.out.println(str);
- }
- System.out.println("NonReachable Events " + poa.getNonReachableEvents().size());
- for (String str: poa.getNonReachableEvents()){
- System.out.println(str);
- }
- System.out.println("Secret Terms " + poa.getSecretTerms().size());
- for (String str: poa.getSecretTerms()){
- System.out.println(str);
- }
- System.out.println("Non Secret Terms " + poa.getNonSecretTerms().size());
- for (String str: poa.getNonSecretTerms()){
- System.out.println(str);
- }
- System.out.println("Satisfied Authenticity " +poa.getSatisfiedAuthenticity().size());
- for (String str: poa.getSatisfiedAuthenticity()){
- System.out.println(str);
- }
- System.out.println("Satisfied Weak Authenticity " +poa.getSatisfiedWeakAuthenticity().size());
- for (String str: poa.getSatisfiedWeakAuthenticity()){
- System.out.println(str);
- }
- System.out.println("Non Satisfied Authenticity " +poa.getNonSatisfiedAuthenticity().size());
- for (String str: poa.getNonSatisfiedAuthenticity()){
- System.out.println(str);
- }
- System.out.println("Errors " +poa.getErrors().size());
- for (String str: poa.getErrors()){
- System.out.println(str);
- }
- System.out.println("Not proved " +poa.getNotProved().size());
- for (String str: poa.getNotProved()){
- System.out.println(str);
- }
-
- } catch (IOException e) {
- e.printStackTrace();
- } finally {
- try {
- if (br != null)br.close();
- } catch (IOException ex) {
- ex.printStackTrace();
- }
- }
-
- }
-}
diff --git a/tests/Avatar/ProVerif/ProVerifOutputAnalyzerTest.java b/tests/Avatar/ProVerif/ProVerifOutputAnalyzerTest.java
new file mode 100644
index 0000000000000000000000000000000000000000..650e2ce0110bc3e271b3b658bfa7c92553825c2f
--- /dev/null
+++ b/tests/Avatar/ProVerif/ProVerifOutputAnalyzerTest.java
@@ -0,0 +1,235 @@
+/**Copyright or (C) or Copr. GET / ENST, Telecom-Paris, Ludovic Apvrille
+ *
+ * ludovic.apvrille AT enst.fr
+ *
+ * This software is a computer program whose purpose is to allow the
+ * edition of TURTLE analysis, design and deployment diagrams, to
+ * allow the generation of RT-LOTOS or Java code from this diagram,
+ * and at last to allow the analysis of formal validation traces
+ * obtained from external tools, e.g. RTL from LAAS-CNRS and CADP
+ * from INRIA Rhone-Alpes.
+ *
+ * This software is governed by the CeCILL license under French law and
+ * abiding by the rules of distribution of free software. You can use,
+ * modify and/ or redistribute the software under the terms of the CeCILL
+ * license as circulated by CEA, CNRS and INRIA at the following URL
+ * "http://www.cecill.info".
+ *
+ * As a counterpart to the access to the source code and rights to copy,
+ * modify and redistribute granted by the license, users are provided only
+ * with a limited warranty and the software's author, the holder of the
+ * economic rights, and the successive licensors have only limited
+ * liability.
+ *
+ * In this respect, the user's attention is drawn to the risks associated
+ * with loading, using, modifying and/or developing or reproducing the
+ * software by the user in light of its specific status of free software,
+ * that may mean that it is complicated to manipulate, and that also
+ * therefore means that it is reserved for developers and experienced
+ * professionals having in-depth computer knowledge. Users are therefore
+ * encouraged to load and test the software's suitability as regards their
+ * requirements in conditions enabling the security of their systems and/or
+ * data to be ensured and, more generally, to use and operate it in the
+ * same conditions as regards security.
+ *
+ * The fact that you are presently reading this means that you have had
+ * knowledge of the CeCILL license and that you accept its terms.
+ *
+ * /**
+ * Class ProVerifOutputAnalyzer
+ * Creation: 16/09/2010
+ * @version 1.0 16/09/2010
+ * @author Ludovic APVRILLE
+ * @see
+ */
+
+import java.io.BufferedReader;
+import java.io.FileReader;
+import java.io.IOException;
+import java.security.MessageDigest;
+import java.security.NoSuchAlgorithmException;
+
+import avatartranslator.AvatarAttribute;
+import avatartranslator.AvatarBlock;
+import avatartranslator.AvatarSpecification;
+import avatartranslator.toproverif.AVATAR2ProVerif;
+import proverifspec.ProVerifOutputAnalyzer;
+
+
+public class ProVerifOutputAnalyzerTest {
+ public static void main(String[] args){
+ BufferedReader br = null;
+ byte[] expected = {-6, -76, -105, 122, 48, -22, 6, -4, 75, 68, 112, -32, 38, 67, 123, -98, -38, -87, 30, -27};
+
+ try {
+ String s="";
+ String sCurrentLine;
+ br = new BufferedReader(new FileReader("typed.txt"));
+ while ((sCurrentLine = br.readLine()) != null) {
+ s= s.concat(sCurrentLine+"\n");
+ }
+ //System.out.println(s);
+
+ System.out.print("==========> Testing ProVerif Output Analyzer");
+
+ AvatarSpecification avspec = new AvatarSpecification ("dummy", null);
+ AvatarBlock aliceBlock = new AvatarBlock ("Alice", avspec, null);
+ aliceBlock.addAttribute (new AvatarAttribute ("sk__data", null, aliceBlock, null));
+ aliceBlock.addAttribute (new AvatarAttribute ("m__data", null, aliceBlock, null));
+ aliceBlock.addAttribute (new AvatarAttribute ("m1__data", null, aliceBlock, null));
+ aliceBlock.addAttribute (new AvatarAttribute ("secretData", null, aliceBlock, null));
+ AvatarBlock bobBlock = new AvatarBlock ("Bob", avspec, null);
+ bobBlock.addAttribute (new AvatarAttribute ("m__data", null, bobBlock, null));
+ bobBlock.addAttribute (new AvatarAttribute ("m2__data", null, bobBlock, null));
+ bobBlock.addAttribute (new AvatarAttribute ("receivedData", null, bobBlock, null));
+ avspec.addBlock (aliceBlock);
+ avspec.addBlock (bobBlock);
+
+ MessageDigest md = MessageDigest.getInstance ("SHA");
+
+ ProVerifOutputAnalyzer poa = new ProVerifOutputAnalyzer(
+ new AVATAR2ProVerif (avspec) {
+ public String getTrueName (AvatarAttribute attr) {
+ return AVATAR2ProVerif.translateTerm (attr, null);
+ }
+ });
+
+ poa.analyzeOutput(s,true);
+
+
+ //Test for Reachable Events
+ //System.out.println("Reachable Events " + poa.getReachableEvents().size());
+ for (String str: poa.getReachableEvents()){
+ md.update(str.getBytes ());
+ }
+
+ //System.out.println("NonReachable Events " + poa.getNonReachableEvents().size());
+ for (String str: poa.getNonReachableEvents()){
+ md.update(str.getBytes ());
+ }
+ //System.out.println("Secret Terms " + poa.getSecretTerms().size());
+ for (AvatarAttribute attr: poa.getSecretTerms()){
+ md.update((attr.getBlock ().getName () + "." + attr.getName ()).getBytes ());
+ }
+ //System.out.println("Non Secret Terms " + poa.getNonSecretTerms().size());
+ for (AvatarAttribute attr: poa.getNonSecretTerms()){
+ md.update((attr.getBlock ().getName () + "." + attr.getName ()).getBytes ());
+ }
+ //System.out.println("Satisfied Authenticity " +poa.getSatisfiedAuthenticity().size());
+ for (String str: poa.getSatisfiedAuthenticity()){
+ md.update(str.getBytes ());
+ }
+ //System.out.println("Satisfied Weak Authenticity " +poa.getSatisfiedWeakAuthenticity().size());
+ for (String str: poa.getSatisfiedWeakAuthenticity()){
+ md.update(str.getBytes ());
+ }
+ //System.out.println("Non Satisfied Authenticity " +poa.getNonSatisfiedAuthenticity().size());
+ for (String str: poa.getNonSatisfiedAuthenticity()){
+ md.update(str.getBytes ());
+ }
+ //System.out.println("Errors " +poa.getErrors().size());
+ for (String str: poa.getErrors()){
+ md.update(str.getBytes ());
+ }
+ //System.out.println("Not proved " +poa.getNotProved().size());
+ for (String str: poa.getNotProved()){
+ md.update(str.getBytes ());
+ }
+
+ byte[] dig = md.digest ();
+ for (int i=0; i<dig.length; i++)
+ if (expected[i] != dig[i]) {
+ System.err.println ("\nCouldn't analyze ProVerif typed output...\n");
+ System.exit (-1);
+ }
+
+ //System.out.print ("{");
+ //for (byte b: dig) {
+ // System.out.print (b);
+ // System.out.print (", ");
+ //}
+ //System.out.println ();
+
+ //Untyped Tests
+ //System.out.println("Untyped Tests");
+
+ br = new BufferedReader(new FileReader("untyped.txt"));
+ while ((sCurrentLine = br.readLine()) != null) {
+ s= s.concat(sCurrentLine+"\n");
+ }
+ //System.out.println(s);
+
+ //System.out.println("__________________________________");
+
+
+ poa = new ProVerifOutputAnalyzer(
+ new AVATAR2ProVerif (avspec) {
+ public String getTrueName (AvatarAttribute attr) {
+ return AVATAR2ProVerif.translateTerm (attr, null);
+ }
+ });
+ poa.analyzeOutput(s,false);
+
+ md.reset ();
+
+ //System.out.println("Reachable Events " + poa.getReachableEvents().size());
+ for (String str: poa.getReachableEvents()){
+ md.update(str.getBytes ());
+ }
+
+ //System.out.println("NonReachable Events " + poa.getNonReachableEvents().size());
+ for (String str: poa.getNonReachableEvents()){
+ md.update(str.getBytes ());
+ }
+ //System.out.println("Secret Terms " + poa.getSecretTerms().size());
+ for (AvatarAttribute attr: poa.getSecretTerms()){
+ md.update((attr.getBlock ().getName () + "." + attr.getName ()).getBytes ());
+ }
+ //System.out.println("Non Secret Terms " + poa.getNonSecretTerms().size());
+ for (AvatarAttribute attr: poa.getNonSecretTerms()){
+ md.update((attr.getBlock ().getName () + "." + attr.getName ()).getBytes ());
+ }
+ //System.out.println("Satisfied Authenticity " +poa.getSatisfiedAuthenticity().size());
+ for (String str: poa.getSatisfiedAuthenticity()){
+ md.update(str.getBytes ());
+ }
+ //System.out.println("Satisfied Weak Authenticity " +poa.getSatisfiedWeakAuthenticity().size());
+ for (String str: poa.getSatisfiedWeakAuthenticity()){
+ md.update(str.getBytes ());
+ }
+ //System.out.println("Non Satisfied Authenticity " +poa.getNonSatisfiedAuthenticity().size());
+ for (String str: poa.getNonSatisfiedAuthenticity()){
+ md.update(str.getBytes ());
+ }
+ //System.out.println("Errors " +poa.getErrors().size());
+ for (String str: poa.getErrors()){
+ md.update(str.getBytes ());
+ }
+ //System.out.println("Not proved " +poa.getNotProved().size());
+ for (String str: poa.getNotProved()){
+ md.update(str.getBytes ());
+ }
+
+ dig = md.digest ();
+ for (int i=0; i<dig.length; i++)
+ if (expected[i] != dig[i]) {
+ System.err.println ("\nCouldn't analyze ProVerif untyped output...\n");
+ System.exit (-1);
+ }
+
+ System.out.println(": ok");
+
+ } catch (IOException | NoSuchAlgorithmException e) {
+ e.printStackTrace();
+ System.exit (-1);
+ } finally {
+ try {
+ if (br != null)br.close();
+ } catch (IOException ex) {
+ ex.printStackTrace();
+ System.exit (-1);
+ }
+ }
+
+ }
+}
diff --git a/src/proverifspec/typed.txt b/tests/Avatar/ProVerif/typed.txt
similarity index 100%
rename from src/proverifspec/typed.txt
rename to tests/Avatar/ProVerif/typed.txt
diff --git a/tests/Avatar/ProVerif/untyped.txt b/tests/Avatar/ProVerif/untyped.txt
new file mode 100644
index 0000000000000000000000000000000000000000..a247237146aa452e1563595d718a83d8413a8a40
--- /dev/null
+++ b/tests/Avatar/ProVerif/untyped.txt
@@ -0,0 +1,599 @@
+Process:
+(
+ {1}!
+ {2}in(chControl, chControlData_101);
+ {3}let call__num_102 = chControlDec(chControlData_101) in
+ {4}if (call__num_102 = call__System__0) then
+ 0
+) | (
+ {5}!
+ {6}in(chControl, chControlData_106);
+ {7}let (call__num_107,Bob__m__data__1_108,Bob__m2__data__1_109,Bob__sk__data__1_110,Bob__receivedData__1_111) = chControlDec(chControlData_106) in
+ {8}if (call__num_107 = call__Bob__0) then
+ {9}event enteringState__Bob__waitingForMessage();
+ {10}event authenticity__Bob__m2__data__waitingForMessage(Bob__m2__data__1_109);
+ {11}in(ch, privChData_112);
+ {12}let Bob__m2__data__2_113 = privChDec(privChData_112) in
+ {13}event enteringState__Bob__messageDecrypt();
+ {14}let Bob__m__data__2_114 = sdecrypt(Bob__m2__data__2_113,Bob__sk__data__1_110) in
+ {15}event enteringState__Bob__messageDecrypted();
+ {16}event authenticity__Bob__m__data__messageDecrypted(Bob__m__data__2_114);
+ {17}let Bob__receivedData__2_115 = Bob__m__data__2_114 in
+ {18}event enteringState__Bob__SecretDataReceived()
+) | (
+ {19}!
+ {20}in(chControl, chControlData_116);
+ {21}let (call__num_117,Alice__secretData__1_118,Alice__m__data__1_119,Alice__m1__data__1_120,Alice__sk__data__1_121) = chControlDec(chControlData_116) in
+ {22}if (call__num_117 = call__Alice__0) then
+ {23}event enteringState__Alice__makingMessage();
+ {24}let Alice__m__data__2_122 = Alice__secretData__1_118 in
+ {25}let Alice__m1__data__2_123 = sencrypt(Alice__m__data__2_122,Alice__sk__data__1_121) in
+ {26}event enteringState__Alice__sendingMessage();
+ {27}event authenticity__Alice__m1__data__sendingMessage(Alice__m1__data__2_123);
+ {28}event authenticity__Alice__m__data__sendingMessage(Alice__m__data__2_122);
+ {29}out(ch, privChEnc(Alice__m1__data__2_123))
+) | (
+ {30}!
+ {31}new Alice__sk__data_124;
+ {32}let Bob__sk__data_125 = Alice__sk__data_124 in
+ (
+ {33}out(chControl, chControlEnc((call__System__0)))
+ ) | (
+ {34}new Bob__m__data_126;
+ {35}new Bob__m2__data_127;
+ {36}new Bob__receivedData_128;
+ {37}out(chControl, chControlEnc((call__Bob__0,Bob__m__data_126,Bob__m2__data_127,Bob__sk__data_125,Bob__receivedData_128)))
+ ) | (
+ {38}new Alice__secretData_129;
+ {39}new Alice__m__data_130;
+ {40}new Alice__m1__data_131;
+ {41}out(chControl, chControlEnc((call__Alice__0,Alice__secretData_129,Alice__m__data_130,Alice__m1__data_131,Alice__sk__data_124)))
+ )
+)
+
+-- Query evinj:authenticity__Bob__m__data__messageDecrypted(dummyM_201) ==> evinj:authenticity__Alice__m__data__sendingMessage(dummyM_201)
+Completing...
+Starting query evinj:authenticity__Bob__m__data__messageDecrypted(dummyM_201) ==> evinj:authenticity__Alice__m__data__sendingMessage(dummyM_201)
+goal reachable: begin:authenticity__Alice__m__data__sendingMessage(Alice__secretData_129[!1 = @sid_731]), chControlData_116 = chControlEnc((call__Alice__0[],Alice__secretData_129[!1 = @sid_731],Alice__m__data_130[!1 = @sid_731],Alice__m1__data_131[!1 = @sid_731],Alice__sk__data_124[!1 = @sid_731])), @sid_494 = @sid_732, @occ28_544 = @occ_cst() -> end:endsid_733,authenticity__Bob__m__data__messageDecrypted(Alice__secretData_129[!1 = @sid_731])
+Abbreviations:
+Alice__secretData_756 = Alice__secretData_129[!1 = @sid_747]
+Alice__sk__data_757 = Alice__sk__data_124[!1 = @sid_747]
+Alice__m__data_758 = Alice__m__data_130[!1 = @sid_747]
+Alice__m1__data_759 = Alice__m1__data_131[!1 = @sid_747]
+Bob__m__data_760 = Bob__m__data_126[!1 = @sid_747]
+Bob__m2__data_761 = Bob__m2__data_127[!1 = @sid_747]
+Bob__receivedData_762 = Bob__receivedData_128[!1 = @sid_747]
+
+1. The message chControlEnc((call__Bob__0[],Bob__m__data_760,Bob__m2__data_761,Alice__sk__data_757,Bob__receivedData_762)) may be sent to the attacker at output {37}.
+attacker:chControlEnc((call__Bob__0[],Bob__m__data_760,Bob__m2__data_761,Alice__sk__data_757,Bob__receivedData_762)).
+
+2. The message chControlEnc((call__Alice__0[],Alice__secretData_756,Alice__m__data_758,Alice__m1__data_759,Alice__sk__data_757)) may be sent to the attacker at output {41}.
+attacker:chControlEnc((call__Alice__0[],Alice__secretData_756,Alice__m__data_758,Alice__m1__data_759,Alice__sk__data_757)).
+
+3. The message chControlEnc((call__Alice__0[],Alice__secretData_756,Alice__m__data_758,Alice__m1__data_759,Alice__sk__data_757)) that the attacker may have by 2 may be received at input {20}.
+The event authenticity__Alice__m__data__sendingMessage(Alice__secretData_756) (with environment chControlData_116 = chControlEnc((call__Alice__0[],Alice__secretData_756,Alice__m__data_758,Alice__m1__data_759,Alice__sk__data_757)), @sid_494 = @sid_746, @occ28_544 = @occ_cst()) may be executed at {28}.
+So the message privChEnc(sencrypt(Alice__secretData_756,Alice__sk__data_757)) may be sent to the attacker at output {29}.
+attacker:privChEnc(sencrypt(Alice__secretData_756,Alice__sk__data_757)).
+
+4. The message chControlEnc((call__Bob__0[],Bob__m__data_760,Bob__m2__data_761,Alice__sk__data_757,Bob__receivedData_762)) that the attacker may have by 1 may be received at input {6}.
+The message privChEnc(sencrypt(Alice__secretData_756,Alice__sk__data_757)) that the attacker may have by 3 may be received at input {11}.
+So event authenticity__Bob__m__data__messageDecrypted(Alice__secretData_756) may be executed at {16} in session endsid_754.
+end:endsid_754,authenticity__Bob__m__data__messageDecrypted(Alice__secretData_756).
+
+
+A more detailed output of the traces is available with
+ param traceDisplay = long.
+
+new Alice__sk__data_124 creating Alice__sk__data_124_769 at {31} in copy a_764
+
+new Alice__secretData_129 creating Alice__secretData_129_766 at {38} in copy a_764
+
+new Alice__m__data_130 creating Alice__m__data_130_767 at {39} in copy a_764
+
+new Alice__m1__data_131 creating Alice__m1__data_131_768 at {40} in copy a_764
+
+out(chControl, chControlEnc((call__Alice__0,Alice__secretData_129_766,Alice__m__data_130_767,Alice__m1__data_131_768,Alice__sk__data_124_769))) at {41} in copy a_764
+
+new Bob__m__data_126 creating Bob__m__data_126_770 at {34} in copy a_764
+
+new Bob__m2__data_127 creating Bob__m2__data_127_771 at {35} in copy a_764
+
+new Bob__receivedData_128 creating Bob__receivedData_128_772 at {36} in copy a_764
+
+out(chControl, chControlEnc((call__Bob__0,Bob__m__data_126_770,Bob__m2__data_127_771,Alice__sk__data_124_769,Bob__receivedData_128_772))) at {37} in copy a_764
+
+out(chControl, chControlEnc((call__System__0))) at {33} in copy a_764
+
+in(chControl, chControlEnc((call__Bob__0,Bob__m__data_126_770,Bob__m2__data_127_771,Alice__sk__data_124_769,Bob__receivedData_128_772))) at {6} in copy a_763
+
+event(enteringState__Bob__waitingForMessage()) at {9} in copy a_763
+
+event(authenticity__Bob__m2__data__waitingForMessage(Bob__m2__data_127_771)) at {10} in copy a_763
+
+in(chControl, chControlEnc((call__Alice__0,Alice__secretData_129_766,Alice__m__data_130_767,Alice__m1__data_131_768,Alice__sk__data_124_769))) at {20} in copy a_765
+
+event(enteringState__Alice__makingMessage()) at {23} in copy a_765
+
+event(enteringState__Alice__sendingMessage()) at {26} in copy a_765
+
+event(authenticity__Alice__m1__data__sendingMessage(sencrypt(Alice__secretData_129_766,Alice__sk__data_124_769))) at {27} in copy a_765
+
+event(authenticity__Alice__m__data__sendingMessage(Alice__secretData_129_766)) at {28} in copy a_765
+
+out(ch, privChEnc(sencrypt(Alice__secretData_129_766,Alice__sk__data_124_769))) at {29} in copy a_765
+
+in(ch, privChEnc(sencrypt(Alice__secretData_129_766,Alice__sk__data_124_769))) at {11} in copy a_763
+
+event(enteringState__Bob__messageDecrypt()) at {13} in copy a_763
+
+event(enteringState__Bob__messageDecrypted()) at {15} in copy a_763
+
+event(authenticity__Bob__m__data__messageDecrypted(Alice__secretData_129_766)) at {16} in copy a_763
+
+The event authenticity__Bob__m__data__messageDecrypted(Alice__secretData_129_766) is executed in session a_763.
+A trace has been found.
+I am now trying to reconstruct a trace that falsifies injectivity.
+Could not find a trace that contradicts injectivity.
+RESULT evinj:authenticity__Bob__m__data__messageDecrypted(dummyM_201) ==> evinj:authenticity__Alice__m__data__sendingMessage(dummyM_201) cannot be proved.
+RESULT (but ev:authenticity__Bob__m__data__messageDecrypted(dummyM_734) ==> ev:authenticity__Alice__m__data__sendingMessage(dummyM_734) is true.)
+-- Query evinj:authenticity__Bob__m2__data__waitingForMessage(dummyM_1132) ==> evinj:authenticity__Alice__m1__data__sendingMessage(dummyM_1132)
+Completing...
+Starting query evinj:authenticity__Bob__m2__data__waitingForMessage(dummyM_1132) ==> evinj:authenticity__Alice__m1__data__sendingMessage(dummyM_1132)
+goal reachable: end:endsid_1604,authenticity__Bob__m2__data__waitingForMessage(Bob__m2__data_127[!1 = @sid_1605])
+Abbreviations:
+Bob__m2__data_1616 = Bob__m2__data_127[!1 = @sid_1608]
+Bob__m__data_1617 = Bob__m__data_126[!1 = @sid_1608]
+Alice__sk__data_1618 = Alice__sk__data_124[!1 = @sid_1608]
+Bob__receivedData_1619 = Bob__receivedData_128[!1 = @sid_1608]
+
+1. The message chControlEnc((call__Bob__0[],Bob__m__data_1617,Bob__m2__data_1616,Alice__sk__data_1618,Bob__receivedData_1619)) may be sent to the attacker at output {37}.
+attacker:chControlEnc((call__Bob__0[],Bob__m__data_1617,Bob__m2__data_1616,Alice__sk__data_1618,Bob__receivedData_1619)).
+
+2. The message chControlEnc((call__Bob__0[],Bob__m__data_1617,Bob__m2__data_1616,Alice__sk__data_1618,Bob__receivedData_1619)) that the attacker may have by 1 may be received at input {6}.
+So event authenticity__Bob__m2__data__waitingForMessage(Bob__m2__data_1616) may be executed at {10} in session endsid_1614.
+end:endsid_1614,authenticity__Bob__m2__data__waitingForMessage(Bob__m2__data_1616).
+
+
+A more detailed output of the traces is available with
+ param traceDisplay = long.
+
+new Alice__sk__data_124 creating Alice__sk__data_124_1624 at {31} in copy a_1621
+
+new Alice__secretData_129 creating Alice__secretData_129_1628 at {38} in copy a_1621
+
+new Alice__m__data_130 creating Alice__m__data_130_1629 at {39} in copy a_1621
+
+new Alice__m1__data_131 creating Alice__m1__data_131_1630 at {40} in copy a_1621
+
+out(chControl, chControlEnc((call__Alice__0,Alice__secretData_129_1628,Alice__m__data_130_1629,Alice__m1__data_131_1630,Alice__sk__data_124_1624))) at {41} in copy a_1621
+
+new Bob__m__data_126 creating Bob__m__data_126_1623 at {34} in copy a_1621
+
+new Bob__m2__data_127 creating Bob__m2__data_127_1622 at {35} in copy a_1621
+
+new Bob__receivedData_128 creating Bob__receivedData_128_1625 at {36} in copy a_1621
+
+out(chControl, chControlEnc((call__Bob__0,Bob__m__data_126_1623,Bob__m2__data_127_1622,Alice__sk__data_124_1624,Bob__receivedData_128_1625))) at {37} in copy a_1621
+
+out(chControl, chControlEnc((call__System__0))) at {33} in copy a_1621
+
+in(chControl, chControlEnc((call__Bob__0,Bob__m__data_126_1623,Bob__m2__data_127_1622,Alice__sk__data_124_1624,Bob__receivedData_128_1625))) at {6} in copy a_1620
+
+event(enteringState__Bob__waitingForMessage()) at {9} in copy a_1620
+
+event(authenticity__Bob__m2__data__waitingForMessage(Bob__m2__data_127_1622)) at {10} in copy a_1620
+
+The event authenticity__Bob__m2__data__waitingForMessage(Bob__m2__data_127_1622) is executed in session a_1620.
+A trace has been found.
+RESULT evinj:authenticity__Bob__m2__data__waitingForMessage(dummyM_1132) ==> evinj:authenticity__Alice__m1__data__sendingMessage(dummyM_1132) is false.
+RESULT (even ev:authenticity__Bob__m2__data__waitingForMessage(dummyM_1606) ==> ev:authenticity__Alice__m1__data__sendingMessage(dummyM_1606) is false.)
+-- Query not ev:enteringState__Alice__makingMessage()
+Completing...
+Starting query not ev:enteringState__Alice__makingMessage()
+goal reachable: end:enteringState__Alice__makingMessage()
+Abbreviations:
+Alice__secretData_2124 = Alice__secretData_129[!1 = @sid_2118]
+Alice__m__data_2125 = Alice__m__data_130[!1 = @sid_2118]
+Alice__m1__data_2126 = Alice__m1__data_131[!1 = @sid_2118]
+Alice__sk__data_2127 = Alice__sk__data_124[!1 = @sid_2118]
+
+1. The message chControlEnc((call__Alice__0[],Alice__secretData_2124,Alice__m__data_2125,Alice__m1__data_2126,Alice__sk__data_2127)) may be sent to the attacker at output {41}.
+attacker:chControlEnc((call__Alice__0[],Alice__secretData_2124,Alice__m__data_2125,Alice__m1__data_2126,Alice__sk__data_2127)).
+
+2. The message chControlEnc((call__Alice__0[],Alice__secretData_2124,Alice__m__data_2125,Alice__m1__data_2126,Alice__sk__data_2127)) that the attacker may have by 1 may be received at input {20}.
+So event enteringState__Alice__makingMessage() may be executed at {23}.
+end:enteringState__Alice__makingMessage().
+
+
+A more detailed output of the traces is available with
+ param traceDisplay = long.
+
+new Alice__sk__data_124 creating Alice__sk__data_124_2133 at {31} in copy a_2128
+
+new Alice__secretData_129 creating Alice__secretData_129_2130 at {38} in copy a_2128
+
+new Alice__m__data_130 creating Alice__m__data_130_2131 at {39} in copy a_2128
+
+new Alice__m1__data_131 creating Alice__m1__data_131_2132 at {40} in copy a_2128
+
+out(chControl, chControlEnc((call__Alice__0,Alice__secretData_129_2130,Alice__m__data_130_2131,Alice__m1__data_131_2132,Alice__sk__data_124_2133))) at {41} in copy a_2128
+
+new Bob__m__data_126 creating Bob__m__data_126_2136 at {34} in copy a_2128
+
+new Bob__m2__data_127 creating Bob__m2__data_127_2137 at {35} in copy a_2128
+
+new Bob__receivedData_128 creating Bob__receivedData_128_2138 at {36} in copy a_2128
+
+out(chControl, chControlEnc((call__Bob__0,Bob__m__data_126_2136,Bob__m2__data_127_2137,Alice__sk__data_124_2133,Bob__receivedData_128_2138))) at {37} in copy a_2128
+
+out(chControl, chControlEnc((call__System__0))) at {33} in copy a_2128
+
+in(chControl, chControlEnc((call__Alice__0,Alice__secretData_129_2130,Alice__m__data_130_2131,Alice__m1__data_131_2132,Alice__sk__data_124_2133))) at {20} in copy a_2129
+
+event(enteringState__Alice__makingMessage()) at {23} in copy a_2129
+
+The event enteringState__Alice__makingMessage() is executed.
+A trace has been found.
+RESULT not ev:enteringState__Alice__makingMessage() is false.
+-- Query not ev:enteringState__Alice__sendingMessage()
+Completing...
+Starting query not ev:enteringState__Alice__sendingMessage()
+goal reachable: end:enteringState__Alice__sendingMessage()
+Abbreviations:
+Alice__secretData_2626 = Alice__secretData_129[!1 = @sid_2620]
+Alice__m__data_2627 = Alice__m__data_130[!1 = @sid_2620]
+Alice__m1__data_2628 = Alice__m1__data_131[!1 = @sid_2620]
+Alice__sk__data_2629 = Alice__sk__data_124[!1 = @sid_2620]
+
+1. The message chControlEnc((call__Alice__0[],Alice__secretData_2626,Alice__m__data_2627,Alice__m1__data_2628,Alice__sk__data_2629)) may be sent to the attacker at output {41}.
+attacker:chControlEnc((call__Alice__0[],Alice__secretData_2626,Alice__m__data_2627,Alice__m1__data_2628,Alice__sk__data_2629)).
+
+2. The message chControlEnc((call__Alice__0[],Alice__secretData_2626,Alice__m__data_2627,Alice__m1__data_2628,Alice__sk__data_2629)) that the attacker may have by 1 may be received at input {20}.
+So event enteringState__Alice__sendingMessage() may be executed at {26}.
+end:enteringState__Alice__sendingMessage().
+
+
+A more detailed output of the traces is available with
+ param traceDisplay = long.
+
+new Alice__sk__data_124 creating Alice__sk__data_124_2635 at {31} in copy a_2630
+
+new Alice__secretData_129 creating Alice__secretData_129_2632 at {38} in copy a_2630
+
+new Alice__m__data_130 creating Alice__m__data_130_2633 at {39} in copy a_2630
+
+new Alice__m1__data_131 creating Alice__m1__data_131_2634 at {40} in copy a_2630
+
+out(chControl, chControlEnc((call__Alice__0,Alice__secretData_129_2632,Alice__m__data_130_2633,Alice__m1__data_131_2634,Alice__sk__data_124_2635))) at {41} in copy a_2630
+
+new Bob__m__data_126 creating Bob__m__data_126_2638 at {34} in copy a_2630
+
+new Bob__m2__data_127 creating Bob__m2__data_127_2639 at {35} in copy a_2630
+
+new Bob__receivedData_128 creating Bob__receivedData_128_2640 at {36} in copy a_2630
+
+out(chControl, chControlEnc((call__Bob__0,Bob__m__data_126_2638,Bob__m2__data_127_2639,Alice__sk__data_124_2635,Bob__receivedData_128_2640))) at {37} in copy a_2630
+
+out(chControl, chControlEnc((call__System__0))) at {33} in copy a_2630
+
+in(chControl, chControlEnc((call__Alice__0,Alice__secretData_129_2632,Alice__m__data_130_2633,Alice__m1__data_131_2634,Alice__sk__data_124_2635))) at {20} in copy a_2631
+
+event(enteringState__Alice__makingMessage()) at {23} in copy a_2631
+
+event(enteringState__Alice__sendingMessage()) at {26} in copy a_2631
+
+The event enteringState__Alice__sendingMessage() is executed.
+A trace has been found.
+RESULT not ev:enteringState__Alice__sendingMessage() is false.
+-- Query not ev:enteringState__Bob__waitingForMessage()
+Completing...
+Starting query not ev:enteringState__Bob__waitingForMessage()
+goal reachable: end:enteringState__Bob__waitingForMessage()
+Abbreviations:
+Bob__m__data_3129 = Bob__m__data_126[!1 = @sid_3123]
+Bob__m2__data_3130 = Bob__m2__data_127[!1 = @sid_3123]
+Alice__sk__data_3131 = Alice__sk__data_124[!1 = @sid_3123]
+Bob__receivedData_3132 = Bob__receivedData_128[!1 = @sid_3123]
+
+1. The message chControlEnc((call__Bob__0[],Bob__m__data_3129,Bob__m2__data_3130,Alice__sk__data_3131,Bob__receivedData_3132)) may be sent to the attacker at output {37}.
+attacker:chControlEnc((call__Bob__0[],Bob__m__data_3129,Bob__m2__data_3130,Alice__sk__data_3131,Bob__receivedData_3132)).
+
+2. The message chControlEnc((call__Bob__0[],Bob__m__data_3129,Bob__m2__data_3130,Alice__sk__data_3131,Bob__receivedData_3132)) that the attacker may have by 1 may be received at input {6}.
+So event enteringState__Bob__waitingForMessage() may be executed at {9}.
+end:enteringState__Bob__waitingForMessage().
+
+
+A more detailed output of the traces is available with
+ param traceDisplay = long.
+
+new Alice__sk__data_124 creating Alice__sk__data_124_3137 at {31} in copy a_3133
+
+new Alice__secretData_129 creating Alice__secretData_129_3141 at {38} in copy a_3133
+
+new Alice__m__data_130 creating Alice__m__data_130_3142 at {39} in copy a_3133
+
+new Alice__m1__data_131 creating Alice__m1__data_131_3143 at {40} in copy a_3133
+
+out(chControl, chControlEnc((call__Alice__0,Alice__secretData_129_3141,Alice__m__data_130_3142,Alice__m1__data_131_3143,Alice__sk__data_124_3137))) at {41} in copy a_3133
+
+new Bob__m__data_126 creating Bob__m__data_126_3135 at {34} in copy a_3133
+
+new Bob__m2__data_127 creating Bob__m2__data_127_3136 at {35} in copy a_3133
+
+new Bob__receivedData_128 creating Bob__receivedData_128_3138 at {36} in copy a_3133
+
+out(chControl, chControlEnc((call__Bob__0,Bob__m__data_126_3135,Bob__m2__data_127_3136,Alice__sk__data_124_3137,Bob__receivedData_128_3138))) at {37} in copy a_3133
+
+out(chControl, chControlEnc((call__System__0))) at {33} in copy a_3133
+
+in(chControl, chControlEnc((call__Bob__0,Bob__m__data_126_3135,Bob__m2__data_127_3136,Alice__sk__data_124_3137,Bob__receivedData_128_3138))) at {6} in copy a_3134
+
+event(enteringState__Bob__waitingForMessage()) at {9} in copy a_3134
+
+The event enteringState__Bob__waitingForMessage() is executed.
+A trace has been found.
+RESULT not ev:enteringState__Bob__waitingForMessage() is false.
+-- Query not ev:enteringState__Bob__messageDecrypt()
+Completing...
+Starting query not ev:enteringState__Bob__messageDecrypt()
+goal reachable: end:enteringState__Bob__messageDecrypt()
+Abbreviations:
+Alice__secretData_3646 = Alice__secretData_129[!1 = @sid_3633]
+Alice__sk__data_3647 = Alice__sk__data_124[!1 = @sid_3633]
+Alice__m__data_3648 = Alice__m__data_130[!1 = @sid_3633]
+Alice__m1__data_3649 = Alice__m1__data_131[!1 = @sid_3633]
+Bob__m__data_3650 = Bob__m__data_126[!1 = @sid_3639]
+Bob__m2__data_3651 = Bob__m2__data_127[!1 = @sid_3639]
+Alice__sk__data_3652 = Alice__sk__data_124[!1 = @sid_3639]
+Bob__receivedData_3653 = Bob__receivedData_128[!1 = @sid_3639]
+
+1. The message chControlEnc((call__Bob__0[],Bob__m__data_3650,Bob__m2__data_3651,Alice__sk__data_3652,Bob__receivedData_3653)) may be sent to the attacker at output {37}.
+attacker:chControlEnc((call__Bob__0[],Bob__m__data_3650,Bob__m2__data_3651,Alice__sk__data_3652,Bob__receivedData_3653)).
+
+2. The message chControlEnc((call__Alice__0[],Alice__secretData_3646,Alice__m__data_3648,Alice__m1__data_3649,Alice__sk__data_3647)) may be sent to the attacker at output {41}.
+attacker:chControlEnc((call__Alice__0[],Alice__secretData_3646,Alice__m__data_3648,Alice__m1__data_3649,Alice__sk__data_3647)).
+
+3. The message chControlEnc((call__Alice__0[],Alice__secretData_3646,Alice__m__data_3648,Alice__m1__data_3649,Alice__sk__data_3647)) that the attacker may have by 2 may be received at input {20}.
+So the message privChEnc(sencrypt(Alice__secretData_3646,Alice__sk__data_3647)) may be sent to the attacker at output {29}.
+attacker:privChEnc(sencrypt(Alice__secretData_3646,Alice__sk__data_3647)).
+
+4. The message chControlEnc((call__Bob__0[],Bob__m__data_3650,Bob__m2__data_3651,Alice__sk__data_3652,Bob__receivedData_3653)) that the attacker may have by 1 may be received at input {6}.
+The message privChEnc(sencrypt(Alice__secretData_3646,Alice__sk__data_3647)) that the attacker may have by 3 may be received at input {11}.
+So event enteringState__Bob__messageDecrypt() may be executed at {13}.
+end:enteringState__Bob__messageDecrypt().
+
+
+A more detailed output of the traces is available with
+ param traceDisplay = long.
+
+new Alice__sk__data_124 creating Alice__sk__data_124_3664 at {31} in copy a_3656
+
+new Alice__secretData_129 creating Alice__secretData_129_3669 at {38} in copy a_3656
+
+new Alice__m__data_130 creating Alice__m__data_130_3670 at {39} in copy a_3656
+
+new Alice__m1__data_131 creating Alice__m1__data_131_3671 at {40} in copy a_3656
+
+out(chControl, chControlEnc((call__Alice__0,Alice__secretData_129_3669,Alice__m__data_130_3670,Alice__m1__data_131_3671,Alice__sk__data_124_3664))) at {41} in copy a_3656
+
+new Bob__m__data_126 creating Bob__m__data_126_3662 at {34} in copy a_3656
+
+new Bob__m2__data_127 creating Bob__m2__data_127_3663 at {35} in copy a_3656
+
+new Bob__receivedData_128 creating Bob__receivedData_128_3665 at {36} in copy a_3656
+
+out(chControl, chControlEnc((call__Bob__0,Bob__m__data_126_3662,Bob__m2__data_127_3663,Alice__sk__data_124_3664,Bob__receivedData_128_3665))) at {37} in copy a_3656
+
+out(chControl, chControlEnc((call__System__0))) at {33} in copy a_3656
+
+new Alice__sk__data_124 creating Alice__sk__data_124_3661 at {31} in copy a_3654
+
+new Alice__secretData_129 creating Alice__secretData_129_3658 at {38} in copy a_3654
+
+new Alice__m__data_130 creating Alice__m__data_130_3659 at {39} in copy a_3654
+
+new Alice__m1__data_131 creating Alice__m1__data_131_3660 at {40} in copy a_3654
+
+out(chControl, chControlEnc((call__Alice__0,Alice__secretData_129_3658,Alice__m__data_130_3659,Alice__m1__data_131_3660,Alice__sk__data_124_3661))) at {41} in copy a_3654
+
+new Bob__m__data_126 creating Bob__m__data_126_3672 at {34} in copy a_3654
+
+new Bob__m2__data_127 creating Bob__m2__data_127_3673 at {35} in copy a_3654
+
+new Bob__receivedData_128 creating Bob__receivedData_128_3674 at {36} in copy a_3654
+
+out(chControl, chControlEnc((call__Bob__0,Bob__m__data_126_3672,Bob__m2__data_127_3673,Alice__sk__data_124_3661,Bob__receivedData_128_3674))) at {37} in copy a_3654
+
+out(chControl, chControlEnc((call__System__0))) at {33} in copy a_3654
+
+in(chControl, chControlEnc((call__Bob__0,Bob__m__data_126_3662,Bob__m2__data_127_3663,Alice__sk__data_124_3664,Bob__receivedData_128_3665))) at {6} in copy a_3657
+
+event(enteringState__Bob__waitingForMessage()) at {9} in copy a_3657
+
+event(authenticity__Bob__m2__data__waitingForMessage(Bob__m2__data_127_3663)) at {10} in copy a_3657
+
+in(chControl, chControlEnc((call__Alice__0,Alice__secretData_129_3658,Alice__m__data_130_3659,Alice__m1__data_131_3660,Alice__sk__data_124_3661))) at {20} in copy a_3655
+
+event(enteringState__Alice__makingMessage()) at {23} in copy a_3655
+
+event(enteringState__Alice__sendingMessage()) at {26} in copy a_3655
+
+event(authenticity__Alice__m1__data__sendingMessage(sencrypt(Alice__secretData_129_3658,Alice__sk__data_124_3661))) at {27} in copy a_3655
+
+event(authenticity__Alice__m__data__sendingMessage(Alice__secretData_129_3658)) at {28} in copy a_3655
+
+out(ch, privChEnc(sencrypt(Alice__secretData_129_3658,Alice__sk__data_124_3661))) at {29} in copy a_3655
+
+in(ch, privChEnc(sencrypt(Alice__secretData_129_3658,Alice__sk__data_124_3661))) at {11} in copy a_3657
+
+event(enteringState__Bob__messageDecrypt()) at {13} in copy a_3657
+
+The event enteringState__Bob__messageDecrypt() is executed.
+A trace has been found.
+RESULT not ev:enteringState__Bob__messageDecrypt() is false.
+-- Query not ev:enteringState__Bob__SecretDataReceived()
+Completing...
+Starting query not ev:enteringState__Bob__SecretDataReceived()
+goal reachable: end:enteringState__Bob__SecretDataReceived()
+Abbreviations:
+Alice__secretData_4211 = Alice__secretData_129[!1 = @sid_4204]
+Alice__sk__data_4212 = Alice__sk__data_124[!1 = @sid_4204]
+Alice__m__data_4213 = Alice__m__data_130[!1 = @sid_4204]
+Alice__m1__data_4214 = Alice__m1__data_131[!1 = @sid_4204]
+Bob__m__data_4215 = Bob__m__data_126[!1 = @sid_4204]
+Bob__m2__data_4216 = Bob__m2__data_127[!1 = @sid_4204]
+Bob__receivedData_4217 = Bob__receivedData_128[!1 = @sid_4204]
+
+1. The message chControlEnc((call__Bob__0[],Bob__m__data_4215,Bob__m2__data_4216,Alice__sk__data_4212,Bob__receivedData_4217)) may be sent to the attacker at output {37}.
+attacker:chControlEnc((call__Bob__0[],Bob__m__data_4215,Bob__m2__data_4216,Alice__sk__data_4212,Bob__receivedData_4217)).
+
+2. The message chControlEnc((call__Alice__0[],Alice__secretData_4211,Alice__m__data_4213,Alice__m1__data_4214,Alice__sk__data_4212)) may be sent to the attacker at output {41}.
+attacker:chControlEnc((call__Alice__0[],Alice__secretData_4211,Alice__m__data_4213,Alice__m1__data_4214,Alice__sk__data_4212)).
+
+3. The message chControlEnc((call__Alice__0[],Alice__secretData_4211,Alice__m__data_4213,Alice__m1__data_4214,Alice__sk__data_4212)) that the attacker may have by 2 may be received at input {20}.
+So the message privChEnc(sencrypt(Alice__secretData_4211,Alice__sk__data_4212)) may be sent to the attacker at output {29}.
+attacker:privChEnc(sencrypt(Alice__secretData_4211,Alice__sk__data_4212)).
+
+4. The message chControlEnc((call__Bob__0[],Bob__m__data_4215,Bob__m2__data_4216,Alice__sk__data_4212,Bob__receivedData_4217)) that the attacker may have by 1 may be received at input {6}.
+The message privChEnc(sencrypt(Alice__secretData_4211,Alice__sk__data_4212)) that the attacker may have by 3 may be received at input {11}.
+So event enteringState__Bob__SecretDataReceived() may be executed at {18}.
+end:enteringState__Bob__SecretDataReceived().
+
+
+A more detailed output of the traces is available with
+ param traceDisplay = long.
+
+new Alice__sk__data_124 creating Alice__sk__data_124_4224 at {31} in copy a_4218
+
+new Alice__secretData_129 creating Alice__secretData_129_4221 at {38} in copy a_4218
+
+new Alice__m__data_130 creating Alice__m__data_130_4222 at {39} in copy a_4218
+
+new Alice__m1__data_131 creating Alice__m1__data_131_4223 at {40} in copy a_4218
+
+out(chControl, chControlEnc((call__Alice__0,Alice__secretData_129_4221,Alice__m__data_130_4222,Alice__m1__data_131_4223,Alice__sk__data_124_4224))) at {41} in copy a_4218
+
+new Bob__m__data_126 creating Bob__m__data_126_4225 at {34} in copy a_4218
+
+new Bob__m2__data_127 creating Bob__m2__data_127_4226 at {35} in copy a_4218
+
+new Bob__receivedData_128 creating Bob__receivedData_128_4227 at {36} in copy a_4218
+
+out(chControl, chControlEnc((call__Bob__0,Bob__m__data_126_4225,Bob__m2__data_127_4226,Alice__sk__data_124_4224,Bob__receivedData_128_4227))) at {37} in copy a_4218
+
+out(chControl, chControlEnc((call__System__0))) at {33} in copy a_4218
+
+in(chControl, chControlEnc((call__Bob__0,Bob__m__data_126_4225,Bob__m2__data_127_4226,Alice__sk__data_124_4224,Bob__receivedData_128_4227))) at {6} in copy a_4220
+
+event(enteringState__Bob__waitingForMessage()) at {9} in copy a_4220
+
+event(authenticity__Bob__m2__data__waitingForMessage(Bob__m2__data_127_4226)) at {10} in copy a_4220
+
+in(chControl, chControlEnc((call__Alice__0,Alice__secretData_129_4221,Alice__m__data_130_4222,Alice__m1__data_131_4223,Alice__sk__data_124_4224))) at {20} in copy a_4219
+
+event(enteringState__Alice__makingMessage()) at {23} in copy a_4219
+
+event(enteringState__Alice__sendingMessage()) at {26} in copy a_4219
+
+event(authenticity__Alice__m1__data__sendingMessage(sencrypt(Alice__secretData_129_4221,Alice__sk__data_124_4224))) at {27} in copy a_4219
+
+event(authenticity__Alice__m__data__sendingMessage(Alice__secretData_129_4221)) at {28} in copy a_4219
+
+out(ch, privChEnc(sencrypt(Alice__secretData_129_4221,Alice__sk__data_124_4224))) at {29} in copy a_4219
+
+in(ch, privChEnc(sencrypt(Alice__secretData_129_4221,Alice__sk__data_124_4224))) at {11} in copy a_4220
+
+event(enteringState__Bob__messageDecrypt()) at {13} in copy a_4220
+
+event(enteringState__Bob__messageDecrypted()) at {15} in copy a_4220
+
+event(authenticity__Bob__m__data__messageDecrypted(Alice__secretData_129_4221)) at {16} in copy a_4220
+
+event(enteringState__Bob__SecretDataReceived()) at {18} in copy a_4220
+
+The event enteringState__Bob__SecretDataReceived() is executed.
+A trace has been found.
+RESULT not ev:enteringState__Bob__SecretDataReceived() is false.
+-- Query not ev:enteringState__Bob__messageDecrypted()
+Completing...
+Starting query not ev:enteringState__Bob__messageDecrypted()
+goal reachable: end:enteringState__Bob__messageDecrypted()
+Abbreviations:
+Alice__secretData_4769 = Alice__secretData_129[!1 = @sid_4762]
+Alice__sk__data_4770 = Alice__sk__data_124[!1 = @sid_4762]
+Alice__m__data_4771 = Alice__m__data_130[!1 = @sid_4762]
+Alice__m1__data_4772 = Alice__m1__data_131[!1 = @sid_4762]
+Bob__m__data_4773 = Bob__m__data_126[!1 = @sid_4762]
+Bob__m2__data_4774 = Bob__m2__data_127[!1 = @sid_4762]
+Bob__receivedData_4775 = Bob__receivedData_128[!1 = @sid_4762]
+
+1. The message chControlEnc((call__Bob__0[],Bob__m__data_4773,Bob__m2__data_4774,Alice__sk__data_4770,Bob__receivedData_4775)) may be sent to the attacker at output {37}.
+attacker:chControlEnc((call__Bob__0[],Bob__m__data_4773,Bob__m2__data_4774,Alice__sk__data_4770,Bob__receivedData_4775)).
+
+2. The message chControlEnc((call__Alice__0[],Alice__secretData_4769,Alice__m__data_4771,Alice__m1__data_4772,Alice__sk__data_4770)) may be sent to the attacker at output {41}.
+attacker:chControlEnc((call__Alice__0[],Alice__secretData_4769,Alice__m__data_4771,Alice__m1__data_4772,Alice__sk__data_4770)).
+
+3. The message chControlEnc((call__Alice__0[],Alice__secretData_4769,Alice__m__data_4771,Alice__m1__data_4772,Alice__sk__data_4770)) that the attacker may have by 2 may be received at input {20}.
+So the message privChEnc(sencrypt(Alice__secretData_4769,Alice__sk__data_4770)) may be sent to the attacker at output {29}.
+attacker:privChEnc(sencrypt(Alice__secretData_4769,Alice__sk__data_4770)).
+
+4. The message chControlEnc((call__Bob__0[],Bob__m__data_4773,Bob__m2__data_4774,Alice__sk__data_4770,Bob__receivedData_4775)) that the attacker may have by 1 may be received at input {6}.
+The message privChEnc(sencrypt(Alice__secretData_4769,Alice__sk__data_4770)) that the attacker may have by 3 may be received at input {11}.
+So event enteringState__Bob__messageDecrypted() may be executed at {15}.
+end:enteringState__Bob__messageDecrypted().
+
+
+A more detailed output of the traces is available with
+ param traceDisplay = long.
+
+new Alice__sk__data_124 creating Alice__sk__data_124_4782 at {31} in copy a_4776
+
+new Alice__secretData_129 creating Alice__secretData_129_4779 at {38} in copy a_4776
+
+new Alice__m__data_130 creating Alice__m__data_130_4780 at {39} in copy a_4776
+
+new Alice__m1__data_131 creating Alice__m1__data_131_4781 at {40} in copy a_4776
+
+out(chControl, chControlEnc((call__Alice__0,Alice__secretData_129_4779,Alice__m__data_130_4780,Alice__m1__data_131_4781,Alice__sk__data_124_4782))) at {41} in copy a_4776
+
+new Bob__m__data_126 creating Bob__m__data_126_4783 at {34} in copy a_4776
+
+new Bob__m2__data_127 creating Bob__m2__data_127_4784 at {35} in copy a_4776
+
+new Bob__receivedData_128 creating Bob__receivedData_128_4785 at {36} in copy a_4776
+
+out(chControl, chControlEnc((call__Bob__0,Bob__m__data_126_4783,Bob__m2__data_127_4784,Alice__sk__data_124_4782,Bob__receivedData_128_4785))) at {37} in copy a_4776
+
+out(chControl, chControlEnc((call__System__0))) at {33} in copy a_4776
+
+in(chControl, chControlEnc((call__Bob__0,Bob__m__data_126_4783,Bob__m2__data_127_4784,Alice__sk__data_124_4782,Bob__receivedData_128_4785))) at {6} in copy a_4778
+
+event(enteringState__Bob__waitingForMessage()) at {9} in copy a_4778
+
+event(authenticity__Bob__m2__data__waitingForMessage(Bob__m2__data_127_4784)) at {10} in copy a_4778
+
+in(chControl, chControlEnc((call__Alice__0,Alice__secretData_129_4779,Alice__m__data_130_4780,Alice__m1__data_131_4781,Alice__sk__data_124_4782))) at {20} in copy a_4777
+
+event(enteringState__Alice__makingMessage()) at {23} in copy a_4777
+
+event(enteringState__Alice__sendingMessage()) at {26} in copy a_4777
+
+event(authenticity__Alice__m1__data__sendingMessage(sencrypt(Alice__secretData_129_4779,Alice__sk__data_124_4782))) at {27} in copy a_4777
+
+event(authenticity__Alice__m__data__sendingMessage(Alice__secretData_129_4779)) at {28} in copy a_4777
+
+out(ch, privChEnc(sencrypt(Alice__secretData_129_4779,Alice__sk__data_124_4782))) at {29} in copy a_4777
+
+in(ch, privChEnc(sencrypt(Alice__secretData_129_4779,Alice__sk__data_124_4782))) at {11} in copy a_4778
+
+event(enteringState__Bob__messageDecrypt()) at {13} in copy a_4778
+
+event(enteringState__Bob__messageDecrypted()) at {15} in copy a_4778
+
+The event enteringState__Bob__messageDecrypted() is executed.
+A trace has been found.
+RESULT not ev:enteringState__Bob__messageDecrypted() is false.
+-- Query not attacker:Alice__secretData_129[!1 = v_4858]
+Completing...
+Starting query not attacker:Alice__secretData_129[!1 = v_4858]
+RESULT not attacker:Alice__secretData_129[!1 = v_4858] is true.
diff --git a/tests/test.mk b/tests/test.mk
new file mode 100644
index 0000000000000000000000000000000000000000..90640359a1ff3c429eee171acb3f4ecd081a48dc
--- /dev/null
+++ b/tests/test.mk
@@ -0,0 +1,7 @@
+CLASS=$(patsubst %.java,%.class,$(wildcard *.java))
+test: $(CLASS)
+ $(foreach var,$(CLASS),$(JAVA) $(CLASSPATH) "$(TTOOL_SRC):." $(patsubst %.class,%,$(var));)
+%.class: %.java
+ $(JAVAC) $(CLASSPATH) $(TTOOL_BIN)/$(JSOUP_BINARY):$(TTOOL_BIN)/$(COMMON_CODEC_BINARY):$(TTOOL_SRC) $<
+clean:
+ rm -f *.class