diff --git a/modeling/SysMLSec/AliceAndBob.xml b/modeling/SysMLSec/AliceAndBob.xml
index c06f7d2abb33ced98e910a1c3bd8ed8a0ae15770..004cc785b24cc0b8653a123b7c25743b62948a09 100644
--- a/modeling/SysMLSec/AliceAndBob.xml
+++ b/modeling/SysMLSec/AliceAndBob.xml
@@ -254,6 +254,8 @@
<Method value="Key getpk(Message cert)" />
<Method value="Key DH(Key pubK, Key privK)" />
<Method value="Message hash(Message msg)" />
+<Method value="Message host(Key k)" />
+<Method value="Key getKey(Message msg)" />
</extraparam>
</SUBCOMPONENT>
<SUBCOMPONENT type="5000" id="123" index="8" uid="32384080-e86a-41de-b441-4f6ae88f1cbe" >
@@ -333,6 +335,8 @@
<Method value="Key getpk(Message cert)" />
<Method value="Key DH(Key pubK, Key privK)" />
<Method value="Message hash(Message msg)" />
+<Method value="Message host(Key k)" />
+<Method value="Key getKey(Message msg)" />
</extraparam>
</SUBCOMPONENT>
@@ -1635,6 +1639,8 @@
<Method value="Key getpk(Message cert)" />
<Method value="Key DH(Key pubK, Key privK)" />
<Method value="Message hash(Message msg)" />
+<Method value="Message host(Key k)" />
+<Method value="Key getKey(Message msg)" />
</extraparam>
</SUBCOMPONENT>
<SUBCOMPONENT type="5000" id="898" index="8" uid="cc150a1e-1348-4fa4-98a9-3a612b6184cc" >
@@ -1717,6 +1723,8 @@
<Method value="Key getpk(Message cert)" />
<Method value="Key DH(Key pubK, Key privK)" />
<Method value="Message hash(Message msg)" />
+<Method value="Message host(Key k)" />
+<Method value="Key getKey(Message msg)" />
</extraparam>
</SUBCOMPONENT>
@@ -3738,6 +3746,8 @@
<Method value="Key getpk(Message cert)" />
<Method value="Key DH(Key pubK, Key privK)" />
<Method value="Message hash(Message msg)" />
+<Method value="Message host(Key k)" />
+<Method value="Key getKey(Message msg)" />
</extraparam>
</SUBCOMPONENT>
<SUBCOMPONENT type="5000" id="2065" index="8" uid="52a07889-a0b4-45e9-a97a-a5a5e144d49b" >
@@ -3825,6 +3835,8 @@
<Method value="Key getpk(Message cert)" />
<Method value="Key DH(Key pubK, Key privK)" />
<Method value="Message hash(Message msg)" />
+<Method value="Message host(Key k)" />
+<Method value="Key getKey(Message msg)" />
</extraparam>
</SUBCOMPONENT>
<SUBCOMPONENT type="5000" id="2106" index="9" uid="7a040a26-feb9-4e9a-a609-908679df2a0b" >
@@ -3910,6 +3922,8 @@
<Method value="get2(Message msg, Message msg1, Message msg2)" />
<Method value="get3(Message msg, Message msg1, Message msg2, Message msg3)" />
<Method value="get4(Message msg, Message msg1, Message msg2, Message msg3, Message msg4)" />
+<Method value="Message host(Key k)" />
+<Method value="Key getKey(Message msg)" />
</extraparam>
</SUBCOMPONENT>
@@ -6797,6 +6811,8 @@
<Method value="Key getpk(Message cert)" />
<Method value="Key DH(Key pubK, Key privK)" />
<Method value="Message hash(Message msg)" />
+<Method value="Message host(Key k)" />
+<Method value="Key getKey(Message msg)" />
</extraparam>
</SUBCOMPONENT>
<SUBCOMPONENT type="5000" id="3683" index="8" uid="58e32c17-1811-4588-ab32-863569a17a48" >
@@ -6874,6 +6890,8 @@
<Method value="Key getpk(Message cert)" />
<Method value="Key DH(Key pubK, Key privK)" />
<Method value="Message hash(Message msg)" />
+<Method value="Message host(Key k)" />
+<Method value="Key getKey(Message msg)" />
</extraparam>
</SUBCOMPONENT>
diff --git a/src/main/java/ui/window/JDialogProverifVerification.java b/src/main/java/ui/window/JDialogProverifVerification.java
index 56a9e77fcfdc70ff9756f95597a3ac6bbf551248..dcf7327ccd7c82c116981092f50d8056b1a784c7 100644
--- a/src/main/java/ui/window/JDialogProverifVerification.java
+++ b/src/main/java/ui/window/JDialogProverifVerification.java
@@ -140,6 +140,8 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
private static boolean DRAW_AVATAR = false;
+ private JLabel labelError;
+
protected MainGUI mgui;
private AvatarDesignPanel adp;
@@ -795,6 +797,7 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
}
CODE_PATH = code1.getText();
EXECUTE_PATH = exe2.getText();
+
if (stateReachabilityAll.isSelected()) {
REACHABILITY_OPTION = REACHABILITY_ALL;
} else if (stateReachabilitySelected.isSelected()) {
@@ -897,6 +900,10 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
mode = NOT_STARTED;
}
else {
+
+
+
+
testGo();
pathCode = code1.getText().trim();
@@ -929,11 +936,37 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
privateChannelDup.isSelected(),
loopLimit.getText())
) {
+ mode = NOT_STARTED; setButtons();
throw new ProVerifVerificationException("Could not generate proverif code");
}
String cmd = exe2.getText().trim();
+ File proverifVerifier= new File(cmd);
+ if (!proverifVerifier.exists()) {
+ mode = NOT_STARTED; setButtons();
+ throw new ProVerifVerificationException(cmd + ": Proverif prover not found");
+ }
+
+ // Must test if this command corresponds to ProVerif
+ this.rshc = new RshClient(hostProVerif);
+ this.rshc.setCmd(cmd + " -help");
+ this.rshc.sendExecuteCommandRequest();
+ RshClientReader readerHelp = this.rshc.getDataReaderFromProcess();
+ BufferedReader bReader = new BufferedReader(readerHelp);
+ String str;
+ boolean foundProverif = false;
+ while ((str = bReader.readLine()) != null) {
+ if (str.contains("Proverif")) {
+ foundProverif = true;
+ }
+ }
+
+ if (!foundProverif) {
+ mode = NOT_STARTED; setButtons();
+ throw new ProVerifVerificationException(cmd + ": invalid Proverif prover");
+ }
+
if (this.typedLanguage.isSelected()) {
cmd += " -in pitype ";
@@ -951,6 +984,7 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
this.rshc.sendExecuteCommandRequest();
RshClientReader reader = this.rshc.getDataReaderFromProcess();
+
if (this.pvoa == null) {
this.pvoa = mgui.gtm.getProVerifOutputAnalyzer();
this.pvoa.addListener(this);
@@ -973,13 +1007,16 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
}
} catch (LauncherException | ProVerifVerificationException le) {
- JLabel label = new JLabel("Error: " + le.getMessage());
- label.setAlignmentX(Component.LEFT_ALIGNMENT);
- this.jta.add(label, this.createGbc(0));
- mode = STOPPED;
+ this.jta.removeAll();
+ labelError = new JLabel("Error: " + le.getMessage());
+ labelError.setAlignmentX(Component.LEFT_ALIGNMENT);
+ this.jta.add(labelError, this.createGbc(0));
+ mode = NOT_STARTED;
} catch (InterruptedException ie) {
+ TraceManager.addDev("Proverif thread interrupted: " + ie.getMessage());
mode = NOT_STARTED;
} catch (FileException e) {
+ TraceManager.addDev("Proverif file couldnot be generated: " + e.getMessage());
System.err.println(e.getMessage() + " : Can't generate proverif file.");
} catch (Exception e) {
mode = STOPPED;
@@ -1109,7 +1146,7 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
this.results = this.pvoa.getResults();
if (this.results.keySet().size() == 0) {
- label = new JLabel("ERROR: no properties to prove");
+ label = new JLabel("ERROR: no properties to be proved");
label.setAlignmentX(Component.LEFT_ALIGNMENT);
this.jta.add(label, this.createGbc(0));
}