Commit 1da84b5c authored by Letitia Li's avatar Letitia Li

Fixed proverif result trace display

parent 2914d855
......@@ -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());
}
......
......@@ -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;
}
......
......@@ -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();
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment