From c5d0bf021cdb311fae4db06a54ca56bcb8c9ec16 Mon Sep 17 00:00:00 2001
From: Letitia Li <letitia.li@telecom-paristech.fr>
Date: Mon, 29 May 2017 09:25:05 +0200
Subject: [PATCH] TML verification update
---
.../toproverif/AVATAR2ProVerif.java | 4 +-
src/tmltranslator/TMLModeling.java | 286 ++++++++++--------
src/tmltranslator/toavatar/TML2Avatar.java | 89 +++---
src/ui/GTURTLEModeling.java | 9 +-
.../JDialogCryptographicConfiguration.java | 2 +-
5 files changed, 217 insertions(+), 173 deletions(-)
diff --git a/src/avatartranslator/toproverif/AVATAR2ProVerif.java b/src/avatartranslator/toproverif/AVATAR2ProVerif.java
index 6de4f4bc0f..709ca3ce8d 100755
--- a/src/avatartranslator/toproverif/AVATAR2ProVerif.java
+++ b/src/avatartranslator/toproverif/AVATAR2ProVerif.java
@@ -1250,7 +1250,9 @@ public class AVATAR2ProVerif implements AvatarTranslator {
if (! (args.get(i) instanceof AvatarAttribute)) {
CheckingError ce = new CheckingError(CheckingError.BEHAVIOR_ERROR, "'" + args.get(i).getName () + "' should be an attribute (ignored)");
ce.setAvatarBlock(arg.block);
- ce.setTDiagramPanel(((AvatarDesignPanel)(this.avspec.getReferenceObject())).getAvatarSMDPanel(arg.block.getName()));
+ if (this.avspec.getReferenceObject() instanceof AvatarDesignPanel){
+ ce.setTDiagramPanel(((AvatarDesignPanel)(this.avspec.getReferenceObject())).getAvatarSMDPanel(arg.block.getName()));
+ }
ce.setTGComponent((TGComponent)(_asme.getReferenceObject()));
this.warnings.add(ce);
ok = false;
diff --git a/src/tmltranslator/TMLModeling.java b/src/tmltranslator/TMLModeling.java
index 281c13a28f..bee0b1c30e 100755
--- a/src/tmltranslator/TMLModeling.java
+++ b/src/tmltranslator/TMLModeling.java
@@ -692,7 +692,7 @@ public class TMLModeling {
}
public void backtrace(ProVerifOutputAnalyzer pvoa, String mappingName){
- //System.out.println("Backtracing Confidentiality");
+ System.out.println("Backtracing Confidentiality");
LinkedList<AvatarAttribute> secretAttributes = pvoa.getSecretTerms ();
LinkedList<AvatarAttribute> nonSecretAttributes = pvoa.getNonSecretTerms ();
for (AvatarAttribute attr: secretAttributes){
@@ -726,18 +726,20 @@ public class TMLModeling {
}
}
List<String> channels=secChannelMap.get(attr.getName());
- for (String channelName: channels){
- // if (channelName!=null){
- channel = getChannelByShortName(channelName);
- if (channel!=null){
- for (TMLCPrimitivePort port:channel.ports){
- if (port.checkConf){
- port.checkSecConfStatus = 2;
- port.secName= attr.getName();
- }
- }
- }
- }
+ if (channels!=null){
+ for (String channelName: channels){
+ // if (channelName!=null){
+ channel = getChannelByShortName(channelName);
+ if (channel!=null){
+ for (TMLCPrimitivePort port:channel.ports){
+ if (port.checkConf){
+ port.checkSecConfStatus = 2;
+ port.secName= attr.getName();
+ }
+ }
+ }
+ }
+ }
for (TMLTask t:getTasks()){
if (t.getReferenceObject()==null){
continue;
@@ -782,18 +784,20 @@ public class TMLModeling {
}
}
List<String> channels=secChannelMap.get(attr.getName());
- for (String channelName: channels){
-// if (channelName!=null){
- channel = getChannelByShortName(channelName);
- if (channel!=null){
- for (TMLCPrimitivePort port:channel.ports){
- if (port.checkConf){
- port.checkSecConfStatus = 3;
- port.secName= attr.getName();
- }
- }
- }
- }
+ if (channels!=null){
+ for (String channelName: channels){
+// if (channelName!=null){
+ channel = getChannelByShortName(channelName);
+ if (channel!=null){
+ for (TMLCPrimitivePort port:channel.ports){
+ if (port.checkConf){
+ port.checkSecConfStatus = 3;
+ port.secName= attr.getName();
+ }
+ }
+ }
+ }
+ }
for (TMLTask t:getTasks()){
if (t.getReferenceObject() instanceof TMLCPrimitiveComponent){
TMLCPrimitiveComponent comp = (TMLCPrimitiveComponent) t.getReferenceObject();
@@ -804,6 +808,7 @@ public class TMLModeling {
}
}
}
+ System.out.println("Finished backtracing");
return;
}
public void backtraceAuthenticity(LinkedList<String> satisfiedAuthenticity, LinkedList<String> satisfiedWeakAuthenticity,LinkedList<String> nonSatisfiedAuthenticity, String mappingName){
@@ -867,19 +872,21 @@ public class TMLModeling {
}*/
signalName=signalName.split("__")[1];
List<String> channels=secChannelMap.get(signalName);
- for (String channelName: channels){
- // if (channelName!=null){
- channel = getChannelByShortName(channelName);
- if (channel!=null){
- for (TMLCPrimitivePort port:channel.ports){
- if (port.checkAuth){
- port.checkStrongAuthStatus = 2;
- port.secName= signalName;
- }
- }
- }
- }
- }
+ if (channels!=null){
+ for (String channelName: channels){
+ // if (channelName!=null){
+ channel = getChannelByShortName(channelName);
+ if (channel!=null){
+ for (TMLCPrimitivePort port:channel.ports){
+ if (port.checkAuth){
+ port.checkStrongAuthStatus = 2;
+ port.secName= signalName;
+ }
+ }
+ }
+ }
+ }
+ }
for (String s: satisfiedWeakAuthenticity){
String signalName = s.split("_chData")[0];
signalName = signalName.split("__")[1];
@@ -932,20 +939,22 @@ public class TMLModeling {
}*/
signalName = signalName.split("__")[1];
List<String> channels=secChannelMap.get(signalName);
- for (String channelName:channels){
-// if (channelName!=null){
- System.out.println("original channel " + channelName);
- channel = getChannelByShortName(channelName);
- if (channel!=null){
- for (TMLCPrimitivePort port:channel.ports){
- if (port.checkAuth){
- port.checkWeakAuthStatus = 2;
- port.secName= signalName;
- }
- }
- }
- }
- }
+ if (channels!=null){
+ for (String channelName:channels){
+// if (channelName!=null){
+ System.out.println("original channel " + channelName);
+ channel = getChannelByShortName(channelName);
+ if (channel!=null){
+ for (TMLCPrimitivePort port:channel.ports){
+ if (port.checkAuth){
+ port.checkWeakAuthStatus = 2;
+ port.secName= signalName;
+ }
+ }
+ }
+ }
+ }
+ }
for (String s: nonSatisfiedAuthenticity){
System.out.println(s);
String signalName = s.split("_chData")[0];
@@ -1009,101 +1018,110 @@ public class TMLModeling {
}
}*/
List<String> channels=secChannelMap.get(signalName);
- for (String channelName:channels){
-// if (channelName!=null){
- channel = getChannelByShortName(channelName);
- if (channel!=null){
- for (TMLCPrimitivePort port:channel.ports){
- if (port.checkAuth){
- port.checkStrongAuthStatus = 3;
- port.secName= signalName;
- }
- }
- }
- }
- }
-
- //In case of HSM
- for (String s: satisfiedWeakAuthenticity){
- String signalName = s.split("__decrypt")[0];
- signalName = signalName.split("__")[1];
- List<String> channels=secChannelMap.get(signalName);
- for (String channelName: channels){
-// if (channelName!=null){
- if (channelName.contains("retData_") || channelName.contains("data_")){
- channelName=channelName.replaceAll("retData_","").replaceAll("data_","");
- //channelName=channelName.split("__retData_")[1];
- String header= channelName.split("__retData_")[0];
- for (TMLTask t: getTasks()){
- if (channelName.contains(t.getName().split("__")[1])){
- channelName = channelName.replace("_"+t.getName().split("__")[1],"");
- }
- }
- TMLChannel channel = getChannelByShortName(channelName);
- if (channel!=null){
- for (TMLCPrimitivePort port:channel.ports){
+ if (channels!=null){
+ for (String channelName:channels){
+// if (channelName!=null){
+ channel = getChannelByShortName(channelName);
+ if (channel!=null){
+ for (TMLCPrimitivePort port:channel.ports){
if (port.checkAuth){
- port.checkWeakAuthStatus = 2;
+ port.checkStrongAuthStatus = 3;
port.secName= signalName;
- }
- }
- }
+ }
+ }
+ }
}
- }
+ }
}
+ //In case of HSM
+
for (String s: nonSatisfiedAuthenticity){
String signalName = s.split("__decrypt")[0];
signalName = signalName.split("__")[1];
List<String> channels=secChannelMap.get(signalName);
- for (String channelName: channels){
- //if (channelName!=null){
- if (channelName.contains("retData_") || channelName.contains("data_")){
- channelName=channelName.replaceAll("retData_","").replaceAll("data_","");
- //channelName=channelName.split("__retData_")[1];
- String header= channelName.split("__retData_")[0];
- for (TMLTask t: getTasks()){
- if (channelName.contains(t.getName().split("__")[1])){
- channelName = channelName.replace("_"+t.getName().split("__")[1],"");
- }
- }
- TMLChannel channel = getChannelByShortName(channelName);
- if (channel!=null){
- for (TMLCPrimitivePort port:channel.ports){
- if (port.checkAuth){
- port.checkWeakAuthStatus = 3;
- port.secName= signalName;
- }
- }
- }
- }
- }
+ if (channels!=null){
+ for (String channelName: channels){
+ //if (channelName!=null){
+ if (channelName.contains("retData_") || channelName.contains("data_")){
+ channelName=channelName.replaceAll("retData_","").replaceAll("data_","");
+ //channelName=channelName.split("__retData_")[1];
+ String header= channelName.split("__retData_")[0];
+ for (TMLTask t: getTasks()){
+ if (channelName.contains(t.getName().split("__")[1])){
+ channelName = channelName.replace("_"+t.getName().split("__")[1],"");
+ }
+ }
+ TMLChannel channel = getChannelByShortName(channelName);
+ if (channel!=null){
+
+ for (TMLCPrimitivePort port:channel.ports){
+ if (port.checkAuth){
+ port.checkWeakAuthStatus = 3;
+ port.secName= signalName;
+ }
+ }
+ }
+ }
+ }
+ }
}
- for (String s: satisfiedAuthenticity){
+ for (String s: satisfiedWeakAuthenticity){
String signalName = s.split("__decrypt")[0];
signalName = signalName.split("__")[1];
List<String> channels=secChannelMap.get(signalName);
- for (String channelName: channels){
+ if (channels!=null){
+ for (String channelName: channels){
// if (channelName!=null){
- if (channelName.contains("retData_") || channelName.contains("data_")){
- channelName=channelName.replaceAll("retData_","").replaceAll("data_","");
- //channelName=channelName.split("__retData_")[1];
- String header= channelName.split("__retData_")[0];
- for (TMLTask t: getTasks()){
- if (channelName.contains(t.getName().split("__")[1])){
- channelName = channelName.replace("_"+t.getName().split("__")[1],"");
- }
- }
- TMLChannel channel = getChannelByShortName(channelName);
- if (channel!=null){
- for (TMLCPrimitivePort port:channel.ports){
- if (port.checkAuth){
- port.checkStrongAuthStatus = 2;
- port.secName= signalName;
- }
- }
- }
- }
- }
+ if (channelName.contains("retData_") || channelName.contains("data_")){
+ channelName=channelName.replaceAll("retData_","").replaceAll("data_","");
+ //channelName=channelName.split("__retData_")[1];
+ String header= channelName.split("__retData_")[0];
+ for (TMLTask t: getTasks()){
+ if (channelName.contains(t.getName().split("__")[1])){
+ channelName = channelName.replace("_"+t.getName().split("__")[1],"");
+ }
+ }
+ TMLChannel channel = getChannelByShortName(channelName);
+ if (channel!=null){
+ for (TMLCPrimitivePort port:channel.ports){
+ if (port.checkAuth){
+ port.checkWeakAuthStatus = 2;
+ port.secName= signalName;
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+ for (String s: satisfiedAuthenticity){
+ String signalName = s.split("__decrypt")[0];
+ signalName = signalName.split("__")[1];
+ List<String> channels=secChannelMap.get(signalName);
+ if (channels!=null){
+ for (String channelName: channels){
+// if (channelName!=null){
+ if (channelName.contains("retData_") || channelName.contains("data_")){
+ channelName=channelName.replaceAll("retData_","").replaceAll("data_","");
+ //channelName=channelName.split("__retData_")[1];
+ String header= channelName.split("__retData_")[0];
+ for (TMLTask t: getTasks()){
+ if (channelName.contains(t.getName().split("__")[1])){
+ channelName = channelName.replace("_"+t.getName().split("__")[1],"");
+ }
+ }
+ TMLChannel channel = getChannelByShortName(channelName);
+ if (channel!=null){
+ for (TMLCPrimitivePort port:channel.ports){
+ if (port.checkAuth){
+ port.checkStrongAuthStatus = 2;
+ port.secName= signalName;
+ }
+ }
+ }
+ }
+ }
+ }
}
}
public void clearBacktracing(){
diff --git a/src/tmltranslator/toavatar/TML2Avatar.java b/src/tmltranslator/toavatar/TML2Avatar.java
index 60d2bc47c4..06045e847b 100644
--- a/src/tmltranslator/toavatar/TML2Avatar.java
+++ b/src/tmltranslator/toavatar/TML2Avatar.java
@@ -670,15 +670,15 @@ public class TML2Avatar {
}
else if (ae.securityPattern.type.equals("Symmetric Encryption")){
if (!ae.securityPattern.nonce.isEmpty()){
- block.addAttribute(new AvatarAttribute("nonce_"+ae.securityPattern.nonce, AvatarType.INTEGER, block, null));
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.nonce, AvatarType.INTEGER, block, null));
AvatarMethod concat2 = new AvatarMethod("concat2",ae);
concat2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
- concat2.addParameter(block.getAvatarAttributeWithName("nonce_"+ae.securityPattern.nonce));
+ concat2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.nonce));
concat2.addReturnParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
- if (block.getAvatarAttributeWithName(ae.securityPattern.name) !=null && block.getAvatarAttributeWithName("nonce_"+ae.securityPattern.nonce)!=null){
+ if (block.getAvatarAttributeWithName(ae.securityPattern.name) !=null && block.getAvatarAttributeWithName(ae.securityPattern.nonce)!=null){
block.addMethod(concat2);
}
- tran.addAction(ae.securityPattern.name+"=concat2("+ae.securityPattern.name + ",nonce_"+ae.securityPattern.nonce+")");
+ tran.addAction(ae.securityPattern.name+"=concat2("+ae.securityPattern.name + ","+ae.securityPattern.nonce+")");
}
//Securing a key instead of data
if (!ae.securityPattern.key.isEmpty()){
@@ -708,14 +708,14 @@ public class TML2Avatar {
}
else if (ae.securityPattern.type.equals("Asymmetric Encryption")){
if (!ae.securityPattern.nonce.isEmpty()){
- block.addAttribute(new AvatarAttribute("nonce_"+ae.securityPattern.nonce, AvatarType.INTEGER, block, null));
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.nonce, AvatarType.INTEGER, block, null));
AvatarMethod concat2 = new AvatarMethod("concat2",ae);
concat2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
- concat2.addParameter(block.getAvatarAttributeWithName("nonce_"+ae.securityPattern.nonce));
- if (block.getAvatarAttributeWithName(ae.securityPattern.name) !=null && block.getAvatarAttributeWithName("nonce_"+ae.securityPattern.nonce)!=null){
+ concat2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.nonce));
+ if (block.getAvatarAttributeWithName(ae.securityPattern.name) !=null && block.getAvatarAttributeWithName(ae.securityPattern.nonce)!=null){
block.addMethod(concat2);
}
- tran.addAction(ae.securityPattern.name+"=concat2("+ae.securityPattern.name + ",nonce_"+ae.securityPattern.nonce+")");
+ tran.addAction(ae.securityPattern.name+"=concat2("+ae.securityPattern.name + ","+ae.securityPattern.nonce+")");
}
//Securing a key instead of data
if (!ae.securityPattern.key.isEmpty()){
@@ -741,7 +741,7 @@ public class TML2Avatar {
ae.securityPattern.state1=as;
}
else if (ae.securityPattern.type.equals("Nonce")){
- block.addAttribute(new AvatarAttribute("nonce_"+ae.securityPattern.name, AvatarType.INTEGER, block, null));
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null));
}
else if (ae.securityPattern.type.equals("Hash")){
AvatarMethod hash = new AvatarMethod("hash", ae);
@@ -774,7 +774,7 @@ public class TML2Avatar {
tran.addAction(ae.securityPattern.name+"_encrypted = concat2("+ae.securityPattern.name+"_mac,"+ae.securityPattern.name+")");
}
- AvatarAttributeState authOrigin = new AvatarAttributeState(ae.securityPattern.name+"1",ae.getReferenceObject(),block.getAvatarAttributeWithName(ae.securityPattern.name), as);
+ AvatarAttributeState authOrigin = new AvatarAttributeState(block.getName()+"."+as.getName(),ae.getReferenceObject(),block.getAvatarAttributeWithName(ae.securityPattern.name), as);
signalAuthOriginMap.put(ae.securityPattern.name, authOrigin);
as.addNext(tran);
elementList.add(as);
@@ -784,9 +784,9 @@ public class TML2Avatar {
block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block, null));
block.addAttribute(new AvatarAttribute(ae.securityPattern.name+"_encrypted", AvatarType.INTEGER, block, null));
if (ae.securityPattern.type.equals("Symmetric Encryption")){
- if (ae.securityPattern.key.isEmpty()){
+ if (ae.securityPattern.key.isEmpty()){
AvatarMethod sdecrypt = new AvatarMethod("sdecrypt", ae);
- block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block,null));
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block,null));
sdecrypt.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name+"_encrypted"));
sdecrypt.addParameter(block.getAvatarAttributeWithName("key_"+ae.securityPattern.name));
if (block.getAvatarAttributeWithName(ae.securityPattern.name+"_encrypted")!=null && block.getAvatarAttributeWithName("key_"+ae.securityPattern.name)!=null){
@@ -808,20 +808,20 @@ public class TML2Avatar {
elementList.add(tran);
as.addNext(tran);
if (!ae.securityPattern.nonce.isEmpty()){
- block.addAttribute(new AvatarAttribute("testnonce_"+ae.securityPattern.nonce, AvatarType.INTEGER, block, null));
- AvatarMethod get2 = new AvatarMethod("get2",ae);
- get2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
- get2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
- get2.addParameter(block.getAvatarAttributeWithName("testnonce_"+ae.securityPattern.nonce));
- if (block.getAvatarAttributeWithName(ae.securityPattern.name)!=null && block.getAvatarAttributeWithName(ae.securityPattern.name)!=null && block.getAvatarAttributeWithName("testnonce_"+ae.securityPattern.nonce)!=null) {
- block.addMethod(get2);
- }
- tran.addAction("get2("+ae.securityPattern.name + ","+ae.securityPattern.name+",testnonce_"+ae.securityPattern.nonce+")");
- AvatarState guardState = new AvatarState(ae.getName()+"_guarded", ae.getReferenceObject());
- tran.addNext(guardState);
- tran=new AvatarTransition(block, "__guard_"+ae.getName(), ae.getReferenceObject());
- guardState.addNext(tran);
- tran.setGuard("testnonce_"+ae.securityPattern.nonce+"== nonce_" + ae.securityPattern.nonce);
+ block.addAttribute(new AvatarAttribute("testnonce_"+ae.securityPattern.nonce, AvatarType.INTEGER, block, null));
+ AvatarMethod get2 = new AvatarMethod("get2",ae);
+ get2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
+ get2.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
+ get2.addParameter(block.getAvatarAttributeWithName("testnonce_"+ae.securityPattern.nonce));
+ if (block.getAvatarAttributeWithName(ae.securityPattern.name)!=null && block.getAvatarAttributeWithName(ae.securityPattern.name)!=null && block.getAvatarAttributeWithName("testnonce_"+ae.securityPattern.nonce)!=null) {
+ block.addMethod(get2);
+ }
+ tran.addAction("get2("+ae.securityPattern.name + ","+ae.securityPattern.name+",testnonce_"+ae.securityPattern.nonce+")");
+ AvatarState guardState = new AvatarState(ae.getName()+"_guarded", ae.getReferenceObject());
+ tran.addNext(guardState);
+ tran=new AvatarTransition(block, "__guard_"+ae.getName(), ae.getReferenceObject());
+ guardState.addNext(tran);
+ tran.setGuard("testnonce_"+ae.securityPattern.nonce+"==" + ae.securityPattern.nonce);
}
AvatarState dummy = new AvatarState(ae.getName()+"_dummy", ae.getReferenceObject());
ae.securityPattern.state2=dummy;
@@ -873,12 +873,13 @@ public class TML2Avatar {
if (block.getAvatarAttributeWithName(ae.securityPattern.name)!=null && block.getAvatarAttributeWithName(ae.securityPattern.name)!=null) {
block.addMethod(get2);
}
+
tran.addAction("get2("+ae.securityPattern.name + ","+ae.securityPattern.name+",testnonce_"+ae.securityPattern.nonce+")");
AvatarState guardState = new AvatarState(ae.getName()+"_guarded", ae.getReferenceObject());
tran.addNext(guardState);
tran=new AvatarTransition(block, "__guard_"+ae.getName(), ae.getReferenceObject());
guardState.addNext(tran);
- tran.setGuard("testnonce_"+ae.securityPattern.nonce+"== nonce_" + ae.securityPattern.nonce);
+ tran.setGuard("testnonce_"+ae.securityPattern.nonce+"==" + ae.securityPattern.nonce);
}
AvatarState dummy = new AvatarState(ae.getName()+"_dummy", ae.getReferenceObject());
tran.addNext(dummy);
@@ -888,7 +889,8 @@ public class TML2Avatar {
elementList.add(tran);
ae.securityPattern.state2=dummy;
if (ae.securityPattern.nonce.isEmpty()){
- AvatarAttributeState authDest = new AvatarAttributeState(ae.securityPattern.name+"2",ae.getReferenceObject(),block.getAvatarAttributeWithName(ae.securityPattern.name), dummy);
+
+ AvatarAttributeState authDest = new AvatarAttributeState(ae.securityPattern.name+"2",ae.getReferenceObject(),block.getAvatarAttributeWithName(ae.securityPattern.name), dummy);
signalAuthDestMap.put(ae.securityPattern.name, authDest);
}
else {
@@ -909,7 +911,9 @@ public class TML2Avatar {
block.addMethod(get2);
tran.addAction("get2("+ae.securityPattern.name+"_encrypted,"+ae.securityPattern.name+","+ae.securityPattern.name+"_mac)");
-
+ if (!ae.securityPattern.nonce.isEmpty()){
+ tran.addAction("get2("+ae.securityPattern.name + ","+ae.securityPattern.name+",testnonce_"+ae.securityPattern.nonce+")");
+ }
AvatarMethod verifymac = new AvatarMethod("verifyMAC", ae);
block.addAttribute(new AvatarAttribute("testnonce_"+ae.securityPattern.name, AvatarType.BOOLEAN, block, null));
verifymac.addParameter(block.getAvatarAttributeWithName(ae.securityPattern.name));
@@ -919,6 +923,7 @@ public class TML2Avatar {
if (block.getAvatarAttributeWithName(ae.securityPattern.name)!=null && block.getAvatarAttributeWithName("key_"+ae.securityPattern.name)!=null){
block.addMethod(verifymac);
+
}
tran.addAction("testnonce_"+ae.securityPattern.name+"=verifyMAC("+ae.securityPattern.name+", key_"+ae.securityPattern.name+","+ae.securityPattern.name+"_mac)");
@@ -928,11 +933,26 @@ public class TML2Avatar {
as.addNext(tran);
AvatarState guardState = new AvatarState(ae.getName()+"_guarded", ae.getReferenceObject());
tran.addNext(guardState);
+
+
tran=new AvatarTransition(block, "__guard_"+ae.getName(), ae.getReferenceObject());
+
elementList.add(guardState);
elementList.add(tran);
guardState.addNext(tran);
+ if (!ae.securityPattern.nonce.isEmpty()){
+ block.addAttribute(new AvatarAttribute("testnonce_"+ae.securityPattern.nonce, AvatarType.INTEGER, block, null));
+ //Add extra state and transition
+ tran.setGuard("testnonce_"+ae.securityPattern.nonce+"==" + ae.securityPattern.nonce);
+ AvatarState guardState2 = new AvatarState(ae.getName()+"_guarded2", ae.getReferenceObject());
+ tran.addNext(guardState2);
+ tran=new AvatarTransition(block, "__guard_"+ae.getName(), ae.getReferenceObject());
+ elementList.add(guardState2);
+ elementList.add(tran);
+
+ guardState2.addNext(tran);
+ }
tran.setGuard("testnonce_"+ae.securityPattern.name);
}
AvatarState dummy = new AvatarState(ae.getName()+"_dummy", ae.getReferenceObject());
@@ -992,8 +1012,8 @@ public class TML2Avatar {
if (ae.securityPattern!=null){
if (ae.securityPattern.type.equals("Nonce")){
- block.addAttribute(new AvatarAttribute("nonce_"+ae.securityPattern.name, AvatarType.INTEGER, block,null));
- as.addValue("nonce_"+ae.securityPattern.name);
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block,null));
+ as.addValue(ae.securityPattern.name);
}
else if (!ae.securityPattern.key.isEmpty()){
as.addValue("encryptedKey_"+ae.securityPattern.key);
@@ -1070,14 +1090,14 @@ public class TML2Avatar {
AvatarAttribute channelData= new AvatarAttribute(getName(ch.getName())+"_chData", AvatarType.INTEGER, block, null);
block.addAttribute(channelData);
}
- AvatarAttributeState authOrigin = new AvatarAttributeState(ch.getName()+"__destination",ae.getReferenceObject(),block.getAvatarAttributeWithName(getName(ch.getName())+"_chData"), signalState);
+ AvatarAttributeState authOrigin = new AvatarAttributeState(block.getName()+signalState.getName(),ae.getReferenceObject(),block.getAvatarAttributeWithName(getName(ch.getName())+"_chData"), signalState);
signalAuthOriginMap.put(ch.getName(), authOrigin);
}
AvatarActionOnSignal as = new AvatarActionOnSignal(ae.getName(), sig, ae.getReferenceObject());
if (ae.securityPattern!=null){
if (ae.securityPattern.type.equals("Nonce")){
- as.addValue("nonce_"+ae.securityPattern.name);
+ as.addValue(ae.securityPattern.name);
}
else if (!ae.securityPattern.key.isEmpty()){
as.addValue("encryptedKey_"+ae.securityPattern.key);
@@ -1586,7 +1606,8 @@ public class TML2Avatar {
//Add authenticity pragmas
for (String s: signalAuthOriginMap.keySet()){
if (signalAuthDestMap.containsKey(s)){
- AvatarPragmaAuthenticity pragma = new AvatarPragmaAuthenticity("#Authenticity "+s, signalAuthOriginMap.get(s).getReferenceObject(), signalAuthOriginMap.get(s), signalAuthDestMap.get(s));
+ AvatarPragmaAuthenticity pragma = new AvatarPragmaAuthenticity("#Authenticity " + signalAuthOriginMap.get(s).getName() + " " + signalAuthDestMap.get(s).getName(), signalAuthOriginMap.get(s).getReferenceObject(), signalAuthOriginMap.get(s), signalAuthDestMap.get(s));
+ //System.out.println("adding pragma " + s);
avspec.addPragma(pragma);
}
}
diff --git a/src/ui/GTURTLEModeling.java b/src/ui/GTURTLEModeling.java
index 751149ff2d..d12f47a9e2 100755
--- a/src/ui/GTURTLEModeling.java
+++ b/src/ui/GTURTLEModeling.java
@@ -2577,7 +2577,7 @@ public class GTURTLEModeling {
}
}
- if (tg.getY() > ypos && tg!=dec){
+ if (tg.getY() > ypos && tg!=dec && tg!=comp){
tg.setCd(tg.getX(), tg.getY()+yShift);
}
@@ -9197,7 +9197,8 @@ public class GTURTLEModeling {
AvatarSMDReceiveSignal smdrs = new AvatarSMDReceiveSignal(x, y, x, x*2, y, y*2, false, null, smp);
tgcomp=smdrs;
smp.addComponent(smdrs, x, y, false, true);
- String name=sig.minString();
+// String name=sig.minString();
+ String name=sig.getName()+"("+((AvatarActionOnSignal)asme).getValues().get(0)+")";
smdrs.setValue(name);
// sig.setName(name);
smdrs.recalculateSize();
@@ -9214,7 +9215,8 @@ public class GTURTLEModeling {
AvatarSMDSendSignal smdss = new AvatarSMDSendSignal(x, y, x, x*2, y, y*2, false, null, smp);
tgcomp=smdss;
smp.addComponent(smdss, x, y, false, true);
- String name=sig.minString();
+ String name=sig.getName()+"("+((AvatarActionOnSignal)asme).getValues().get(0)+")";
+ //String name=sig.minString();
smdss.setValue(name);
smdss.recalculateSize();
SMDMap.put(asme, smdss);
@@ -9516,6 +9518,7 @@ public class GTURTLEModeling {
}
}
else if (p.getName().contains("Authenticity")){
+ t=p.getName();
}
s=s.concat(t+"\n");
// i++;
diff --git a/src/ui/window/JDialogCryptographicConfiguration.java b/src/ui/window/JDialogCryptographicConfiguration.java
index 187b3c3e90..2045bc4c3d 100644
--- a/src/ui/window/JDialogCryptographicConfiguration.java
+++ b/src/ui/window/JDialogCryptographicConfiguration.java
@@ -115,7 +115,7 @@ public class JDialogCryptographicConfiguration extends javax.swing.JDialog imple
setDefaultCloseOperation(JFrame.DISPOSE_ON_CLOSE);
- if (values[1].contains("Encryption") || values[1].isEmpty()){
+ if (values[1].contains("Encryption") || values[1].equals("MAC") || values[1].isEmpty()){
panel1= new EncryptPanel(this);
}
else {
--
GitLab