From 705c3896b8ffbf2d015a6dfea417dd041ae6b84b Mon Sep 17 00:00:00 2001
From: jawher-j <92947144+jawher-j@users.noreply.github.com>
Date: Wed, 5 Jun 2024 09:54:49 +0200
Subject: [PATCH] Generate security for Conf and Weak Auth properties

---
 .../SecurityGenerationForTMAP.java            | 385 ++++++++----------
 1 file changed, 177 insertions(+), 208 deletions(-)

diff --git a/src/main/java/tmltranslator/patternhandling/SecurityGenerationForTMAP.java b/src/main/java/tmltranslator/patternhandling/SecurityGenerationForTMAP.java
index df3f6a2df9..f6df844c16 100644
--- a/src/main/java/tmltranslator/patternhandling/SecurityGenerationForTMAP.java
+++ b/src/main/java/tmltranslator/patternhandling/SecurityGenerationForTMAP.java
@@ -40,13 +40,13 @@
 package tmltranslator.patternhandling;
 /**
  * Class SecurityGenerationForTMAP
- * 
+ *
  * Creation: 28/09/2023
  *
  * @author Jawher JERRAY
  * @version 1.0 28/09/2023
  */
- 
+
 import avatartranslator.AvatarPragma;
 import avatartranslator.AvatarPragmaAuthenticity;
 import avatartranslator.AvatarPragmaSecret;
@@ -68,28 +68,26 @@ import java.util.*;
 public class SecurityGenerationForTMAP implements Runnable {
     final private String  SELECT_CHOICE_HSM = "channelIndex";
 
-    private String appName;
-    private TMLMapping<?> tmap;
-    private String encComp;
-    private String overhead;
-    private String decComp;
-    private Map<String, List<String>> selectedCPUTasks;
-
-    private AVATAR2ProVerif avatar2proverif;
-
-    private Map<TMLTask, TMLTask> taskAndItsHSMMap = new HashMap<TMLTask, TMLTask>();
-    private Map<TMLTask, List<HwCommunicationNode>> taskHSMCommunicationNodesMap = new HashMap<TMLTask, List<HwCommunicationNode>>();
-    private Map<TMLTask, List<TMLActivityElement>> taskHSMBranchesMap = new HashMap<TMLTask, List<TMLActivityElement>>();
-    private Map<Pair<TMLTask, TMLTask>, SecurityPattern> tasksNonceSPMap = new HashMap<Pair<TMLTask, TMLTask>, SecurityPattern>();
-    private Map<Pair<TMLTask, TMLTask>, TMLChannel> tasksNonceChannelMap = new HashMap<Pair<TMLTask, TMLTask>, TMLChannel>();
-    private Map<TMLChannel, TMLChannel> channelNonceToHsmMap = new HashMap<TMLChannel, TMLChannel>();
-    private Map<TMLChannel, TMLChannel> channelNonceFromHsmMap = new HashMap<TMLChannel, TMLChannel>();
-    private Map<TMLTask, TMLRequest> hsmTaskRequestMap = new HashMap<TMLTask, TMLRequest>();
-    private Map<Pair<TMLTask, TMLChannel>, TMLChannel> channelToHsmMap = new HashMap<Pair<TMLTask, TMLChannel>, TMLChannel>();
-    private Map<Pair<TMLTask, TMLChannel>, TMLChannel> channelFromHsmMap = new HashMap<Pair<TMLTask, TMLChannel>, TMLChannel>();
-    private Map<TMLChannel, SecurityPattern> channelSecMap = new HashMap<TMLChannel, SecurityPattern>();
-
-    public SecurityGenerationForTMAP(String appName, TMLMapping<?> tmap, String encComp, String overhead, String decComp, Map<String, List<String>> selectedCPUTasks) {
+    private final String appName;
+    private final TMLMapping<?> tmap;
+    private final String encComp;
+    private final String overhead;
+    private final String decComp;
+    private final Map<String, List<String>> selectedCPUTasks;
+
+    private final Map<TMLTask, TMLTask> taskAndItsHSMMap = new HashMap<>();
+    private final Map<TMLTask, List<HwCommunicationNode>> taskHSMCommunicationNodesMap = new HashMap<>();
+    private final Map<TMLTask, List<TMLActivityElement>> taskHSMBranchesMap = new HashMap<>();
+    private final Map<Pair<TMLTask, TMLTask>, SecurityPattern> tasksNonceSPMap = new HashMap<>();
+    private final Map<Pair<TMLTask, TMLTask>, TMLChannel> tasksNonceChannelMap = new HashMap<>();
+    private final Map<TMLChannel, TMLChannel> channelNonceToHsmMap = new HashMap<>();
+    private final Map<TMLChannel, TMLChannel> channelNonceFromHsmMap = new HashMap<>();
+    private final Map<TMLTask, TMLRequest> hsmTaskRequestMap = new HashMap<>();
+    private final Map<Pair<TMLTask, TMLChannel>, TMLChannel> channelToHsmMap = new HashMap<>();
+    private final Map<Pair<TMLTask, TMLChannel>, TMLChannel> channelFromHsmMap = new HashMap<>();
+
+    public SecurityGenerationForTMAP(String appName, TMLMapping<?> tmap, String encComp, String overhead, String decComp,
+                                     Map<String, List<String>> selectedCPUTasks) {
         this.appName = appName;
         this.tmap = tmap;
         this.overhead = overhead;
@@ -98,14 +96,14 @@ public class SecurityGenerationForTMAP implements Runnable {
         this.selectedCPUTasks = selectedCPUTasks;
     }
     
-    public void proverifAnalysis(TMLMapping<?> tmap, List<TMLChannel> nonConfChans, List<TMLChannel> nonWeakAuthChans, List<TMLChannel> nonStrongAuthChans) {
+    private void proverifAnalysis(TMLMapping<?> tmap, List<TMLChannel> nonConfChans, List<TMLChannel> nonWeakAuthChans,
+                                  List<TMLChannel> nonStrongAuthChans) {
         if (tmap == null) {
             TraceManager.addDev("No mapping");
             return;
         }
 
         //Perform ProVerif Analysis
-
         Object o = null;
         if (tmap.getTMLModeling().getReference() instanceof TGComponent) {
             o = ((TGComponent)(tmap.getTMLModeling().getReference())).getTDiagramPanel().tp;
@@ -118,9 +116,9 @@ public class SecurityGenerationForTMAP implements Runnable {
             return;
         }
 
-        avatar2proverif = new AVATAR2ProVerif(avatarspec);
+        AVATAR2ProVerif avatar2proverif = new AVATAR2ProVerif(avatarspec);
         try {
-            ProVerifSpec proverif = avatar2proverif.generateProVerif(true, true, 3, true, true);
+            avatar2proverif.generateProVerif(true, true, 3, true, true);
             //warnings = avatar2proverif.getWarnings();
 
             if (!avatar2proverif.saveInFile("pvspec")) {
@@ -146,7 +144,7 @@ public class SecurityGenerationForTMAP implements Runnable {
             Map<AvatarPragmaAuthenticity, ProVerifQueryAuthResult> authenticityResults = pvoa.getAuthenticityResults();
             for (TMLChannel ch : tmap.getTMLModeling().getSecChannelMap().keySet()) {
                 if (ch.isCheckConfChannel()) {
-                    List<Integer> confStatus = new ArrayList<Integer>();
+                    List<Integer> confStatus = new ArrayList<>();
                     for (AvatarPragma pragma : tmap.getTMLModeling().getSecChannelMap().get(ch)) {
                         if (pragma instanceof AvatarPragmaSecret) {
                             AvatarPragmaSecret pragmaSecret = (AvatarPragmaSecret) pragma;
@@ -176,8 +174,8 @@ public class SecurityGenerationForTMAP implements Runnable {
                     }
                 }
                 if (ch.isCheckAuthChannel()) {
-                    List<Integer> weakAuthStatus = new ArrayList<Integer>();
-                    List<Integer> strongAuthStatus = new ArrayList<Integer>();
+                    List<Integer> weakAuthStatus = new ArrayList<>();
+                    List<Integer> strongAuthStatus = new ArrayList<>();
                     for (AvatarPragma pragma : tmap.getTMLModeling().getSecChannelMap().get(ch)) {
                         if (pragma instanceof AvatarPragmaAuthenticity) {
                             AvatarPragmaAuthenticity pragmaAuth = (AvatarPragmaAuthenticity) pragma;
@@ -232,8 +230,7 @@ public class SecurityGenerationForTMAP implements Runnable {
             }
 
         } catch (Exception e) {
-            System.out.println("SECGEN EXCEPTION " + e);
-
+            TraceManager.addDev("SECGEN EXCEPTION " + e);
         }
     }
 
@@ -244,39 +241,16 @@ public class SecurityGenerationForTMAP implements Runnable {
             t.join();
         } catch (Exception e) {
             TraceManager.addDev("SECGEN. Error in Security Generation Thread");
-            System.out.println("SECGEN. Error in Security Generation Thread");
         }
         return tmap;
     }
 
-    public boolean portInTask(TMLTask task, TMLChannel ch) {
-        TMLActivity adTask = task.getActivityDiagram();
-        for (TMLActivityElement elem : adTask.getElements()) {
-            if (elem instanceof TMLWriteChannel) {
-                TMLWriteChannel writeChannel = (TMLWriteChannel) elem;
-                for (int i = 0; i < writeChannel.getNbOfChannels(); i++) {
-                    if (writeChannel.getChannel(i).equals(ch)) {
-                        return true;
-                    }
-                }
-            } else if (elem instanceof TMLReadChannel) {
-                TMLReadChannel readChannel = (TMLReadChannel) elem;
-                for (int i = 0; i < readChannel.getNbOfChannels(); i++) {
-                    if (readChannel.getChannel(i).equals(ch)) {
-                        return true;
-                    }
-                }
-            }
-        }
-        return false;
-    }
-
     public void run() {
         TMLModeling<?> tmlmodel = tmap.getTMLModeling();
         //Proverif Analysis channels
-        List<TMLChannel> nonConfChans = new ArrayList<TMLChannel>();
-        List<TMLChannel> nonWeakAuthChans = new ArrayList<TMLChannel>();
-        List<TMLChannel> nonStrongAuthChans = new ArrayList<TMLChannel>();
+        List<TMLChannel> nonConfChans = new ArrayList<>();
+        List<TMLChannel> nonWeakAuthChans = new ArrayList<>();
+        List<TMLChannel> nonStrongAuthChans = new ArrayList<>();
 
         List<TMLChannel> channels = tmlmodel.getChannels();
         for (TMLChannel channel : channels) {
@@ -310,22 +284,22 @@ public class SecurityGenerationForTMAP implements Runnable {
 
         //With the proverif results, check which channels need to be secured
 
-        HashSet<TMLChannel> chAddCSA = new HashSet<TMLChannel>();
-        HashSet<TMLChannel> chAddCWA = new HashSet<TMLChannel>();
-        HashSet<TMLChannel> chAddSA = new HashSet<TMLChannel>();
-        HashSet<TMLChannel> chAddWA = new HashSet<TMLChannel>();
-        HashSet<TMLChannel> chAddC = new HashSet<TMLChannel>();
+        HashSet<TMLChannel> chAddCSA = new HashSet<>();
+        HashSet<TMLChannel> chAddCWA = new HashSet<>();
+        HashSet<TMLChannel> chAddSA = new HashSet<>();
+        HashSet<TMLChannel> chAddWA = new HashSet<>();
+        HashSet<TMLChannel> chAddC = new HashSet<>();
 
         for (TMLChannel chan : tmlmodel.getChannels()) {
             boolean nonConf = nonConfChans.contains(chan);
             boolean nonWeakAuth = nonWeakAuthChans.contains(chan);
             boolean nonStrongAuth = nonStrongAuthChans.contains(chan);
             // add Confidentiality and Strong Authenticity
-            if (chan.isSecurityGoalConf() && nonConf && chan.isSecurityGoalStrongAuth() && nonStrongAuth) {
+            if (chan.isSecurityGoalConf() && chan.isSecurityGoalStrongAuth() && (nonStrongAuth || nonConf)) {
                 chAddCSA.add(chan);
             }
             // add Confidentiality and Weak Authenticity
-            else if (chan.isSecurityGoalConf() && nonConf && chan.isSecurityGoalWeakAuth() && nonWeakAuth) {
+            else if (chan.isSecurityGoalConf() && chan.isSecurityGoalWeakAuth() && (nonWeakAuth || nonConf)) {
                 chAddCWA.add(chan);
             }
             // add Strong Authenticity
@@ -355,80 +329,54 @@ public class SecurityGenerationForTMAP implements Runnable {
 
             SecurityPattern secPattern = new SecurityPattern(secPatternName, SecurityPattern.SYMMETRIC_ENC_PATTERN, overhead, "",
                     encComp, decComp, spNonce.getName(), "", "");
-            channelSecMap.put(ch, secPattern);
-            tmlmodel.addSecurityPattern(secPattern);
-            List<TMLWriteChannel> listWr = WriteOperatorsOfChannel(ch.getOriginTask(), ch);
-            List<TMLReadChannel> listRd = ReadOperatorsOfChannel(ch.getDestinationTask(), ch);
-            if (taskAndItsHSMMap.containsKey(ch.getOriginTask())) {
-                TMLTask hsmTask = taskAndItsHSMMap.get(ch.getOriginTask());
-                TMLChannel chToHSM = FindOrCreateChannelToHSM(hsmTask, ch.getOriginTask(), ch);
-                TMLChannel chFromHSM = FindOrCreateChannelFromHSM(hsmTask, ch.getOriginTask(), ch);
-                addToSecurityTaskMap(hsmTask, secPattern);
-                if (!nonceChannelExist) {
-                    TMLActivityElement NonceBranch = addNonceExchangeBranchHSM(hsmTask, channelNonceToHsmMap.get(chNonce), spNonce, false);
-                    taskHSMBranchesMap.get(hsmTask).add(NonceBranch);
-                    nonceCommunicationWithHsmAD(ch.getOriginTask(), spNonce, channelNonceToHsmMap.get(chNonce), hsmTaskRequestMap.get(hsmTask),
-                            taskHSMBranchesMap.get(hsmTask).size() - 1, true, chNonce, ch.getOriginTask().getActivityDiagram().getFirst());
-                }
-                try {
-                    TMLActivityElement branch = addBranchHSM(hsmTask, chToHSM, chFromHSM, secPattern, true);
-                    taskHSMBranchesMap.get(hsmTask).add(branch);
-                } catch (TMLCheckingError e) {
-                    throw new RuntimeException(e);
-                }
+            HandleSecurityGoalsForChannels(tmlmodel, ch, secPattern, !nonceChannelExist, spNonce, chNonce);
+        }
+        HashSet<TMLChannel> chAddCAndCWA = new HashSet<>(chAddCWA);
+        chAddCAndCWA.addAll(chAddC);
 
-                for (TMLWriteChannel wr : listWr) {
-                    communicationWithHSMAD(ch.getOriginTask(), wr, secPattern, chToHSM, chFromHSM, hsmTaskRequestMap.get(hsmTask), taskHSMBranchesMap.get(hsmTask).size()-1);
-                }
-            } else {
-                addToSecurityTaskMap(ch.getOriginTask(), secPattern);
-                try {
-                    addEncryptionAD(ch.getOriginTask(), listWr, secPattern);
-                } catch (TMLCheckingError e) {
-                    throw new RuntimeException(e);
-                }
-                if (!nonceChannelExist) {
-                    addNonceReceiveAD(ch.getOriginTask(), chNonce, spNonce, ch.getOriginTask().getActivityDiagram().getFirst());
-                }
+        for (TMLChannel ch : chAddCAndCWA) {
+            String secPatternNameInit = "se_" + ch.getChannelName();
+            String secPatternName = secPatternNameInit;
+            int index = 0;
+            while (tmap.getSecurityPatternByName(secPatternName) != null) {
+                secPatternName = secPatternNameInit + index;
+                index ++;
             }
 
-            if (taskAndItsHSMMap.containsKey(ch.getDestinationTask())) {
-                TMLTask hsmTask = taskAndItsHSMMap.get(ch.getDestinationTask());
-                TMLChannel chToHSM = FindOrCreateChannelToHSM(hsmTask, ch.getDestinationTask(), ch);
-                TMLChannel chFromHSM = FindOrCreateChannelFromHSM(hsmTask, ch.getDestinationTask(), ch);
-                addToSecurityTaskMap(hsmTask, secPattern);
-                if (!nonceChannelExist) {
-                    TMLActivityElement NonceBranch = addNonceExchangeBranchHSM(hsmTask, channelNonceFromHsmMap.get(chNonce), spNonce, true);
-                    taskHSMBranchesMap.get(hsmTask).add(NonceBranch);
-                    nonceCommunicationWithHsmAD(ch.getDestinationTask(), spNonce, channelNonceFromHsmMap.get(chNonce), hsmTaskRequestMap.get(hsmTask),
-                            taskHSMBranchesMap.get(hsmTask).size() - 1, false, chNonce, ch.getDestinationTask().getActivityDiagram().getFirst());
-                }
-                try {
-                    TMLActivityElement branch = addBranchHSM(hsmTask, chToHSM, chFromHSM, secPattern, false);
-                    taskHSMBranchesMap.get(hsmTask).add(branch);
-                } catch (TMLCheckingError e) {
-                    throw new RuntimeException(e);
-                }
+            SecurityPattern secPattern = new SecurityPattern(secPatternName, SecurityPattern.SYMMETRIC_ENC_PATTERN, overhead, "",
+                    encComp, decComp, "", "", "");
+            HandleSecurityGoalsForChannels(tmlmodel, ch, secPattern, false, null, null);
+        }
 
-                for (TMLReadChannel rd : listRd) {
-                    communicationWithHSMAD(ch.getDestinationTask(), rd, secPattern, chToHSM, chFromHSM, hsmTaskRequestMap.get(hsmTask), taskHSMBranchesMap.get(hsmTask).size()-1);
-                }
-            } else {
-                try {
-                    addDecryptionAD(ch.getDestinationTask(), listRd, secPattern);
-                } catch (TMLCheckingError e) {
-                    throw new RuntimeException(e);
-                }
-                if (!nonceChannelExist) {
-                    addNonceSendAD(ch.getDestinationTask(), chNonce, spNonce, ch.getDestinationTask().getActivityDiagram().getFirst());
-                }
-                addToSecurityTaskMap(ch.getDestinationTask(), secPattern);
+        for (TMLChannel ch : chAddSA) {
+            SecurityPattern spNonce = FindOrCreateNonceSecurityPattern(ch.getOriginTask(), ch.getDestinationTask());
+            boolean nonceChannelExist = nonceChannelIsCreated(ch.getDestinationTask(), ch.getOriginTask());
+            TMLChannel chNonce = FindOrCreateNonceChannel(ch.getDestinationTask(), ch.getOriginTask());
+            String secPatternNameInit = "mac_" + ch.getChannelName();
+            String secPatternName = secPatternNameInit;
+            int index = 0;
+            while (tmap.getSecurityPatternByName(secPatternName) != null) {
+                secPatternName = secPatternNameInit + index;
+                index ++;
             }
-            for (HwCommunicationNode commNode :tmap.getAllCommunicationNodesOfChannel(ch)) {
-                if (!tmap.isCommNodeMappedOn(chNonce, commNode)) {
-                    tmap.addCommToHwCommNode(chNonce, commNode);
-                }
+
+            SecurityPattern secPattern = new SecurityPattern(secPatternName, SecurityPattern.MAC_PATTERN, overhead, "",
+                    encComp, decComp, spNonce.getName(), "", "");
+            HandleSecurityGoalsForChannels(tmlmodel, ch, secPattern, !nonceChannelExist, spNonce, chNonce);
+        }
+
+        for (TMLChannel ch : chAddWA) {
+            String secPatternNameInit = "mac_" + ch.getChannelName();
+            String secPatternName = secPatternNameInit;
+            int index = 0;
+            while (tmap.getSecurityPatternByName(secPatternName) != null) {
+                secPatternName = secPatternNameInit + index;
+                index ++;
             }
+
+            SecurityPattern secPattern = new SecurityPattern(secPatternName, SecurityPattern.MAC_PATTERN, overhead, "",
+                    encComp, decComp, "", "", "");
+            HandleSecurityGoalsForChannels(tmlmodel, ch, secPattern, false, null, null);
         }
 
         for (TMLTask hsmTask : taskHSMBranchesMap.keySet()) {
@@ -441,6 +389,87 @@ public class SecurityGenerationForTMAP implements Runnable {
         }
     }
 
+    private void HandleSecurityGoalsForChannels(TMLModeling<?> tmlmodel, TMLChannel ch, SecurityPattern secPattern, boolean nonceGenerationNeeded,
+                                                SecurityPattern spNonce, TMLChannel chNonce) {
+        tmlmodel.addSecurityPattern(secPattern);
+        List<TMLWriteChannel> listWr = WriteOperatorsOfChannel(ch.getOriginTask(), ch);
+        List<TMLReadChannel> listRd = ReadOperatorsOfChannel(ch.getDestinationTask(), ch);
+        if (taskAndItsHSMMap.containsKey(ch.getOriginTask())) {
+            TMLTask hsmTask = taskAndItsHSMMap.get(ch.getOriginTask());
+            TMLChannel chToHSM = FindOrCreateChannelToHSM(hsmTask, ch.getOriginTask(), ch);
+            TMLChannel chFromHSM = FindOrCreateChannelFromHSM(hsmTask, ch.getOriginTask(), ch);
+            addToSecurityTaskMap(hsmTask, secPattern);
+            if (nonceGenerationNeeded) {
+                TMLActivityElement NonceBranch = addNonceExchangeBranchHSM(hsmTask, channelNonceToHsmMap.get(chNonce), spNonce, false);
+                taskHSMBranchesMap.get(hsmTask).add(NonceBranch);
+                nonceCommunicationWithHsmAD(ch.getOriginTask(), spNonce, channelNonceToHsmMap.get(chNonce), hsmTaskRequestMap.get(hsmTask),
+                        taskHSMBranchesMap.get(hsmTask).size() - 1, true, chNonce, ch.getOriginTask().getActivityDiagram().getFirst());
+            }
+            try {
+                TMLActivityElement branch = addBranchHSM(hsmTask, chToHSM, chFromHSM, secPattern, true);
+                taskHSMBranchesMap.get(hsmTask).add(branch);
+            } catch (TMLCheckingError e) {
+                throw new RuntimeException(e);
+            }
+
+            for (TMLWriteChannel wr : listWr) {
+                communicationWithHSMAD(ch.getOriginTask(), wr, secPattern, chToHSM, chFromHSM, hsmTaskRequestMap.get(hsmTask),
+                        taskHSMBranchesMap.get(hsmTask).size()-1);
+            }
+        } else {
+            addToSecurityTaskMap(ch.getOriginTask(), secPattern);
+            try {
+                addEncryptionAD(ch.getOriginTask(), listWr, secPattern);
+            } catch (TMLCheckingError e) {
+                throw new RuntimeException(e);
+            }
+            if (nonceGenerationNeeded) {
+                addNonceReceiveAD(ch.getOriginTask(), chNonce, spNonce, ch.getOriginTask().getActivityDiagram().getFirst());
+            }
+        }
+
+        if (taskAndItsHSMMap.containsKey(ch.getDestinationTask())) {
+            TMLTask hsmTask = taskAndItsHSMMap.get(ch.getDestinationTask());
+            TMLChannel chToHSM = FindOrCreateChannelToHSM(hsmTask, ch.getDestinationTask(), ch);
+            TMLChannel chFromHSM = FindOrCreateChannelFromHSM(hsmTask, ch.getDestinationTask(), ch);
+            addToSecurityTaskMap(hsmTask, secPattern);
+            if (nonceGenerationNeeded) {
+                TMLActivityElement NonceBranch = addNonceExchangeBranchHSM(hsmTask, channelNonceFromHsmMap.get(chNonce), spNonce, true);
+                taskHSMBranchesMap.get(hsmTask).add(NonceBranch);
+                nonceCommunicationWithHsmAD(ch.getDestinationTask(), spNonce, channelNonceFromHsmMap.get(chNonce), hsmTaskRequestMap.get(hsmTask),
+                        taskHSMBranchesMap.get(hsmTask).size() - 1, false, chNonce, ch.getDestinationTask().getActivityDiagram().getFirst());
+            }
+            try {
+                TMLActivityElement branch = addBranchHSM(hsmTask, chToHSM, chFromHSM, secPattern, false);
+                taskHSMBranchesMap.get(hsmTask).add(branch);
+            } catch (TMLCheckingError e) {
+                throw new RuntimeException(e);
+            }
+
+            for (TMLReadChannel rd : listRd) {
+                communicationWithHSMAD(ch.getDestinationTask(), rd, secPattern, chToHSM, chFromHSM, hsmTaskRequestMap.get(hsmTask),
+                        taskHSMBranchesMap.get(hsmTask).size()-1);
+            }
+        } else {
+            try {
+                addDecryptionAD(ch.getDestinationTask(), listRd, secPattern);
+            } catch (TMLCheckingError e) {
+                throw new RuntimeException(e);
+            }
+            if (nonceGenerationNeeded) {
+                addNonceSendAD(ch.getDestinationTask(), chNonce, spNonce, ch.getDestinationTask().getActivityDiagram().getFirst());
+            }
+            addToSecurityTaskMap(ch.getDestinationTask(), secPattern);
+        }
+        if (nonceGenerationNeeded) {
+            for (HwCommunicationNode commNode : tmap.getAllCommunicationNodesOfChannel(ch)) {
+                if (!tmap.isCommNodeMappedOn(chNonce, commNode)) {
+                    tmap.addCommToHwCommNode(chNonce, commNode);
+                }
+            }
+        }
+    }
+
     private void initHSMTaskDiagram(TMLTask task) {
         String hsmTaskNameInit = appName + "__" + "HSM_" + task.getTaskName();
         int index = 0;
@@ -470,7 +499,7 @@ public class SecurityGenerationForTMAP implements Runnable {
         request.addParam(new TMLType(TMLType.NATURAL));
         tmap.getTMLModeling().addRequest(request);
         hsmTaskRequestMap.put(hsm, request);
-        taskHSMBranchesMap.put(hsm, new ArrayList<TMLActivityElement>());
+        taskHSMBranchesMap.put(hsm, new ArrayList<>());
         initHSMArchDiagram(hsm, task);
     }
 
@@ -517,7 +546,7 @@ public class SecurityGenerationForTMAP implements Runnable {
 
     private void initHSMArchDiagram(TMLTask hsmTask, TMLTask task) {
         TMLArchitecture arch = tmap.getArch();
-        List<HwCommunicationNode> communicationNodesOfHSM = new ArrayList<HwCommunicationNode>();
+        List<HwCommunicationNode> communicationNodesOfHSM = new ArrayList<>();
         //Find the CPU where the task is mapped to
         HwExecutionNode cpuTask = tmap.getHwNodeOf(task);
 
@@ -586,7 +615,8 @@ public class SecurityGenerationForTMAP implements Runnable {
         taskHSMCommunicationNodesMap.put(hsmTask, communicationNodesOfHSM);
     }
 
-    private TMLActivityElement addBranchHSM(TMLTask hsmTask, TMLChannel dataCh, TMLChannel retrieveDataCh, SecurityPattern sp, boolean isEncryption) throws TMLCheckingError {
+    private TMLActivityElement addBranchHSM(TMLTask hsmTask, TMLChannel dataCh, TMLChannel retrieveDataCh, SecurityPattern sp,
+                                            boolean isEncryption) throws TMLCheckingError {
         TMLActivity hsmTaskAD = hsmTask.getActivityDiagram();
         TMLReadChannel rd = new TMLReadChannel(dataCh.getChannelName(), hsmTaskAD.getReferenceObject());
         rd.addChannel(dataCh);
@@ -657,34 +687,6 @@ public class SecurityGenerationForTMAP implements Runnable {
         }
     }
 
-    /*private TMLActivityElement addNonceExchangeHSM(TMLTask hsmTask, TMLChannel nonceCh, SecurityPattern sp, boolean isNonceSender,
-                                                   TMLActivityElement headerElement) {
-        TMLActivity hsmTaskAD = hsmTask.getActivityDiagram();
-        if (isNonceSender) {
-            TMLExecC exec = new TMLExecC(sp.getName(), hsmTaskAD.getReferenceObject());
-            exec.setSecurityPattern(sp);
-            exec.setAction(Integer.toString(sp.getEncTime()));
-            hsmTaskAD.addElement(exec);
-            headerElement.addNext(exec);
-
-            TMLWriteChannel wr = new TMLWriteChannel(nonceCh.getChannelName(), hsmTaskAD.getReferenceObject());
-            wr.addChannel(nonceCh);
-            hsmTaskAD.addElement(wr);
-            wr.setNbOfSamples("1");
-            wr.setSecurityPattern(sp);
-            exec.addNext(wr);
-            return wr;
-        } else {
-            TMLReadChannel rd = new TMLReadChannel(nonceCh.getChannelName(), hsmTaskAD.getReferenceObject());
-            rd.addChannel(nonceCh);
-            rd.setSecurityPattern(sp);
-            rd.setNbOfSamples("1");
-            hsmTaskAD.addElement(rd);
-            headerElement.addNext(rd);
-            return rd;
-        }
-    }*/
-
     private void communicationWithHSMAD(TMLTask task, TMLActivityElementChannel comm, SecurityPattern sp, TMLChannel dataCh,
                                         TMLChannel retrieveDataCh, TMLRequest request, int indexRequest) {
         TMLActivity taskAD = task.getActivityDiagram();
@@ -846,7 +848,7 @@ public class SecurityGenerationForTMAP implements Runnable {
     }
 
     private List<TMLReadChannel> ReadOperatorsOfChannel(TMLTask task, TMLChannel ch) {
-        List<TMLReadChannel> elems = new ArrayList<TMLReadChannel>();
+        List<TMLReadChannel> elems = new ArrayList<>();
         for (TMLActivityElement elem : task.getActivityDiagram().getElements()) {
             if (elem instanceof TMLReadChannel) {
                 TMLReadChannel rc = (TMLReadChannel) elem;
@@ -861,7 +863,7 @@ public class SecurityGenerationForTMAP implements Runnable {
     }
 
     private List<TMLWriteChannel> WriteOperatorsOfChannel(TMLTask task, TMLChannel ch) {
-        List<TMLWriteChannel> elems = new ArrayList<TMLWriteChannel>();
+        List<TMLWriteChannel> elems = new ArrayList<>();
         for (TMLActivityElement elem : task.getActivityDiagram().getElements()) {
             if (elem instanceof TMLWriteChannel) {
                 TMLWriteChannel wc = (TMLWriteChannel) elem;
@@ -888,7 +890,8 @@ public class SecurityGenerationForTMAP implements Runnable {
         if (tasksNonceSPMap.containsKey(taskPair)) {
             return tasksNonceSPMap.get(taskPair);
         }
-        SecurityPattern secPatternNonce = new SecurityPattern("nonce_" + destinationTaskInit.getTaskName() + "_" + originTaskInit.getTaskName(), SecurityPattern.NONCE_PATTERN, overhead, "", encComp, decComp, "", "", "");
+        SecurityPattern secPatternNonce = new SecurityPattern("nonce_" + destinationTaskInit.getTaskName() + "_" + originTaskInit.getTaskName(),
+                SecurityPattern.NONCE_PATTERN, overhead, "", encComp, decComp, "", "", "");
         tasksNonceSPMap.put(taskPair, secPatternNonce);
         tmap.getTMLModeling().addSecurityPattern(secPatternNonce);
         return secPatternNonce;
@@ -1013,7 +1016,7 @@ public class SecurityGenerationForTMAP implements Runnable {
                 tmlmodel.getSecurityTaskMap().get(sec).add(task);
             }
         } else {
-            List<TMLTask> listTask = new ArrayList<TMLTask>();
+            List<TMLTask> listTask = new ArrayList<>();
             listTask.add(task);
             tmlmodel.getSecurityTaskMap().put(sec, listTask);
         }
@@ -1021,7 +1024,7 @@ public class SecurityGenerationForTMAP implements Runnable {
 
     public TMLMapping<?> autoMapKeys() {
         if (tmap == null) {
-            return tmap;
+            return null;
         }
         //Find all Security Patterns, if they don't have an associated memory at encrypt and decrypt, tmap them
         TMLModeling<?> tmlm = tmap.getTMLModeling();
@@ -1029,7 +1032,8 @@ public class SecurityGenerationForTMAP implements Runnable {
             return tmap;
         }
         for (SecurityPattern sp : tmlm.getSecurityTaskMap().keySet()) {
-            if (sp.getType().equals(SecurityPattern.SYMMETRIC_ENC_PATTERN) || sp.getType().equals(SecurityPattern.MAC_PATTERN) || sp.getType().equals(SecurityPattern.ASYMMETRIC_ENC_PATTERN)) {
+            if (sp.getType().equals(SecurityPattern.SYMMETRIC_ENC_PATTERN) || sp.getType().equals(SecurityPattern.MAC_PATTERN) ||
+                    sp.getType().equals(SecurityPattern.ASYMMETRIC_ENC_PATTERN)) {
                 for (TMLTask t : tmlm.getSecurityTaskMap().get(sp)) {
                     HwExecutionNode node1 = tmap.getHwNodeOf(t);
                     boolean taskMappedToCPU = false;
@@ -1046,7 +1050,6 @@ public class SecurityGenerationForTMAP implements Runnable {
                                     HwBus curBus = link.bus;
                                     boolean keyFound = false;
                                     HwMemory memNodeToMap = null;
-                                    outer:
                                     for (HwLink linkBus : tmap.getArch().getHwLinks()) {
                                         if (linkBus.bus == curBus) {
                                             if (linkBus.hwnode instanceof HwMemory) {
@@ -1055,7 +1058,7 @@ public class SecurityGenerationForTMAP implements Runnable {
                                                 if (keys.contains(sp)) {
                                                     keyFound = true;
                                                     keyMappedtoMem = true;
-                                                    break outer;
+                                                    break;
                                                 }
                                             }
                                         }
@@ -1064,7 +1067,6 @@ public class SecurityGenerationForTMAP implements Runnable {
                                         if (memNodeToMap != null) {
                                             TraceManager.addDev("Adding " + sp.getName() + " key to " + memNodeToMap.getName());
                                             tmap.addSecurityPattern(memNodeToMap, sp);
-                                            keyMappedtoMem = true;
                                         } else {
                                             HwMemory newHwMemory = new HwMemory(cpuNode.getName() + "KeysMemory");
                                             TraceManager.addDev("Creating new memory: " + newHwMemory.getName());
@@ -1076,8 +1078,8 @@ public class SecurityGenerationForTMAP implements Runnable {
                                             tmap.getArch().getHwLinks().add(linkNewMemWithBus);
                                             tmap.addSecurityPattern(newHwMemory, sp);
                                             TraceManager.addDev("Adding " + sp.getName() + " key to " + newHwMemory.getName());
-                                            keyMappedtoMem = true;
                                         }
+                                        keyMappedtoMem = true;
                                     }
                                 }
                             }
@@ -1105,7 +1107,6 @@ public class SecurityGenerationForTMAP implements Runnable {
 
                                 tmap.addSecurityPattern(memNodeToMap, sp);
                                 TraceManager.addDev("Adding " + sp.getName() + " key to " + memNodeToMap.getName());
-                                keyMappedtoMem = true;
 
                                 //Connect Bus and Memory
                                 HwLink newLinkBusMemory = new HwLink("Link_"+newPrivateBus.getName() + "_" + memNodeToMap.getName());
@@ -1153,36 +1154,4 @@ public class SecurityGenerationForTMAP implements Runnable {
         return tmap;
     }
 
-    class HSMChannel {
-        public static final int SENC = 0;
-        public static final int NONCE_ENC = 1;
-        public static final int MAC = 2;
-        public static final int DEC = 3;
-        public static final int AENC = 4;
-        public static final int NONCE = 5;
-        public TMLChannel channel;
-        public TMLTask task;
-        public int secType;
-        public String nonceName = "";
-
-        public HSMChannel(TMLChannel n, TMLTask t, int type) {
-            channel = n;
-            task = t;
-            secType = type;
-        }
-    }
-
-    class ChannelData {
-        public String name;
-        public boolean isOrigin;
-        public boolean isChan;
-
-        public ChannelData(String n, boolean orig, boolean isCh) {
-            name = n;
-            isOrigin = orig;
-            isChan = isCh;
-        }
-
-    }
-
 }
-- 
GitLab