From 1da84b5cdb3155ac0c047b71c777e4b6c90884d4 Mon Sep 17 00:00:00 2001
From: L <letitia.li@telecom-paristech.fr>
Date: Wed, 26 Sep 2018 12:37:21 -0400
Subject: [PATCH] Fixed proverif result trace display
---
src/main/java/tmltranslator/TMLModeling.java | 20 +++++++++----------
.../tmltranslator/toavatar/TML2Avatar.java | 12 ++++++++---
.../java/ui/tmlcompd/TMLCPrimitivePort.java | 11 ++++++++--
3 files changed, 28 insertions(+), 15 deletions(-)
diff --git a/src/main/java/tmltranslator/TMLModeling.java b/src/main/java/tmltranslator/TMLModeling.java
index a193a0ef80..69dfa06bf3 100755
--- a/src/main/java/tmltranslator/TMLModeling.java
+++ b/src/main/java/tmltranslator/TMLModeling.java
@@ -838,7 +838,7 @@ public class TMLModeling<E> {
port.mappingName= mappingName;
//Add Result Trace also
ProVerifResultTrace trace = pvoa.getResults().get(pragma).getTrace();
- if (trace !=null){
+ if (trace !=null && port.isOrigin){
port.setResultTrace(trace);
port.setPragmaString(pragma.toString());
}
@@ -929,7 +929,7 @@ public class TMLModeling<E> {
port.checkStrongAuthStatus = 3;
port.mappingName= mappingName;
ProVerifResultTrace trace = pvoa.getResults().get(pragma).getTrace();
- if (trace !=null){
+ if (trace !=null && !port.isOrigin){
port.setResultTrace(trace);
port.setPragmaString(pragma.toString());
}
@@ -981,7 +981,7 @@ public class TMLModeling<E> {
TraceManager.addDev("not verified " + signalName);
port.secName= signalName;
ProVerifResultTrace trace = pvoa.getResults().get(pragma).getTrace();
- if (trace !=null){
+ if (trace !=null && !port.isOrigin){
port.setResultTrace(trace);
port.setPragmaString(pragma.toString());
}
@@ -1012,7 +1012,7 @@ public class TMLModeling<E> {
port.checkWeakAuthStatus = 3;
port.secName= signalName;
ProVerifResultTrace trace = pvoa.getResults().get(pragma).getTrace();
- if (trace !=null){
+ if (trace !=null && !port.isOrigin){
port.setResultTrace(trace);
port.setPragmaString(pragma.toString());
}
@@ -1035,7 +1035,7 @@ public class TMLModeling<E> {
port.checkWeakAuthStatus = 2;
port.mappingName= mappingName;
ProVerifResultTrace trace = pvoa.getResults().get(pragma).getTrace();
- if (trace !=null){
+ if (trace !=null && !port.isOrigin){
port.setResultTrace(trace);
port.setPragmaString(pragma.toString());
}
@@ -1092,7 +1092,7 @@ public class TMLModeling<E> {
port.checkWeakAuthStatus = 2;
port.secName= signalName;
ProVerifResultTrace trace = pvoa.getResults().get(pragma).getTrace();
- if (trace !=null){
+ if (trace !=null && !port.isOrigin){
port.setResultTrace(trace);
port.setPragmaString(pragma.toString());
}
@@ -1123,7 +1123,7 @@ public class TMLModeling<E> {
port.checkWeakAuthStatus = 2;
port.secName= signalName;
ProVerifResultTrace trace = pvoa.getResults().get(pragma).getTrace();
- if (trace !=null){
+ if (trace !=null && !port.isOrigin){
port.setResultTrace(trace);
port.setPragmaString(pragma.toString());
}
@@ -1150,7 +1150,7 @@ public class TMLModeling<E> {
port.checkStrongAuthStatus = 2;
port.mappingName= mappingName;
ProVerifResultTrace trace = pvoa.getResults().get(pragma).getTrace();
- if (trace !=null){
+ if (trace !=null && !port.isOrigin){
port.setResultTrace(trace);
port.setPragmaString(pragma.toString());
}
@@ -1210,7 +1210,7 @@ public class TMLModeling<E> {
port.checkStrongAuthStatus = 2;
port.secName= signalName;
ProVerifResultTrace trace = pvoa.getResults().get(pragma).getTrace();
- if (trace !=null){
+ if (trace !=null && !port.isOrigin){
port.setResultTrace(trace);
port.setPragmaString(pragma.toString());
}
@@ -1242,7 +1242,7 @@ public class TMLModeling<E> {
port.checkStrongAuthStatus = 2;
port.secName= signalName;
ProVerifResultTrace trace = pvoa.getResults().get(pragma).getTrace();
- if (trace !=null){
+ if (trace !=null && !port.isOrigin){
port.setResultTrace(trace);
port.setPragmaString(pragma.toString());
}
diff --git a/src/main/java/tmltranslator/toavatar/TML2Avatar.java b/src/main/java/tmltranslator/toavatar/TML2Avatar.java
index 723ac0a3c5..707d11a76a 100644
--- a/src/main/java/tmltranslator/toavatar/TML2Avatar.java
+++ b/src/main/java/tmltranslator/toavatar/TML2Avatar.java
@@ -2195,15 +2195,21 @@ public class TML2Avatar {
for (SecurityPattern sp:pubKeys.keySet()){
if (pubKeys.get(sp).size()!=0){
String keys = "";
+ List<String> pubKeyNames = new ArrayList<String>();
for (AvatarAttribute key: pubKeys.get(sp)){
- keys= keys+" "+key.getBlock().getName() + "."+key.getName();
+ if (!pubKeyNames.contains(key.getBlock().getName()+"."+key.getName())){
+ keys= keys+" "+key.getBlock().getName() + "."+key.getName();
+ pubKeyNames.add(key.getBlock().getName()+"."+key.getName());
+ }
}
- avspec.addPragma(new AvatarPragmaInitialKnowledge("#InitialSessionKnowledge "+keys, null, pubKeys.get(sp),true));
+ // avspec.addPragma(new AvatarPragmaInitialKnowledge("#InitialSessionKnowledge "+keys, null, pubKeys.get(sp),true));
+ //System.out.println("pragma " + keys);
}
}
+
tmlmap.getTMLModeling().secChannelMap = secChannelMap;
- // System.out.println("avatar spec\n" +avspec);
+// System.out.println("avatar spec\n" +avspec);
return avspec;
}
diff --git a/src/main/java/ui/tmlcompd/TMLCPrimitivePort.java b/src/main/java/ui/tmlcompd/TMLCPrimitivePort.java
index aef9c3a0e8..a13e3a2c2a 100755
--- a/src/main/java/ui/tmlcompd/TMLCPrimitivePort.java
+++ b/src/main/java/ui/tmlcompd/TMLCPrimitivePort.java
@@ -671,12 +671,19 @@ public abstract class TMLCPrimitivePort extends TGCScalableWithInternalComponent
try {
PipedInputStream pis = new PipedInputStream(pos, 4096);
BufferedWriter bw = new BufferedWriter(new OutputStreamWriter(pos));
-
- JFrameSimulationSDPanel jfssdp = new JFrameSimulationSDPanel(null, tdp.getMGUI(), "Trace for confidentiality property of " + pragma);
+ String title = "";
+ if (isOrigin){
+ title = "Trace for confidentiality property of ";
+ }
+ else {
+ title = "Trace for authenticity property of ";
+ }
+ JFrameSimulationSDPanel jfssdp = new JFrameSimulationSDPanel(null, tdp.getMGUI(), title + pragma);
jfssdp.setIconImage(IconManager.img8);
GraphicLib.centerOnParent(jfssdp, 600, 600);
jfssdp.setFileReference(new BufferedReader(new InputStreamReader(pis)));
jfssdp.setVisible(true);
+ jfssdp.setLimitEntity(false);
//jfssdp.setModalExclusionType(ModalExclusionType
// .APPLICATION_EXCLUDE);
jfssdp.toFront();
--
GitLab