Skip to content
Snippets Groups Projects
Commit 42f61be2 authored by Pierre Dontenville's avatar Pierre Dontenville Committed by Guillaume Blanc
Browse files

test build failure fixed

parent d0a0164a
No related branches found
No related tags found
1 merge request!485Avatar security tests
Hide whitespace changes
Inline Side-by-side
ttool/src/test/java/tmltranslator/DiplodocusSecurityTest.java
+ 5
− 5
View file @ 42f61be2
...@@ -31,9 +31,8 @@ import static org.junit.Assert.assertTrue; ...@@ -31,9 +31,8 @@ import static org.junit.Assert.assertTrue;
@RunWith(Parameterized.class) @RunWith(Parameterized.class)
public class DiplodocusSecurityTest extends AbstractTest { 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 DIR_MODELS = "tmltranslator/DiplodocusSecurityTest/Models/";
final static String PVSPEC_FILENAME = "generatedPvspec";
private static String currentModel; private static String currentModel;
private static ArrayList<String> currentTabs; private static ArrayList<String> currentTabs;
private static HashMap<String, String[]> goldenMap; private static HashMap<String, String[]> goldenMap;
...@@ -149,14 +148,15 @@ public class DiplodocusSecurityTest extends AbstractTest { ...@@ -149,14 +148,15 @@ public class DiplodocusSecurityTest extends AbstractTest {
ProVerifSpec proverif = avatar2proverif.generateProVerif(true, true, 0, true, ProVerifSpec proverif = avatar2proverif.generateProVerif(true, true, 0, true,
true); true);
TraceManager.addDev("Saving spec in " + PROVERIF_DIR + PVSPEC_FILENAME); String pvspecFilename = currentModel + "_" + tab;
FileUtils.saveFile(PROVERIF_DIR + PVSPEC_FILENAME, proverif.getStringSpec()); TraceManager.addDev("Saving spec in " + PROVERIF_DIR + pvspecFilename);
FileUtils.saveFile(PROVERIF_DIR + pvspecFilename, proverif.getStringSpec());
TraceManager.addDev("Running Proverif"); TraceManager.addDev("Running Proverif");
Process proc; Process proc;
BufferedReader proc_in; BufferedReader proc_in;
String str; String str;
String cmd = "proverif -in pitype " + PROVERIF_DIR + PVSPEC_FILENAME; String cmd = "proverif -in pitype " + PROVERIF_DIR + pvspecFilename;
boolean summaryFound = false; boolean summaryFound = false;
commMap.clear(); commMap.clear();
......
ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/generatedPvspec deleted 100644 → 0
+ 0
− 153
View file @ d0a0164a
(* 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
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment