diff --git a/executablecode/Makefile.src b/executablecode/Makefile.src
index 02289288021f7e37d828948d164b5ef886242577..6dbb11d0823000cde14ba77c6acfb7c4fe652f9c 100755
--- a/executablecode/Makefile.src
+++ b/executablecode/Makefile.src
@@ -1 +1 @@
-SRCS = generated_src/main.c generated_src/SPI_RST_line.c generated_src/HOST_INT_line.c generated_src/HSM_Board.c generated_src/WHIRPOOL.c generated_src/SBB_AES.c generated_src/SBB_CMAC.c generated_src/SBB_SHA_256.c generated_src/SBB_ECC.c generated_src/SBB_PRNG.c generated_src/SBB_Keys.c generated_src/HSM_Mgmt.c generated_src/CCS.c generated_src/SPI_Slave.c generated_src/SharedMessageRAM.c generated_src/GPIO.c generated_src/TC1797_Board.c generated_src/EVITA_ICU.c generated_src/EVITA_DIO.c generated_src/EVITA_SPI.c generated_src/LLD.c generated_src/HSM_ListDriver.c generated_src/HSM_Comm_Driver.c generated_src/HSM_QueueDriver.c generated_src/HSM_Driver.c generated_src/Middleware.c generated_src/TESTCASE_DRVREQS.c generated_src/TESTCASE_INIT.c generated_src/SPI_Connection.c generated_src/ObserverVGoal6.c generated_src/Timer__SCLK.c
\ No newline at end of file
+SRCS = generated_src/main.c generated_src/SecuredSystem.c generated_src/ECU1.c generated_src/ECU2.c
\ No newline at end of file
diff --git a/modeling/proverif_sylvia_0.xml b/modeling/proverif_sylvia_0.xml
index 101ab61b0827f26c2f3035ce0a8b33221263cfc4..d00ca1d6a6bd82e1e2e2651e84fd87c15cc7afbb 100644
--- a/modeling/proverif_sylvia_0.xml
+++ b/modeling/proverif_sylvia_0.xml
@@ -4614,8 +4614,8 @@
<TGConnectingPoint num="0" id="2428" />
<TGConnectingPoint num="1" id="2429" />
<TGConnectingPoint num="2" id="2430" />
-<P1 x="841" y="549" id="2540" />
-<P2 x="841" y="658" id="2549" />
+<P1 x="860" y="529" id="2540" />
+<P2 x="860" y="638" id="2549" />
<Point x="865" y="549" />
<Point x="865" y="658" />
<AutomaticDrawing data="true" />
@@ -4706,29 +4706,27 @@
</COMPONENT>
<COMPONENT type="301" id="2467" >
-<cdparam x="48" y="10" />
-<sizeparam width="313" height="290" minWidth="50" minHeight="20" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
+<cdparam x="23" y="10" />
+<sizeparam width="313" height="275" minWidth="50" minHeight="20" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="1400" />
-<infoparam name="UML Note" value="
-#PrivatePublicKeys ECU1 mvksk mvkpk
+<infoparam name="UML Note" value="#PrivatePublicKeys ECU1 mvksk mvkpk
#InitialSystemKnowledge ECU1.mvksk ECU2.mvksk
-#InitialSessionKnowledge ts0
-#InitialSessionKnowledge ts1
-
+#InitialSessionKnowledge ECU1.ts0 ECU2.ts0
+#InitialSessionKnowledge ECU1.ts1 ECU2.ts1
#SecrecyAssumption ECU1.idk1sk
-#SecrecyAssumtion ECU2.idk2sk
+#SecrecyAssumption ECU2.idk2sk
#SecrecyAssumption ECU1.mvksk
-#SecrecyAssumption ECU2.mvksk
#Constant ECU1.ack ECU2.ack
-#Constant rpk
-#Contant ecu1id
-#Constant ecu2id
-" />
+#Constant ECU1.rpk ECU2.rpk
+#Constant ECU1.ecu1id ECU2.ecu1id
+#Constant ECU2.ecu2id ECU1.ecu2id
+
+#Confidentiality ECU1.mvksk" />
<TGConnectingPoint num="0" id="2459" />
<TGConnectingPoint num="1" id="2460" />
<TGConnectingPoint num="2" id="2461" />
@@ -4738,24 +4736,23 @@
<TGConnectingPoint num="6" id="2465" />
<TGConnectingPoint num="7" id="2466" />
<extraparam>
-<Line value="" />
<Line value="#PrivatePublicKeys ECU1 mvksk mvkpk" />
<Line value="" />
<Line value="#InitialSystemKnowledge ECU1.mvksk ECU2.mvksk" />
<Line value="" />
-<Line value="#InitialSessionKnowledge ts0" />
-<Line value="#InitialSessionKnowledge ts1" />
-<Line value="" />
+<Line value="#InitialSessionKnowledge ECU1.ts0 ECU2.ts0" />
+<Line value="#InitialSessionKnowledge ECU1.ts1 ECU2.ts1" />
<Line value="" />
<Line value="#SecrecyAssumption ECU1.idk1sk" />
-<Line value="#SecrecyAssumtion ECU2.idk2sk" />
+<Line value="#SecrecyAssumption ECU2.idk2sk" />
<Line value="#SecrecyAssumption ECU1.mvksk" />
-<Line value="#SecrecyAssumption ECU2.mvksk" />
<Line value="" />
<Line value="#Constant ECU1.ack ECU2.ack" />
-<Line value="#Constant rpk" />
-<Line value="#Contant ecu1id" />
-<Line value="#Constant ecu2id" />
+<Line value="#Constant ECU1.rpk ECU2.rpk" />
+<Line value="#Constant ECU1.ecu1id ECU2.ecu1id" />
+<Line value="#Constant ECU2.ecu2id ECU1.ecu2id" />
+<Line value="" />
+<Line value="#Confidentiality ECU1.mvksk" />
</extraparam>
</COMPONENT>
@@ -4798,7 +4795,7 @@
</COMPONENT>
<COMPONENT type="5000" id="2560" >
-<cdparam x="50" y="332" />
+<cdparam x="69" y="312" />
<sizeparam width="791" height="435" minWidth="5" minHeight="2" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="10" maxX="1400" minY="10" maxY="1400" />
@@ -4828,7 +4825,6 @@
<TGConnectingPoint num="22" id="2558" />
<TGConnectingPoint num="23" id="2559" />
<extraparam>
-<Attribute access="0" id="ack" value="1" type="8" typeOther="" />
<Signal value="in chin(Message msg)" />
<Signal value="out chout(Message msg)" />
<Signal value="in chinprivate(Message msg)" />
@@ -4837,7 +4833,7 @@
</COMPONENT>
<SUBCOMPONENT type="5000" id="2510" >
<father id="2560" num="0" />
-<cdparam x="127" y="447" />
+<cdparam x="146" y="427" />
<sizeparam width="250" height="200" minWidth="5" minHeight="2" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="0" maxX="541" minY="0" maxY="235" />
@@ -4868,6 +4864,14 @@
<TGConnectingPoint num="23" id="2509" />
<extraparam>
<Attribute access="0" id="ack" value="1" type="8" typeOther="" />
+<Attribute access="0" id="mvksk" value="" type="5" typeOther="Key" />
+<Attribute access="0" id="mvkpk" value="" type="5" typeOther="Key" />
+<Attribute access="0" id="ts0" value="" type="8" typeOther="" />
+<Attribute access="0" id="ts1" value="" type="8" typeOther="" />
+<Attribute access="0" id="idk1sk" value="" type="5" typeOther="Key" />
+<Attribute access="0" id="rpk" value="" type="8" typeOther="" />
+<Attribute access="0" id="ecu1id" value="" type="8" typeOther="" />
+<Attribute access="0" id="ecu2id" value="" type="8" typeOther="" />
<Method value="Message aencrypt(Message msg, Key k)" />
<Method value="Message adecrypt(Message msg, Key k)" />
<Method value="Key pk(Key k)" />
@@ -4890,7 +4894,7 @@
</SUBCOMPONENT>
<SUBCOMPONENT type="5000" id="2535" >
<father id="2560" num="1" />
-<cdparam x="458" y="448" />
+<cdparam x="431" y="427" />
<sizeparam width="250" height="200" minWidth="5" minHeight="2" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
<hidden value="false" />
<cdrectangleparam minX="0" maxX="541" minY="0" maxY="235" />
@@ -4921,6 +4925,12 @@
<TGConnectingPoint num="23" id="2534" />
<extraparam>
<Attribute access="0" id="ack" value="1" type="8" typeOther="" />
+<Attribute access="0" id="ts0" value="" type="8" typeOther="" />
+<Attribute access="0" id="ts1" value="" type="8" typeOther="" />
+<Attribute access="0" id="idk2sk" value="" type="5" typeOther="Key" />
+<Attribute access="0" id="rpk" value="" type="8" typeOther="" />
+<Attribute access="0" id="ecu1id" value="" type="8" typeOther="" />
+<Attribute access="0" id="ecu2id" value="" type="8" typeOther="" />
<Method value="Message aencrypt(Message msg, Key k)" />
<Method value="Message adecrypt(Message msg, Key k)" />
<Method value="Key pk(Key k)" />
diff --git a/src/avatartranslator/toproverif/AVATAR2ProVerif.java b/src/avatartranslator/toproverif/AVATAR2ProVerif.java
index 85af962d7a5e7543db8057f34a02ea751c22e37d..6e220e9bb68962e169966b45287bf7e8610adc39 100755
--- a/src/avatartranslator/toproverif/AVATAR2ProVerif.java
+++ b/src/avatartranslator/toproverif/AVATAR2ProVerif.java
@@ -114,27 +114,13 @@ public class AVATAR2ProVerif {
makeHeader(_stateReachability);
- makeBlocks();
-
makeStartingProcess();
- //TraceManager.addDev("-> Spec:" + avspec.toString());
-
-
- // Deal with blocks
- //translateBlocks();
-
- //translationRelations();
-
- //makeGlobal();
-
+ makeBlocks();
- // Generate system
- //makeGlobal(effectiveNb);
- //makeParallel(nb);
+ //TraceManager.addDev("-> Spec:" + avspec.toString());
- //makeSystem();
/*if (_optimize) {
spec.optimize();
@@ -154,26 +140,32 @@ public class AVATAR2ProVerif {
String tmpH = declarations.get(tmp);
if (tmpH == null) {
declarations.put(tmp, tmp);
- tmp = "new " + tmp + ".\n";
+ tmp = "new " + tmp + ";\n";
return tmp;
}
return "";
}
- private String addDeclarationsFromList(int startIndex, String[] list, String result) {
+ private void addDeclarationsFromList(int startIndex, String[] list, String result) {
String tmp, blockName, paramName;
String tmp1;
+ int index;
+
+ TraceManager.addDev("Add declaration list length=" + list.length);
for(int i=startIndex; i<list.length; i++) {
+
tmp = list[i];
+ TraceManager.addDev("tmp=" + tmp);
index = tmp.indexOf('.');
if (index != -1) {
blockName = tmp.substring(0, index).trim();
paramName = tmp.substring(index+1, tmp.length());
tmp1 = makeAttrName(blockName, paramName);
- if (tmp1 == null) {
+ if (tmp1 != null) {
declarations.put(tmp1, result);
+ TraceManager.addDev("Adding declaration: " + tmp1 + " result=" + result);
}
}
}
@@ -204,23 +196,62 @@ public class AVATAR2ProVerif {
}
}*/
+
+ spec.addToGlobalSpecification("\n(* Data *)\n");
+ LinkedList<AvatarBlock> blocks = avspec.getListOfBlocks();
+ String[] list;
+ String pragma;
+
+
+ /* Data */
+ for(AvatarBlock block: blocks) {
+ for(AvatarAttribute attribute: block.getAttributes()) {
+ pragma = hasConstantPragmaStartingWithAttribute(block.getName(), attribute.getName());
+ if (pragma != null) {
+ spec.addToGlobalSpecification("data " + makeAttrName(block.getName(), attribute.getName()) + "/0.\n");
+ declarations.put(makeAttrName(block.getName(), attribute.getName()), makeAttrName(block.getName(), attribute.getName()));
+ list = getListOfBlockParams(pragma);
+ addDeclarationsFromList(1, list, makeAttrName(block.getName(), attribute.getName()));
+ }
+ }
+ }
+
+
+ spec.addToGlobalSpecification("\n(* Secrecy Assumptions *)\n");
+ /* Secrecy Assumptions */
+ int index;
+ String tmp, blockName, paramName, tmp1;
+ for(String pr: avspec.getPragmas()) {
+ if (isSecrecyAssumptionPragma(pr)) {
+ list = getListOfBlockParams(pr);
+ for(int i=0; i<list.length; i++) {
+ tmp = list[i];
+ index = tmp.indexOf('.');
+ if (index != -1) {
+ blockName = tmp.substring(0, index).trim();
+ paramName = tmp.substring(index+1, tmp.length());
+ tmp1 = makeAttrName(blockName, paramName);
+ if (tmp1 != null) {
+ spec.addToGlobalSpecification("not " + tmp1 +".\n");
+ }
+ }
+ }
+ }
+ }
+
/* Queries */
/* Parse all attributes starting with "secret" and declare them as non accesible to attacker" */
spec.addToGlobalSpecification("\n(* Queries *)\n");
- LinkedList<AvatarBlock> blocks = avspec.getListOfBlocks();
for(AvatarBlock block: blocks) {
for(AvatarAttribute attribute: block.getAttributes()) {
// Attribute is preinitialized if it is in a secret pragma
//TraceManager.addDev("Testing secret of " + block.getName() + "." + attribute.getName() + " ?");
if (hasSecretPragmaWithAttribute(block.getName(), attribute.getName())) {
//TraceManager.addDev("Secret!");
- //spec.addToGlobalSpecification("private free " + attribute.getName() + ".\n");
+ spec.addToGlobalSpecification("private free " + makeAttrName(block.getName(), attribute.getName()) + ".\n");
+ declarations.put(makeAttrName(block.getName(), attribute.getName()), makeAttrName(block.getName(), attribute.getName()));
spec.addToGlobalSpecification("query attacker:" + makeAttrName(block.getName(), attribute.getName()) + ".\n\n");
}
-
- if (hasConstantPragmaStartingWithAttribute(block.getName(), attribute.getName())) {
- spec.addToGlobalSpecification("data " + makeAttrName(block.getName(), attribute.getName()) + "/0.\n\n");
- }
}
// Queries for states
if (_stateReachability) {
@@ -231,6 +262,7 @@ public class AVATAR2ProVerif {
}
}
}
+
/* Autenticity */
makeAuthenticityPragmas();
@@ -512,20 +544,20 @@ public class AVATAR2ProVerif {
return false;
}
- public boolean hasConstantPragmaStartingWithAttribute(String _blockName, String attributeName) {
+ public String hasConstantPragmaStartingWithAttribute(String _blockName, String attributeName) {
LinkedList<String> pragmas = avspec.getPragmas();
String tmp;
String tmps [];
int index;
for(String pragma: pragmas) {
- if (isSecretPragma(pragma)) {
- tmp = pragma.substring(7, pragma.length()).trim();
+ if (isConstantPragma(pragma)) {
+ tmp = pragma.substring(8, pragma.length()).trim();
- //TraceManager.addDev("Testing prama: " + tmp);
+ TraceManager.addDev("Testing CONSTANT pragma: " + tmp);
if (tmp.length() == 0) {
- return false;
+ return null;
}
tmps = tmp.split(" ");
@@ -536,7 +568,7 @@ public class AVATAR2ProVerif {
try {
if (tmp.substring(0, index).compareTo(_blockName) == 0) {
if (tmp.substring(index+1, tmp.length()).compareTo(attributeName) == 0) {
- return true;
+ return pragma;
}
}
} catch (Exception e) {
@@ -547,7 +579,7 @@ public class AVATAR2ProVerif {
}
- return false;
+ return null;
}
public boolean hasSecretPragmaWithAttribute(String attributeName) {
@@ -683,6 +715,18 @@ public class AVATAR2ProVerif {
return _pragma.startsWith("InitialSystemKnowledge ");
}
+ public boolean isInitialSessionKnowledgePragma(String _pragma) {
+ return _pragma.startsWith("InitialSessionKnowledge ");
+ }
+
+ public boolean isConstantPragma(String _pragma) {
+ return _pragma.startsWith("Constant ");
+ }
+
+ public boolean isSecrecyAssumptionPragma(String _pragma) {
+ return _pragma.startsWith("SecrecyAssumption ");
+ }
+
public boolean isPrivatePublicKeyPragma(String _pragma) {
return _pragma.startsWith("PrivatePublicKeys ");
}
@@ -694,6 +738,12 @@ public class AVATAR2ProVerif {
s = s.substring(7, s.length()).trim();
} else if (isInitialSystemKnowledgePragma(s)) {
s = s.substring(23, s.length()).trim();
+ } else if (isInitialSessionKnowledgePragma(s)) {
+ s = s.substring(24, s.length()).trim();
+ } else if (isConstantPragma(s)) {
+ s = s.substring(8, s.length()).trim();
+ } else if (isSecrecyAssumptionPragma(s)) {
+ s = s.substring(17, s.length()).trim();
} else {
return null;
}
@@ -711,7 +761,7 @@ public class AVATAR2ProVerif {
p.processName = "starting__";
LinkedList<AvatarBlock> blocks = avspec.getListOfBlocks();
- LinkedList<String> createdVariables = new LinkedList<String>();
+ //LinkedList<String> createdVariables = new LinkedList<String>();
String[] list;
String blockName, paramName;
@@ -771,16 +821,33 @@ public class AVATAR2ProVerif {
index = tmp2.indexOf(" ");
if (index != -1) {
privK = tmp2.substring(0, index).trim();
- pubK = tmp2.substring(index+1, tmp2.length());
+ pubK = tmp2.substring(index+1, tmp2.length()).trim();
action += makeActionFromBlockParam(blockName, privK);
action += "let " + makeAttrName(blockName, pubK) + " = pk(" + makeAttrName(blockName, privK) + ") in \n";
action += "out(ch, " + makeAttrName(blockName, pubK) + ");\n";
+ TraceManager.addDev("Putting :" + makeAttrName(blockName, pubK + " -> " + makeAttrName(blockName, pubK)));
declarations.put(makeAttrName(blockName, pubK), makeAttrName(blockName, pubK));
}
}
}
+ } else if (isSecrecyAssumptionPragma(pragma)) {
+ // Identify each blockName / paramName
+ list = getListOfBlockParams(pragma);
+
+
+ // Declare only the first one of the list
+ if (list.length > 0) {
+ tmp = list[0];
+ index = tmp.indexOf('.');
+ if (index != -1) {
+ blockName = tmp.substring(0, index).trim();
+ paramName = tmp.substring(index+1, tmp.length());
+
+ action += makeActionFromBlockParam(blockName, paramName);
+ }
+ }
}
}
@@ -789,9 +856,23 @@ public class AVATAR2ProVerif {
// Must add Session Knowledge
for(String pragma: avspec.getPragmas()) {
TraceManager.addDev("Working on pragma: " + pragma);
- /*if (isInitialSessionKnowledgePragma(pragma)) {
+ if (isInitialSessionKnowledgePragma(pragma)) {
+ list = getListOfBlockParams(pragma);
- }*/
+
+ // Declare only the first one of the list
+ if (list.length > 0) {
+ tmp = list[0];
+ index = tmp.indexOf('.');
+ if (index != -1) {
+ blockName = tmp.substring(0, index).trim();
+ paramName = tmp.substring(index+1, tmp.length());
+
+ action += makeActionFromBlockParam(blockName, paramName);
+ addDeclarationsFromList(1, list, makeAttrName(blockName, paramName));
+ }
+ }
+ }
}
index = 0;
for(AvatarBlock block: blocks) {
@@ -815,6 +896,8 @@ public class AVATAR2ProVerif {
}
public void makeBlock(AvatarBlock ab) {
+ String dec;
+
LinkedList<ProVerifProcess> tmpprocesses = new LinkedList<ProVerifProcess>();
LinkedList<AvatarState> states = new LinkedList<AvatarState>();
@@ -824,12 +907,22 @@ public class AVATAR2ProVerif {
for(AvatarAttribute aa: ab.getAttributes()) {
//TraceManager.addDev("Testing: " + ab.getName() + "." + aa.getName());
- if ((!hasInitialSystemKnowledgePragmaWithAttribute(ab.getName(), aa.getName())) && (!(hasSecretPragmaWithAttribute(ab.getName(), aa.getName())))) {
+ /*if ((!hasInitialSystemKnowledgePragmaWithAttribute(ab.getName(), aa.getName())) && (!(hasSecretPragmaWithAttribute(ab.getName(), aa.getName())))) {
if (!isPublicPrivateKeyPragma(ab.getName(), aa.getName())) {
TraceManager.addDev(" Adding: " + aa.getName());
addLine(p, "new " + aa.getName());
}
+ }*/
+ TraceManager.addDev("Getting:" + makeAttrName(ab.getName(), aa.getName()));
+ dec = declarations.get(makeAttrName(ab.getName(), aa.getName()));
+ if (dec == null) {
+ addLine(p, "new " + aa.getName());
+ } else {
+ if (dec.compareTo(aa.getName()) != 0) {
+ addLineNoEnd(p, "let " + aa.getName() + " = " + dec + " in");
+ }
}
+
}
AvatarStateMachine asm = ab.getStateMachine();
diff --git a/src/ui/AvatarDesignPanelTranslator.java b/src/ui/AvatarDesignPanelTranslator.java
index d2dbf5ab0acc0c553503c2129557df021793f282..2211b0f03a5d590d676d8e84dc93c4eb62d6885c 100644
--- a/src/ui/AvatarDesignPanelTranslator.java
+++ b/src/ui/AvatarDesignPanelTranslator.java
@@ -343,7 +343,7 @@ public class AvatarDesignPanelTranslator {
} else {
- // Other: confidentiality, initial system knowledge, initial session knowledge, contant
+ // Other: confidentiality, initial system knowledge, initial session knowledge, constant
paramName = tmp.substring(index+1, tmp.length());
for(Object oo: block.getAttributeList()) {
ta = (TAttribute)oo;