diff --git a/ttool/src/test/java/ui/AvatarSecurityTests.java b/ttool/src/test/java/ui/AvatarSecurityTests.java index b65315aa8e0fca8f286e911373ecd53b2097d3dd..0c3ab47ef0b19f6c76f98f12bbb6ce28475e4b55 100644 --- a/ttool/src/test/java/ui/AvatarSecurityTests.java +++ b/ttool/src/test/java/ui/AvatarSecurityTests.java @@ -1,14 +1,21 @@ package ui; +import avatartranslator.AvatarSpecification; +import avatartranslator.toproverif.AVATAR2ProVerif; import common.ConfigurationTTool; import common.SpecConfigTTool; +import myutil.FileException; +import myutil.FileUtils; +import myutil.TraceManager; import org.junit.BeforeClass; import org.junit.Test; +import proverifspec.ProVerifSpec; import java.io.*; +import java.util.ArrayList; +import java.util.List; -import static org.junit.Assert.assertNull; -import static org.junit.Assert.assertTrue; +import static org.junit.Assert.*; public class AvatarSecurityTests extends AbstractUITest { @@ -16,7 +23,11 @@ public class AvatarSecurityTests extends AbstractUITest { final static String INPUT_FOLDER = "input/"; final static String GOLDEN_SUFFIX = "_golden"; final static String OUTPUT_FOLDER = "output/"; + final static String PVSPEC_SUFFIX = "_pvspec"; static String OUTPUT_DIR; + static final String PROVERIF_SUMMARY = "Verification summary:"; + static final String PROVERIF_QUERY_PREFIX = "Query"; + final static String[] MODELS = { "AliceAndBob", @@ -51,45 +62,74 @@ public class AvatarSecurityTests extends AbstractUITest { } } - private void runTest(String model){ + private void runTest(String model) { + TraceManager.addDev("Start testing " + model); + openModel(model); + AvatarSpecification avatarSpecification = mainGUI.gtm.getAvatarSpecification(); mainGUI.checkModelingSyntax(true); - mainGUI.avatarProVerifVerification(); - // TODO click on start button + String pvspecPath = OUTPUT_DIR + model + PVSPEC_SUFFIX; + boolean pvspecGenerated = mainGUI.gtm.generateProVerifFromAVATAR(pvspecPath, 0, true, true); + assertTrue(pvspecGenerated); - String cmd = "proverif -in pitype " + OUTPUT_DIR + "pvspec"; + + String cmd = "proverif -in pitype " + pvspecPath; String goldenPath = INPUT_DIR + model + GOLDEN_SUFFIX; Process process; BufferedReader cmdOutput; - try { process = Runtime.getRuntime().exec(cmd); cmdOutput = new BufferedReader(new InputStreamReader(process.getInputStream())); - BufferedReader goldenFile = new BufferedReader(new FileReader(goldenPath)); + List<String> golden = generateGoldenList(goldenPath); String outputLine; - String goldenLine = null; - boolean result = true; + int checked = 0; + boolean summaryFound = false; while ((outputLine = cmdOutput.readLine()) != null){ - if(outputLine.contains("RESULT")){ - goldenLine = goldenFile.readLine(); - if (!outputLine.equals(goldenLine)) { - result = false; - break; + if (summaryFound){ + if(outputLine.startsWith(PROVERIF_QUERY_PREFIX)){ + if (golden.contains(outputLine)) { + checked += 1; + } else { + checked = -1; + break; + } + } + + } else { + if (outputLine.contains(PROVERIF_SUMMARY)){ + summaryFound = true; } } } - goldenLine = goldenFile.readLine(); - assertTrue(result); - assertNull(goldenLine); // check if golden was entirely read + assertEquals(golden.size(), checked); + + } catch (Exception e) { + throw new RuntimeException(e); + } + } - } catch (IOException e) { + private List<String> generateGoldenList(String goldenPath) throws IOException { + BufferedReader goldenFile = null; + try { + goldenFile = new BufferedReader(new FileReader(goldenPath)); + } catch (FileNotFoundException e) { + TraceManager.addDev("File " + goldenPath + " not found"); throw new RuntimeException(e); } + List<String> goldenList = new ArrayList<>(); + String line; + while ((line = goldenFile.readLine()) != null){ + if (line.startsWith(PROVERIF_QUERY_PREFIX)) + goldenList.add(line); + } + return goldenList; } + } + diff --git a/ttool/src/test/resources/ui/avatarsecuritytests/input/AliceAndBob_golden b/ttool/src/test/resources/ui/avatarsecuritytests/input/AliceAndBob_golden index 36d148912c30a4e36234621ff71aa732f0fad2a3..de8e58560fe23d9606bdf19302a53057524e6cc6 100644 --- a/ttool/src/test/resources/ui/avatarsecuritytests/input/AliceAndBob_golden +++ b/ttool/src/test/resources/ui/avatarsecuritytests/input/AliceAndBob_golden @@ -1,10 +1,22 @@ -RESULT not attacker(Alice___secretData[!1 = v]) is true. -RESULT not event(enteringState___Alice___makingMessage) is false. -RESULT not event(enteringState___Alice___sendingMessage) is false. -RESULT not event(enteringState___Alice___beforeFinish) is false. -RESULT not event(enteringState___Bob___waitingForMessage) is false. -RESULT not event(enteringState___Bob___messageDecrypt) is false. -RESULT not event(enteringState___Bob___messageDecrypted) is false. -RESULT not event(enteringState___Bob___SecretDataReceived) is false. -RESULT inj-event(authenticity___Bob___m__data___messageDecrypted(dummyM)) ==> inj-event(authenticity___Alice___m__data___sendingMessage(dummyM)) is false. -RESULT (but event(authenticity___Bob___m__data___messageDecrypted(dummyM)) ==> event(authenticity___Alice___m__data___sendingMessage(dummyM)) is true.) +-------------------------------------------------------------- +Verification summary: + +Query not attacker(Alice___secretData[!1 = v]) is true. + +Query not event(enteringState___Alice___makingMessage) is true. + +Query not event(enteringState___Alice___sendingMessage) is true. + +Query not event(enteringState___Alice___beforeFinish) is true. + +Query not event(enteringState___Bob___waitingForMessage) is true. + +Query not event(enteringState___Bob___messageDecrypt) is true. + +Query not event(enteringState___Bob___messageDecrypted) is true. + +Query not event(enteringState___Bob___SecretDataReceived) is true. + +Query inj-event(authenticity___Bob___m__data___messageDecrypted(dummyM)) ==> inj-event(authenticity___Alice___m__data___sendingMessage(dummyM)) is false. + +--------------------------------------------------------------