diff --git a/.gitignore b/.gitignore
index b5481914bc59ea2336b683b570b8e1162ace40d8..952793a25e4e2c5fc3d7c5d266714414f721ca76 100644
--- a/.gitignore
+++ b/.gitignore
@@ -18,4 +18,3 @@
/bin
/release
/TTool_install
-/ttool/src/test/resources/tmltranslator/DiplodocusSecurityTest/GeneratedPvspec
diff --git a/src/main/java/tmltranslator/TMLTextSpecification.java b/src/main/java/tmltranslator/TMLTextSpecification.java
index 28fe661c691e839e6702f0c94ef003232d714dd8..827bb057ef18130a2055637f94f8c47c529e3cd5 100755
--- a/src/main/java/tmltranslator/TMLTextSpecification.java
+++ b/src/main/java/tmltranslator/TMLTextSpecification.java
@@ -77,6 +77,9 @@ public class TMLTextSpecification<E> {
public final static String EMPTY_KEY_NONCE = "-";
+ public final static int ENCRYPTION_PROCESS = 1;
+ public final static int DECRYPTION_PROCESS = 2;
+
private String spec;
private String title;
@@ -415,37 +418,37 @@ public class TMLTextSpecification<E> {
return code + makeBehavior(task, elt.getNextElement(0));
} else if (elt instanceof TMLExecC) {
- if (elt.securityPattern == null) {
+ if (elt.getSecurityPattern() == null) {
code = "EXECC" + SP + modifyString(((TMLExecC) elt).getAction()) + CR;
} else {
String type = "";
- if (elt.securityPattern.type.equals(SecurityPattern.ASYMMETRIC_ENC_PATTERN)) {
+ if (elt.getSecurityPattern().getType().equals(SecurityPattern.ASYMMETRIC_ENC_PATTERN)) {
type = AENCRYPT;
- } else if (elt.securityPattern.type.equals(SecurityPattern.SYMMETRIC_ENC_PATTERN)) {
+ } else if (elt.getSecurityPattern().getType().equals(SecurityPattern.SYMMETRIC_ENC_PATTERN)) {
type = SENCRYPT;
- } else if (elt.securityPattern.type.equals(SecurityPattern.MAC_PATTERN)) {
+ } else if (elt.getSecurityPattern().getType().equals(SecurityPattern.MAC_PATTERN)) {
type = MAC;
- } else if (elt.securityPattern.type.equals(SecurityPattern.NONCE_PATTERN)) {
+ } else if (elt.getSecurityPattern().getType().equals(SecurityPattern.NONCE_PATTERN)) {
type = NONCE;
- } else if (elt.securityPattern.type.equals(SecurityPattern.HASH_PATTERN)) {
+ } else if (elt.getSecurityPattern().getType().equals(SecurityPattern.HASH_PATTERN)) {
type = HASH;
- } else if (elt.securityPattern.type.equals(SecurityPattern.ADVANCED_PATTERN)) {
+ } else if (elt.getSecurityPattern().getType().equals(SecurityPattern.ADVANCED_PATTERN)) {
type = ADV;
}
- String nonce = elt.securityPattern.nonce;
+ String nonce = elt.getSecurityPattern().getNonce();
if (nonce.length() == 0) {
nonce = EMPTY_KEY_NONCE;
}
- String key = elt.securityPattern.nonce;
+ String key = elt.getSecurityPattern().getKey();
if (key.length() == 0) {
key = EMPTY_KEY_NONCE;
}
-
- code = "EXECC" + SP + modifyString(((TMLExecC) elt).getAction()) + SP + elt.securityPattern.name + SP + type + SP +
- elt.securityPattern.encTime + SP + elt.securityPattern.decTime + SP + elt.securityPattern.overhead + SP +
- elt.securityPattern.size + SP + nonce + SP + key + SP + elt.securityPattern.process + CR;
+ int process = (((TMLExecC) elt).isDecryptionProcess()) ? DECRYPTION_PROCESS : ENCRYPTION_PROCESS;
+ code = "EXECC" + SP + modifyString(((TMLExecC) elt).getAction()) + SP + elt.getSecurityPattern().getName() + SP + type + SP +
+ elt.getSecurityPattern().getEncTime() + SP + elt.getSecurityPattern().getDecTime() + SP + elt.getSecurityPattern().getOverhead() + SP +
+ elt.getSecurityPattern().getSize() + SP + nonce + SP + key + SP + process + CR;
}
return code + makeBehavior(task, elt.getNextElement(0));
@@ -496,8 +499,8 @@ public class TMLTextSpecification<E> {
}
//TraceManager.addDev("Nb of samples in task " + task.getName() + " = " + tmlch.getNbOfSamples());
code = code + modifyString(tmlch.getNbOfSamples());
- if (elt.securityPattern != null) {
- code = code + SP + elt.securityPattern.name + CR;
+ if (elt.getSecurityPattern() != null) {
+ code = code + SP + elt.getSecurityPattern().getName() + CR;
} else {
code = code + CR;
}
@@ -505,10 +508,10 @@ public class TMLTextSpecification<E> {
} else if (elt instanceof TMLReadChannel) {
tmlch = (TMLActivityElementChannel) elt;
- if (elt.securityPattern == null) {
+ if (elt.getSecurityPattern() == null) {
code = "READ " + tmlch.getChannel(0).getName() + SP + modifyString(tmlch.getNbOfSamples()) + CR;
} else {
- code = "READ " + tmlch.getChannel(0).getName() + SP + modifyString(tmlch.getNbOfSamples()) + SP + elt.securityPattern.name + CR;
+ code = "READ " + tmlch.getChannel(0).getName() + SP + modifyString(tmlch.getNbOfSamples()) + SP + elt.getSecurityPattern().getName() + CR;
}
return code + makeBehavior(task, elt.getNextElement(0));
@@ -729,7 +732,11 @@ public class TMLTextSpecification<E> {
if (s1 != null) {
split = s1.split("\\s");
if (split.length > 0) {
- findSec(split);
+ if (isInstruction(split[0], "EXECC")) {
+ if (!findAndCheckSec(split)) {
+ addError(0, lineNb, 0, "The Security Pattern " + split[2] + " already exists");
+ }
+ }
}
}
@@ -771,55 +778,50 @@ public class TMLTextSpecification<E> {
}
}
- public void findSec(String[] _split) {
- if (isInstruction(_split[0], "EXECC")) {
-
- if (_split.length > 10) {
- TraceManager.addDev("Found EXECC in: " + _split.length + " name=" + _split[2] + " type=" + _split[3]);
+ public boolean findAndCheckSec(String[] _split) {
+ boolean isNewSec = true;
+ if (_split.length > 10) {
+ TraceManager.addDev("Found EXECC in: " + _split.length + " name=" + _split[2] + " type=" + _split[3]);
+ if (_split[10].compareTo("" + ENCRYPTION_PROCESS) == 0) {
String ccName = _split[2];
- String type = _split[3];
- String stringType = "";
- int process;
-
- if (type.equals(AENCRYPT)) {
- stringType = SecurityPattern.ASYMMETRIC_ENC_PATTERN;
- } else if (type.equals(SENCRYPT)) {
- stringType = SecurityPattern.SYMMETRIC_ENC_PATTERN;
- } else if (type.equals(HASH)) {
- stringType = SecurityPattern.HASH_PATTERN;
- } else if (type.equals(MAC)) {
- stringType = SecurityPattern.MAC_PATTERN;
- } else if (type.equals(NONCE)) {
- stringType = SecurityPattern.NONCE_PATTERN;
- } else if (type.equals(ADV)) {
- stringType = SecurityPattern.ADVANCED_PATTERN;
- }
-
- if (stringType.length() > 0) {
- TraceManager.addDev("Found security pattern: " + ccName + " with type: " + stringType);
- String nonce = _split[8];
- if (_split[8].compareTo(EMPTY_KEY_NONCE) == 0) {
- nonce = "";
- }
- String key = _split[9];
- if (_split[9].compareTo(EMPTY_KEY_NONCE) == 0) {
- key = "";
- }
- process = SecurityPattern.DECRYPTION_PROCESS;
- if (_split[10].compareTo("" + SecurityPattern.ENCRYPTION_PROCESS) == 0) {
- process = SecurityPattern.ENCRYPTION_PROCESS;
+ if (securityPatternMap.containsKey(ccName)) {
+ isNewSec = false;
+ } else {
+ String type = _split[3];
+ String stringType = "";
+ if (type.equals(AENCRYPT)) {
+ stringType = SecurityPattern.ASYMMETRIC_ENC_PATTERN;
+ } else if (type.equals(SENCRYPT)) {
+ stringType = SecurityPattern.SYMMETRIC_ENC_PATTERN;
+ } else if (type.equals(HASH)) {
+ stringType = SecurityPattern.HASH_PATTERN;
+ } else if (type.equals(MAC)) {
+ stringType = SecurityPattern.MAC_PATTERN;
+ } else if (type.equals(NONCE)) {
+ stringType = SecurityPattern.NONCE_PATTERN;
+ } else if (type.equals(ADV)) {
+ stringType = SecurityPattern.ADVANCED_PATTERN;
}
- SecurityPattern sp = new SecurityPattern(ccName, stringType, _split[6], _split[7], _split[4], _split[5], nonce, "",
- key);
- sp.process = process;
- if (securityPatternMap.get(ccName) == null) {
+ if (!stringType.isEmpty()) {
+ TraceManager.addDev("Found security pattern: " + ccName + " with type: " + stringType);
+ String nonce = _split[8];
+ if (_split[8].compareTo(EMPTY_KEY_NONCE) == 0) {
+ nonce = "";
+ }
+ String key = _split[9];
+ if (_split[9].compareTo(EMPTY_KEY_NONCE) == 0) {
+ key = "";
+ }
+ SecurityPattern sp = new SecurityPattern(ccName, stringType, _split[6], _split[7], _split[4], _split[5], nonce, "",
+ key);
tmlm.addSecurityPattern(sp);
+ securityPatternMap.put(ccName, sp);
+ TraceManager.addDev("Security pattern " + ccName + " added");
}
- securityPatternMap.put(ccName, sp);
- TraceManager.addDev("Security pattern " + ccName + " added");
}
}
}
+ return isNewSec;
}
public void addError(int _type, int _lineNb, int _charNb, String _msg) {
@@ -830,7 +832,7 @@ public class TMLTextSpecification<E> {
errors.add(error);
}
- public int analyseInstruction(String _line, int _lineNb, String[] _split) {
+ public int analyseInstruction(String _line, int _lineNb, String[] _split) throws TMLCheckingError {
String error;
String params;
String id;
@@ -1690,7 +1692,7 @@ public class TMLTextSpecification<E> {
if (_split.length == 4) {
if (securityPatternMap.containsKey(_split[3])) {
- tmlrch.securityPattern = securityPatternMap.get(_split[3]);
+ tmlrch.setSecurityPattern(securityPatternMap.get(_split[3]));
}
}
@@ -1727,10 +1729,10 @@ public class TMLTextSpecification<E> {
TMLWriteChannel tmlwch = new TMLWriteChannel(_split[1], null);
if (_split.length > 3) {
if (securityPatternMap.containsKey(_split[_split.length - 1])) {
- tmlwch.securityPattern = securityPatternMap.get(_split[_split.length - 1]);
+ tmlwch.setSecurityPattern(securityPatternMap.get(_split[_split.length - 1]));
TraceManager.addDev("Nb of samples in task " + task.getName() +
- " security pattern: " + tmlwch.securityPattern.name);
- tmlwch.securityPattern.originTask = task.getTaskName();
+ " security pattern: " + tmlwch.getSecurityPattern().getName());
+ //tmlwch.getSecurityPattern().setOriginTask(task.getTaskName());
}
for (int k = 0; k < _split.length - 3; k++) {
//TraceManager.addDev("Handling write channel 1.1");
@@ -2785,20 +2787,24 @@ public class TMLTextSpecification<E> {
if (_split.length == 11) {
if (securityPatternMap.containsKey(_split[2])) {
- //Security operation
- TraceManager.addDev("Found security pattern: " + _split[2]);
- TMLExecC execc = new TMLExecC("execc", null);
- execc.setAction(_split[1]);
-// execc.securityPattern = securityPatternMap.get(_split[2]);
- SecurityPattern sp = new SecurityPattern(securityPatternMap.get(_split[2]));
- sp.process = SecurityPattern.DECRYPTION_PROCESS;
- if (_split[10].compareTo("" + SecurityPattern.ENCRYPTION_PROCESS)==0){
- sp.process = SecurityPattern.ENCRYPTION_PROCESS;
+ if ((_split[10].compareTo("" + DECRYPTION_PROCESS) == 0) || (_split[10].compareTo("" + ENCRYPTION_PROCESS) == 0)) {
+ //Security operation
+ TraceManager.addDev("Found security pattern: " + _split[2]);
+ TMLExecC execc = new TMLExecC("encrypt_" + _split[2], null);
+ execc.setAction(_split[1]);
+ execc.setSecurityPattern(securityPatternMap.get(_split[2]));
+ if (_split[10].compareTo("" + DECRYPTION_PROCESS) == 0) {
+ execc.setDecryptionProcess(true);
+ execc.setName("decrypt_" + _split[2]);
+ }
+ tmlae.addNext(execc);
+ task.getActivityDiagram().addElement(execc);
+ tmlae = execc;
+ } else {
+ error = "EXECC " + _split[2] + " has an unknown security process";
+ addError(0, _lineNb, 0, error);
+ return -1;
}
- execc.securityPattern = sp;
- tmlae.addNext(execc);
- task.getActivityDiagram().addElement(execc);
- tmlae = execc;
} else {
error = "An EXECC with a security configuration must contain a valid security configuration name " + (_split[2]);
addError(0, _lineNb, 0, error);
diff --git a/src/main/java/tmltranslator/toavatarsec/TML2Avatar.java b/src/main/java/tmltranslator/toavatarsec/TML2Avatar.java
index 1e1cdb967defe359ef4b6dacc8afc172807cbcd1..cbe62a043bfb61cc798a15b48d4cdacb7d289846 100644
--- a/src/main/java/tmltranslator/toavatarsec/TML2Avatar.java
+++ b/src/main/java/tmltranslator/toavatarsec/TML2Avatar.java
@@ -1706,9 +1706,7 @@ public class TML2Avatar {
//TODO: Make state names readable
//TODO: Put back numeric guards
//TODO: Calculate for temp variable
- if(tmlmap.getTMLModeling() != null) {
- TraceManager.addDev(tmlmap.getTMLModeling().toString());
- TraceManager.addDev(tmlmap.getTMLModeling().getTasks().size() +"");
+ if (tmlmap.getTMLModeling() != null) {
if (tmlmap.getTMLModeling().getReference() != null) {
this.avspec = new AvatarSpecification("spec", referenceObject);
} else {
diff --git a/src/main/java/ui/MainGUI.java b/src/main/java/ui/MainGUI.java
index b2116464f411aec0e05db53e420438cb751e2751..e90a2af40af322c0eaffe3a8c4069f2f69828d75 100644
--- a/src/main/java/ui/MainGUI.java
+++ b/src/main/java/ui/MainGUI.java
@@ -331,9 +331,6 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener, Per
// Thread for autosave
private PeriodicBehaviorThread pbt;
- private JDialogLoadingNetworkModel jdlnm;
-
-
private boolean hidden = false;
public MainGUI(boolean _openLast, boolean _turtleOn, boolean _systemcOn, boolean _lotosOn, boolean _proactiveOn, boolean _tpnOn, boolean _osOn,
@@ -2871,7 +2868,7 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener, Per
*/
}
- jdlnm = new JDialogLoadingNetworkModel(frame, this,
+ JDialogLoadingNetworkModel jdlnm = new JDialogLoadingNetworkModel(frame, this,
"Opening a model from TTool's repository", ConfigurationTTool.URL_MODEL);
GraphicLib.centerOnParent(jdlnm, 700, 800);
jdlnm.setVisible(true); // blocked until dialog has been closed
@@ -4503,8 +4500,9 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener, Per
}
}
// dtree.toBeUpdated();
- if (forceTreeUpdate)
+ if (forceTreeUpdate) {
dtree.forceUpdate();
+ }
return ret;
}
@@ -10480,8 +10478,4 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener, Per
return tmlcpsList;
}
- public JDialogLoadingNetworkModel getJdlnm(){
- return jdlnm;
- }
-
} // Class MainGUI
diff --git a/src/main/java/ui/networkmodelloader/JDialogLoadingNetworkModel.java b/src/main/java/ui/networkmodelloader/JDialogLoadingNetworkModel.java
index 9b81d26bbd59a7642c877383c263b4625ee12824..62c5687cbf1ce1a953c1b8315970f6b3ec248490 100644
--- a/src/main/java/ui/networkmodelloader/JDialogLoadingNetworkModel.java
+++ b/src/main/java/ui/networkmodelloader/JDialogLoadingNetworkModel.java
@@ -443,7 +443,4 @@ public class JDialogLoadingNetworkModel extends javax.swing.JFrame implements Ac
jta.append(s);
}
- public ArrayList<NetworkModel> getListOfModels() {
- return listOfModels;
- }
}
diff --git a/src/main/java/ui/networkmodelloader/NetworkModel.java b/src/main/java/ui/networkmodelloader/NetworkModel.java
index 647ecec380b39b4ddc91ab3a679af6b8020089ea..c7e71cc88048b7f98555d8b89d8659a90e9bc09c 100644
--- a/src/main/java/ui/networkmodelloader/NetworkModel.java
+++ b/src/main/java/ui/networkmodelloader/NetworkModel.java
@@ -79,10 +79,6 @@ public class NetworkModel {
}
- public String getFileName(){
- return fileName;
- }
-
/*public static NetworkModelType stringToNetworkModelType(String type) {
type = type.toLowerCase();
if (type.compareTo("software design") == 0) {
diff --git a/src/main/java/ui/window/JDialogProverifVerification.java b/src/main/java/ui/window/JDialogProverifVerification.java
index 3c506740a95abd594be88f72b81fbda7edc1b7c7..af4f9a1ced8b3f45622f61a96ad17a0261da263f 100644
--- a/src/main/java/ui/window/JDialogProverifVerification.java
+++ b/src/main/java/ui/window/JDialogProverifVerification.java
@@ -126,7 +126,6 @@ import ui.util.IconManager;
public class JDialogProverifVerification extends JDialog implements ActionListener, ListSelectionListener, MouseListener, Runnable,
MasterProcessInterface, ProVerifOutputListener {
-
private static final Insets insets = new Insets(0, 0, 0, 0);
private static final Insets WEST_INSETS = new Insets(0, 0, 0, 0);
@@ -140,6 +139,7 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
private static boolean MSG_DUPLICATION = true;
private static boolean PI_CALCULUS = true;
public static int LOOP_ITERATION = 1;
+
public static String ADD_CONFIDENTIALITY = "Conf";
public static String ADD_WEAK_AUTHENTICITY = "Integrity";
public static String ADD_STRONG_AUTHENTICITY = "Strong Authenticity";
@@ -1768,10 +1768,10 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
this.rshc.sendExecuteCommandRequest();
RshClientReader reader = this.rshc.getDataReaderFromProcess();
- if (this.pvoa == null) {
+ //if (this.pvoa == null) {
this.pvoa = mgui.gtm.getProVerifOutputAnalyzer();
this.pvoa.addListener(this);
- }
+ //}
//try {
this.pvoa.analyzeOutput(reader, typedLanguage.isSelected());
/*} catch (Exception e) {