From 04f87d4a27f4b8950dfb72da6184f0351cd5c5c6 Mon Sep 17 00:00:00 2001
From: jerray <jawher.jerray@eurecom.fr>
Date: Fri, 28 Apr 2023 18:43:31 +0200
Subject: [PATCH] Delete TMLEncryption and TMLDecryption classes + add new
attribut in SecurityPattern class
---
.../java/tmltranslator/SecurityPattern.java | 20 +++++++
.../java/tmltranslator/TMLDecryption.java | 56 -------------------
.../java/tmltranslator/TMLEncryption.java | 56 -------------------
.../toavatar/FullTML2Avatar.java | 4 +-
.../tmltranslator/toavatarsec/TML2Avatar.java | 4 +-
.../ui/ActivityDiagram2TMLTranslator.java | 24 ++++----
src/main/java/ui/SecurityGeneration.java | 20 -------
7 files changed, 36 insertions(+), 148 deletions(-)
delete mode 100644 src/main/java/tmltranslator/TMLDecryption.java
delete mode 100644 src/main/java/tmltranslator/TMLEncryption.java
diff --git a/src/main/java/tmltranslator/SecurityPattern.java b/src/main/java/tmltranslator/SecurityPattern.java
index 09d9fdb83c..5c4e4718a8 100644
--- a/src/main/java/tmltranslator/SecurityPattern.java
+++ b/src/main/java/tmltranslator/SecurityPattern.java
@@ -48,6 +48,8 @@ import java.util.Objects;
public class SecurityPattern {
+ public final static int ENCRYPTION_PROCESS = 1;
+ public final static int DECRYPTION_PROCESS = 2;
public String name = "";
public String type = "";
@@ -62,6 +64,7 @@ public class SecurityPattern {
public String formula;
public String key;
public String algorithm = "";
+ public int process = 0;
public SecurityPattern(String _name, String _type, String _overhead, String _size, String _enctime, String _dectime, String _nonce,
String _formula, String _key) {
@@ -88,6 +91,19 @@ public class SecurityPattern {
} catch (NumberFormatException e) {}
}
+
+ public SecurityPattern(SecurityPattern secPattern) {
+ this.name = secPattern.name;
+ this.type = secPattern.type;
+ this.nonce = secPattern.nonce;
+ this.formula = secPattern.formula;
+ this.key = secPattern.key;
+ this.overhead = secPattern.overhead;
+ this.size = secPattern.size;
+ this.decTime = secPattern.decTime;
+ this.encTime = secPattern.encTime;
+ }
+
public String toXML() {
String s = "<SECURITYPATTERN ";
@@ -141,4 +157,8 @@ public class SecurityPattern {
return type.toLowerCase(Locale.ROOT).equals("nonce");
}
+ public void setProcess(int _process){
+ this.process = _process;
+ }
+
}
diff --git a/src/main/java/tmltranslator/TMLDecryption.java b/src/main/java/tmltranslator/TMLDecryption.java
deleted file mode 100644
index a879a8ff4c..0000000000
--- a/src/main/java/tmltranslator/TMLDecryption.java
+++ /dev/null
@@ -1,56 +0,0 @@
-/* Copyright or (C) or Copr. GET / ENST, Telecom-Paris, Ludovic Apvrille
- *
- * ludovic.apvrille AT enst.fr
- *
- * This software is a computer program whose purpose is to allow the
- * edition of TURTLE analysis, design and deployment diagrams, to
- * allow the generation of RT-LOTOS or Java code from this diagram,
- * and at last to allow the analysis of formal validation traces
- * obtained from external tools, e.g. RTL from LAAS-CNRS and CADP
- * from INRIA Rhone-Alpes.
- *
- * This software is governed by the CeCILL license under French law and
- * abiding by the rules of distribution of free software. You can use,
- * modify and/ or redistribute the software under the terms of the CeCILL
- * license as circulated by CEA, CNRS and INRIA at the following URL
- * "http://www.cecill.info".
- *
- * As a counterpart to the access to the source code and rights to copy,
- * modify and redistribute granted by the license, users are provided only
- * with a limited warranty and the software's author, the holder of the
- * economic rights, and the successive licensors have only limited
- * liability.
- *
- * In this respect, the user's attention is drawn to the risks associated
- * with loading, using, modifying and/or developing or reproducing the
- * software by the user in light of its specific status of free software,
- * that may mean that it is complicated to manipulate, and that also
- * therefore means that it is reserved for developers and experienced
- * professionals having in-depth computer knowledge. Users are therefore
- * encouraged to load and test the software's suitability as regards their
- * requirements in conditions enabling the security of their systems and/or
- * data to be ensured and, more generally, to use and operate it in the
- * same conditions as regards security.
- *
- * The fact that you are presently reading this means that you have had
- * knowledge of the CeCILL license and that you accept its terms.
- */
-
-
-
-
-package tmltranslator;
-
-
-/**
- * Class TMLDecryption
- * Creation: 18/04/2023
- * @version 1.0 18/04/2023
- */
-public class TMLDecryption extends TMLActivityElementWithAction {
-
- public TMLDecryption(String _name, Object _referenceObject) {
- super(_name, _referenceObject);
- }
-
-}
\ No newline at end of file
diff --git a/src/main/java/tmltranslator/TMLEncryption.java b/src/main/java/tmltranslator/TMLEncryption.java
deleted file mode 100644
index 7734869798..0000000000
--- a/src/main/java/tmltranslator/TMLEncryption.java
+++ /dev/null
@@ -1,56 +0,0 @@
-/* Copyright or (C) or Copr. GET / ENST, Telecom-Paris, Ludovic Apvrille
- *
- * ludovic.apvrille AT enst.fr
- *
- * This software is a computer program whose purpose is to allow the
- * edition of TURTLE analysis, design and deployment diagrams, to
- * allow the generation of RT-LOTOS or Java code from this diagram,
- * and at last to allow the analysis of formal validation traces
- * obtained from external tools, e.g. RTL from LAAS-CNRS and CADP
- * from INRIA Rhone-Alpes.
- *
- * This software is governed by the CeCILL license under French law and
- * abiding by the rules of distribution of free software. You can use,
- * modify and/ or redistribute the software under the terms of the CeCILL
- * license as circulated by CEA, CNRS and INRIA at the following URL
- * "http://www.cecill.info".
- *
- * As a counterpart to the access to the source code and rights to copy,
- * modify and redistribute granted by the license, users are provided only
- * with a limited warranty and the software's author, the holder of the
- * economic rights, and the successive licensors have only limited
- * liability.
- *
- * In this respect, the user's attention is drawn to the risks associated
- * with loading, using, modifying and/or developing or reproducing the
- * software by the user in light of its specific status of free software,
- * that may mean that it is complicated to manipulate, and that also
- * therefore means that it is reserved for developers and experienced
- * professionals having in-depth computer knowledge. Users are therefore
- * encouraged to load and test the software's suitability as regards their
- * requirements in conditions enabling the security of their systems and/or
- * data to be ensured and, more generally, to use and operate it in the
- * same conditions as regards security.
- *
- * The fact that you are presently reading this means that you have had
- * knowledge of the CeCILL license and that you accept its terms.
- */
-
-
-
-
-package tmltranslator;
-
-
-/**
- * Class TMLEncryption
- * Creation: 21/05/2008
- * @version 1.0 21/05/2008
- */
-public class TMLEncryption extends TMLActivityElementWithAction {
-
- public TMLEncryption(String _name, Object _referenceObject) {
- super(_name, _referenceObject);
- }
-
-}
\ No newline at end of file
diff --git a/src/main/java/tmltranslator/toavatar/FullTML2Avatar.java b/src/main/java/tmltranslator/toavatar/FullTML2Avatar.java
index 63a257bb1d..1093b1af13 100644
--- a/src/main/java/tmltranslator/toavatar/FullTML2Avatar.java
+++ b/src/main/java/tmltranslator/toavatar/FullTML2Avatar.java
@@ -1168,7 +1168,7 @@ public class FullTML2Avatar {
if (security && ae.securityPattern != null) {
//If encryption
- if (ae.securityPattern != null && ae instanceof TMLEncryption) {
+ if (ae.securityPattern != null && ae.securityPattern.process == SecurityPattern.ENCRYPTION_PROCESS) {
secPatterns.add(ae.securityPattern);
if (ae.securityPattern.type.equals("Advanced")) {
//Type Advanced
@@ -1352,7 +1352,7 @@ public class FullTML2Avatar {
signalAuthOriginMap.put(ae.securityPattern.name, authOrigin);
}
- } else if (ae.securityPattern != null && ae instanceof TMLDecryption) {
+ } else if (ae.securityPattern != null && ae.securityPattern.process == SecurityPattern.DECRYPTION_PROCESS) {
//Decryption action
//block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null));
//block.addAttribute(new AvatarAttribute(ae.securityPattern.name+"_encrypted", AvatarType.INTEGER, block, null));
diff --git a/src/main/java/tmltranslator/toavatarsec/TML2Avatar.java b/src/main/java/tmltranslator/toavatarsec/TML2Avatar.java
index 59739a70b7..5b24369897 100644
--- a/src/main/java/tmltranslator/toavatarsec/TML2Avatar.java
+++ b/src/main/java/tmltranslator/toavatarsec/TML2Avatar.java
@@ -677,7 +677,7 @@ public class TML2Avatar {
elementList.add(tran);
if (security && ae.securityPattern != null) {
//If encryption
- if (ae.securityPattern != null && ae instanceof TMLEncryption) {
+ if (ae.securityPattern != null && ae.securityPattern.process == SecurityPattern.ENCRYPTION_PROCESS) {
secPatterns.add(ae.securityPattern);
if (ae.securityPattern.type.equals("Advanced")) {
//Type Advanced
@@ -863,7 +863,7 @@ public class TML2Avatar {
signalAuthOriginMap.put(ae.securityPattern.name, authOrigin);
}
- } else if (ae.securityPattern != null && ae instanceof TMLDecryption) {
+ } else if (ae.securityPattern != null && ae.securityPattern.process == SecurityPattern.DECRYPTION_PROCESS) {
//Decryption action
//block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null));
//block.addAttribute(new AvatarAttribute(ae.securityPattern.name+"_encrypted", AvatarType.INTEGER, block, null));
diff --git a/src/main/java/ui/ActivityDiagram2TMLTranslator.java b/src/main/java/ui/ActivityDiagram2TMLTranslator.java
index 39567c7319..4117efae56 100644
--- a/src/main/java/ui/ActivityDiagram2TMLTranslator.java
+++ b/src/main/java/ui/ActivityDiagram2TMLTranslator.java
@@ -99,8 +99,6 @@ public class ActivityDiagram2TMLTranslator {
TMLRandomSequence tmlrsequence;
TMLSelectEvt tmlselectevt;
TMLDelay tmldelay;
- TMLEncryption tmlencryption;
- TMLDecryption tmldecryption;
int staticLoopIndex = 0;
String sl = "", tmp;
TMLType tt;
@@ -190,8 +188,8 @@ public class ActivityDiagram2TMLTranslator {
corrTgElement.addCor(tmlexecii, tgc);
} else if (tgc instanceof TMLADEncrypt) {
- tmlencryption = new TMLEncryption("encrypt_" + ((TMLADEncrypt) tgc).securityContext, tgc);
- activity.addElement(tmlencryption);
+ tmlexecc = new TMLExecC("encrypt_" + ((TMLADEncrypt) tgc).securityContext, tgc);
+ activity.addElement(tmlexecc);
SecurityPattern sp = securityPatterns.get(((TMLADEncrypt) tgc).securityContext);
if (sp == null) {
//Throw error for missing security pattern
@@ -200,15 +198,16 @@ public class ActivityDiagram2TMLTranslator {
ce.setTGComponent(tgc);
checkingErrors.add(ce);
} else {
- tmlencryption.securityPattern = sp;
- tmlencryption.setAction(Integer.toString(sp.encTime));
+ tmlexecc.securityPattern = new SecurityPattern(sp);
+ tmlexecc.securityPattern.setProcess(SecurityPattern.ENCRYPTION_PROCESS);
+ tmlexecc.setAction(Integer.toString(sp.encTime));;
((BasicErrorHighlight) tgc).setStateAction(ErrorHighlight.OK);
tmlm.securityTaskMap.get(sp).add(tmltask);
- corrTgElement.addCor(tmlencryption, tgc);
+ corrTgElement.addCor(tmlexecc, tgc);
}
} else if (tgc instanceof TMLADDecrypt) {
- tmldecryption = new TMLDecryption("decrypt_" + ((TMLADDecrypt) tgc).securityContext, tgc);
- activity.addElement(tmldecryption);
+ tmlexecc = new TMLExecC("decrypt_" + ((TMLADDecrypt) tgc).securityContext, tgc);
+ activity.addElement(tmlexecc);
SecurityPattern sp = securityPatterns.get(((TMLADDecrypt) tgc).securityContext);
if (sp == null) {
//Throw error for missing security pattern
@@ -217,10 +216,11 @@ public class ActivityDiagram2TMLTranslator {
ce.setTGComponent(tgc);
checkingErrors.add(ce);
} else {
- tmldecryption.securityPattern = sp;
- tmldecryption.setAction(Integer.toString(sp.decTime));
+ tmlexecc.securityPattern = new SecurityPattern(sp);
+ tmlexecc.setAction(Integer.toString(sp.decTime));
+ tmlexecc.securityPattern.setProcess(SecurityPattern.DECRYPTION_PROCESS);
((BasicErrorHighlight) tgc).setStateAction(ErrorHighlight.OK);
- corrTgElement.addCor(tmldecryption, tgc);
+ corrTgElement.addCor(tmlexecc, tgc);
tmlm.securityTaskMap.get(sp).add(tmltask);
}
diff --git a/src/main/java/ui/SecurityGeneration.java b/src/main/java/ui/SecurityGeneration.java
index 4c54b9f531..377dfbf66b 100644
--- a/src/main/java/ui/SecurityGeneration.java
+++ b/src/main/java/ui/SecurityGeneration.java
@@ -142,13 +142,7 @@ public class SecurityGeneration implements Runnable {
Map<AvatarPragmaAuthenticity, ProVerifQueryAuthResult> authResults = pvoa.getAuthenticityResults();
- TraceManager.addDev("authResults= " + authResults);
for (AvatarPragmaAuthenticity pragma : authResults.keySet()) {
- TraceManager.addDev("pragma= " + pragma.getName());
- TraceManager.addDev("pragma.getAttrA()= " + pragma.getAttrA());
- TraceManager.addDev("pragma.getAttrB()= " + pragma.getAttrB());
- TraceManager.addDev("authResults.get(pragma).isProved()= " + authResults.get(pragma).isProved());
- TraceManager.addDev("!authResults.get(pragma).isSatisfied()= " + !authResults.get(pragma).isSatisfied());
if (authResults.get(pragma).isProved() && !authResults.get(pragma).isSatisfied()) {
nonAuthChans.add(pragma.getAttrA().getAttribute().getBlock().getName() + "__" + pragma.getAttrA().getAttribute().getName().replaceAll("_chData", ""));
nonAuthChans.add(pragma.getAttrB().getAttribute().getBlock().getName() + "__" + pragma.getAttrB().getAttribute().getName().replaceAll("_chData", ""));
@@ -343,9 +337,6 @@ public class SecurityGeneration implements Runnable {
nonConf = true;
TraceManager.addDev("SECGEN. non conf basic ch = true");
}
- TraceManager.addDev("nonAuthChans="+nonAuthChans);
- TraceManager.addDev("if1="+chan.getDestinationTask().getName().split("__")[1] + "__" + title + "__" + chan.getDestinationPort().getName());
- TraceManager.addDev("if2="+chan.getDestinationTask().getName().split("__")[1] + "__" + chan.getName());
if (nonAuthChans.contains(chan.getDestinationTask().getName().split("__")[1] + "__" + title + "__" + chan.getDestinationPort().getName())) {
nonAuth = true;
@@ -394,8 +385,6 @@ public class SecurityGeneration implements Runnable {
for (String chanName : portNames) {
//Classify channels based on the type of security requirements and unsatisfied properties
if (chan.isBasicChannel()) {
- TraceManager.addDev("chan.isBasicChannel()="+chan.getName());
- TraceManager.addDev("chan.checkAuth="+chan.checkAuth+" autoWeakAuth="+autoWeakAuth+" nonAuth="+nonAuth);
if (chan.checkConf && autoConf && nonConf) {
toSecure.get(chan.getOriginTask()).add(chan.getDestinationTask());
if (chan.checkAuth && autoStrongAuth) {
@@ -403,7 +392,6 @@ public class SecurityGeneration implements Runnable {
toSecureRev.get(chan.getDestinationTask()).add(chan.getOriginTask());
}
}
- TraceManager.addDev("(chan.checkConf && autoConf && nonConf)");
if (hsmTasks.contains(chan.getOriginTask().getName().split("__")[1])) {
channelSecMap.put(chanName, "hsmSec_" + secName);
if (!hsmSecOutChannels.get(chan.getOriginTask()).contains(chanName) && portInTask(chan.getOriginTask(), chanName)) {
@@ -417,10 +405,8 @@ public class SecurityGeneration implements Runnable {
}
}
} else {
- TraceManager.addDev("else hsmTasks.contains(chan.getOriginTask().getName().split(__)[1])");
if (!secOutChannels.get(chan.getOriginTask()).contains(chanName)) {
secOutChannels.get(chan.getOriginTask()).add(chanName);
- TraceManager.addDev("!secOutChannels.get(chan.getOriginTask()).contains(chanName)");
channelSecMap.put(chanName, "autoEncrypt_" + secName);
if (chan.checkAuth && autoStrongAuth) {
nonceOutChannels.get(chan.getOriginTask()).add(chanName);
@@ -448,7 +434,6 @@ public class SecurityGeneration implements Runnable {
}
} else if (chan.checkAuth && autoWeakAuth && nonAuth) {
- TraceManager.addDev("(chan.checkAuth && autoWeakAuth && nonAuth)");
toSecure.get(chan.getOriginTask()).add(chan.getDestinationTask());
if (autoStrongAuth) {
if (!toSecureRev.get(chan.getDestinationTask()).contains(chan.getOriginTask())) {
@@ -475,7 +460,6 @@ public class SecurityGeneration implements Runnable {
}
} else {
if (!macInChannels.get(chan.getOriginTask()).contains(chanName)) {
- TraceManager.addDev("(!macInChannels.get(chan.getOriginTask()).contains(chanName)");
macOutChannels.get(chan.getOriginTask()).add(chanName);
channelSecMap.put(chanName, "autoEncrypt_" + secName);
if (autoStrongAuth) {
@@ -515,7 +499,6 @@ public class SecurityGeneration implements Runnable {
toSecureRev.get(dest).add(orig);
}
}*/
- TraceManager.addDev("(chan.checkConf && autoConf && nonConf)"+ " dest="+dest.getName() +" orig=" + orig.getName());
if (hsmTasks.contains(orig.getName().split("__")[1])) {
channelSecMap.put(chanName, "hsmSec_" + secName);
if (!hsmSecOutChannels.get(orig).contains(chanName) && portInTask(orig, chanName)) {
@@ -530,7 +513,6 @@ public class SecurityGeneration implements Runnable {
}
} else {
if (!secOutChannels.get(orig).contains(chanName)) {
- TraceManager.addDev("(!secOutChannels.get(orig).contains(chanName))");
secOutChannels.get(orig).add(chanName);
channelSecMap.put(chanName, "autoEncrypt_" + secName);
/* if (chan.checkAuth && autoStrongAuth) {
@@ -559,7 +541,6 @@ public class SecurityGeneration implements Runnable {
}
} else if (chan.checkAuth && autoWeakAuth && nonAuth) {
- TraceManager.addDev("(chan.checkAuth && autoWeakAuth && nonAuth)"+ " dest="+dest.getName() +" orig=" + orig.getName());
toSecure.get(orig).add(dest);
/* if (autoStrongAuth) {
/* if (chan.getOriginTask().getReferenceObject() instanceof TMLCPrimitiveComponent && chan.getDestinationTask().getReferenceObject() instanceof TMLCPrimitiveComponent){*/
@@ -589,7 +570,6 @@ public class SecurityGeneration implements Runnable {
if (!macInChannels.get(orig).contains(chanName)) {
macOutChannels.get(orig).add(chanName);
channelSecMap.put(chanName, "autoEncrypt_" + secName);
- TraceManager.addDev("(!macInChannels.get(orig).contains(chanName))");
/* if (autoStrongAuth) {
nonceOutChannels.get(orig).add(chanName);
}*/
--
GitLab