diff --git a/ttool/src/test/java/tmltranslator/DiplodocusSecurityTest.java b/ttool/src/test/java/tmltranslator/DiplodocusSecurityTest.java
index c509187259fdd47d17f7a26eb836c3ba3dcd3055..120fdd4df74e8b19e1c0237fb1d84629cf950046 100644
--- a/ttool/src/test/java/tmltranslator/DiplodocusSecurityTest.java
+++ b/ttool/src/test/java/tmltranslator/DiplodocusSecurityTest.java
@@ -31,9 +31,8 @@ import static org.junit.Assert.assertTrue;
@RunWith(Parameterized.class)
public class DiplodocusSecurityTest extends AbstractTest {
- final static String DIR_GEN = "tmltranslator/DiplodocusSecurityTest/";
+ final static String DIR_GEN = "tmltranslator/DiplodocusSecurityTest/GeneratedPvspec/";
final static String DIR_MODELS = "tmltranslator/DiplodocusSecurityTest/Models/";
- final static String PVSPEC_FILENAME = "generatedPvspec";
private static String currentModel;
private static ArrayList<String> currentTabs;
private static HashMap<String, String[]> goldenMap;
@@ -149,14 +148,15 @@ public class DiplodocusSecurityTest extends AbstractTest {
ProVerifSpec proverif = avatar2proverif.generateProVerif(true, true, 0, true,
true);
- TraceManager.addDev("Saving spec in " + PROVERIF_DIR + PVSPEC_FILENAME);
- FileUtils.saveFile(PROVERIF_DIR + PVSPEC_FILENAME, proverif.getStringSpec());
+ String pvspecFilename = currentModel + "_" + tab;
+ TraceManager.addDev("Saving spec in " + PROVERIF_DIR + pvspecFilename);
+ FileUtils.saveFile(PROVERIF_DIR + pvspecFilename, proverif.getStringSpec());
TraceManager.addDev("Running Proverif");
Process proc;
BufferedReader proc_in;
String str;
- String cmd = "proverif -in pitype " + PROVERIF_DIR + PVSPEC_FILENAME;
+ String cmd = "proverif -in pitype " + PROVERIF_DIR + pvspecFilename;
boolean summaryFound = false;
commMap.clear();
diff --git a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/generatedPvspec b/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/generatedPvspec
deleted file mode 100644
index d3667333e5e28cddc53d770758b63b642e6065c1..0000000000000000000000000000000000000000
--- a/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/generatedPvspec
+++ /dev/null
@@ -1,153 +0,0 @@
-
-
-(* Generated ProVerif specification *)
-set abbreviateDerivation = false.
-
-(* Boolean return types *)
-const TRUE: bitstring [data].
-const FALSE: bitstring [data].
-
-(* Functions data *)
-const UNKNOWN: bitstring [data].
-
-(* Public key cryptography *)
-fun pk (bitstring): bitstring.
-fun aencrypt (bitstring, bitstring): bitstring.
-reduc forall x: bitstring, y: bitstring; adecrypt (aencrypt (x, pk (y)), y) = x.
-fun sign (bitstring, bitstring): bitstring.
-fun verifySign (bitstring, bitstring, bitstring): bitstring
- reduc forall m: bitstring, sk: bitstring; verifySign (m, sign (m, sk), pk (sk)) = TRUE
- otherwise forall m: bitstring, m2: bitstring, ppk: bitstring; verifySign (m, m2, ppk) = FALSE.
-
-(* Certificates *)
-fun cert (bitstring, bitstring): bitstring.
-fun verifyCert (bitstring, bitstring): bitstring
- reduc forall epk: bitstring, sk: bitstring; verifyCert (cert (epk, sign (epk, sk)), pk (sk)) = TRUE
- otherwise forall m: bitstring, ppk: bitstring; verifyCert (m, ppk) = FALSE.
-reduc forall epk: bitstring, sk: bitstring; getpk (cert (epk, sign (epk,sk))) = epk.
-
-(* Symmetric key cryptography *)
-fun sencrypt (bitstring, bitstring): bitstring.
-reduc forall x: bitstring, k: bitstring; sdecrypt (sencrypt (x, k), k) = x.
-
-(* Diffie-Hellman *)
-fun DH (bitstring, bitstring): bitstring.
-equation forall x: bitstring, y: bitstring; DH (pk (x), y) = DH (pk (y), x).
-
-(* MAC *)
-fun MAC (bitstring, bitstring): bitstring.
-fun verifyMAC (bitstring, bitstring, bitstring): bitstring
- reduc forall m: bitstring, k: bitstring; verifyMAC (m, k, MAC (m, k)) = TRUE
- otherwise forall m: bitstring, m2: bitstring, k: bitstring; verifyMAC (m, k, m2) = FALSE.
-
-(* HASH *)
-fun hash (bitstring): bitstring.
-
-(* Key and host *)
-fun host (bitstring): bitstring.
-reduc forall x: bitstring; getKey (host (x)) = x.
-
-(* Channel *)
-free ch: channel.
-
-(* Control Channel *)
-free chControl: channel.
-fun chControlEnc (bitstring): bitstring [private].
-reduc forall x: bitstring; chControlDec (chControlEnc (x)) = x [private].
-
-(* Basic Peano Arithmetic *)
-const O: bitstring [data].
-fun N (bitstring): bitstring.
-free call___Alice___0: bitstring [private].
-free call___Bob___0: bitstring [private].
-
-(* Constants *)
-
-(* Secrecy Assumptions *)
-
-(* Queries Secret *)
-query attacker(new Alice___KeyExchange__comm_chData).
-
-(* Queries Event *)
-
-(* Authenticity *)
-event authenticity___Alice___comm_chData___signalstate_KeyExchange_comm_KeyExchange_comm(bitstring).
-event authenticity___Bob___comm_chData___aftersignalstate_KeyExchange_comm_KeyExchange_comm(bitstring).
-query dummyM: bitstring; inj-event(authenticity___Bob___comm_chData___aftersignalstate_KeyExchange_comm_KeyExchange_comm (dummyM)) ==> inj-event(authenticity___Alice___comm_chData___signalstate_KeyExchange_comm_KeyExchange_comm (dummyM)).
-event authenticity___Bob___comm_chData___aftersignalstate_KeyExchange_comm_KeyExchange_comm727(bitstring).
-query dummyM: bitstring; inj-event(authenticity___Bob___comm_chData___aftersignalstate_KeyExchange_comm_KeyExchange_comm727 (dummyM)) ==> inj-event(authenticity___Alice___comm_chData___signalstate_KeyExchange_comm_KeyExchange_comm (dummyM)).
-event authenticity___Alice___comm_chData___signalstate_KeyExchange_comm_KeyExchange_comm681(bitstring).
-query dummyM: bitstring; inj-event(authenticity___Bob___comm_chData___aftersignalstate_KeyExchange_comm_KeyExchange_comm (dummyM)) ==> inj-event(authenticity___Alice___comm_chData___signalstate_KeyExchange_comm_KeyExchange_comm681 (dummyM)).
-query dummyM: bitstring; inj-event(authenticity___Bob___comm_chData___aftersignalstate_KeyExchange_comm_KeyExchange_comm727 (dummyM)) ==> inj-event(authenticity___Alice___comm_chData___signalstate_KeyExchange_comm_KeyExchange_comm681 (dummyM)).
-
-let Alice___start (sessionID: bitstring) =
- new Alice___key_symKey[]: bitstring;
- new Alice___pubKey_aenc[]: bitstring;
- new Alice___KeyExchange__comm_chData[]: bitstring;
- new Alice___tmp[]: bitstring;
- new Alice___loop_index[]: bitstring;
- new Alice___aenc_encrypted[]: bitstring;
- new Alice___aenc[]: bitstring;
- new Alice___privKey_aenc[]: bitstring;
- new Alice___comm_chData[]: bitstring;
- new Alice___symKey[]: bitstring;
- new Alice___symKey_encrypted[]: bitstring;
- in (chControl, strong___Alice___01: bitstring);
- out (chControl, chControlEnc ((sessionID, call___Alice___0, strong___Alice___01, Alice___key_symKey, Alice___pubKey_aenc, Alice___KeyExchange__comm_chData, Alice___tmp, Alice___loop_index, Alice___aenc_encrypted, Alice___aenc, Alice___privKey_aenc, Alice___comm_chData, Alice___symKey, Alice___symKey_encrypted))).
-
-let Alice___0 (sessionID: bitstring) =
- new strong___Alice___02[]: bitstring;
- out (chControl, strong___Alice___02);
- in (chControl, chControlData: bitstring);
- let (=sessionID, =call___Alice___0, =strong___Alice___02, Alice___key_symKey___1: bitstring, Alice___pubKey_aenc___1: bitstring, Alice___KeyExchange__comm_chData___1: bitstring, Alice___tmp___1: bitstring, Alice___loop_index___1: bitstring, Alice___aenc_encrypted___1: bitstring, Alice___aenc___1: bitstring, Alice___privKey_aenc___1: bitstring, Alice___comm_chData___1: bitstring, Alice___symKey___1: bitstring, Alice___symKey_encrypted___1: bitstring) = chControlDec (chControlData) in
- let Alice___aenc___2: bitstring = adecrypt (Alice___aenc_encrypted___1, Alice___privKey_aenc___1) in
- event authenticity___Alice___comm_chData___signalstate_KeyExchange_comm_KeyExchange_comm (Alice___comm_chData___1);
- out (ch, Alice___aenc_encrypted___1);
- let Alice___symKey___2: bitstring = sdecrypt (Alice___symKey_encrypted___1, Alice___key_symKey___1) in
- event authenticity___Alice___comm_chData___signalstate_KeyExchange_comm_KeyExchange_comm681 (Alice___comm_chData___1);
- out (ch, Alice___symKey_encrypted___1).
-
-let Bob___start (sessionID: bitstring) =
- new Bob___privKey_aenc[]: bitstring;
- let Bob___pubKey_aenc: bitstring = pk(Bob___privKey_aenc) in
- out (ch, Bob___pubKey_aenc);
- new Bob___KeyExchange__comm_chData[]: bitstring;
- new Bob___tmp[]: bitstring;
- new Bob___loop_index[]: bitstring;
- new Bob___aenc_encrypted[]: bitstring;
- new Bob___comm_chData[]: bitstring;
- new Bob___aenc[]: bitstring;
- new Bob___symKey_encrypted[]: bitstring;
- new Bob___symKey[]: bitstring;
- new Bob___key_symKey[]: bitstring;
- in (chControl, strong___Bob___03: bitstring);
- out (chControl, chControlEnc ((sessionID, call___Bob___0, strong___Bob___03, Bob___pubKey_aenc, Bob___privKey_aenc, Bob___KeyExchange__comm_chData, Bob___tmp, Bob___loop_index, Bob___aenc_encrypted, Bob___comm_chData, Bob___aenc, Bob___symKey_encrypted, Bob___symKey, Bob___key_symKey))).
-
-let Bob___0 (sessionID: bitstring) =
- new strong___Bob___04[]: bitstring;
- out (chControl, strong___Bob___04);
- in (chControl, chControlData: bitstring);
- let (=sessionID, =call___Bob___0, =strong___Bob___04, Bob___pubKey_aenc___1: bitstring, Bob___privKey_aenc___1: bitstring, Bob___KeyExchange__comm_chData___1: bitstring, Bob___tmp___1: bitstring, Bob___loop_index___1: bitstring, Bob___aenc_encrypted___1: bitstring, Bob___comm_chData___1: bitstring, Bob___aenc___1: bitstring, Bob___symKey_encrypted___1: bitstring, Bob___symKey___1: bitstring, Bob___key_symKey___1: bitstring) = chControlDec (chControlData) in
- in (ch, Bob___aenc_encrypted___2: bitstring);
- event authenticity___Bob___comm_chData___aftersignalstate_KeyExchange_comm_KeyExchange_comm (Bob___comm_chData___1);
- let Bob___aenc___2: bitstring = adecrypt (Bob___aenc_encrypted___2, Bob___privKey_aenc___1) in
- in (ch, Bob___symKey_encrypted___2: bitstring);
- event authenticity___Bob___comm_chData___aftersignalstate_KeyExchange_comm_KeyExchange_comm727 (Bob___comm_chData___1);
- let Bob___symKey___2: bitstring = sdecrypt (Bob___symKey_encrypted___2, Bob___key_symKey___1) in
- 0.
-
-process
- ! (
- new sessionID[]: bitstring;
- ((
- Alice___0 (sessionID)
- ) | (
- Bob___0 (sessionID)
- ) | (
- (
- ((
- Alice___start (sessionID)
- ) | (
- Bob___start (sessionID)
- )))
- )))
\ No newline at end of file