diff --git a/build.txt b/build.txt index 61dc6deb99bad5146df4c21c2ce4624a034d2549..4394f27e47f10dde3adf0530067ad52d2fbf6fd6 100644 --- a/build.txt +++ b/build.txt @@ -1 +1 @@ -14753 \ No newline at end of file +14758 \ No newline at end of file diff --git a/modeling/SysMLSec/AliceAndBob.xml b/modeling/SysMLSec/AliceAndBob.xml index 99445900f4ef0453dda21e9397315a41678d66da..b460e86ce751f3dcd123d8effe788198066c93ad 100644 --- a/modeling/SysMLSec/AliceAndBob.xml +++ b/modeling/SysMLSec/AliceAndBob.xml @@ -177,13 +177,13 @@ <Signal value="out chout(Message msg)" attached="true" /> </extraparam> </COMPONENT> -<SUBCOMPONENT type="5000" id="82" index="7" uid="32384080-e86a-41de-b441-4f6ae88f1cbe" > +<SUBCOMPONENT type="5000" id="82" index="7" uid="a1c44cc9-9334-4d03-8988-e402248c1447" > <father id="164" num="0" /> -<cdparam x="36" y="233" /> -<sizeparam width="215" height="126" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" /> +<cdparam x="263" y="233" /> +<sizeparam width="139" height="126" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" /> <hidden value="false" /> -<cdrectangleparam minX="0" maxX="223" minY="0" maxY="93" /> -<infoparam name="Block0" value="Alice" /> +<cdrectangleparam minX="0" maxX="299" minY="0" maxY="93" /> +<infoparam name="Block0" value="Bob" /> <new d="false" /> <TGConnectingPoint num="0" id="42" /> <TGConnectingPoint num="1" id="43" /> @@ -228,10 +228,10 @@ <extraparam> <blockType data="cryptoblock" color="-4072719" /> <CryptoBlock value="true" /> -<Attribute access="0" var="0" id="secretData" value="" type="8" typeOther="" /> <Attribute access="0" var="0" id="m" value="" type="5" typeOther="Message" /> -<Attribute access="0" var="0" id="m1" value="" type="5" typeOther="Message" /> +<Attribute access="0" var="0" id="m2" value="" type="5" typeOther="Message" /> <Attribute access="0" var="0" id="sk" value="" type="5" typeOther="Key" /> +<Attribute access="0" var="0" id="receivedData" value="" type="8" typeOther="" /> <Method value="Message encrypt(Message msg, Key k)" /> <Method value="Message decrypt(Message msg, Key k)" /> <Method value="Message sencrypt(Message msg, Key k)" /> @@ -258,13 +258,13 @@ <Method value="Key getKey(Message msg)" /> </extraparam> </SUBCOMPONENT> -<SUBCOMPONENT type="5000" id="123" index="8" uid="a1c44cc9-9334-4d03-8988-e402248c1447" > +<SUBCOMPONENT type="5000" id="123" index="8" uid="32384080-e86a-41de-b441-4f6ae88f1cbe" > <father id="164" num="1" /> -<cdparam x="263" y="233" /> -<sizeparam width="139" height="126" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" /> +<cdparam x="36" y="233" /> +<sizeparam width="215" height="126" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" /> <hidden value="false" /> -<cdrectangleparam minX="0" maxX="299" minY="0" maxY="93" /> -<infoparam name="Block0" value="Bob" /> +<cdrectangleparam minX="0" maxX="223" minY="0" maxY="93" /> +<infoparam name="Block0" value="Alice" /> <new d="false" /> <TGConnectingPoint num="0" id="83" /> <TGConnectingPoint num="1" id="84" /> @@ -309,10 +309,10 @@ <extraparam> <blockType data="cryptoblock" color="-4072719" /> <CryptoBlock value="true" /> +<Attribute access="0" var="0" id="secretData" value="" type="8" typeOther="" /> <Attribute access="0" var="0" id="m" value="" type="5" typeOther="Message" /> -<Attribute access="0" var="0" id="m2" value="" type="5" typeOther="Message" /> +<Attribute access="0" var="0" id="m1" value="" type="5" typeOther="Message" /> <Attribute access="0" var="0" id="sk" value="" type="5" typeOther="Key" /> -<Attribute access="0" var="0" id="receivedData" value="" type="8" typeOther="" /> <Method value="Message encrypt(Message msg, Key k)" /> <Method value="Message decrypt(Message msg, Key k)" /> <Method value="Message sencrypt(Message msg, Key k)" /> @@ -1559,13 +1559,13 @@ <Signal value="out chout(Message msg)" attached="true" /> </extraparam> </COMPONENT> -<SUBCOMPONENT type="5000" id="857" index="7" uid="cc150a1e-1348-4fa4-98a9-3a612b6184cc" > +<SUBCOMPONENT type="5000" id="857" index="7" uid="e802e723-57b4-4734-af20-cddadacc10e6" > <father id="939" num="0" /> -<cdparam x="263" y="233" /> -<sizeparam width="139" height="126" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" /> +<cdparam x="36" y="233" /> +<sizeparam width="215" height="126" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" /> <hidden value="false" /> -<cdrectangleparam minX="0" maxX="299" minY="0" maxY="93" /> -<infoparam name="Block0" value="Bob" /> +<cdrectangleparam minX="0" maxX="223" minY="0" maxY="93" /> +<infoparam name="Block0" value="Alice" /> <new d="false" /> <TGConnectingPoint num="0" id="817" /> <TGConnectingPoint num="1" id="818" /> @@ -1610,13 +1610,13 @@ <extraparam> <blockType data="cryptoblock" color="-4072719" /> <CryptoBlock value="true" /> +<Attribute access="0" var="0" id="secretData" value="" type="8" typeOther="" /> <Attribute access="0" var="0" id="m" value="" type="5" typeOther="Message" /> -<Attribute access="0" var="0" id="m2" value="" type="5" typeOther="Message" /> +<Attribute access="0" var="0" id="m1" value="" type="5" typeOther="Message" /> <Attribute access="0" var="0" id="sk" value="" type="5" typeOther="Key" /> -<Attribute access="0" var="0" id="receivedData" value="" type="8" typeOther="" /> -<Attribute access="0" var="0" id="privK" value="" type="5" typeOther="Key" /> <Attribute access="0" var="0" id="pubK" value="" type="5" typeOther="Key" /> -<Attribute access="0" var="0" id="alicePubK" value="" type="5" typeOther="Key" /> +<Attribute access="0" var="0" id="privK" value="" type="5" typeOther="Key" /> +<Attribute access="0" var="0" id="bobPubK" value="" type="5" typeOther="Key" /> <Method value="Message encrypt(Message msg, Key k)" /> <Method value="Message decrypt(Message msg, Key k)" /> <Method value="Message sencrypt(Message msg, Key k)" /> @@ -1643,13 +1643,13 @@ <Method value="Key getKey(Message msg)" /> </extraparam> </SUBCOMPONENT> -<SUBCOMPONENT type="5000" id="898" index="8" uid="e802e723-57b4-4734-af20-cddadacc10e6" > +<SUBCOMPONENT type="5000" id="898" index="8" uid="cc150a1e-1348-4fa4-98a9-3a612b6184cc" > <father id="939" num="1" /> -<cdparam x="36" y="233" /> -<sizeparam width="215" height="126" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" /> +<cdparam x="263" y="233" /> +<sizeparam width="139" height="126" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" /> <hidden value="false" /> -<cdrectangleparam minX="0" maxX="223" minY="0" maxY="93" /> -<infoparam name="Block0" value="Alice" /> +<cdrectangleparam minX="0" maxX="299" minY="0" maxY="93" /> +<infoparam name="Block0" value="Bob" /> <new d="false" /> <TGConnectingPoint num="0" id="858" /> <TGConnectingPoint num="1" id="859" /> @@ -1694,13 +1694,13 @@ <extraparam> <blockType data="cryptoblock" color="-4072719" /> <CryptoBlock value="true" /> -<Attribute access="0" var="0" id="secretData" value="" type="8" typeOther="" /> <Attribute access="0" var="0" id="m" value="" type="5" typeOther="Message" /> -<Attribute access="0" var="0" id="m1" value="" type="5" typeOther="Message" /> +<Attribute access="0" var="0" id="m2" value="" type="5" typeOther="Message" /> <Attribute access="0" var="0" id="sk" value="" type="5" typeOther="Key" /> -<Attribute access="0" var="0" id="pubK" value="" type="5" typeOther="Key" /> +<Attribute access="0" var="0" id="receivedData" value="" type="8" typeOther="" /> <Attribute access="0" var="0" id="privK" value="" type="5" typeOther="Key" /> -<Attribute access="0" var="0" id="bobPubK" value="" type="5" typeOther="Key" /> +<Attribute access="0" var="0" id="pubK" value="" type="5" typeOther="Key" /> +<Attribute access="0" var="0" id="alicePubK" value="" type="5" typeOther="Key" /> <Method value="Message encrypt(Message msg, Key k)" /> <Method value="Message decrypt(Message msg, Key k)" /> <Method value="Message sencrypt(Message msg, Key k)" /> @@ -3661,13 +3661,13 @@ <Signal value="out chout(Message msg)" attached="true" /> </extraparam> </COMPONENT> -<SUBCOMPONENT type="5000" id="2024" index="7" uid="7a040a26-feb9-4e9a-a609-908679df2a0b" > +<SUBCOMPONENT type="5000" id="2024" index="7" uid="f24348ab-6d4a-40e6-a942-342d6222b23f" > <father id="2147" num="0" /> -<cdparam x="115" y="249" /> -<sizeparam width="261" height="83" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" /> +<cdparam x="263" y="108" /> +<sizeparam width="139" height="126" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" /> <hidden value="false" /> -<cdrectangleparam minX="0" maxX="177" minY="0" maxY="261" /> -<infoparam name="Block0" value="CA" /> +<cdrectangleparam minX="0" maxX="299" minY="0" maxY="218" /> +<infoparam name="Block0" value="Bob" /> <new d="false" /> <TGConnectingPoint num="0" id="1984" /> <TGConnectingPoint num="1" id="1985" /> @@ -3712,30 +3712,22 @@ <extraparam> <blockType data="cryptoblock" color="-4072719" /> <CryptoBlock value="true" /> +<Attribute access="0" var="0" id="m" value="" type="5" typeOther="Message" /> +<Attribute access="0" var="0" id="m2" value="" type="5" typeOther="Message" /> +<Attribute access="0" var="0" id="sk" value="" type="5" typeOther="Key" /> +<Attribute access="0" var="0" id="receivedData" value="" type="8" typeOther="" /> <Attribute access="0" var="0" id="privK" value="" type="5" typeOther="Key" /> <Attribute access="0" var="0" id="pubK" value="" type="5" typeOther="Key" /> <Attribute access="0" var="0" id="alicePubK" value="" type="5" typeOther="Key" /> -<Attribute access="0" var="0" id="bobPubK" value="" type="5" typeOther="Key" /> +<Attribute access="0" var="0" id="CAPubK" value="" type="5" typeOther="Key" /> <Attribute access="0" var="0" id="aliceID" value="" type="8" typeOther="" /> -<Attribute access="0" var="0" id="bobID" value="" type="8" typeOther="" /> -<Attribute access="0" var="0" id="m" value="" type="5" typeOther="Message" /> -<Attribute access="0" var="0" id="newK" value="" type="5" typeOther="Key" /> -<Attribute access="0" var="0" id="newCert" value="" type="5" typeOther="Message" /> <Attribute access="0" var="0" id="m1" value="" type="5" typeOther="Message" /> -<Attribute access="0" var="0" id="m2" value="" type="5" typeOther="Message" /> -<Attribute access="0" var="0" id="newID" 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)" /> -<Method value="Message sign(Message msg, Key k)" /> -<Method value="bool verifySign(Message msg1, Message sig, Key k)" /> -<Method value="Message cert(Key k, Message msg)" /> -<Method value="bool verifyCert(Message cert, Key k)" /> -<Method value="Key getpk(Message cert)" /> +<Attribute access="0" var="0" id="sig" value="" type="5" typeOther="Message" /> +<Attribute access="0" var="0" id="certOK" value="" type="4" typeOther="" /> +<Method value="Message encrypt(Message msg, Key k)" /> +<Method value="Message decrypt(Message msg, Key k)" /> <Method value="Message sencrypt(Message msg, Key k)" /> <Method value="Message sdecrypt(Message msg, Key k)" /> -<Method value="Key DH(Key pubK, Key privK)" /> -<Method value="Message hash(Message msg)" /> <Method value="Message MAC(Message msg, Key k)" /> <Method value="bool verifyMAC(Message msg, Key k, Message macmsg)" /> <Method value="Message concat2(Message msg1, Message msg2)" /> @@ -3744,6 +3736,16 @@ <Method value="get2(Message msg, Message msg1, Message msg2)" /> <Method value="get3(Message msg, Message msg1, Message msg2, Message msg3)" /> <Method value="get4(Message msg, Message msg1, Message msg2, Message msg3, Message msg4)" /> +<Method value="Message aencrypt(Message msg, Key k)" /> +<Method value="Message adecrypt(Message msg, Key k)" /> +<Method value="Key pk(Key k)" /> +<Method value="Message sign(Message msg, Key k)" /> +<Method value="bool verifySign(Message msg1, Message sig, Key k)" /> +<Method value="Message cert(Key k, Message msg)" /> +<Method value="bool verifyCert(Message cert, Key k)" /> +<Method value="Key getpk(Message cert)" /> +<Method value="Key DH(Key pubK, Key privK)" /> +<Method value="Message hash(Message msg)" /> <Method value="Message host(Key k)" /> <Method value="Key getKey(Message msg)" /> </extraparam> @@ -3837,13 +3839,13 @@ <Method value="Key getKey(Message msg)" /> </extraparam> </SUBCOMPONENT> -<SUBCOMPONENT type="5000" id="2106" index="9" uid="f24348ab-6d4a-40e6-a942-342d6222b23f" > +<SUBCOMPONENT type="5000" id="2106" index="9" uid="7a040a26-feb9-4e9a-a609-908679df2a0b" > <father id="2147" num="2" /> -<cdparam x="263" y="108" /> -<sizeparam width="139" height="126" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" /> +<cdparam x="115" y="249" /> +<sizeparam width="261" height="83" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" /> <hidden value="false" /> -<cdrectangleparam minX="0" maxX="299" minY="0" maxY="218" /> -<infoparam name="Block0" value="Bob" /> +<cdrectangleparam minX="0" maxX="177" minY="0" maxY="261" /> +<infoparam name="Block0" value="CA" /> <new d="false" /> <TGConnectingPoint num="0" id="2066" /> <TGConnectingPoint num="1" id="2067" /> @@ -3888,30 +3890,18 @@ <extraparam> <blockType data="cryptoblock" color="-4072719" /> <CryptoBlock value="true" /> -<Attribute access="0" var="0" id="m" value="" type="5" typeOther="Message" /> -<Attribute access="0" var="0" id="m2" value="" type="5" typeOther="Message" /> -<Attribute access="0" var="0" id="sk" value="" type="5" typeOther="Key" /> -<Attribute access="0" var="0" id="receivedData" value="" type="8" typeOther="" /> <Attribute access="0" var="0" id="privK" value="" type="5" typeOther="Key" /> <Attribute access="0" var="0" id="pubK" value="" type="5" typeOther="Key" /> <Attribute access="0" var="0" id="alicePubK" value="" type="5" typeOther="Key" /> -<Attribute access="0" var="0" id="CAPubK" value="" type="5" typeOther="Key" /> +<Attribute access="0" var="0" id="bobPubK" value="" type="5" typeOther="Key" /> <Attribute access="0" var="0" id="aliceID" value="" type="8" typeOther="" /> +<Attribute access="0" var="0" id="bobID" value="" type="8" typeOther="" /> +<Attribute access="0" var="0" id="m" value="" type="5" typeOther="Message" /> +<Attribute access="0" var="0" id="newK" value="" type="5" typeOther="Key" /> +<Attribute access="0" var="0" id="newCert" value="" type="5" typeOther="Message" /> <Attribute access="0" var="0" id="m1" value="" type="5" typeOther="Message" /> -<Attribute access="0" var="0" id="sig" value="" type="5" typeOther="Message" /> -<Attribute access="0" var="0" id="certOK" value="" type="4" typeOther="" /> -<Method value="Message encrypt(Message msg, Key k)" /> -<Method value="Message decrypt(Message msg, Key k)" /> -<Method value="Message sencrypt(Message msg, Key k)" /> -<Method value="Message sdecrypt(Message msg, Key k)" /> -<Method value="Message MAC(Message msg, Key k)" /> -<Method value="bool verifyMAC(Message msg, Key k, Message macmsg)" /> -<Method value="Message concat2(Message msg1, Message msg2)" /> -<Method value="Message concat3(Message msg1, Message msg2, Message msg3)" /> -<Method value="Message concat4(Message msg1, Message msg2, Message msg3, Message msg4)" /> -<Method value="get2(Message msg, Message msg1, Message msg2)" /> -<Method value="get3(Message msg, Message msg1, Message msg2, Message msg3)" /> -<Method value="get4(Message msg, Message msg1, Message msg2, Message msg3, Message msg4)" /> +<Attribute access="0" var="0" id="m2" value="" type="5" typeOther="Message" /> +<Attribute access="0" var="0" id="newID" 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)" /> @@ -3920,8 +3910,18 @@ <Method value="Message cert(Key k, Message msg)" /> <Method value="bool verifyCert(Message cert, Key k)" /> <Method value="Key getpk(Message cert)" /> +<Method value="Message sencrypt(Message msg, Key k)" /> +<Method value="Message sdecrypt(Message msg, Key k)" /> <Method value="Key DH(Key pubK, Key privK)" /> <Method value="Message hash(Message msg)" /> +<Method value="Message MAC(Message msg, Key k)" /> +<Method value="bool verifyMAC(Message msg, Key k, Message macmsg)" /> +<Method value="Message concat2(Message msg1, Message msg2)" /> +<Method value="Message concat3(Message msg1, Message msg2, Message msg3)" /> +<Method value="Message concat4(Message msg1, Message msg2, Message msg3, Message msg4)" /> +<Method value="get2(Message msg, Message msg1, Message msg2)" /> +<Method value="get3(Message msg, Message msg1, Message msg2, Message msg3)" /> +<Method value="get4(Message msg, Message msg1, Message msg2, Message msg3, Message msg4)" /> <Method value="Message host(Key k)" /> <Method value="Key getKey(Message msg)" /> </extraparam> @@ -6736,13 +6736,13 @@ <Signal value="out chout(Message msg)" attached="true" /> </extraparam> </COMPONENT> -<SUBCOMPONENT type="5000" id="3642" index="7" uid="58e32c17-1811-4588-ab32-863569a17a48" > +<SUBCOMPONENT type="5000" id="3642" index="7" uid="7bb99390-2a74-452a-8601-e344bd028850" > <father id="3724" num="0" /> -<cdparam x="36" y="233" /> -<sizeparam width="215" height="126" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" /> +<cdparam x="263" y="233" /> +<sizeparam width="139" height="126" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" /> <hidden value="false" /> -<cdrectangleparam minX="0" maxX="223" minY="0" maxY="93" /> -<infoparam name="Block0" value="Alice" /> +<cdrectangleparam minX="0" maxX="299" minY="0" maxY="93" /> +<infoparam name="Block0" value="Bob" /> <new d="false" /> <TGConnectingPoint num="0" id="3602" /> <TGConnectingPoint num="1" id="3603" /> @@ -6787,8 +6787,8 @@ <extraparam> <blockType data="cryptoblock" color="-4072719" /> <CryptoBlock value="true" /> -<Attribute access="0" var="0" id="secretData" value="" type="8" typeOther="" /> <Attribute access="0" var="0" id="m" value="" type="5" typeOther="Message" /> +<Attribute access="0" var="0" id="receivedData" value="" type="8" typeOther="" /> <Method value="Message encrypt(Message msg, Key k)" /> <Method value="Message decrypt(Message msg, Key k)" /> <Method value="Message sencrypt(Message msg, Key k)" /> @@ -6815,13 +6815,13 @@ <Method value="Key getKey(Message msg)" /> </extraparam> </SUBCOMPONENT> -<SUBCOMPONENT type="5000" id="3683" index="8" uid="7bb99390-2a74-452a-8601-e344bd028850" > +<SUBCOMPONENT type="5000" id="3683" index="8" uid="58e32c17-1811-4588-ab32-863569a17a48" > <father id="3724" num="1" /> -<cdparam x="263" y="233" /> -<sizeparam width="139" height="126" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" /> +<cdparam x="36" y="233" /> +<sizeparam width="215" height="126" minWidth="5" minHeight="2" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" /> <hidden value="false" /> -<cdrectangleparam minX="0" maxX="299" minY="0" maxY="93" /> -<infoparam name="Block0" value="Bob" /> +<cdrectangleparam minX="0" maxX="223" minY="0" maxY="93" /> +<infoparam name="Block0" value="Alice" /> <new d="false" /> <TGConnectingPoint num="0" id="3643" /> <TGConnectingPoint num="1" id="3644" /> @@ -6866,8 +6866,8 @@ <extraparam> <blockType data="cryptoblock" color="-4072719" /> <CryptoBlock value="true" /> +<Attribute access="0" var="0" id="secretData" value="" type="8" typeOther="" /> <Attribute access="0" var="0" id="m" value="" type="5" typeOther="Message" /> -<Attribute access="0" var="0" id="receivedData" value="" type="8" typeOther="" /> <Method value="Message encrypt(Message msg, Key k)" /> <Method value="Message decrypt(Message msg, Key k)" /> <Method value="Message sencrypt(Message msg, Key k)" /> diff --git a/src/main/java/avatartranslator/toproverif/AVATAR2ProVerif.java b/src/main/java/avatartranslator/toproverif/AVATAR2ProVerif.java index 9ce51e4947c1d86bcaf9eead69497bd5705eb06b..bf910bbedafbfee390b75e7b0c8400817352a8b1 100755 --- a/src/main/java/avatartranslator/toproverif/AVATAR2ProVerif.java +++ b/src/main/java/avatartranslator/toproverif/AVATAR2ProVerif.java @@ -117,6 +117,9 @@ public class AVATAR2ProVerif implements AvatarTranslator { private LinkedList<CheckingError> warnings; public AVATAR2ProVerif(AvatarSpecification _avspec) { + + TraceManager.addDev("BEFORE Translating spec:\n" + _avspec.toString() + "\n\n"); + this.avspec = _avspec; this.spec = null; } @@ -135,9 +138,11 @@ public class AVATAR2ProVerif implements AvatarTranslator { } protected static String translateTerm(AvatarTerm term, LinkedHashMap<AvatarAttribute, Integer> attributeCmp) { + + if (term instanceof AvatarAttribute) { AvatarAttribute attr = (AvatarAttribute) term; - + //TraceManager.addDev("Attribute:" + attr.toString()); if (attributeCmp != null) { //TraceManager.addDev("Make Attr name 1"); return AVATAR2ProVerif.makeAttrName(attr.getBlock().getName(), attr.getName(), attributeCmp.get(attr).toString()); @@ -451,6 +456,8 @@ public class AVATAR2ProVerif implements AvatarTranslator { this.avspec.removeTimers(); + TraceManager.addDev("AFTER Translating spec:\n" + this.avspec.toString() + "\n\n"); + // Reset parser AvatarIBSolver.clearAttributes(); @@ -464,7 +471,9 @@ public class AVATAR2ProVerif implements AvatarTranslator { TraceManager.addDev("Make blocks"); this.makeBlocks(allKnowledge); - TraceManager.addDev("Spec generated"); + TraceManager.addDev("Proverif spec generated"); + + return this.spec; } diff --git a/src/main/java/ui/TDiagramPanel.java b/src/main/java/ui/TDiagramPanel.java index 1630804faa2827a00df92aca2214ed2e1563a2f7..de1835932f86596a6d9097bacfed3e24bdd637fd 100644 --- a/src/main/java/ui/TDiagramPanel.java +++ b/src/main/java/ui/TDiagramPanel.java @@ -1724,7 +1724,7 @@ public abstract class TDiagramPanel extends JPanel implements GenericTree { gotoReference = new JMenuItem("Go to reference"); gotoReference.addActionListener(menuAL); - showProVerifTrace = new JMenuItem("Show ProVerif Trace"); + showProVerifTrace = new JMenuItem("Show attack trace"); showProVerifTrace.addActionListener(menuAL); search = new JMenuItem("External Search"); diff --git a/src/main/java/ui/util/DefaultText.java b/src/main/java/ui/util/DefaultText.java index d5c6f6d93be49886be87e2271da6707fc84e2e03..9d09051f8190aa7293b6b4b0eb91d994defcdd27 100755 --- a/src/main/java/ui/util/DefaultText.java +++ b/src/main/java/ui/util/DefaultText.java @@ -50,8 +50,8 @@ package ui.util; */ public class DefaultText { - public static String BUILD = "14752"; - public static String DATE = "2024/04/18 03:22:02 CET"; + public static String BUILD = "14757"; + public static String DATE = "2024/04/23 03:22:04 CET"; public static StringBuffer sbAbout = makeAbout();