diff --git a/modeling/SysMLSec/AliceAndBob.xml b/modeling/SysMLSec/AliceAndBob.xml
index 9a44aed37329e570ead53472ee23b1cea20116f1..aea31a0210c1bd65a291aaf8097af5d1b4393451 100644
--- a/modeling/SysMLSec/AliceAndBob.xml
+++ b/modeling/SysMLSec/AliceAndBob.xml
@@ -1,6 +1,6 @@
<?xml version="1.0" encoding="UTF-8"?>
-<TURTLEGMODELING version="1.0beta" ANIMATE_INTERACTIVE_SIMULATION="true" ACTIVATE_PENALTIES="true" UPDATE_INFORMATION_DIPLO_SIM="true" ANIMATE_WITH_INFO_DIPLO_SIM="true" OPEN_DIAG_DIPLO_SIM="false" LAST_SELECTED_MAIN_TAB="2" LAST_SELECTED_SUB_TAB="0">
+<TURTLEGMODELING version="1.0beta" ANIMATE_INTERACTIVE_SIMULATION="true" ACTIVATE_PENALTIES="true" UPDATE_INFORMATION_DIPLO_SIM="true" ANIMATE_WITH_INFO_DIPLO_SIM="true" OPEN_DIAG_DIPLO_SIM="false" LAST_SELECTED_MAIN_TAB="0" LAST_SELECTED_SUB_TAB="0">
<Modeling type="AVATAR Design" nameTab="Example" tabs="Block Diagram$System$Alice$Bob" >
<AVATARBlockDiagramPanel name="Block Diagram" minX="10" maxX="1400" minY="10" maxY="900" zoom="1.0" >
@@ -170,13 +170,13 @@
<Signal value="out chout(Message msg)" attached="true" />
</extraparam>
</COMPONENT>
-<SUBCOMPONENT type="5000" id="82" index="7" uid="a1c44cc9-9334-4d03-8988-e402248c1447" >
+<SUBCOMPONENT type="5000" id="82" index="7" uid="32384080-e86a-41de-b441-4f6ae88f1cbe" >
<father id="164" 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" />
<TGConnectingPoint num="0" id="42" />
<TGConnectingPoint num="1" id="43" />
<TGConnectingPoint num="2" id="44" />
@@ -220,10 +220,10 @@
<extraparam>
<blockType data="cryptoblock" color="-4072719" />
<CryptoBlock value="true" />
+<Attribute access="0" id="secretData" value="" type="8" typeOther="" />
<Attribute access="0" id="m" value="" type="5" typeOther="Message" />
-<Attribute access="0" id="m2" value="" type="5" typeOther="Message" />
+<Attribute access="0" id="m1" value="" type="5" typeOther="Message" />
<Attribute access="0" id="sk" value="" type="5" typeOther="Key" />
-<Attribute access="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)" />
@@ -248,13 +248,13 @@
<Method value="Message hash(Message msg)" />
</extraparam>
</SUBCOMPONENT>
-<SUBCOMPONENT type="5000" id="123" index="8" uid="32384080-e86a-41de-b441-4f6ae88f1cbe" >
+<SUBCOMPONENT type="5000" id="123" index="8" uid="a1c44cc9-9334-4d03-8988-e402248c1447" >
<father id="164" 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" />
<TGConnectingPoint num="0" id="83" />
<TGConnectingPoint num="1" id="84" />
<TGConnectingPoint num="2" id="85" />
@@ -298,10 +298,10 @@
<extraparam>
<blockType data="cryptoblock" color="-4072719" />
<CryptoBlock value="true" />
-<Attribute access="0" id="secretData" value="" type="8" typeOther="" />
<Attribute access="0" id="m" value="" type="5" typeOther="Message" />
-<Attribute access="0" id="m1" value="" type="5" typeOther="Message" />
+<Attribute access="0" id="m2" value="" type="5" typeOther="Message" />
<Attribute access="0" id="sk" value="" type="5" typeOther="Key" />
+<Attribute access="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)" />
@@ -330,7 +330,7 @@
</AVATARBlockDiagramPanel>
-<AVATARStateMachineDiagramPanel name="System" minX="10" maxX="1400" minY="10" maxY="900" >
+<AVATARStateMachineDiagramPanel name="System" minX="10" maxX="1400" minY="10" maxY="900" zoom="1.0" >
<COMPONENT type="5100" id="166" index="0" uid="a0925a50-0bd2-4287-9a2e-8e4a88ffc8ec" >
<cdparam x="400" y="50" />
<sizeparam width="15" height="15" minWidth="1" minHeight="1" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
@@ -343,7 +343,7 @@
</AVATARStateMachineDiagramPanel>
-<AVATARStateMachineDiagramPanel name="Alice" minX="10" maxX="1400" minY="10" maxY="900" >
+<AVATARStateMachineDiagramPanel name="Alice" minX="10" maxX="1400" minY="10" maxY="900" zoom="1.0" >
<CONNECTOR type="5102" id="173" index="0" uid="3c79ec25-70e2-45c6-90de-c2c5c8dee80b" >
<cdparam x="407" y="310" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
@@ -800,7 +800,7 @@
</AVATARStateMachineDiagramPanel>
-<AVATARStateMachineDiagramPanel name="Bob" minX="10" maxX="1400" minY="10" maxY="900" >
+<AVATARStateMachineDiagramPanel name="Bob" minX="10" maxX="1400" minY="10" maxY="900" zoom="1.0" >
<CONNECTOR type="5102" id="442" index="0" uid="2093fd68-e5a8-4300-870b-a98ff405412a" >
<cdparam x="416" y="379" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
@@ -1342,7 +1342,7 @@
<MainCode value="}"/>
<Optimized value="true" />
<considerTimingOperators value="true" />
-<Validated value="System;Alice;Bob;" />
+<Validated value="" />
<Ignored value="" />
<CONNECTOR type="5002" id="781" index="0" uid="04cf395e-e1ee-41be-9e4a-649d5fdce7f9" >
@@ -1506,13 +1506,13 @@
<Signal value="out chout(Message msg)" attached="true" />
</extraparam>
</COMPONENT>
-<SUBCOMPONENT type="5000" id="857" index="7" uid="e802e723-57b4-4734-af20-cddadacc10e6" >
+<SUBCOMPONENT type="5000" id="857" index="7" uid="cc150a1e-1348-4fa4-98a9-3a612b6184cc" >
<father id="939" 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" />
<TGConnectingPoint num="0" id="817" />
<TGConnectingPoint num="1" id="818" />
<TGConnectingPoint num="2" id="819" />
@@ -1556,13 +1556,13 @@
<extraparam>
<blockType data="cryptoblock" color="-4072719" />
<CryptoBlock value="true" />
-<Attribute access="0" id="secretData" value="" type="8" typeOther="" />
<Attribute access="0" id="m" value="" type="5" typeOther="Message" />
-<Attribute access="0" id="m1" value="" type="5" typeOther="Message" />
+<Attribute access="0" id="m2" value="" type="5" typeOther="Message" />
<Attribute access="0" id="sk" value="" type="5" typeOther="Key" />
-<Attribute access="0" id="pubK" value="" type="5" typeOther="Key" />
+<Attribute access="0" id="receivedData" value="" type="8" typeOther="" />
<Attribute access="0" id="privK" value="" type="5" typeOther="Key" />
-<Attribute access="0" id="bobPubK" value="" type="5" typeOther="Key" />
+<Attribute access="0" id="pubK" value="" type="5" typeOther="Key" />
+<Attribute access="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)" />
@@ -1587,13 +1587,13 @@
<Method value="Message hash(Message msg)" />
</extraparam>
</SUBCOMPONENT>
-<SUBCOMPONENT type="5000" id="898" index="8" uid="cc150a1e-1348-4fa4-98a9-3a612b6184cc" >
+<SUBCOMPONENT type="5000" id="898" index="8" uid="e802e723-57b4-4734-af20-cddadacc10e6" >
<father id="939" 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" />
<TGConnectingPoint num="0" id="858" />
<TGConnectingPoint num="1" id="859" />
<TGConnectingPoint num="2" id="860" />
@@ -1637,13 +1637,13 @@
<extraparam>
<blockType data="cryptoblock" color="-4072719" />
<CryptoBlock value="true" />
+<Attribute access="0" id="secretData" value="" type="8" typeOther="" />
<Attribute access="0" id="m" value="" type="5" typeOther="Message" />
-<Attribute access="0" id="m2" value="" type="5" typeOther="Message" />
+<Attribute access="0" id="m1" value="" type="5" typeOther="Message" />
<Attribute access="0" id="sk" value="" type="5" typeOther="Key" />
-<Attribute access="0" id="receivedData" value="" type="8" typeOther="" />
-<Attribute access="0" id="privK" value="" type="5" typeOther="Key" />
<Attribute access="0" id="pubK" value="" type="5" typeOther="Key" />
-<Attribute access="0" id="alicePubK" value="" type="5" typeOther="Key" />
+<Attribute access="0" id="privK" value="" type="5" typeOther="Key" />
+<Attribute access="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)" />
@@ -1672,7 +1672,7 @@
</AVATARBlockDiagramPanel>
-<AVATARStateMachineDiagramPanel name="System" minX="10" maxX="1400" minY="10" maxY="900" >
+<AVATARStateMachineDiagramPanel name="System" minX="10" maxX="1400" minY="10" maxY="900" zoom="1.0" >
<COMPONENT type="5100" id="941" index="0" uid="f1ab80ad-4a92-4500-9a3b-fcf0b3c4b63e" >
<cdparam x="400" y="50" />
<sizeparam width="15" height="15" minWidth="1" minHeight="1" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
@@ -1685,7 +1685,7 @@
</AVATARStateMachineDiagramPanel>
-<AVATARStateMachineDiagramPanel name="Bob" minX="10" maxX="1400" minY="10" maxY="900" >
+<AVATARStateMachineDiagramPanel name="Bob" minX="10" maxX="1400" minY="10" maxY="900" zoom="1.0" >
<CONNECTOR type="5102" id="948" index="0" uid="6743571d-b9c1-4558-b1e8-f57dc2554fa6" >
<cdparam x="418" y="632" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="1000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
@@ -2555,7 +2555,7 @@
</AVATARStateMachineDiagramPanel>
-<AVATARStateMachineDiagramPanel name="Alice" minX="10" maxX="1400" minY="10" maxY="900" >
+<AVATARStateMachineDiagramPanel name="Alice" minX="10" maxX="1400" minY="10" maxY="900" zoom="1.0" >
<CONNECTOR type="5102" id="1484" index="0" uid="370d8ae6-1c4d-408a-8adf-01ff5f6e5b35" >
<cdparam x="411" y="567" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
@@ -3362,7 +3362,7 @@
<MainCode value="}"/>
<Optimized value="true" />
<considerTimingOperators value="true" />
-<Validated value="System;CA;Alice;Bob;" />
+<Validated value="" />
<Ignored value="" />
<CONNECTOR type="5002" id="1948" index="0" uid="7a6e9dbc-0dbd-40e4-8038-05098e6c4bd1" >
@@ -3538,13 +3538,13 @@
<Signal value="out chout(Message msg)" attached="true" />
</extraparam>
</COMPONENT>
-<SUBCOMPONENT type="5000" id="2024" index="7" uid="f24348ab-6d4a-40e6-a942-342d6222b23f" >
+<SUBCOMPONENT type="5000" id="2024" index="7" uid="7a040a26-feb9-4e9a-a609-908679df2a0b" >
<father id="2147" num="0" />
-<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" />
<TGConnectingPoint num="0" id="1984" />
<TGConnectingPoint num="1" id="1985" />
<TGConnectingPoint num="2" id="1986" />
@@ -3588,30 +3588,18 @@
<extraparam>
<blockType data="cryptoblock" color="-4072719" />
<CryptoBlock value="true" />
-<Attribute access="0" id="m" value="" type="5" typeOther="Message" />
-<Attribute access="0" id="m2" value="" type="5" typeOther="Message" />
-<Attribute access="0" id="sk" value="" type="5" typeOther="Key" />
-<Attribute access="0" id="receivedData" value="" type="8" typeOther="" />
<Attribute access="0" id="privK" value="" type="5" typeOther="Key" />
<Attribute access="0" id="pubK" value="" type="5" typeOther="Key" />
<Attribute access="0" id="alicePubK" value="" type="5" typeOther="Key" />
-<Attribute access="0" id="CAPubK" value="" type="5" typeOther="Key" />
+<Attribute access="0" id="bobPubK" value="" type="5" typeOther="Key" />
<Attribute access="0" id="aliceID" value="" type="8" typeOther="" />
+<Attribute access="0" id="bobID" value="" type="8" typeOther="" />
+<Attribute access="0" id="m" value="" type="5" typeOther="Message" />
+<Attribute access="0" id="newK" value="" type="5" typeOther="Key" />
+<Attribute access="0" id="newCert" value="" type="5" typeOther="Message" />
<Attribute access="0" id="m1" value="" type="5" typeOther="Message" />
-<Attribute access="0" id="sig" value="" type="5" typeOther="Message" />
-<Attribute access="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" id="m2" value="" type="5" typeOther="Message" />
+<Attribute access="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)" />
@@ -3620,8 +3608,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)" />
</extraparam>
</SUBCOMPONENT>
<SUBCOMPONENT type="5000" id="2065" index="8" uid="52a07889-a0b4-45e9-a97a-a5a5e144d49b" >
@@ -3710,13 +3708,13 @@
<Method value="Message hash(Message msg)" />
</extraparam>
</SUBCOMPONENT>
-<SUBCOMPONENT type="5000" id="2106" index="9" uid="7a040a26-feb9-4e9a-a609-908679df2a0b" >
+<SUBCOMPONENT type="5000" id="2106" index="9" uid="f24348ab-6d4a-40e6-a942-342d6222b23f" >
<father id="2147" num="2" />
-<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" />
<TGConnectingPoint num="0" id="2066" />
<TGConnectingPoint num="1" id="2067" />
<TGConnectingPoint num="2" id="2068" />
@@ -3760,30 +3758,22 @@
<extraparam>
<blockType data="cryptoblock" color="-4072719" />
<CryptoBlock value="true" />
+<Attribute access="0" id="m" value="" type="5" typeOther="Message" />
+<Attribute access="0" id="m2" value="" type="5" typeOther="Message" />
+<Attribute access="0" id="sk" value="" type="5" typeOther="Key" />
+<Attribute access="0" id="receivedData" value="" type="8" typeOther="" />
<Attribute access="0" id="privK" value="" type="5" typeOther="Key" />
<Attribute access="0" id="pubK" value="" type="5" typeOther="Key" />
<Attribute access="0" id="alicePubK" value="" type="5" typeOther="Key" />
-<Attribute access="0" id="bobPubK" value="" type="5" typeOther="Key" />
+<Attribute access="0" id="CAPubK" value="" type="5" typeOther="Key" />
<Attribute access="0" id="aliceID" value="" type="8" typeOther="" />
-<Attribute access="0" id="bobID" value="" type="8" typeOther="" />
-<Attribute access="0" id="m" value="" type="5" typeOther="Message" />
-<Attribute access="0" id="newK" value="" type="5" typeOther="Key" />
-<Attribute access="0" id="newCert" value="" type="5" typeOther="Message" />
<Attribute access="0" id="m1" value="" type="5" typeOther="Message" />
-<Attribute access="0" id="m2" value="" type="5" typeOther="Message" />
-<Attribute access="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" id="sig" value="" type="5" typeOther="Message" />
+<Attribute access="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)" />
@@ -3792,13 +3782,23 @@
<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)" />
</extraparam>
</SUBCOMPONENT>
</AVATARBlockDiagramPanel>
-<AVATARStateMachineDiagramPanel name="System" minX="10" maxX="1400" minY="10" maxY="900" >
+<AVATARStateMachineDiagramPanel name="System" minX="10" maxX="1400" minY="10" maxY="900" zoom="1.0" >
<COMPONENT type="5100" id="2149" index="0" uid="f616c80f-32a9-437d-a505-ed8f7a7ab4e6" >
<cdparam x="400" y="50" />
<sizeparam width="15" height="15" minWidth="1" minHeight="1" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
@@ -3811,7 +3811,7 @@
</AVATARStateMachineDiagramPanel>
-<AVATARStateMachineDiagramPanel name="CA" minX="10" maxX="2500" minY="10" maxY="1500" >
+<AVATARStateMachineDiagramPanel name="CA" minX="10" maxX="2500" minY="10" maxY="1500" zoom="1.0" >
<CONNECTOR type="5102" id="2160" index="0" uid="02aecba8-0752-4a5d-b095-367acaec4137" >
<cdparam x="331" y="296" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
@@ -4534,7 +4534,7 @@
</AVATARStateMachineDiagramPanel>
-<AVATARStateMachineDiagramPanel name="Alice" minX="10" maxX="1400" minY="10" maxY="900" >
+<AVATARStateMachineDiagramPanel name="Alice" minX="10" maxX="1400" minY="10" maxY="900" zoom="1.0" >
<CONNECTOR type="5102" id="2442" index="0" uid="a8a09122-7a18-4e88-a81c-37f86e8d805a" >
<cdparam x="608" y="388" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
@@ -5396,7 +5396,7 @@
</AVATARStateMachineDiagramPanel>
-<AVATARStateMachineDiagramPanel name="Bob" minX="10" maxX="1400" minY="10" maxY="900" >
+<AVATARStateMachineDiagramPanel name="Bob" minX="10" maxX="1400" minY="10" maxY="900" zoom="1.0" >
<CONNECTOR type="5102" id="2969" index="0" uid="83e638e1-4f1b-463a-951a-ed1b11db467e" >
<cdparam x="407" y="70" />
<sizeparam width="0" height="0" minWidth="0" minHeight="0" maxWidth="2000" maxHeight="2000" minDesiredWidth="0" minDesiredHeight="0" />
diff --git a/src/main/java/avatartranslator/toproverif/AVATAR2ProVerif.java b/src/main/java/avatartranslator/toproverif/AVATAR2ProVerif.java
index 01ede72d409c2cdf7f3ea85543b409843c29be41..45929e4572917e033503194ecb1a0519ea98ac4d 100755
--- a/src/main/java/avatartranslator/toproverif/AVATAR2ProVerif.java
+++ b/src/main/java/avatartranslator/toproverif/AVATAR2ProVerif.java
@@ -1,26 +1,26 @@
/* Copyright or (C) or Copr. GET / ENST, Telecom-Paris, Ludovic Apvrille
- *
+ *
* ludovic.apvrille AT enst.fr
- *
+ *
* This software is a computer program whose purpose is to allow the
* edition of TURTLE analysis, design and deployment diagrams, to
* allow the generation of RT-LOTOS or Java code from this diagram,
* and at last to allow the analysis of formal validation traces
* obtained from external tools, e.g. RTL from LAAS-CNRS and CADP
* from INRIA Rhone-Alpes.
- *
+ *
* This software is governed by the CeCILL license under French law and
* abiding by the rules of distribution of free software. You can use,
* modify and/ or redistribute the software under the terms of the CeCILL
* license as circulated by CEA, CNRS and INRIA at the following URL
* "http://www.cecill.info".
- *
+ *
* As a counterpart to the access to the source code and rights to copy,
* modify and redistribute granted by the license, users are provided only
* with a limited warranty and the software's author, the holder of the
* economic rights, and the successive licensors have only limited
* liability.
- *
+ *
* In this respect, the user's attention is drawn to the risks associated
* with loading, using, modifying and/or developing or reproducing the
* software by the user in light of its specific status of free software,
@@ -31,7 +31,7 @@
* requirements in conditions enabling the security of their systems and/or
* data to be ensured and, more generally, to use and operate it in the
* same conditions as regards security.
- *
+ *
* The fact that you are presently reading this means that you have had
* knowledge of the CeCILL license and that you accept its terms.
*/
@@ -39,15 +39,15 @@
package avatartranslator.toproverif;
import avatartranslator.*;
+import common.ConfigurationTTool;
import myutil.FileException;
import myutil.FileUtils;
import myutil.TraceManager;
import proverifspec.*;
-import ui.AvatarDesignPanel;
-import ui.UICheckingError;
import translator.CheckingError;
-import common.ConfigurationTTool;
+import ui.AvatarDesignPanel;
import ui.TGComponent;
+import ui.UICheckingError;
import ui.window.JDialogProverifVerification;
import javax.swing.*;
@@ -55,49 +55,37 @@ import java.io.BufferedReader;
import java.io.File;
import java.io.FileReader;
import java.io.IOException;
-import java.util.HashMap;
-import java.util.HashSet;
-import java.util.LinkedList;
-import java.util.List;
-import java.util.Map;
+import java.util.*;
/**
* Class AVATAR2ProVerif
* Creation: 03/09/2010
- * @version 1.1 03/09/2010
+ *
* @author Ludovic APVRILLE
+ * @version 1.1 03/09/2010
*/
public class AVATAR2ProVerif implements AvatarTranslator {
public final static String ATTR_DELIM = "___";
-
+ public final static String CH_ENCRYPT = "privChEnc__";
private final static String UNKNOWN = "UNKNOWN";
-
private final static String TRUE = "TRUE";
private final static String FALSE = "FALSE";
-
private final static String PK_PK = "pk";
private final static String PK_ENCRYPT = "aencrypt";
private final static String PK_DECRYPT = "adecrypt";
private final static String PK_SIGN = "sign";
private final static String PK_VERIFYSIGN = "verifySign";
-
private final static String CERT_CERT = "cert";
private final static String CERT_VERIFYCERT = "verifyCert";
private final static String CERT_GETPK = "getpk";
-
private final static String SK_ENCRYPT = "sencrypt";
private final static String SK_DECRYPT = "sdecrypt";
-
private final static String DH_DH = "DH";
-
private final static String MAC_MAC = "MAC";
private final static String MAC_VERIFYMAC = "verifyMAC";
-
private final static String HASH_HASH = "hash";
-
private final static String CH_MAINCH = "ch";
- public final static String CH_ENCRYPT = "privChEnc__";
private final static String CH_DECRYPT = "privChDec__";
private final static String CHCTRL_CH = "chControl";
@@ -107,7 +95,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
private final static String ZERO = "O";
private final static String PEANO_N = "N";
- private final static int MAX_INT = 50;
+ private final static int MAX_INT = 50;
private final static String SEC_TRANS = "Security verification: ";
@@ -130,95 +118,10 @@ public class AVATAR2ProVerif implements AvatarTranslator {
this.spec = null;
}
- public boolean saveInFile(String path) throws FileException {
- //Our hash is saved in config
- String hashCode= Integer.toString(this.spec.getStringSpec().hashCode());
- File file = new File(path);
- BufferedReader br = null;
- if (file.exists()){
- String hash = ConfigurationTTool.ProVerifHash;
- if (!hash.equals("")){
- try {
- br = new BufferedReader(new FileReader(path));
- String s = br.readLine();
- String tmp;
- while ((tmp = br.readLine()) !=null){
- s = s+"\n" + tmp;
- }
- String fileHash = Integer.toString(s.hashCode());
- if (!hash.equals(fileHash)){
- if(JOptionPane.showConfirmDialog(null, "File " + path + " already exists. Do you want to overwrite?", "Overwrite File?", JOptionPane.YES_NO_OPTION) == JOptionPane.NO_OPTION){
- return false;
- }
- }
-// br.close();
- } catch (Exception e) {
- e.printStackTrace();
- }
- finally {
- if ( br != null ) {
- try {
- br.close();
- } catch (IOException e) {
- e.printStackTrace();
- }
- }
- }
- }
- }
- FileUtils.saveFile(path, this.spec.getStringSpec());
- ConfigurationTTool.ProVerifHash = hashCode;
- try {
- ConfigurationTTool.saveConfiguration();
- } catch (Exception e){
- //
- }
- return true;
- }
-
- public LinkedList<CheckingError> getWarnings() {
- return this.warnings;
- }
-
- public AvatarSpecification getAvatarSpecification () {
- return this.avspec;
- }
-
- public ProVerifSpec generateProVerif(boolean _debug, boolean _optimize, int _stateReachability, boolean _typed, boolean allowPrivateChannelDuplication) {
- this.allowPrivateChannelDuplication = allowPrivateChannelDuplication;
- this.stateReachability = _stateReachability;
- this.warnings = new LinkedList<CheckingError> ();
- if (_typed)
- this.spec = new ProVerifSpec (new ProVerifPitypeSyntaxer ());
- else
- this.spec = new ProVerifSpec (new ProVerifPiSyntaxer ());
-
- // TODO: What are composite states ?
- this.avspec.removeCompositeStates();
-
- this.avspec.removeLibraryFunctionCalls ();
-
- this.avspec.removeTimers();
-
- this.dummyDataCounter = 0;
-
- List<AvatarAttribute> allKnowledge = this.makeStartingProcess();
-
- this.makeHeader();
-
- this.makeBlocks(allKnowledge);
-
- return this.spec;
- }
-
- public ProVerifOutputAnalyzer getOutputAnalyzer () {
- return new ProVerifOutputAnalyzer (this);
- }
-
- private static String makeAttrName (String... _params) {
+ private static String makeAttrName(String... _params) {
String result = "";
boolean first = true;
- for (String p: _params) {
+ for (String p : _params) {
if (first)
first = false;
else
@@ -228,13 +131,13 @@ public class AVATAR2ProVerif implements AvatarTranslator {
return result;
}
- protected static String translateTerm (AvatarTerm term, Map<AvatarAttribute, Integer> attributeCmp) {
+ protected static String translateTerm(AvatarTerm term, Map<AvatarAttribute, Integer> attributeCmp) {
if (term instanceof AvatarAttribute) {
AvatarAttribute attr = (AvatarAttribute) term;
if (attributeCmp != null) {
//TraceManager.addDev("Mae Attr name 1");
- return AVATAR2ProVerif.makeAttrName (attr.getBlock ().getName (), attr.getName (), attributeCmp.get (attr).toString ());
+ return AVATAR2ProVerif.makeAttrName(attr.getBlock().getName(), attr.getName(), attributeCmp.get(attr).toString());
} else {
//TraceManager.addDev("Mae Attr name 2");
return AVATAR2ProVerif.makeAttrName(attr.getBlock().getName(), attr.getName());
@@ -246,39 +149,41 @@ public class AVATAR2ProVerif implements AvatarTranslator {
//TraceManager.addDev("AvatarConstant");
try {
- int i = Integer.parseInt (constant.getName ());
+ int i = Integer.parseInt(constant.getName());
//TraceManager.addDev("AvatarConstant Integer");
if (i <= MAX_INT) {
int j;
- StringBuilder sb = new StringBuilder ();
- for (j=i; j>0; j--) {
- sb.append (PEANO_N);
- sb.append ("(");
+ StringBuilder sb = new StringBuilder();
+ for (j = i; j > 0; j--) {
+ sb.append(PEANO_N);
+ sb.append("(");
}
- sb.append (ZERO);
- for (; i>0; i--)
- sb.append (")");
+ sb.append(ZERO);
+ for (; i > 0; i--)
+ sb.append(")");
//TraceManager.addDev("AvatarConstant Integer Lower: " + sb.toString ());
- return sb.toString ();
+ return sb.toString();
} else {
TraceManager.addDev("ERROR=ZERO");
// TODO: raise error
return ZERO;
}
- } catch (NumberFormatException e) { TraceManager.addDev("ERROR=NFE");}
+ } catch (NumberFormatException e) {
+ TraceManager.addDev("ERROR=NFE");
+ }
- return constant.getName ();
+ return constant.getName();
}
if (term instanceof AvatarArithmeticOp) {
AvatarArithmeticOp op = (AvatarArithmeticOp) term;
- TraceManager.addDev("TERM=" + op.toString());
- if (op.getOperator ().compareTo ("+") == 0) {
+ //TraceManager.addDev("TERM=" + op.toString());
+ if (op.getOperator().compareTo("+") == 0) {
AvatarTerm t1, t2;
- t1 = op.getTerm1 ();
- t2 = op.getTerm2 ();
+ t1 = op.getTerm1();
+ t2 = op.getTerm2();
if (t1 instanceof AvatarConstant) {
AvatarTerm t = t1;
t1 = t2;
@@ -290,26 +195,26 @@ public class AVATAR2ProVerif implements AvatarTranslator {
}
try {
- int i = Integer.parseInt (t2.getName ());
+ int i = Integer.parseInt(t2.getName());
if (i <= MAX_INT) {
int j;
- StringBuilder sb = new StringBuilder ();
- for (j=i; j>0; j--) {
- sb.append (PEANO_N);
- sb.append ("(");
+ StringBuilder sb = new StringBuilder();
+ for (j = i; j > 0; j--) {
+ sb.append(PEANO_N);
+ sb.append("(");
}
- sb.append (AVATAR2ProVerif.translateTerm(t1, attributeCmp));
- for (; i>0; i--)
- sb.append (")");
+ sb.append(AVATAR2ProVerif.translateTerm(t1, attributeCmp));
+ for (; i > 0; i--)
+ sb.append(")");
- return sb.toString ();
+ return sb.toString();
} else {
// TODO: raise error
TraceManager.addDev("ERROR= max int");
return AVATAR2ProVerif.translateTerm(t1, attributeCmp);
}
- } catch (NumberFormatException e) {
+ } catch (NumberFormatException e) {
// TODO: raise error
TraceManager.addDev("ERROR= NumberFormatException");
return AVATAR2ProVerif.translateTerm(t1, attributeCmp);
@@ -324,21 +229,21 @@ public class AVATAR2ProVerif implements AvatarTranslator {
}
if (term instanceof AvatarTermFunction) {
- AvatarTuple args = ((AvatarTermFunction) term).getArgs ();
- AvatarMethod method = ((AvatarTermFunction) term).getMethod ();
+ AvatarTuple args = ((AvatarTermFunction) term).getArgs();
+ AvatarMethod method = ((AvatarTermFunction) term).getMethod();
- return method.getName () + " " + AVATAR2ProVerif.translateTerm (args, attributeCmp);
+ return method.getName() + " " + AVATAR2ProVerif.translateTerm(args, attributeCmp);
}
if (term instanceof AvatarTuple) {
String result = "(";
boolean first = true;
- for (AvatarTerm arg: ((AvatarTuple) term).getComponents ()) {
+ for (AvatarTerm arg : ((AvatarTuple) term).getComponents()) {
if (first)
first = false;
else
result += ", ";
- result += AVATAR2ProVerif.translateTerm (arg, attributeCmp);
+ result += AVATAR2ProVerif.translateTerm(arg, attributeCmp);
}
result += ")";
@@ -351,7 +256,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
// Supported guards: a == b, not(a == b), g1 and g2, g1 or g2
// -> transformed into a = b, a <> b, g1 && g2, g1 || g2
// Returns nulls otherwise
- private static String translateGuard (AvatarGuard _guard, Map<AvatarAttribute, Integer> attributeCmp) {
+ private static String translateGuard(AvatarGuard _guard, Map<AvatarAttribute, Integer> attributeCmp) {
TraceManager.addDev("Handling Guard:" + _guard.toString());
if (_guard == null || _guard instanceof AvatarGuardEmpty) {
TraceManager.addDev("Null or empty guard");
@@ -363,8 +268,8 @@ public class AVATAR2ProVerif implements AvatarTranslator {
return null;
if (_guard instanceof AvatarSimpleGuardMono) {
- TraceManager.addDev("SimpleGuardMono:" + _guard);
- String term = AVATAR2ProVerif.translateTerm (((AvatarSimpleGuardMono) _guard).getTerm (), attributeCmp);
+ //TraceManager.addDev("SimpleGuardMono:" + _guard);
+ String term = AVATAR2ProVerif.translateTerm(((AvatarSimpleGuardMono) _guard).getTerm(), attributeCmp);
//TraceManager.addDev("guard/ term=" + term);
if (term != null)
return term + " = " + TRUE;
@@ -373,16 +278,16 @@ public class AVATAR2ProVerif implements AvatarTranslator {
}
if (_guard instanceof AvatarSimpleGuardDuo) {
- TraceManager.addDev("SimpleGuardDuo");
+ //TraceManager.addDev("SimpleGuardDuo");
String delim = null;
- String termA = AVATAR2ProVerif.translateTerm (((AvatarSimpleGuardDuo) _guard).getTermA (), attributeCmp);
- String termB = AVATAR2ProVerif.translateTerm (((AvatarSimpleGuardDuo) _guard).getTermB (), attributeCmp);
+ String termA = AVATAR2ProVerif.translateTerm(((AvatarSimpleGuardDuo) _guard).getTermA(), attributeCmp);
+ String termB = AVATAR2ProVerif.translateTerm(((AvatarSimpleGuardDuo) _guard).getTermB(), attributeCmp);
- if (((AvatarSimpleGuardDuo) _guard).getBinaryOp ().equals ("=="))
+ if (((AvatarSimpleGuardDuo) _guard).getBinaryOp().equals("=="))
delim = "=";
/*else if (((AvatarSimpleGuardDuo) _guard).getBinaryOp ().equals ("<"))
delim = "<";*/
- else if (((AvatarSimpleGuardDuo) _guard).getBinaryOp ().equals ("!="))
+ else if (((AvatarSimpleGuardDuo) _guard).getBinaryOp().equals("!="))
delim = "<>";
/*else if (((AvatarSimpleGuardDuo) _guard).getBinaryOp ().equals (">"))
delim = ">";*/
@@ -394,20 +299,19 @@ public class AVATAR2ProVerif implements AvatarTranslator {
}
if (_guard instanceof AvatarUnaryGuard) {
- TraceManager.addDev("UnaryGuard");
- String unary = ((AvatarUnaryGuard) _guard).getUnaryOp ();
- AvatarGuard guard = ((AvatarUnaryGuard) _guard).getGuard ();
+ //TraceManager.addDev("UnaryGuard");
+ String unary = ((AvatarUnaryGuard) _guard).getUnaryOp();
+ AvatarGuard guard = ((AvatarUnaryGuard) _guard).getGuard();
String beforeProV = null;
String afterProV = ")";
- if (unary.equals ("not"))
+ if (unary.equals("not"))
beforeProV = "not (";
- else if (unary.equals (""))
+ else if (unary.equals(""))
beforeProV = "(";
- String guardProV = AVATAR2ProVerif.translateGuard (guard, attributeCmp);
-
+ String guardProV = AVATAR2ProVerif.translateGuard(guard, attributeCmp);
if (beforeProV != null && guardProV != null)
@@ -417,284 +321,367 @@ public class AVATAR2ProVerif implements AvatarTranslator {
}
if (_guard instanceof AvatarBinaryGuard) {
- TraceManager.addDev("BinaryGuard");
- String delim = ((AvatarBinaryGuard) _guard).getBinaryOp ();
- AvatarGuard guardA = ((AvatarBinaryGuard) _guard).getGuardA ();
- AvatarGuard guardB = ((AvatarBinaryGuard) _guard).getGuardB ();
+ //TraceManager.addDev("BinaryGuard");
+ String delim = ((AvatarBinaryGuard) _guard).getBinaryOp();
+ AvatarGuard guardA = ((AvatarBinaryGuard) _guard).getGuardA();
+ AvatarGuard guardB = ((AvatarBinaryGuard) _guard).getGuardB();
String delimProV = null;
- if (delim.equals ("and") || delim.equals("&&"))
+ if (delim.equals("and") || delim.equals("&&"))
delimProV = "&&";
- else if (delim.equals ("or") || delim.equals("||"))
+ else if (delim.equals("or") || delim.equals("||"))
delimProV = "||";
- String guardAProV = AVATAR2ProVerif.translateGuard (guardA, attributeCmp);
- String guardBProV = AVATAR2ProVerif.translateGuard (guardB, attributeCmp);
+ String guardAProV = AVATAR2ProVerif.translateGuard(guardA, attributeCmp);
+ String guardBProV = AVATAR2ProVerif.translateGuard(guardB, attributeCmp);
if (delimProV != null && guardAProV != null && guardBProV != null)
return guardAProV + " " + delimProV + " " + guardBProV;
}
if (_guard instanceof AvatarConstantGuard) {
- TraceManager.addDev("ConstantGuard");
+ //TraceManager.addDev("ConstantGuard");
AvatarConstantGuard constant = (AvatarConstantGuard) _guard;
- if (constant.getConstant () == AvatarConstant.TRUE)
+ if (constant.getConstant() == AvatarConstant.TRUE)
return "TRUE";
- if (constant.getConstant () == AvatarConstant.FALSE)
+ if (constant.getConstant() == AvatarConstant.FALSE)
return "FALSE";
}
TraceManager.addDev("No valid guard found");
-
return null;
}
- public String getTrueName (AvatarAttribute attr) {
- AvatarAttribute trueAttr = this.nameEquivalence.get (attr);
+ public boolean saveInFile(String path) throws FileException {
+ //Our hash is saved in config
+ String hashCode = Integer.toString(this.spec.getStringSpec().hashCode());
+ File file = new File(path);
+ BufferedReader br = null;
+ if (file.exists()) {
+ String hash = ConfigurationTTool.ProVerifHash;
+ if (!hash.equals("")) {
+ try {
+ br = new BufferedReader(new FileReader(path));
+ String s = br.readLine();
+ String tmp;
+ while ((tmp = br.readLine()) != null) {
+ s = s + "\n" + tmp;
+ }
+ String fileHash = Integer.toString(s.hashCode());
+ if (!hash.equals(fileHash)) {
+ if (JOptionPane.showConfirmDialog(null, "File " + path + " already exists. Do you want to overwrite?", "Overwrite File?", JOptionPane.YES_NO_OPTION) == JOptionPane.NO_OPTION) {
+ return false;
+ }
+ }
+// br.close();
+ } catch (Exception e) {
+ e.printStackTrace();
+ } finally {
+ if (br != null) {
+ try {
+ br.close();
+ } catch (IOException e) {
+ e.printStackTrace();
+ }
+ }
+ }
+ }
+ }
+ FileUtils.saveFile(path, this.spec.getStringSpec());
+ ConfigurationTTool.ProVerifHash = hashCode;
+ try {
+ ConfigurationTTool.saveConfiguration();
+ } catch (Exception e) {
+ //
+ }
+ return true;
+ }
+
+ public LinkedList<CheckingError> getWarnings() {
+ return this.warnings;
+ }
+
+ public AvatarSpecification getAvatarSpecification() {
+ return this.avspec;
+ }
+
+ public ProVerifSpec generateProVerif(boolean _debug, boolean _optimize, int _stateReachability, boolean _typed, boolean allowPrivateChannelDuplication) {
+ this.allowPrivateChannelDuplication = allowPrivateChannelDuplication;
+ this.stateReachability = _stateReachability;
+ this.warnings = new LinkedList<CheckingError>();
+ if (_typed)
+ this.spec = new ProVerifSpec(new ProVerifPitypeSyntaxer());
+ else
+ this.spec = new ProVerifSpec(new ProVerifPiSyntaxer());
+
+ // TODO: What are composite states ?
+ this.avspec.removeCompositeStates();
+
+ this.avspec.removeLibraryFunctionCalls();
+
+ this.avspec.removeTimers();
+
+ this.dummyDataCounter = 0;
+
+ List<AvatarAttribute> allKnowledge = this.makeStartingProcess();
+
+ this.makeHeader();
+
+ this.makeBlocks(allKnowledge);
+
+ return this.spec;
+ }
+
+ public ProVerifOutputAnalyzer getOutputAnalyzer() {
+ return new ProVerifOutputAnalyzer(this);
+ }
+
+ public String getTrueName(AvatarAttribute attr) {
+ AvatarAttribute trueAttr = this.nameEquivalence.get(attr);
if (trueAttr == null)
return null;
- return AVATAR2ProVerif.translateTerm (trueAttr, null);
+ return AVATAR2ProVerif.translateTerm(trueAttr, null);
}
public void makeHeader() {
TraceManager.addDev("\n\n=+=+=+ Making Headers +=+=+=");
- this.spec.addDeclaration (new ProVerifProperty ("abbreviateDerivation = false"));
- this.spec.addDeclaration (new ProVerifComment ("Boolean return types"));
- this.spec.addDeclaration (new ProVerifConst (TRUE, "bitstring"));
- this.spec.addDeclaration (new ProVerifConst (FALSE, "bitstring"));
- this.spec.addDeclaration (new ProVerifComment ("Functions data"));
- this.spec.addDeclaration (new ProVerifConst (UNKNOWN, "bitstring"));
-
- this.spec.addDeclaration (new ProVerifComment ("Public key cryptography"));
- this.spec.addDeclaration (new ProVerifFunc (PK_PK, new String[] {"bitstring"}, "bitstring"));
- this.spec.addDeclaration (new ProVerifFunc (PK_ENCRYPT, new String[] {"bitstring", "bitstring"}, "bitstring"));
- this.spec.addDeclaration (new ProVerifReduc (new ProVerifVar[] {new ProVerifVar ("x", "bitstring"), new ProVerifVar ("y", "bitstring")}, PK_DECRYPT + " (" + PK_ENCRYPT + " (x, " + PK_PK + " (y)), y) = x"));
- this.spec.addDeclaration (new ProVerifFunc (PK_SIGN, new String[] {"bitstring", "bitstring"}, "bitstring"));
- this.spec.addDeclaration (new ProVerifFunc (PK_VERIFYSIGN, new String[] {"bitstring", "bitstring", "bitstring"}, "bitstring",
- new ProVerifReduc (new ProVerifVar[] {new ProVerifVar ("m", "bitstring"), new ProVerifVar ("sk", "bitstring")}, PK_VERIFYSIGN + " (m, " + PK_SIGN + " (m, sk), " + PK_PK + " (sk)) = " + TRUE,
- new ProVerifReduc (new ProVerifVar[] {new ProVerifVar ("m", "bitstring"), new ProVerifVar ("m2", "bitstring"), new ProVerifVar ("ppk", "bitstring")}, PK_VERIFYSIGN + " (m, m2, ppk) = " + FALSE))));
-
-
- this.spec.addDeclaration (new ProVerifComment ("Certificates"));
- this.spec.addDeclaration (new ProVerifFunc (CERT_CERT, new String[] {"bitstring", "bitstring"}, "bitstring"));
- this.spec.addDeclaration (new ProVerifFunc (CERT_VERIFYCERT, new String[] {"bitstring", "bitstring"}, "bitstring",
- new ProVerifReduc (new ProVerifVar[] {new ProVerifVar ("epk", "bitstring"), new ProVerifVar ("sk", "bitstring")}, CERT_VERIFYCERT + " (" + CERT_CERT + " (epk, " + PK_SIGN + " (epk, sk)), " + PK_PK + " (sk)) = " + TRUE,
- new ProVerifReduc (new ProVerifVar[] {new ProVerifVar ("m", "bitstring"), new ProVerifVar ("ppk", "bitstring")}, CERT_VERIFYCERT + " (m, ppk) = " + FALSE))));
- this.spec.addDeclaration (new ProVerifReduc (new ProVerifVar[] {new ProVerifVar ("epk", "bitstring"), new ProVerifVar ("sk", "bitstring")}, CERT_GETPK + " (" + CERT_CERT + " (epk, " + PK_SIGN + " (epk,sk))) = epk"));
-
- this.spec.addDeclaration (new ProVerifComment ("Symmetric key cryptography"));
- this.spec.addDeclaration (new ProVerifFunc (SK_ENCRYPT, new String[] {"bitstring", "bitstring"}, "bitstring"));
- this.spec.addDeclaration (new ProVerifReduc (new ProVerifVar[] {new ProVerifVar ("x", "bitstring"), new ProVerifVar ("k", "bitstring")}, SK_DECRYPT + " (" + SK_ENCRYPT + " (x, k), k) = x"));
-
- this.spec.addDeclaration (new ProVerifComment ("Diffie-Hellman"));
- this.spec.addDeclaration (new ProVerifFunc (DH_DH, new String[] {"bitstring", "bitstring"}, "bitstring"));
- this.spec.addDeclaration (new ProVerifEquation (new ProVerifVar[] {new ProVerifVar ("x", "bitstring"), new ProVerifVar ("y", "bitstring")}, DH_DH + " (" + PK_PK + " (x), y) = " + DH_DH + " (" + PK_PK + " (y), x)"));
-
- this.spec.addDeclaration (new ProVerifComment ("MAC"));
- this.spec.addDeclaration (new ProVerifFunc (MAC_MAC, new String[] {"bitstring", "bitstring"}, "bitstring"));
- this.spec.addDeclaration (new ProVerifFunc (MAC_VERIFYMAC, new String[] {"bitstring", "bitstring", "bitstring"}, "bitstring",
- new ProVerifReduc (new ProVerifVar[] {new ProVerifVar ("m", "bitstring"), new ProVerifVar ("k", "bitstring")}, MAC_VERIFYMAC + " (m, k, " + MAC_MAC + " (m, k)) = " + TRUE,
- new ProVerifReduc (new ProVerifVar[] {new ProVerifVar ("m", "bitstring"), new ProVerifVar ("m2", "bitstring"), new ProVerifVar ("k", "bitstring")}, MAC_VERIFYMAC + " (m, k, m2) = " + FALSE))));
-
- this.spec.addDeclaration (new ProVerifComment ("HASH"));
- this.spec.addDeclaration (new ProVerifFunc (HASH_HASH, new String[] {"bitstring"}, "bitstring"));
-
- this.spec.addDeclaration (new ProVerifComment ("Channel"));
- this.spec.addDeclaration (new ProVerifVar (CH_MAINCH, "channel"));
+ this.spec.addDeclaration(new ProVerifProperty("abbreviateDerivation = false"));
+ this.spec.addDeclaration(new ProVerifComment("Boolean return types"));
+ this.spec.addDeclaration(new ProVerifConst(TRUE, "bitstring"));
+ this.spec.addDeclaration(new ProVerifConst(FALSE, "bitstring"));
+ this.spec.addDeclaration(new ProVerifComment("Functions data"));
+ this.spec.addDeclaration(new ProVerifConst(UNKNOWN, "bitstring"));
+
+ this.spec.addDeclaration(new ProVerifComment("Public key cryptography"));
+ this.spec.addDeclaration(new ProVerifFunc(PK_PK, new String[]{"bitstring"}, "bitstring"));
+ this.spec.addDeclaration(new ProVerifFunc(PK_ENCRYPT, new String[]{"bitstring", "bitstring"}, "bitstring"));
+ this.spec.addDeclaration(new ProVerifReduc(new ProVerifVar[]{new ProVerifVar("x", "bitstring"), new ProVerifVar("y", "bitstring")}, PK_DECRYPT + " (" + PK_ENCRYPT + " (x, " + PK_PK + " (y)), y) = x"));
+ this.spec.addDeclaration(new ProVerifFunc(PK_SIGN, new String[]{"bitstring", "bitstring"}, "bitstring"));
+ this.spec.addDeclaration(new ProVerifFunc(PK_VERIFYSIGN, new String[]{"bitstring", "bitstring", "bitstring"}, "bitstring",
+ new ProVerifReduc(new ProVerifVar[]{new ProVerifVar("m", "bitstring"), new ProVerifVar("sk", "bitstring")}, PK_VERIFYSIGN + " (m, " + PK_SIGN + " (m, sk), " + PK_PK + " (sk)) = " + TRUE,
+ new ProVerifReduc(new ProVerifVar[]{new ProVerifVar("m", "bitstring"), new ProVerifVar("m2", "bitstring"), new ProVerifVar("ppk", "bitstring")}, PK_VERIFYSIGN + " (m, m2, ppk) = " + FALSE))));
+
+
+ this.spec.addDeclaration(new ProVerifComment("Certificates"));
+ this.spec.addDeclaration(new ProVerifFunc(CERT_CERT, new String[]{"bitstring", "bitstring"}, "bitstring"));
+ this.spec.addDeclaration(new ProVerifFunc(CERT_VERIFYCERT, new String[]{"bitstring", "bitstring"}, "bitstring",
+ new ProVerifReduc(new ProVerifVar[]{new ProVerifVar("epk", "bitstring"), new ProVerifVar("sk", "bitstring")}, CERT_VERIFYCERT + " (" + CERT_CERT + " (epk, " + PK_SIGN + " (epk, sk)), " + PK_PK + " (sk)) = " + TRUE,
+ new ProVerifReduc(new ProVerifVar[]{new ProVerifVar("m", "bitstring"), new ProVerifVar("ppk", "bitstring")}, CERT_VERIFYCERT + " (m, ppk) = " + FALSE))));
+ this.spec.addDeclaration(new ProVerifReduc(new ProVerifVar[]{new ProVerifVar("epk", "bitstring"), new ProVerifVar("sk", "bitstring")}, CERT_GETPK + " (" + CERT_CERT + " (epk, " + PK_SIGN + " (epk,sk))) = epk"));
+
+ this.spec.addDeclaration(new ProVerifComment("Symmetric key cryptography"));
+ this.spec.addDeclaration(new ProVerifFunc(SK_ENCRYPT, new String[]{"bitstring", "bitstring"}, "bitstring"));
+ this.spec.addDeclaration(new ProVerifReduc(new ProVerifVar[]{new ProVerifVar("x", "bitstring"), new ProVerifVar("k", "bitstring")}, SK_DECRYPT + " (" + SK_ENCRYPT + " (x, k), k) = x"));
+
+ this.spec.addDeclaration(new ProVerifComment("Diffie-Hellman"));
+ this.spec.addDeclaration(new ProVerifFunc(DH_DH, new String[]{"bitstring", "bitstring"}, "bitstring"));
+ this.spec.addDeclaration(new ProVerifEquation(new ProVerifVar[]{new ProVerifVar("x", "bitstring"), new ProVerifVar("y", "bitstring")}, DH_DH + " (" + PK_PK + " (x), y) = " + DH_DH + " (" + PK_PK + " (y), x)"));
+
+ this.spec.addDeclaration(new ProVerifComment("MAC"));
+ this.spec.addDeclaration(new ProVerifFunc(MAC_MAC, new String[]{"bitstring", "bitstring"}, "bitstring"));
+ this.spec.addDeclaration(new ProVerifFunc(MAC_VERIFYMAC, new String[]{"bitstring", "bitstring", "bitstring"}, "bitstring",
+ new ProVerifReduc(new ProVerifVar[]{new ProVerifVar("m", "bitstring"), new ProVerifVar("k", "bitstring")}, MAC_VERIFYMAC + " (m, k, " + MAC_MAC + " (m, k)) = " + TRUE,
+ new ProVerifReduc(new ProVerifVar[]{new ProVerifVar("m", "bitstring"), new ProVerifVar("m2", "bitstring"), new ProVerifVar("k", "bitstring")}, MAC_VERIFYMAC + " (m, k, m2) = " + FALSE))));
+
+ this.spec.addDeclaration(new ProVerifComment("HASH"));
+ this.spec.addDeclaration(new ProVerifFunc(HASH_HASH, new String[]{"bitstring"}, "bitstring"));
+
+ this.spec.addDeclaration(new ProVerifComment("Channel"));
+ this.spec.addDeclaration(new ProVerifVar(CH_MAINCH, "channel"));
// TODO: add one encryption function per signal
- for (AvatarRelation ar: this.avspec.getRelations ())
- if (ar.isPrivate ()) {
- int nbOfSignals = ar.nbOfSignals ();
+ for (AvatarRelation ar : this.avspec.getRelations())
+ if (ar.isPrivate()) {
+ int nbOfSignals = ar.nbOfSignals();
int i;
- for (i=0; i<nbOfSignals; i++) {
- String name = ar.getBlock1().getName() + ar.getSignal1 (i).getName () + "__" + ar.getBlock2().getName() + ar.getSignal2 (i).getName ();
- this.spec.addDeclaration (new ProVerifFunc (CH_ENCRYPT + name, new String[] {"bitstring"}, "bitstring", true));
- this.spec.addDeclaration (new ProVerifReduc (new ProVerifVar[] {new ProVerifVar ("x", "bitstring")}, CH_DECRYPT + name + " (" + CH_ENCRYPT + name + " (x)) = x", true));
+ for (i = 0; i < nbOfSignals; i++) {
+ String name = ar.getBlock1().getName() + ar.getSignal1(i).getName() + "__" + ar.getBlock2().getName() + ar.getSignal2(i).getName();
+ this.spec.addDeclaration(new ProVerifFunc(CH_ENCRYPT + name, new String[]{"bitstring"}, "bitstring", true));
+ this.spec.addDeclaration(new ProVerifReduc(new ProVerifVar[]{new ProVerifVar("x", "bitstring")}, CH_DECRYPT + name + " (" + CH_ENCRYPT + name + " (x)) = x", true));
}
}
- this.spec.addDeclaration (new ProVerifComment ("Control Channel"));
- this.spec.addDeclaration (new ProVerifVar (CHCTRL_CH, "channel"));
- this.spec.addDeclaration (new ProVerifFunc (CHCTRL_ENCRYPT, new String[] {"bitstring"}, "bitstring", true));
- this.spec.addDeclaration (new ProVerifReduc (new ProVerifVar[] {new ProVerifVar ("x", "bitstring")}, CHCTRL_DECRYPT + " (" + CHCTRL_ENCRYPT + " (x)) = x", true));
+ this.spec.addDeclaration(new ProVerifComment("Control Channel"));
+ this.spec.addDeclaration(new ProVerifVar(CHCTRL_CH, "channel"));
+ this.spec.addDeclaration(new ProVerifFunc(CHCTRL_ENCRYPT, new String[]{"bitstring"}, "bitstring", true));
+ this.spec.addDeclaration(new ProVerifReduc(new ProVerifVar[]{new ProVerifVar("x", "bitstring")}, CHCTRL_DECRYPT + " (" + CHCTRL_ENCRYPT + " (x)) = x", true));
- this.spec.addDeclaration (new ProVerifComment ("Basic Peano Arithmetic"));
- this.spec.addDeclaration (new ProVerifConst (ZERO, "bitstring"));
- this.spec.addDeclaration (new ProVerifFunc (PEANO_N, new String[] {"bitstring"}, "bitstring"));
+ this.spec.addDeclaration(new ProVerifComment("Basic Peano Arithmetic"));
+ this.spec.addDeclaration(new ProVerifConst(ZERO, "bitstring"));
+ this.spec.addDeclaration(new ProVerifFunc(PEANO_N, new String[]{"bitstring"}, "bitstring"));
/* Declare all the call*** variables */
List<AvatarBlock> blocks = this.avspec.getListOfBlocks();
- // String action = "(";
- for(AvatarBlock block: blocks) {
- Map<AvatarStateMachineElement, Integer> simplifiedElements = block.getStateMachine ().getSimplifiedElements ();
- if (simplifiedElements.get (block.getStateMachine ().getStartState ()) == null)
- simplifiedElements.put (block.getStateMachine ().getStartState (), Integer.valueOf(0));
-
- for (AvatarStateMachineElement asme: simplifiedElements.keySet ())
- this.spec.addDeclaration (new ProVerifVar ("call" + ATTR_DELIM + block.getName() + ATTR_DELIM + simplifiedElements.get (asme), "bitstring", true));
+ // String action = "(";
+ for (AvatarBlock block : blocks) {
+ Map<AvatarStateMachineElement, Integer> simplifiedElements = block.getStateMachine().getSimplifiedElements();
+ if (simplifiedElements.get(block.getStateMachine().getStartState()) == null)
+ simplifiedElements.put(block.getStateMachine().getStartState(), Integer.valueOf(0));
+
+ for (AvatarStateMachineElement asme : simplifiedElements.keySet())
+ this.spec.addDeclaration(new ProVerifVar("call" + ATTR_DELIM + block.getName() + ATTR_DELIM + simplifiedElements.get(asme), "bitstring", true));
}
- this.spec.addDeclaration (new ProVerifComment ("Constants"));
- TraceManager.addDev("Constants");
- for (AvatarPragma pragma: this.avspec.getPragmas ())
+ this.spec.addDeclaration(new ProVerifComment("Constants"));
+ //TraceManager.addDev("Constants");
+ for (AvatarPragma pragma : this.avspec.getPragmas())
if (pragma instanceof AvatarPragmaConstant)
- for (AvatarConstant constant: ((AvatarPragmaConstant) pragma).getConstants ()) {
- String constName = constant.getName ();
- TraceManager.addDev("| " + constName);
- this.spec.addDeclaration (new ProVerifVar (constName, "bitstring", ! ((AvatarPragmaConstant) pragma).isPublic ()));
+ for (AvatarConstant constant : ((AvatarPragmaConstant) pragma).getConstants()) {
+ String constName = constant.getName();
+ //TraceManager.addDev("| " + constName);
+ this.spec.addDeclaration(new ProVerifVar(constName, "bitstring", !((AvatarPragmaConstant) pragma).isPublic()));
}
/* Secrecy Assumptions */
- this.secrecyChecked = new HashSet<AvatarAttribute> ();
+ this.secrecyChecked = new HashSet<AvatarAttribute>();
- this.spec.addDeclaration (new ProVerifComment ("Secrecy Assumptions"));
- TraceManager.addDev("Secrecy Assumptions");
- for (AvatarPragma pragma: this.avspec.getPragmas ())
+ this.spec.addDeclaration(new ProVerifComment("Secrecy Assumptions"));
+ //TraceManager.addDev("Secrecy Assumptions");
+ for (AvatarPragma pragma : this.avspec.getPragmas())
if (pragma instanceof AvatarPragmaSecrecyAssumption)
- for (AvatarAttribute attribute: ((AvatarPragmaSecrecyAssumption) pragma).getArgs ()) {
- AvatarAttribute trueAttr = this.nameEquivalence.get (attribute);
+ for (AvatarAttribute attribute : ((AvatarPragmaSecrecyAssumption) pragma).getArgs()) {
+ AvatarAttribute trueAttr = this.nameEquivalence.get(attribute);
if (trueAttr == null)
trueAttr = attribute;
- if (this.secrecyChecked.contains (trueAttr))
+ if (this.secrecyChecked.contains(trueAttr))
continue;
- String name = AVATAR2ProVerif.translateTerm (trueAttr, null);
- TraceManager.addDev("| " + name);
+ String name = AVATAR2ProVerif.translateTerm(trueAttr, null);
+ //TraceManager.addDev("| " + name);
// TODO: this doesn't work. Replacing by an attacker(...) query
// this.spec.addDeclaration (new ProVerifSecrecyAssum (name));
- this.spec.addDeclaration (new ProVerifQueryAtt (name, true));
+ this.spec.addDeclaration(new ProVerifQueryAtt(name, true));
- this.secrecyChecked.add (trueAttr);
+ this.secrecyChecked.add(trueAttr);
}
/* Queries */
- this.spec.addDeclaration (new ProVerifComment ("Queries Secret"));
- TraceManager.addDev("Queries Secret");
- for (AvatarPragma pragma: this.avspec.getPragmas ())
- if (pragma instanceof AvatarPragmaSecret)
- {
- AvatarAttribute attribute = ((AvatarPragmaSecret) pragma).getArg ();
- AvatarAttribute trueAttr = this.nameEquivalence.get (attribute);
+ this.spec.addDeclaration(new ProVerifComment("Queries Secret"));
+ //TraceManager.addDev("Queries Secret");
+ for (AvatarPragma pragma : this.avspec.getPragmas())
+ if (pragma instanceof AvatarPragmaSecret) {
+ AvatarAttribute attribute = ((AvatarPragmaSecret) pragma).getArg();
+ AvatarAttribute trueAttr = this.nameEquivalence.get(attribute);
if (trueAttr == null)
trueAttr = attribute;
- if (this.secrecyChecked.contains (trueAttr))
+ if (this.secrecyChecked.contains(trueAttr))
continue;
- String varName = AVATAR2ProVerif.translateTerm (trueAttr, null);
- this.spec.addDeclaration (new ProVerifQueryAtt (varName, true));
-
- TraceManager.addDev("| attacker (" + varName + ")");
+ String varName = AVATAR2ProVerif.translateTerm(trueAttr, null);
+ this.spec.addDeclaration(new ProVerifQueryAtt(varName, true));
- this.secrecyChecked.add (trueAttr);
+ //TraceManager.addDev("| attacker (" + varName + ")");
+
+ this.secrecyChecked.add(trueAttr);
}
// Queries for states
- TraceManager.addDev ("Queries Event (" + (this.stateReachability == JDialogProverifVerification.REACHABILITY_ALL ? "ALL" : this.stateReachability == JDialogProverifVerification.REACHABILITY_SELECTED ? "SELECTED" : "NONE") + ")");
+ //TraceManager.addDev ("Queries Event (" + (this.stateReachability == JDialogProverifVerification.REACHABILITY_ALL ? "ALL" :
+ // this.stateReachability == JDialogProverifVerification.REACHABILITY_SELECTED ? "SELECTED" : "NONE") + ")");
if (this.stateReachability != JDialogProverifVerification.REACHABILITY_NONE) {
- this.spec.addDeclaration (new ProVerifComment ("Queries Event"));
- for (AvatarBlock block: this.avspec.getListOfBlocks ()) {
- HashSet<AvatarStateMachineElement> visited = new HashSet<AvatarStateMachineElement> ();
- LinkedList<AvatarStateMachineElement> toVisit = new LinkedList<AvatarStateMachineElement> ();
- toVisit.add (block.getStateMachine ().getStartState ());
- while (! toVisit.isEmpty ()) {
- AvatarStateMachineElement asme = toVisit.remove ();
- if (visited.contains (asme))
+ this.spec.addDeclaration(new ProVerifComment("Queries Event"));
+ for (AvatarBlock block : this.avspec.getListOfBlocks()) {
+ HashSet<AvatarStateMachineElement> visited = new HashSet<AvatarStateMachineElement>();
+ LinkedList<AvatarStateMachineElement> toVisit = new LinkedList<AvatarStateMachineElement>();
+ toVisit.add(block.getStateMachine().getStartState());
+ while (!toVisit.isEmpty()) {
+ AvatarStateMachineElement asme = toVisit.remove();
+ if (visited.contains(asme))
continue;
- visited.add (asme);
+ visited.add(asme);
- if (asme instanceof AvatarState && (this.stateReachability == JDialogProverifVerification.REACHABILITY_ALL || asme.isCheckable ())) {
- this.spec.addDeclaration (new ProVerifQueryEv (new ProVerifVar[] {}, "enteringState" + ATTR_DELIM + block.getName() + ATTR_DELIM + asme.getName()));
- this.spec.addDeclaration (new ProVerifEvDecl ("enteringState" + ATTR_DELIM + block.getName() + ATTR_DELIM + asme.getName(), new String[] {}));
- TraceManager.addDev("| event (enteringState" + ATTR_DELIM + block.getName() + ATTR_DELIM + asme.getName() + ")");
+ if (asme instanceof AvatarState && (this.stateReachability == JDialogProverifVerification.REACHABILITY_ALL || asme.isCheckable())) {
+ this.spec.addDeclaration(new ProVerifQueryEv(new ProVerifVar[]{}, "enteringState" + ATTR_DELIM + block.getName() + ATTR_DELIM + asme.getName()));
+ this.spec.addDeclaration(new ProVerifEvDecl("enteringState" + ATTR_DELIM + block.getName() + ATTR_DELIM + asme.getName(), new String[]{}));
+ //TraceManager.addDev("| event (enteringState" + ATTR_DELIM + block.getName() + ATTR_DELIM + asme.getName() + ")");
}
- for (AvatarStateMachineElement _asme: asme.getNexts ())
- toVisit.add (_asme);
+ for (AvatarStateMachineElement _asme : asme.getNexts())
+ toVisit.add(_asme);
}
}
}
/* Autenticity */
- this.spec.addDeclaration (new ProVerifComment ("Authenticity"));
- TraceManager.addDev ("Authenticity");
- HashSet<String> authenticityEvents = new HashSet<String> ();
- for (AvatarPragma pragma: this.avspec.getPragmas ())
+ this.spec.addDeclaration(new ProVerifComment("Authenticity"));
+ //TraceManager.addDev ("Authenticity");
+ HashSet<String> authenticityEvents = new HashSet<String>();
+ for (AvatarPragma pragma : this.avspec.getPragmas())
if (pragma instanceof AvatarPragmaAuthenticity) {
- AvatarAttributeState attrA = ((AvatarPragmaAuthenticity) pragma).getAttrA ();
- AvatarAttributeState attrB = ((AvatarPragmaAuthenticity) pragma).getAttrB ();
+ AvatarAttributeState attrA = ((AvatarPragmaAuthenticity) pragma).getAttrA();
+ AvatarAttributeState attrB = ((AvatarPragmaAuthenticity) pragma).getAttrB();
if (attrA != null && attrB != null) {
- String sA = AVATAR2ProVerif.makeAttrName (attrA.getAttribute ().getBlock ().getName (), attrA.getAttribute ().getName (), attrA.getState ().getName ());
- String sB = AVATAR2ProVerif.makeAttrName (attrB.getAttribute ().getBlock ().getName (), attrB.getAttribute ().getName (), attrB.getState ().getName ());
- TraceManager.addDev("| authenticity" + ATTR_DELIM + sB + " (dummyM) ==> authenticity" + ATTR_DELIM + sA + " (dummyM)");
- if (!authenticityEvents.contains (sA)) {
- authenticityEvents.add (sA);
- spec.addDeclaration (new ProVerifEvDecl ("authenticity" + ATTR_DELIM + sA, new String[] {"bitstring"}));
+ String sA = AVATAR2ProVerif.makeAttrName(attrA.getAttribute().getBlock().getName(), attrA.getAttribute().getName(), attrA.getState().getName());
+ String sB = AVATAR2ProVerif.makeAttrName(attrB.getAttribute().getBlock().getName(), attrB.getAttribute().getName(), attrB.getState().getName());
+ //TraceManager.addDev("| authenticity" + ATTR_DELIM + sB + " (dummyM) ==> authenticity" + ATTR_DELIM + sA + " (dummyM)");
+ if (!authenticityEvents.contains(sA)) {
+ authenticityEvents.add(sA);
+ spec.addDeclaration(new ProVerifEvDecl("authenticity" + ATTR_DELIM + sA, new String[]{"bitstring"}));
}
- if (!authenticityEvents.contains (sB)) {
- authenticityEvents.add (sB);
- spec.addDeclaration (new ProVerifEvDecl ("authenticity" + ATTR_DELIM + sB, new String[] {"bitstring"}));
+ if (!authenticityEvents.contains(sB)) {
+ authenticityEvents.add(sB);
+ spec.addDeclaration(new ProVerifEvDecl("authenticity" + ATTR_DELIM + sB, new String[]{"bitstring"}));
}
- spec.addDeclaration (new ProVerifQueryEvinj (new ProVerifVar[] {new ProVerifVar ("dummyM", "bitstring")}, "authenticity" + ATTR_DELIM + sB + " (dummyM)", "authenticity" + ATTR_DELIM + sA + " (dummyM)"));
+ spec.addDeclaration(new ProVerifQueryEvinj(new ProVerifVar[]{new ProVerifVar("dummyM", "bitstring")}, "authenticity" + ATTR_DELIM + sB + " (dummyM)", "authenticity" + ATTR_DELIM + sA + " (dummyM)"));
}
}
}
private List<AvatarAttribute> makeStartingProcess() {
- TraceManager.addDev("\n\n=+=+=+ Making Starting Process +=+=+=");
+ //TraceManager.addDev("\n\n=+=+=+ Making Starting Process +=+=+=");
// Create starting process
- ProVerifProcess p = new ProVerifProcess("starting" + ATTR_DELIM, new ProVerifVar[] {});
+ ProVerifProcess p = new ProVerifProcess("starting" + ATTR_DELIM, new ProVerifVar[]{});
ProVerifProcInstr lastInstr = p;
// Get all the blocks
List<AvatarBlock> blocks = avspec.getListOfBlocks();
// Used to store the names that are public keys
- this.pubs = new HashMap<AvatarAttribute, AvatarAttribute> ();
- for (AvatarPragma pragma: this.avspec.getPragmas ())
+ this.pubs = new HashMap<AvatarAttribute, AvatarAttribute>();
+ for (AvatarPragma pragma : this.avspec.getPragmas())
if (pragma instanceof AvatarPragmaPrivatePublicKey)
- this.pubs.put (((AvatarPragmaPrivatePublicKey) pragma).getPublicKey (), ((AvatarPragmaPrivatePublicKey) pragma).getPrivateKey ());
+ this.pubs.put(((AvatarPragmaPrivatePublicKey) pragma).getPublicKey(), ((AvatarPragmaPrivatePublicKey) pragma).getPrivateKey());
//String blockName, paramName;
// Store all the names that are system knowledge
// Enable to raise warning when an attribute is both system and session knowledge
- List<AvatarAttribute> systemKnowledge = new LinkedList<AvatarAttribute> ();
+ List<AvatarAttribute> systemKnowledge = new LinkedList<AvatarAttribute>();
- this.nameEquivalence = new HashMap<AvatarAttribute, AvatarAttribute> ();
+ this.nameEquivalence = new HashMap<AvatarAttribute, AvatarAttribute>();
- TraceManager.addDev("Finding constants");
- for (AvatarBlock block: blocks)
- for (AvatarAttribute attr: block.getAttributes ())
- if (this.avspec.getAvatarConstantWithName (attr.getName ()) != null) {
- if (attr.isInt () || attr.isBool ()) {
- lastInstr = lastInstr.setNextInstr (new ProVerifProcLet (new ProVerifVar[] {new ProVerifVar (AVATAR2ProVerif.translateTerm (attr, null), "bitstring")}, attr.getName ()));
- systemKnowledge.add (attr);
+ //TraceManager.addDev("Finding constants");
+ for (AvatarBlock block : blocks)
+ for (AvatarAttribute attr : block.getAttributes())
+ if (this.avspec.getAvatarConstantWithName(attr.getName()) != null) {
+ if (attr.isInt() || attr.isBool()) {
+ lastInstr = lastInstr.setNextInstr(new ProVerifProcLet(new ProVerifVar[]{new ProVerifVar(AVATAR2ProVerif.translateTerm(attr, null), "bitstring")}, attr.getName()));
+ systemKnowledge.add(attr);
} else {
- UICheckingError ce = new UICheckingError(CheckingError.BEHAVIOR_ERROR, "Attribute " + attr.getBlock ().getName () + "." + attr.getName () + " should be of type int or bool to be considered as a constant.");
- ce.setTDiagramPanel(((AvatarDesignPanel)(avspec.getReferenceObject())).getAvatarBDPanel());
- ce.setTGComponent((TGComponent)attr.getReferenceObject());
+ UICheckingError ce = new UICheckingError(CheckingError.BEHAVIOR_ERROR, "Attribute " + attr.getBlock().getName() + "." + attr.getName() + " should be of type int or bool to be considered as a constant.");
+ ce.setTDiagramPanel(((AvatarDesignPanel) (avspec.getReferenceObject())).getAvatarBDPanel());
+ ce.setTGComponent((TGComponent) attr.getReferenceObject());
warnings.add(ce);
continue;
}
}
- TraceManager.addDev("Finding system knowledge");
- for (AvatarPragma pragma: this.avspec.getPragmas ())
+ //TraceManager.addDev("Finding system knowledge");
+ for (AvatarPragma pragma : this.avspec.getPragmas())
// Check if pragma is system initial knowledge
- if (pragma instanceof AvatarPragmaInitialKnowledge && ((AvatarPragmaInitialKnowledge) pragma).isSystem ()) {
+ if (pragma instanceof AvatarPragmaInitialKnowledge && ((AvatarPragmaInitialKnowledge) pragma).isSystem()) {
AvatarAttribute first = null;
AvatarAttribute containsPublicKey = null;
- for (AvatarAttribute arg: ((AvatarPragmaInitialKnowledge) pragma).getArgs ()) {
+ for (AvatarAttribute arg : ((AvatarPragmaInitialKnowledge) pragma).getArgs()) {
// ignore if the attribute was already declared
- if (systemKnowledge.contains (arg)) {
- UICheckingError ce = new UICheckingError(CheckingError.BEHAVIOR_ERROR, "Attribute " + arg.getBlock ().getName () + "." + arg.getName () + " already appears in another initial knowledge pragma or is a constant (ignored).");
- // ce.setTDiagramPanel(((AvatarDesignPanel)(avspec.getReferenceObject())).getAvatarBDPanel());
- ce.setTGComponent((TGComponent)pragma.getReferenceObject());
+ if (systemKnowledge.contains(arg)) {
+ UICheckingError ce = new UICheckingError(CheckingError.BEHAVIOR_ERROR, "Attribute " + arg.getBlock().getName() + "." + arg.getName() + " already appears in another initial knowledge pragma or is a constant (ignored).");
+ // ce.setTDiagramPanel(((AvatarDesignPanel)(avspec.getReferenceObject())).getAvatarBDPanel());
+ ce.setTGComponent((TGComponent) pragma.getReferenceObject());
warnings.add(ce);
continue;
}
@@ -703,29 +690,29 @@ public class AVATAR2ProVerif implements AvatarTranslator {
// Check if it is the first from the list
if (first == null) {
first = arg;
- this.nameEquivalence.put (first, first);
+ this.nameEquivalence.put(first, first);
- AvatarAttribute privateK = this.pubs.get (arg);
+ AvatarAttribute privateK = this.pubs.get(arg);
// Check if it is a public key
if (privateK != null) {
- String privateKStr = AVATAR2ProVerif.translateTerm (privateK, null);
+ String privateKStr = AVATAR2ProVerif.translateTerm(privateK, null);
// Check if the corresponding private key has already been declared
- if (!systemKnowledge.contains (privateK)) {
- this.nameEquivalence.put (privateK, privateK);
- lastInstr = lastInstr.setNextInstr (new ProVerifProcNew (privateKStr, "bitstring"));
- systemKnowledge.add (privateK);
+ if (!systemKnowledge.contains(privateK)) {
+ this.nameEquivalence.put(privateK, privateK);
+ lastInstr = lastInstr.setNextInstr(new ProVerifProcNew(privateKStr, "bitstring"));
+ systemKnowledge.add(privateK);
}
- containsPublicKey = this.nameEquivalence.get (privateK);
+ containsPublicKey = this.nameEquivalence.get(privateK);
// Let the public key
- lastInstr = lastInstr.setNextInstr (new ProVerifProcLet (new ProVerifVar[] {new ProVerifVar (AVATAR2ProVerif.translateTerm (first, null), "bitstring")}, PK_PK + "(" + privateKStr + ")"));
+ lastInstr = lastInstr.setNextInstr(new ProVerifProcLet(new ProVerifVar[]{new ProVerifVar(AVATAR2ProVerif.translateTerm(first, null), "bitstring")}, PK_PK + "(" + privateKStr + ")"));
// Make the public key public
- tmpInstr = new ProVerifProcRaw ("out (" + CH_MAINCH + ", " + AVATAR2ProVerif.translateTerm (first, null) + ");");
+ tmpInstr = new ProVerifProcRaw("out (" + CH_MAINCH + ", " + AVATAR2ProVerif.translateTerm(first, null) + ");");
} else
- tmpInstr = new ProVerifProcNew (AVATAR2ProVerif.translateTerm (first, null), "bitstring");
+ tmpInstr = new ProVerifProcNew(AVATAR2ProVerif.translateTerm(first, null), "bitstring");
} else {
- AvatarAttribute privateK = this.pubs.get (arg);
+ AvatarAttribute privateK = this.pubs.get(arg);
// If there is a public key in the middle, ignore it
if (privateK != null) {
@@ -736,72 +723,72 @@ public class AVATAR2ProVerif implements AvatarTranslator {
continue;
}
- String str = AVATAR2ProVerif.translateTerm (arg, null);
+ String str = AVATAR2ProVerif.translateTerm(arg, null);
if (containsPublicKey != null)
- tmpInstr = new ProVerifProcLet (new ProVerifVar[] {new ProVerifVar (str, "bitstring")}, PK_PK + "(" + AVATAR2ProVerif.translateTerm (containsPublicKey, null) + ")");
+ tmpInstr = new ProVerifProcLet(new ProVerifVar[]{new ProVerifVar(str, "bitstring")}, PK_PK + "(" + AVATAR2ProVerif.translateTerm(containsPublicKey, null) + ")");
else {
- tmpInstr = new ProVerifProcLet (new ProVerifVar[] {new ProVerifVar (str, "bitstring")}, AVATAR2ProVerif.translateTerm (first, null));
- this.nameEquivalence.put (arg, first);
+ tmpInstr = new ProVerifProcLet(new ProVerifVar[]{new ProVerifVar(str, "bitstring")}, AVATAR2ProVerif.translateTerm(first, null));
+ this.nameEquivalence.put(arg, first);
}
}
- TraceManager.addDev("| Initial system knowledge pragma: " + AVATAR2ProVerif.translateTerm (first, null));
- lastInstr = lastInstr.setNextInstr (tmpInstr);
- systemKnowledge.add (arg);
+ //TraceManager.addDev("| Initial system knowledge pragma: " + AVATAR2ProVerif.translateTerm (first, null));
+ lastInstr = lastInstr.setNextInstr(tmpInstr);
+ systemKnowledge.add(arg);
}
}
// Call all the processes corresponding to crossroads in the state machine
- ProVerifProcRawGlobing globing = new ProVerifProcRawGlobing ("! (", ")");
- lastInstr.setNextInstr (globing);
- lastInstr = globing.getIntra ();
+ ProVerifProcRawGlobing globing = new ProVerifProcRawGlobing("! (", ")");
+ lastInstr.setNextInstr(globing);
+ lastInstr = globing.getIntra();
- lastInstr = lastInstr.setNextInstr (new ProVerifProcNew ("sessionID", "bitstring"));
+ lastInstr = lastInstr.setNextInstr(new ProVerifProcNew("sessionID", "bitstring"));
- ProVerifProcParallel paral = new ProVerifProcParallel ();
- lastInstr = lastInstr.setNextInstr (paral);
+ ProVerifProcParallel paral = new ProVerifProcParallel();
+ lastInstr = lastInstr.setNextInstr(paral);
- for(AvatarBlock block: blocks) {
- Map<AvatarStateMachineElement, Integer> simplifiedElements = block.getStateMachine ().getSimplifiedElements ();
+ for (AvatarBlock block : blocks) {
+ Map<AvatarStateMachineElement, Integer> simplifiedElements = block.getStateMachine().getSimplifiedElements();
- if (simplifiedElements.get (block.getStateMachine ().getStartState ()) == null)
- paral.addInstr (new ProVerifProcCall (block.getName () + ATTR_DELIM + "0", new ProVerifVar[] {new ProVerifVar ("sessionID", "bitstring")}));
+ if (simplifiedElements.get(block.getStateMachine().getStartState()) == null)
+ paral.addInstr(new ProVerifProcCall(block.getName() + ATTR_DELIM + "0", new ProVerifVar[]{new ProVerifVar("sessionID", "bitstring")}));
- for (AvatarStateMachineElement asme: simplifiedElements.keySet ()) {
- globing = new ProVerifProcRawGlobing ("!", "");
- paral.addInstr (globing);
- globing.getIntra ().setNextInstr (new ProVerifProcCall (block.getName () + ATTR_DELIM + simplifiedElements.get (asme), new ProVerifVar[] {new ProVerifVar ("sessionID", "bitstring")}));
+ for (AvatarStateMachineElement asme : simplifiedElements.keySet()) {
+ globing = new ProVerifProcRawGlobing("!", "");
+ paral.addInstr(globing);
+ globing.getIntra().setNextInstr(new ProVerifProcCall(block.getName() + ATTR_DELIM + simplifiedElements.get(asme), new ProVerifVar[]{new ProVerifVar("sessionID", "bitstring")}));
}
}
- globing = new ProVerifProcRawGlobing ("(", ")");
- paral.addInstr (globing);
- lastInstr = globing.getIntra ();
+ globing = new ProVerifProcRawGlobing("(", ")");
+ paral.addInstr(globing);
+ lastInstr = globing.getIntra();
- TraceManager.addDev("Finding session knowledge");
- LinkedList<AvatarAttribute> sessionKnowledge = new LinkedList<AvatarAttribute> ();
- for (AvatarPragma pragma: this.avspec.getPragmas ())
+ //TraceManager.addDev("Finding session knowledge");
+ LinkedList<AvatarAttribute> sessionKnowledge = new LinkedList<AvatarAttribute>();
+ for (AvatarPragma pragma : this.avspec.getPragmas())
// Check if pragma is session initial knowledge
- if (pragma instanceof AvatarPragmaInitialKnowledge && !((AvatarPragmaInitialKnowledge) pragma).isSystem ()) {
+ if (pragma instanceof AvatarPragmaInitialKnowledge && !((AvatarPragmaInitialKnowledge) pragma).isSystem()) {
AvatarAttribute first = null;
AvatarAttribute containsPublicKey = null;
- for (AvatarAttribute arg: ((AvatarPragmaInitialKnowledge) pragma).getArgs ()) {
+ for (AvatarAttribute arg : ((AvatarPragmaInitialKnowledge) pragma).getArgs()) {
// ignore if the attribute was already declared
- if (sessionKnowledge.contains (arg)) {
- UICheckingError ce = new UICheckingError(CheckingError.BEHAVIOR_ERROR, "Attribute " + arg.getBlock ().getName () + "." + arg.getName () + " already appears in another initial knowledge pragma (ignored).");
- ce.setTDiagramPanel(((AvatarDesignPanel)(avspec.getReferenceObject())).getAvatarBDPanel());
- ce.setTGComponent((TGComponent)pragma.getReferenceObject());
+ if (sessionKnowledge.contains(arg)) {
+ UICheckingError ce = new UICheckingError(CheckingError.BEHAVIOR_ERROR, "Attribute " + arg.getBlock().getName() + "." + arg.getName() + " already appears in another initial knowledge pragma (ignored).");
+ ce.setTDiagramPanel(((AvatarDesignPanel) (avspec.getReferenceObject())).getAvatarBDPanel());
+ ce.setTGComponent((TGComponent) pragma.getReferenceObject());
warnings.add(ce);
continue;
}
// ignore if the attribute was sytem knowledge
- if (systemKnowledge.contains (arg)) {
+ if (systemKnowledge.contains(arg)) {
UICheckingError ce = new UICheckingError(CheckingError.BEHAVIOR_ERROR, "You can't define an attribute as both system and session knowledge.");
- ce.setTDiagramPanel(((AvatarDesignPanel)(this.avspec.getReferenceObject())).getAvatarBDPanel());
- ce.setTGComponent((TGComponent)pragma.getReferenceObject());
+ ce.setTDiagramPanel(((AvatarDesignPanel) (this.avspec.getReferenceObject())).getAvatarBDPanel());
+ ce.setTGComponent((TGComponent) pragma.getReferenceObject());
warnings.add(ce);
continue;
}
@@ -810,68 +797,68 @@ public class AVATAR2ProVerif implements AvatarTranslator {
// Check if it is the first from the list
if (first == null) {
first = arg;
- this.nameEquivalence.put (first, first);
+ this.nameEquivalence.put(first, first);
- AvatarAttribute privateK = this.pubs.get (arg);
+ AvatarAttribute privateK = this.pubs.get(arg);
// Check if it is a public key
if (privateK != null) {
- String privateKStr = AVATAR2ProVerif.translateTerm (privateK, null);
+ String privateKStr = AVATAR2ProVerif.translateTerm(privateK, null);
// Check if the corresponding private key has already been declared
- if (!systemKnowledge.contains (privateK) && !sessionKnowledge.contains (privateK)) {
- this.nameEquivalence.put (privateK, privateK);
- lastInstr = lastInstr.setNextInstr (new ProVerifProcNew (privateKStr, "bitstring"));
- sessionKnowledge.add (privateK);
+ if (!systemKnowledge.contains(privateK) && !sessionKnowledge.contains(privateK)) {
+ this.nameEquivalence.put(privateK, privateK);
+ lastInstr = lastInstr.setNextInstr(new ProVerifProcNew(privateKStr, "bitstring"));
+ sessionKnowledge.add(privateK);
}
- containsPublicKey = this.nameEquivalence.get (privateK);
+ containsPublicKey = this.nameEquivalence.get(privateK);
// Let the public key
- lastInstr = lastInstr.setNextInstr (new ProVerifProcLet (new ProVerifVar[] {new ProVerifVar (AVATAR2ProVerif.translateTerm (first, null), "bitstring")}, PK_PK + "(" + privateKStr + ")"));
+ lastInstr = lastInstr.setNextInstr(new ProVerifProcLet(new ProVerifVar[]{new ProVerifVar(AVATAR2ProVerif.translateTerm(first, null), "bitstring")}, PK_PK + "(" + privateKStr + ")"));
// Make the public key public
- tmpInstr = new ProVerifProcRaw ("out (" + CH_MAINCH + ", " + AVATAR2ProVerif.translateTerm (first, null) + ");");
+ tmpInstr = new ProVerifProcRaw("out (" + CH_MAINCH + ", " + AVATAR2ProVerif.translateTerm(first, null) + ");");
} else
- tmpInstr = new ProVerifProcNew (AVATAR2ProVerif.translateTerm (first, null), "bitstring");
+ tmpInstr = new ProVerifProcNew(AVATAR2ProVerif.translateTerm(first, null), "bitstring");
} else {
- AvatarAttribute privateK = this.pubs.get (arg);
+ AvatarAttribute privateK = this.pubs.get(arg);
// If there is a public key in the middle, ignore it
if (privateK != null) {
UICheckingError ce = new UICheckingError(CheckingError.BEHAVIOR_ERROR, "When defining equality between public keys, " +
"the first to appear in the pragma should be the one belonging to the block that owns the private key.");
- ce.setTDiagramPanel(((AvatarDesignPanel)(this.avspec.getReferenceObject())).getAvatarBDPanel());
- ce.setTGComponent((TGComponent)pragma.getReferenceObject ());
+ ce.setTDiagramPanel(((AvatarDesignPanel) (this.avspec.getReferenceObject())).getAvatarBDPanel());
+ ce.setTGComponent((TGComponent) pragma.getReferenceObject());
warnings.add(ce);
continue;
}
- String str = AVATAR2ProVerif.translateTerm (arg, null);
+ String str = AVATAR2ProVerif.translateTerm(arg, null);
if (containsPublicKey != null)
- tmpInstr = new ProVerifProcLet (new ProVerifVar[] {new ProVerifVar (str, "bitstring")}, PK_PK + "(" + AVATAR2ProVerif.translateTerm (containsPublicKey, null) + ")");
+ tmpInstr = new ProVerifProcLet(new ProVerifVar[]{new ProVerifVar(str, "bitstring")}, PK_PK + "(" + AVATAR2ProVerif.translateTerm(containsPublicKey, null) + ")");
else {
- tmpInstr = new ProVerifProcLet (new ProVerifVar[] {new ProVerifVar (str, "bitstring")}, AVATAR2ProVerif.translateTerm (first, null));
- this.nameEquivalence.put (arg, first);
+ tmpInstr = new ProVerifProcLet(new ProVerifVar[]{new ProVerifVar(str, "bitstring")}, AVATAR2ProVerif.translateTerm(first, null));
+ this.nameEquivalence.put(arg, first);
}
}
- TraceManager.addDev("| Initial session knowledge pragma: " + AVATAR2ProVerif.translateTerm (first, null));
- lastInstr = lastInstr.setNextInstr (tmpInstr);
- sessionKnowledge.add (arg);
+ //TraceManager.addDev("| Initial session knowledge pragma: " + AVATAR2ProVerif.translateTerm (first, null));
+ lastInstr = lastInstr.setNextInstr(tmpInstr);
+ sessionKnowledge.add(arg);
}
}
// Concatenate system and session knowledge
- systemKnowledge.addAll (sessionKnowledge);
+ systemKnowledge.addAll(sessionKnowledge);
- List<ProVerifVar> processArgs = this.getProVerifVarFromAttr (systemKnowledge);
- processArgs.add (new ProVerifVar ("sessionID", "bitstring"));
+ List<ProVerifVar> processArgs = this.getProVerifVarFromAttr(systemKnowledge);
+ processArgs.add(new ProVerifVar("sessionID", "bitstring"));
// Call every start process
- TraceManager.addDev("Finding processes");
- paral = new ProVerifProcParallel ();
- for(AvatarBlock block: blocks)
- paral.addInstr (new ProVerifProcCall (block.getName() + ATTR_DELIM + "start", processArgs.toArray (new ProVerifVar[processArgs.size ()])));
- lastInstr = lastInstr.setNextInstr (paral);
+ //TraceManager.addDev("Finding processes");
+ paral = new ProVerifProcParallel();
+ for (AvatarBlock block : blocks)
+ paral.addInstr(new ProVerifProcCall(block.getName() + ATTR_DELIM + "start", processArgs.toArray(new ProVerifVar[processArgs.size()])));
+ lastInstr = lastInstr.setNextInstr(paral);
// Set main process
spec.setMainProcess(p);
@@ -882,133 +869,133 @@ public class AVATAR2ProVerif implements AvatarTranslator {
/**
* Generate ProVerif code for each process for each Avatar block
*/
- private void makeBlocks( List<AvatarAttribute> allKnowledge) {
- TraceManager.addDev("\n\n=+=+=+ Making Blocks +=+=+=");
+ private void makeBlocks(List<AvatarAttribute> allKnowledge) {
+ //TraceManager.addDev("\n\n=+=+=+ Making Blocks +=+=+=");
List<AvatarBlock> blocks = avspec.getListOfBlocks();
-
- for(AvatarBlock block: blocks)
+
+ for (AvatarBlock block : blocks)
makeBlock(block, allKnowledge);
}
- private List<ProVerifVar> getProVerifVarFromAttr (List<AvatarAttribute> attrs) {
- List<ProVerifVar> result = new LinkedList<ProVerifVar> ();
-
- for(AvatarAttribute aa: attrs)
- result.add (new ProVerifVar (AVATAR2ProVerif.translateTerm (aa, null), "bitstring"));
-
+ private List<ProVerifVar> getProVerifVarFromAttr(List<AvatarAttribute> attrs) {
+ List<ProVerifVar> result = new LinkedList<ProVerifVar>();
+
+ for (AvatarAttribute aa : attrs)
+ result.add(new ProVerifVar(AVATAR2ProVerif.translateTerm(aa, null), "bitstring"));
+
return result;
}
/**
* Compute a list of ProVerifVar corresponding to the attributes of the block
*/
- private ProVerifVar[] getAttributesFromBlock (AvatarBlock ab) {
- List<ProVerifVar> result = this.getProVerifVarFromAttr (ab.getAttributes ());
-
- return result.toArray (new ProVerifVar[result.size ()]);
+ private ProVerifVar[] getAttributesFromBlock(AvatarBlock ab) {
+ List<ProVerifVar> result = this.getProVerifVarFromAttr(ab.getAttributes());
+
+ return result.toArray(new ProVerifVar[result.size()]);
}
/**
* Generate ProVerif code for one Avatar block
*/
private void makeBlock(AvatarBlock ab, List<AvatarAttribute> _allKnowledge) {
- TraceManager.addDev("\nAvatarBlock: " + ab.getName ());
- List<AvatarAttribute> allKnowledge = new LinkedList<AvatarAttribute>( _allKnowledge );//.clone();
+ //TraceManager.addDev("\nAvatarBlock: " + ab.getName ());
+ List<AvatarAttribute> allKnowledge = new LinkedList<AvatarAttribute>(_allKnowledge);//.clone();
// Create first ProVerif process for this block and add it to the ProVerif specification
- List<ProVerifVar> knowledgeArray = this.getProVerifVarFromAttr (allKnowledge);
- List<ProVerifVar> processArgs = new LinkedList<ProVerifVar>( knowledgeArray );//.clone ();
- processArgs.add (new ProVerifVar ("sessionID", "bitstring"));
+ List<ProVerifVar> knowledgeArray = this.getProVerifVarFromAttr(allKnowledge);
+ List<ProVerifVar> processArgs = new LinkedList<ProVerifVar>(knowledgeArray);//.clone ();
+ processArgs.add(new ProVerifVar("sessionID", "bitstring"));
- ProVerifProcInstr lastInstr = new ProVerifProcess(ab.getName() + ATTR_DELIM + "start", processArgs.toArray (new ProVerifVar[processArgs.size ()]));
- spec.addDeclaration (lastInstr);
+ ProVerifProcInstr lastInstr = new ProVerifProcess(ab.getName() + ATTR_DELIM + "start", processArgs.toArray(new ProVerifVar[processArgs.size()]));
+ spec.addDeclaration(lastInstr);
// Create a ProVerif Variable corresponding to each attribute block
- for (AvatarAttribute arg: ab.getAttributes ()) {
+ for (AvatarAttribute arg : ab.getAttributes()) {
// ignore if the attribute was already declared
- if (allKnowledge.contains (arg))
+ if (allKnowledge.contains(arg))
continue;
ProVerifProcInstr tmpInstr;
- String str = AVATAR2ProVerif.translateTerm (arg, null);
+ String str = AVATAR2ProVerif.translateTerm(arg, null);
- AvatarAttribute privateK = this.pubs.get (arg);
+ AvatarAttribute privateK = this.pubs.get(arg);
// Check if it is a public key
if (privateK != null) {
- String privateKStr = AVATAR2ProVerif.translateTerm (privateK, null);
+ String privateKStr = AVATAR2ProVerif.translateTerm(privateK, null);
// Check if the corresponding private key has already been declared
- if (!allKnowledge.contains (privateK)) {
- lastInstr = lastInstr.setNextInstr (new ProVerifProcNew (privateKStr, "bitstring"));
- this.nameEquivalence.put (privateK, privateK);
- allKnowledge.add (privateK);
+ if (!allKnowledge.contains(privateK)) {
+ lastInstr = lastInstr.setNextInstr(new ProVerifProcNew(privateKStr, "bitstring"));
+ this.nameEquivalence.put(privateK, privateK);
+ allKnowledge.add(privateK);
}
// Let the public key
- lastInstr = lastInstr.setNextInstr (new ProVerifProcLet (new ProVerifVar[] {new ProVerifVar (str, "bitstring")}, PK_PK + "(" + privateKStr + ")"));
+ lastInstr = lastInstr.setNextInstr(new ProVerifProcLet(new ProVerifVar[]{new ProVerifVar(str, "bitstring")}, PK_PK + "(" + privateKStr + ")"));
// Make the public key public
- tmpInstr = new ProVerifProcRaw ("out (" + CH_MAINCH + ", " + str + ");");
+ tmpInstr = new ProVerifProcRaw("out (" + CH_MAINCH + ", " + str + ");");
} else {
- tmpInstr = new ProVerifProcNew (str, "bitstring");
- this.nameEquivalence.put (arg, arg);
+ tmpInstr = new ProVerifProcNew(str, "bitstring");
+ this.nameEquivalence.put(arg, arg);
}
- TraceManager.addDev("| AvatarAttribute: " + str);
- lastInstr = lastInstr.setNextInstr (tmpInstr);
- allKnowledge.add (arg);
+ //TraceManager.addDev("| AvatarAttribute: " + str);
+ lastInstr = lastInstr.setNextInstr(tmpInstr);
+ allKnowledge.add(arg);
}
- for (AvatarPragma pragma: this.avspec.getPragmas ())
+ for (AvatarPragma pragma : this.avspec.getPragmas())
if (pragma instanceof AvatarPragmaPublic)
- for (AvatarAttribute attr: ((AvatarPragmaPublic) pragma).getArgs ())
- if (attr.getBlock () == ab)
- lastInstr = lastInstr.setNextInstr ( new ProVerifProcRaw ("out (" + CH_MAINCH + ", " + AVATAR2ProVerif.translateTerm (attr, null) + ");"));
+ for (AvatarAttribute attr : ((AvatarPragmaPublic) pragma).getArgs())
+ if (attr.getBlock() == ab)
+ lastInstr = lastInstr.setNextInstr(new ProVerifProcRaw("out (" + CH_MAINCH + ", " + AVATAR2ProVerif.translateTerm(attr, null) + ");"));
// Call the first "real" process
- this.dummyDataCounter ++;
- String strong = "strong" + ATTR_DELIM + AVATAR2ProVerif.makeAttrName (ab.getName (), "0") + this.dummyDataCounter;
- lastInstr = lastInstr.setNextInstr (new ProVerifProcIn (CHCTRL_CH, new ProVerifVar[] {new ProVerifVar (strong, "bitstring")}));
- String tmp = "out (" + CHCTRL_CH + ", " + CHCTRL_ENCRYPT + " ((sessionID, call" + ATTR_DELIM + ab.getName () + ATTR_DELIM + "0" + ", " + strong;
- for(ProVerifVar aa: this.getAttributesFromBlock (ab))
- tmp += ", " + aa.getName ();
- lastInstr = lastInstr.setNextInstr (new ProVerifProcRaw (tmp + ")))"));
+ this.dummyDataCounter++;
+ String strong = "strong" + ATTR_DELIM + AVATAR2ProVerif.makeAttrName(ab.getName(), "0") + this.dummyDataCounter;
+ lastInstr = lastInstr.setNextInstr(new ProVerifProcIn(CHCTRL_CH, new ProVerifVar[]{new ProVerifVar(strong, "bitstring")}));
+ String tmp = "out (" + CHCTRL_CH + ", " + CHCTRL_ENCRYPT + " ((sessionID, call" + ATTR_DELIM + ab.getName() + ATTR_DELIM + "0" + ", " + strong;
+ for (ProVerifVar aa : this.getAttributesFromBlock(ab))
+ tmp += ", " + aa.getName();
+ lastInstr = lastInstr.setNextInstr(new ProVerifProcRaw(tmp + ")))"));
// Generate a new process for every simplified element of the block's state machine
- Map<AvatarStateMachineElement, Integer> simplifiedElements = ab.getStateMachine ().getSimplifiedElements ();
- if (simplifiedElements.get (ab.getStateMachine ().getStartState ()) == null)
- simplifiedElements.put (ab.getStateMachine ().getStartState (), Integer.valueOf(0));
+ Map<AvatarStateMachineElement, Integer> simplifiedElements = ab.getStateMachine().getSimplifiedElements();
+ if (simplifiedElements.get(ab.getStateMachine().getStartState()) == null)
+ simplifiedElements.put(ab.getStateMachine().getStartState(), Integer.valueOf(0));
- for (AvatarStateMachineElement asme: simplifiedElements.keySet ())
+ for (AvatarStateMachineElement asme : simplifiedElements.keySet())
if (asme != null) {
- HashMap<AvatarAttribute, Integer> attributeCmp = new HashMap<AvatarAttribute, Integer> ();
- for (AvatarAttribute attr: ab.getAttributes ()) {
- TraceManager.addDev ("=== " + attr.getName());
- attributeCmp.put (attr, 0);
+ HashMap<AvatarAttribute, Integer> attributeCmp = new HashMap<AvatarAttribute, Integer>();
+ for (AvatarAttribute attr : ab.getAttributes()) {
+ //TraceManager.addDev ("=== " + attr.getName());
+ attributeCmp.put(attr, 0);
}
// Create the ProVerif process and add it to the ProVerif specification
- ProVerifProcInstr p = new ProVerifProcess(AVATAR2ProVerif.makeAttrName(ab.getName(), simplifiedElements.get (asme).toString ()), new ProVerifVar[] {new ProVerifVar ("sessionID", "bitstring")});
- this.spec.addDeclaration (p);
+ ProVerifProcInstr p = new ProVerifProcess(AVATAR2ProVerif.makeAttrName(ab.getName(), simplifiedElements.get(asme).toString()), new ProVerifVar[]{new ProVerifVar("sessionID", "bitstring")});
+ this.spec.addDeclaration(p);
// Read and decrypt control data: variables sent to the process and the call*** variable
- this.dummyDataCounter ++;
- strong = "strong" + ATTR_DELIM + AVATAR2ProVerif.makeAttrName (ab.getName(), simplifiedElements.get (asme).toString ()) + this.dummyDataCounter;
- p = p.setNextInstr (new ProVerifProcNew (strong, "bitstring"));
- p = p.setNextInstr (new ProVerifProcRaw ("out (" + CHCTRL_CH + ", " + strong + ");"));
- p = p.setNextInstr (new ProVerifProcIn (CHCTRL_CH, new ProVerifVar[] {new ProVerifVar ("chControlData", "bitstring")}));
- LinkedList<ProVerifVar> attributes = new LinkedList<ProVerifVar> ();
- attributes.add (new ProVerifVar ("sessionID", "bitstring", false, true));
- attributes.add (new ProVerifVar ("call" + ATTR_DELIM + ab.getName () + ATTR_DELIM + simplifiedElements.get (asme), "bitstring", false, true));
- attributes.add (new ProVerifVar (strong, "bitstring", false, true));
- for (AvatarAttribute attr: ab.getAttributes ()) {
- Integer c = attributeCmp.get (attr) + 1;
- attributeCmp.put (attr, c);
- attributes.add (new ProVerifVar (AVATAR2ProVerif.translateTerm (attr, attributeCmp), "bitstring"));
+ this.dummyDataCounter++;
+ strong = "strong" + ATTR_DELIM + AVATAR2ProVerif.makeAttrName(ab.getName(), simplifiedElements.get(asme).toString()) + this.dummyDataCounter;
+ p = p.setNextInstr(new ProVerifProcNew(strong, "bitstring"));
+ p = p.setNextInstr(new ProVerifProcRaw("out (" + CHCTRL_CH + ", " + strong + ");"));
+ p = p.setNextInstr(new ProVerifProcIn(CHCTRL_CH, new ProVerifVar[]{new ProVerifVar("chControlData", "bitstring")}));
+ LinkedList<ProVerifVar> attributes = new LinkedList<ProVerifVar>();
+ attributes.add(new ProVerifVar("sessionID", "bitstring", false, true));
+ attributes.add(new ProVerifVar("call" + ATTR_DELIM + ab.getName() + ATTR_DELIM + simplifiedElements.get(asme), "bitstring", false, true));
+ attributes.add(new ProVerifVar(strong, "bitstring", false, true));
+ for (AvatarAttribute attr : ab.getAttributes()) {
+ Integer c = attributeCmp.get(attr) + 1;
+ attributeCmp.put(attr, c);
+ attributes.add(new ProVerifVar(AVATAR2ProVerif.translateTerm(attr, attributeCmp), "bitstring"));
}
- p = p.setNextInstr (new ProVerifProcLet (attributes.toArray (new ProVerifVar[attributes.size()]), CHCTRL_DECRYPT + " (chControlData)"));
+ p = p.setNextInstr(new ProVerifProcLet(attributes.toArray(new ProVerifVar[attributes.size()]), CHCTRL_DECRYPT + " (chControlData)"));
// Create an object that will serve as an argument passed to the translation functions
- ProVerifTranslatorParameter arg = new ProVerifTranslatorParameter ();
+ ProVerifTranslatorParameter arg = new ProVerifTranslatorParameter();
arg.block = ab;
arg.lastInstr = p;
arg.simplifiedElements = simplifiedElements;
@@ -1016,50 +1003,41 @@ public class AVATAR2ProVerif implements AvatarTranslator {
arg.lastASME = null;
// Translate this simplified element
- asme.translate (this, arg);
+ asme.translate(this, arg);
}
}
- class ProVerifTranslatorParameter {
- AvatarBlock block;
- ProVerifProcInstr lastInstr;
- Map<AvatarStateMachineElement, Integer> simplifiedElements;
- Map<AvatarAttribute, Integer> attributeCmp;
- AvatarStateMachineElement lastASME;
- }
-
/**
* Commodity method that translates the transition to the next Avatar state machine element
*/
- private void translateNext (AvatarStateMachineElement next, Object _arg) {
+ private void translateNext(AvatarStateMachineElement next, Object _arg) {
ProVerifTranslatorParameter arg = (ProVerifTranslatorParameter) _arg;
// Check if next is not null
if (next != null) {
// Check if next is the root of a process
- Integer n = arg.simplifiedElements.get (next);
+ Integer n = arg.simplifiedElements.get(next);
if (n != null) {
// If next is the root of a process send the attributes on the control channel
- this.dummyDataCounter ++;
- String strong = "strong" + ATTR_DELIM + AVATAR2ProVerif.makeAttrName (arg.block.getName (), n.toString ()) + this.dummyDataCounter;
- arg.lastInstr = arg.lastInstr.setNextInstr (new ProVerifProcIn (CHCTRL_CH, new ProVerifVar[] {new ProVerifVar (strong, "bitstring")}));
- String tmp = "out (" + CHCTRL_CH + ", " + CHCTRL_ENCRYPT + " ((sessionID, call" + ATTR_DELIM + arg.block.getName () + ATTR_DELIM + n + ", " + strong;
- for(AvatarAttribute aa: arg.block.getAttributes ())
- tmp += ", " + AVATAR2ProVerif.translateTerm (aa, arg.attributeCmp);
-
- arg.lastInstr.setNextInstr (new ProVerifProcRaw (tmp + ")))"));
- }
- else
+ this.dummyDataCounter++;
+ String strong = "strong" + ATTR_DELIM + AVATAR2ProVerif.makeAttrName(arg.block.getName(), n.toString()) + this.dummyDataCounter;
+ arg.lastInstr = arg.lastInstr.setNextInstr(new ProVerifProcIn(CHCTRL_CH, new ProVerifVar[]{new ProVerifVar(strong, "bitstring")}));
+ String tmp = "out (" + CHCTRL_CH + ", " + CHCTRL_ENCRYPT + " ((sessionID, call" + ATTR_DELIM + arg.block.getName() + ATTR_DELIM + n + ", " + strong;
+ for (AvatarAttribute aa : arg.block.getAttributes())
+ tmp += ", " + AVATAR2ProVerif.translateTerm(aa, arg.attributeCmp);
+
+ arg.lastInstr.setNextInstr(new ProVerifProcRaw(tmp + ")))"));
+ } else
// If the next state machine element is not the root of a process, simply translate it
- next.translate (this, arg);
+ next.translate(this, arg);
}
}
/**
* Translation function handling ActionOnSignal states
*/
- public void translateActionOnSignal (AvatarActionOnSignal _asme, Object _arg) {
- TraceManager.addDev("| Action on signal");
+ public void translateActionOnSignal(AvatarActionOnSignal _asme, Object _arg) {
+ //TraceManager.addDev("| Action on signal");
ProVerifTranslatorParameter arg = (ProVerifTranslatorParameter) _arg;
avatartranslator.AvatarSignal as = _asme.getSignal();
@@ -1068,8 +1046,8 @@ public class AVATAR2ProVerif implements AvatarTranslator {
// Check if the channel is private
boolean isPrivate = false;
AvatarRelation ar = this.avspec.getAvatarRelationWithSignal(as);
- int index = ar.getIndexOfSignal (as);
- String name = ar.getBlock1().getName() + ar.getSignal1 (index).getName () + "__" + ar.getBlock2().getName() + ar.getSignal2 (index).getName ();
+ int index = ar.getIndexOfSignal(as);
+ String name = ar.getBlock1().getName() + ar.getSignal1(index).getName() + "__" + ar.getBlock2().getName() + ar.getSignal2(index).getName();
isPrivate = ar.isPrivate();
@@ -1078,14 +1056,14 @@ public class AVATAR2ProVerif implements AvatarTranslator {
// Use a dummy name if no value is sent
if (_asme.getNbOfValues() == 0) {
- this.dummyDataCounter ++;
- _lastInstr = _lastInstr.setNextInstr (new ProVerifProcNew ("data" + ATTR_DELIM + this.dummyDataCounter, "bitstring"));
+ this.dummyDataCounter++;
+ _lastInstr = _lastInstr.setNextInstr(new ProVerifProcNew("data" + ATTR_DELIM + this.dummyDataCounter, "bitstring"));
}
String tmp = "out (" + CH_MAINCH + ", ";
if (isPrivate) {
if (this.allowPrivateChannelDuplication)
- tmp += CH_ENCRYPT + name + " (";
+ tmp += CH_ENCRYPT + name + " (";
else {
this.dummyDataCounter++;
_lastInstr = _lastInstr.setNextInstr(new ProVerifProcIn(CHCTRL_CH, new ProVerifVar[]{new ProVerifVar("strong" + ATTR_DELIM + "priv" + this.dummyDataCounter, "bitstring")}));
@@ -1093,20 +1071,20 @@ public class AVATAR2ProVerif implements AvatarTranslator {
}
}
- if (_asme.getNbOfValues()>1){
- tmp +="(";
+ if (_asme.getNbOfValues() > 1) {
+ tmp += "(";
}
if (_asme.getNbOfValues() == 0)
tmp += "data" + ATTR_DELIM + this.dummyDataCounter;
else {
boolean first = true;
- for(String value: _asme.getValues ()) {
- AvatarTerm term = AvatarTerm.createFromString (arg.block, value);
+ for (String value : _asme.getValues()) {
+ AvatarTerm term = AvatarTerm.createFromString(arg.block, value);
if (term == null || term instanceof AvatarTermRaw) {
UICheckingError ce = new UICheckingError(CheckingError.BEHAVIOR_ERROR, "Unknown term '" + value + "' (ignored)");
- ce.setTDiagramPanel(((AvatarDesignPanel)(this.avspec.getReferenceObject())).getAvatarSMDPanel(arg.block.getName()));
- ce.setTGComponent((TGComponent)(_asme.getReferenceObject()));
+ ce.setTDiagramPanel(((AvatarDesignPanel) (this.avspec.getReferenceObject())).getAvatarSMDPanel(arg.block.getName()));
+ ce.setTGComponent((TGComponent) (_asme.getReferenceObject()));
this.warnings.add(ce);
continue;
}
@@ -1115,7 +1093,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
first = false;
else
tmp += ", ";
- tmp += AVATAR2ProVerif.translateTerm (term, arg.attributeCmp);
+ tmp += AVATAR2ProVerif.translateTerm(term, arg.attributeCmp);
}
}
@@ -1126,44 +1104,44 @@ public class AVATAR2ProVerif implements AvatarTranslator {
}
tmp += ")";
- if (_asme.getNbOfValues()>1){
- tmp +=")";
- }
- TraceManager.addDev("| | " + tmp);
+ if (_asme.getNbOfValues() > 1) {
+ tmp += ")";
+ }
+ //TraceManager.addDev("| | " + tmp);
- _lastInstr = _lastInstr.setNextInstr (new ProVerifProcRaw (tmp, true));
+ _lastInstr = _lastInstr.setNextInstr(new ProVerifProcRaw(tmp, true));
} else {
// If it's an In operation
- LinkedList<ProVerifVar> vars = new LinkedList<ProVerifVar> ();
+ LinkedList<ProVerifVar> vars = new LinkedList<ProVerifVar>();
if (_asme.getNbOfValues() == 0) {
- this.dummyDataCounter ++;
- vars.add (new ProVerifVar ("data" + ATTR_DELIM + this.dummyDataCounter, "bitstring"));
+ this.dummyDataCounter++;
+ vars.add(new ProVerifVar("data" + ATTR_DELIM + this.dummyDataCounter, "bitstring"));
} else
- for(String value: _asme.getValues ()) {
- AvatarTerm term = AvatarTerm.createFromString (arg.block, value);
- if (term == null || ! (term instanceof AvatarAttribute)) {
+ for (String value : _asme.getValues()) {
+ AvatarTerm term = AvatarTerm.createFromString(arg.block, value);
+ if (term == null || !(term instanceof AvatarAttribute)) {
UICheckingError ce = new UICheckingError(CheckingError.BEHAVIOR_ERROR, "Unknown attribute '" + value + "' (ignored)");
- // ce.setTDiagramPanel(((AvatarDesignPanel)(this.avspec.getReferenceObject())).getAvatarSMDPanel(arg.block.getName()));
- ce.setTGComponent((TGComponent)(_asme.getReferenceObject()));
+ // ce.setTDiagramPanel(((AvatarDesignPanel)(this.avspec.getReferenceObject())).getAvatarSMDPanel(arg.block.getName()));
+ ce.setTGComponent((TGComponent) (_asme.getReferenceObject()));
this.warnings.add(ce);
continue;
}
AvatarAttribute attr = (AvatarAttribute) term;
- Integer c = arg.attributeCmp.get (attr) + 1;
- arg.attributeCmp.put (attr, c);
- vars.add (new ProVerifVar (AVATAR2ProVerif.translateTerm (attr, arg.attributeCmp), "bitstring"));
+ Integer c = arg.attributeCmp.get(attr) + 1;
+ arg.attributeCmp.put(attr, c);
+ vars.add(new ProVerifVar(AVATAR2ProVerif.translateTerm(attr, arg.attributeCmp), "bitstring"));
}
// If the channel is private use the CH_DECRYPT function
if (isPrivate) {
- TraceManager.addDev("| | in (chPriv, ...)");
+ //TraceManager.addDev("| | in (chPriv, ...)");
if (!this.allowPrivateChannelDuplication) {
this.dummyDataCounter++;
String strong = "strong" + ATTR_DELIM + "priv" + this.dummyDataCounter;
_lastInstr = _lastInstr.setNextInstr(new ProVerifProcNew(strong, "bitstring"));
- _lastInstr = _lastInstr.setNextInstr(new ProVerifProcRaw ("out (" + CHCTRL_CH + ", " + strong + ");"));
+ _lastInstr = _lastInstr.setNextInstr(new ProVerifProcRaw("out (" + CHCTRL_CH + ", " + strong + ");"));
this.dummyDataCounter++;
_lastInstr = _lastInstr.setNextInstr(new ProVerifProcIn(CH_MAINCH, new ProVerifVar[]{new ProVerifVar("privChData" + this.dummyDataCounter, "bitstring")}));
@@ -1172,7 +1150,7 @@ public class AVATAR2ProVerif implements AvatarTranslator {
LinkedList<ProVerifVar> strongCheckVars = new LinkedList<>();
strongCheckVars.add(new ProVerifVar(strong, "bitstring", false, true));
strongCheckVars.add(new ProVerifVar("privChData" + this.dummyDataCounter, "bitstring"));
- _lastInstr = _lastInstr.setNextInstr(new ProVerifProcLet(strongCheckVars.toArray(new ProVerifVar[strongCheckVars.size()]), CH_DECRYPT + name + " (privChData" + (this.dummyDataCounter-1) + ")"));
+ _lastInstr = _lastInstr.setNextInstr(new ProVerifProcLet(strongCheckVars.toArray(new ProVerifVar[strongCheckVars.size()]), CH_DECRYPT + name + " (privChData" + (this.dummyDataCounter - 1) + ")"));
_lastInstr = _lastInstr.setNextInstr(new ProVerifProcLet(vars.toArray(new ProVerifVar[vars.size()]), "privChData" + this.dummyDataCounter));
} else {
@@ -1181,175 +1159,176 @@ public class AVATAR2ProVerif implements AvatarTranslator {
_lastInstr = _lastInstr.setNextInstr(new ProVerifProcLet(vars.toArray(new ProVerifVar[vars.size()]), CH_DECRYPT + name + " (privChData" + this.dummyDataCounter + ")"));
}
} else {
- TraceManager.addDev("| | in (ch, ...)");
- _lastInstr = _lastInstr.setNextInstr (new ProVerifProcIn (CH_MAINCH, vars.toArray (new ProVerifVar[vars.size()])));
+ //TraceManager.addDev("| | in (ch, ...)");
+ _lastInstr = _lastInstr.setNextInstr(new ProVerifProcIn(CH_MAINCH, vars.toArray(new ProVerifVar[vars.size()])));
}
}
arg.lastInstr = _lastInstr;
arg.lastASME = _asme;
- this.translateNext (_asme.getNext(0), arg);
+ this.translateNext(_asme.getNext(0), arg);
}
/**
* Translation function handling Avatar Transitions
*/
- public void translateTransition (AvatarTransition _asme, Object _arg) {
- TraceManager.addDev("| Transition");
+ public void translateTransition(AvatarTransition _asme, Object _arg) {
+ //TraceManager.addDev("| Transition");
ProVerifTranslatorParameter arg = (ProVerifTranslatorParameter) _arg;
ProVerifProcInstr _lastInstr = arg.lastInstr;
// Check if the transition is guarded
- if (_asme.isGuarded() && !arg.lastASME.hasElseChoiceType1 ()) {
- TraceManager.addDev("Analyzing GUARD: " + _asme.getGuard() + " real guard=" + _asme.getGuard().getRealGuard (arg.lastASME));
- String tmp = AVATAR2ProVerif.translateGuard(_asme.getGuard().getRealGuard (arg.lastASME), arg.attributeCmp);
+ if (_asme.isGuarded() && !arg.lastASME.hasElseChoiceType1()) {
+ //TraceManager.addDev("Analyzing GUARD: " + _asme.getGuard() + " real guard=" + _asme.getGuard().getRealGuard(arg.lastASME));
+ String tmp = AVATAR2ProVerif.translateGuard(_asme.getGuard().getRealGuard(arg.lastASME), arg.attributeCmp);
if (tmp != null) {
- TraceManager.addDev("| | transition is guarded by " + tmp);
- _lastInstr = _lastInstr.setNextInstr (new ProVerifProcITE (tmp));
+ //TraceManager.addDev("| | transition is guarded by " + tmp);
+ _lastInstr = _lastInstr.setNextInstr(new ProVerifProcITE(tmp));
} else {
- TraceManager.addDev ("!!! Guard: " + _asme.getGuard() + " in block " + arg.block.getName() + " is not supported. " +
- "Replacing by an empty guard");
+ //TraceManager.addDev("!!! Guard: " + _asme.getGuard() + " in block " + arg.block.getName() + " is not supported. " +
+ // "Replacing by an empty guard");
UICheckingError ce = new UICheckingError(CheckingError.BEHAVIOR_ERROR,
SEC_TRANS + "Guard: " + _asme.getGuard() + " in block " + arg.block.getName() + " is not supported. " +
"Replacing by an empty " +
- "guard");
+ "guard");
//ce.setTDiagramPanel(((AvatarDesignPanel)(avspec.getReferenceObject())).getAvatarSMDPanel(arg.block.getName()));
- ce.setTGComponent((TGComponent)(_asme.getReferenceObject()));
+ ce.setTGComponent((TGComponent) (_asme.getReferenceObject()));
warnings.add(ce);
- _lastInstr = _lastInstr.setNextInstr (new ProVerifProcRaw ("(* Unsupported guard:" + _asme.getGuard() + " *)"));
+ _lastInstr = _lastInstr.setNextInstr(new ProVerifProcRaw("(* Unsupported guard:" + _asme.getGuard() + " *)"));
}
}
- TraceManager.addDev("| | Actions");
+ //TraceManager.addDev("| | Actions");
// Loop over all assigment functions
- for(AvatarAction aaction: _asme.getActions ()) {
+ for (AvatarAction aaction : _asme.getActions()) {
if (aaction instanceof AvatarActionAssignment) {
AvatarActionAssignment action = (AvatarActionAssignment) aaction;
- TraceManager.addDev("| | | assignment found: " + action);
- AvatarLeftHand leftHand = action.getLeftHand ();
+ //TraceManager.addDev("| | | assignment found: " + action);
+ AvatarLeftHand leftHand = action.getLeftHand();
// Compute right part of assignment
- AvatarTerm rightHand = action.getRightHand ();
+ AvatarTerm rightHand = action.getRightHand();
String proVerifRightHand = null;
if (rightHand instanceof AvatarTermFunction) {
// If it's a function call
- String name = ((AvatarTermFunction) rightHand).getMethod ().getName ();
- List<AvatarTerm> args = ((AvatarTermFunction) rightHand).getArgs ().getComponents ();
+ String name = ((AvatarTermFunction) rightHand).getMethod().getName();
+ List<AvatarTerm> args = ((AvatarTermFunction) rightHand).getArgs().getComponents();
- if (name.equals ("concat2") || name.equals ("concat3") || name.equals ("concat4")) {
+ if (name.equals("concat2") || name.equals("concat3") || name.equals("concat4")) {
// If it's a concat function, just use tuples
boolean first = true;
proVerifRightHand = "(";
- for (AvatarTerm argTerm: args) {
+ for (AvatarTerm argTerm : args) {
if (first)
first = false;
else
proVerifRightHand += ", ";
- proVerifRightHand += AVATAR2ProVerif.translateTerm (argTerm, arg.attributeCmp);
+ proVerifRightHand += AVATAR2ProVerif.translateTerm(argTerm, arg.attributeCmp);
}
proVerifRightHand += ")";
} else
// Else use the function as is
- proVerifRightHand = AVATAR2ProVerif.translateTerm (rightHand, arg.attributeCmp);
- //
+ proVerifRightHand = AVATAR2ProVerif.translateTerm(rightHand, arg.attributeCmp);
+ //
} else {
// If it's not a function, use it as is
- proVerifRightHand = AVATAR2ProVerif.translateTerm (rightHand, arg.attributeCmp);
- //
- }
+ proVerifRightHand = AVATAR2ProVerif.translateTerm(rightHand, arg.attributeCmp);
+ //
+ }
// Compute left hand part of the assignment
- LinkedList<ProVerifVar> proVerifLeftHand = new LinkedList<ProVerifVar> ();
+ LinkedList<ProVerifVar> proVerifLeftHand = new LinkedList<ProVerifVar>();
if (proVerifRightHand != null) {
if (leftHand instanceof AvatarTuple)
- for (AvatarTerm term: ((AvatarTuple) leftHand).getComponents ()) {
- if (! (term instanceof AvatarAttribute)) {
- UICheckingError ce = new UICheckingError(CheckingError.BEHAVIOR_ERROR, "'" + term.getName () + "' should be an attribute (ignored)");
- ce.setTDiagramPanel(((AvatarDesignPanel)(this.avspec.getReferenceObject())).getAvatarSMDPanel(arg.block.getName()));
- ce.setTGComponent((TGComponent)(_asme.getReferenceObject()));
+ for (AvatarTerm term : ((AvatarTuple) leftHand).getComponents()) {
+ if (!(term instanceof AvatarAttribute)) {
+ UICheckingError ce = new UICheckingError(CheckingError.BEHAVIOR_ERROR, "'" + term.getName() + "' should be an attribute (ignored)");
+ ce.setTDiagramPanel(((AvatarDesignPanel) (this.avspec.getReferenceObject())).getAvatarSMDPanel(arg.block.getName()));
+ ce.setTGComponent((TGComponent) (_asme.getReferenceObject()));
this.warnings.add(ce);
continue;
}
AvatarAttribute attr = (AvatarAttribute) term;
- Integer c = arg.attributeCmp.get (attr) + 1;
- arg.attributeCmp.put (attr, c);
- proVerifLeftHand.add (new ProVerifVar (AVATAR2ProVerif.translateTerm (attr, arg.attributeCmp), "bitstring"));
-
- if (this.secrecyChecked.contains (attr)) {
- UICheckingError ce = new UICheckingError(CheckingError.BEHAVIOR_ERROR, "'" + term.getName () + "' is re-assigned while its secrecy is being checked. Note that the proof will only guarantee the secrecy of the initial value of " + term.getName () + ".");
- ce.setTDiagramPanel(((AvatarDesignPanel)(this.avspec.getReferenceObject())).getAvatarSMDPanel(arg.block.getName()));
- ce.setTGComponent((TGComponent)(_asme.getReferenceObject()));
+ Integer c = arg.attributeCmp.get(attr) + 1;
+ arg.attributeCmp.put(attr, c);
+ proVerifLeftHand.add(new ProVerifVar(AVATAR2ProVerif.translateTerm(attr, arg.attributeCmp), "bitstring"));
+
+ if (this.secrecyChecked.contains(attr)) {
+ UICheckingError ce = new UICheckingError(CheckingError.BEHAVIOR_ERROR, "'" + term.getName() + "' is re-assigned while its secrecy is being checked. Note that the proof will only guarantee the secrecy of the initial value of " + term.getName() + ".");
+ ce.setTDiagramPanel(((AvatarDesignPanel) (this.avspec.getReferenceObject())).getAvatarSMDPanel(arg.block.getName()));
+ ce.setTGComponent((TGComponent) (_asme.getReferenceObject()));
this.warnings.add(ce);
}
}
else if (leftHand instanceof AvatarAttribute) {
AvatarAttribute attr = (AvatarAttribute) leftHand;
- Integer c = arg.attributeCmp.get (attr) + 1;
- arg.attributeCmp.put (attr, c);
- proVerifLeftHand.add (new ProVerifVar (AVATAR2ProVerif.translateTerm (attr, arg.attributeCmp), "bitstring"));
-
- if (this.secrecyChecked.contains (attr)) {
- UICheckingError ce = new UICheckingError(CheckingError.BEHAVIOR_ERROR, "'" + attr.getName () + "' is re-assigned while its secrecy is being checked. Note that the proof will only guarantee the secrecy of the initial value of " + attr.getName () + ".");
- if (this.avspec.getReferenceObject() instanceof AvatarDesignPanel){
- ce.setTDiagramPanel(((AvatarDesignPanel)(this.avspec.getReferenceObject())).getAvatarSMDPanel(arg.block.getName()));
- }
- ce.setTGComponent((TGComponent)(_asme.getReferenceObject()));
+ Integer c = arg.attributeCmp.get(attr) + 1;
+ arg.attributeCmp.put(attr, c);
+ proVerifLeftHand.add(new ProVerifVar(AVATAR2ProVerif.translateTerm(attr, arg.attributeCmp), "bitstring"));
+
+ if (this.secrecyChecked.contains(attr)) {
+ UICheckingError ce = new UICheckingError(CheckingError.BEHAVIOR_ERROR, "'" + attr.getName() + "' is re-assigned while its secrecy is being checked. Note that the proof will only guarantee the secrecy of the initial value of " + attr.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);
}
}
}
- if (proVerifRightHand != null && proVerifLeftHand.size () > 0)
- _lastInstr = _lastInstr.setNextInstr (new ProVerifProcLet (proVerifLeftHand.toArray (new ProVerifVar[proVerifLeftHand.size ()]),
+ if (proVerifRightHand != null && proVerifLeftHand.size() > 0)
+ _lastInstr = _lastInstr.setNextInstr(new ProVerifProcLet(proVerifLeftHand.toArray(new ProVerifVar[proVerifLeftHand.size()]),
modifyExprProVerif(proVerifRightHand)));
else {
- TraceManager.addDev ("!!! Assignment: " + action.toString () + " in block " + arg.block.getName() + " is not supported. Removing it.");
+ //TraceManager.addDev("!!! Assignment: " + action.toString() + " in block " + arg.block.getName() + " is not supported. " +
+ // "Removing it.");
UICheckingError ce = new UICheckingError(CheckingError.BEHAVIOR_ERROR,
- SEC_TRANS + "Assignment: " + action.toString () + " in block " + arg.block.getName() + " is not supported. Removing it.");
+ SEC_TRANS + "Assignment: " + action.toString() + " in block " + arg.block.getName() + " is not supported. Removing it.");
//ce.setTDiagramPanel(((AvatarDesignPanel)(avspec.getReferenceObject())).getAvatarSMDPanel(arg.block.getName()));
- ce.setTGComponent((TGComponent)(_asme.getReferenceObject()));
+ ce.setTGComponent((TGComponent) (_asme.getReferenceObject()));
warnings.add(ce);
}
} else if (aaction instanceof AvatarTermFunction) {
AvatarTermFunction action = (AvatarTermFunction) aaction;
- String name = action.getMethod ().getName ();
+ String name = action.getMethod().getName();
- if (name.equals ("get2") || name.equals ("get3") || name.equals ("get4")) {
+ if (name.equals("get2") || name.equals("get3") || name.equals("get4")) {
// If the function called is get[234]
- List<AvatarTerm> args = action.getArgs ().getComponents ();
- int index = (int) name.charAt (3) - 48;
+ List<AvatarTerm> args = action.getArgs().getComponents();
+ int index = (int) name.charAt(3) - 48;
boolean ok = true;
for (int i = 1; i <= index; i++)
- if (! (args.get(i) instanceof AvatarAttribute)) {
- UICheckingError ce = new UICheckingError(CheckingError.BEHAVIOR_ERROR, "'" + args.get(i).getName () + "' should be an attribute (ignored)");
- if (this.avspec.getReferenceObject() instanceof AvatarDesignPanel){
- ce.setTDiagramPanel(((AvatarDesignPanel)(this.avspec.getReferenceObject())).getAvatarSMDPanel(arg.block.getName()));
- }
- ce.setTGComponent((TGComponent)(_asme.getReferenceObject()));
+ if (!(args.get(i) instanceof AvatarAttribute)) {
+ UICheckingError ce = new UICheckingError(CheckingError.BEHAVIOR_ERROR, "'" + args.get(i).getName() + "' should be an attribute (ignored)");
+ 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;
}
if (ok) {
// Create the corresponding assignment
- String rightHand = AVATAR2ProVerif.translateTerm (args.get (0), arg.attributeCmp);
+ String rightHand = AVATAR2ProVerif.translateTerm(args.get(0), arg.attributeCmp);
- LinkedList<ProVerifVar> tup = new LinkedList<ProVerifVar> ();
+ LinkedList<ProVerifVar> tup = new LinkedList<ProVerifVar>();
for (int i = 1; i <= index; i++) {
- AvatarAttribute attr = (AvatarAttribute) args.get (i);
- Integer c = arg.attributeCmp.get (attr) + 1;
- arg.attributeCmp.put (attr, c);
- tup.add (new ProVerifVar (AVATAR2ProVerif.translateTerm (attr, arg.attributeCmp), "bitstring"));
- if (this.secrecyChecked.contains (attr)) {
- UICheckingError ce = new UICheckingError(CheckingError.BEHAVIOR_ERROR, "'" + attr.getName () + "' is re-assigned while its secrecy is being checked. Note that the proof will only guarantee the secrecy of the initial value of " + attr.getName () + ".");
- // ce.setTDiagramPanel(((AvatarDesignPanel)(this.avspec.getReferenceObject())).getAvatarSMDPanel(arg.block.getName()));
- ce.setTGComponent((TGComponent)(_asme.getReferenceObject()));
+ AvatarAttribute attr = (AvatarAttribute) args.get(i);
+ Integer c = arg.attributeCmp.get(attr) + 1;
+ arg.attributeCmp.put(attr, c);
+ tup.add(new ProVerifVar(AVATAR2ProVerif.translateTerm(attr, arg.attributeCmp), "bitstring"));
+ if (this.secrecyChecked.contains(attr)) {
+ UICheckingError ce = new UICheckingError(CheckingError.BEHAVIOR_ERROR, "'" + attr.getName() + "' is re-assigned while its secrecy is being checked. Note that the proof will only guarantee the secrecy of the initial value of " + attr.getName() + ".");
+ // ce.setTDiagramPanel(((AvatarDesignPanel)(this.avspec.getReferenceObject())).getAvatarSMDPanel(arg.block.getName()));
+ ce.setTGComponent((TGComponent) (_asme.getReferenceObject()));
this.warnings.add(ce);
}
}
- _lastInstr = _lastInstr.setNextInstr (new ProVerifProcLet (tup.toArray (new ProVerifVar[tup.size ()]), rightHand));
+ _lastInstr = _lastInstr.setNextInstr(new ProVerifProcLet(tup.toArray(new ProVerifVar[tup.size()]), rightHand));
}
}
}
@@ -1357,144 +1336,144 @@ public class AVATAR2ProVerif implements AvatarTranslator {
arg.lastInstr = _lastInstr;
arg.lastASME = _asme;
- this.translateNext (_asme.getNext(0), arg);
+ this.translateNext(_asme.getNext(0), arg);
}
- public void translateState (AvatarState _asme, Object _arg) {
- TraceManager.addDev("| State " + _asme.getName ());
+ public void translateState(AvatarState _asme, Object _arg) {
+ //TraceManager.addDev("| State " + _asme.getName());
ProVerifTranslatorParameter arg = (ProVerifTranslatorParameter) _arg;
ProVerifProcInstr _lastInstr = arg.lastInstr;
if (this.stateReachability == JDialogProverifVerification.REACHABILITY_ALL ||
- (this.stateReachability == JDialogProverifVerification.REACHABILITY_SELECTED && _asme.isCheckable ()))
+ (this.stateReachability == JDialogProverifVerification.REACHABILITY_SELECTED && _asme.isCheckable()))
// Adding an event for reachability of the state
- _lastInstr = _lastInstr.setNextInstr (new ProVerifProcRaw ("event enteringState" + ATTR_DELIM + arg.block.getName() + ATTR_DELIM + _asme.getName() + "()", true));
+ _lastInstr = _lastInstr.setNextInstr(new ProVerifProcRaw("event enteringState" + ATTR_DELIM + arg.block.getName() + ATTR_DELIM + _asme.getName() + "()", true));
// Adding an event if authenticity is concerned with that state
- HashSet<String> authenticityEvents = new HashSet<String> ();
- for (AvatarPragma pragma: this.avspec.getPragmas ())
+ HashSet<String> authenticityEvents = new HashSet<String>();
+ for (AvatarPragma pragma : this.avspec.getPragmas())
if (pragma instanceof AvatarPragmaAuthenticity) {
- AvatarAttributeState attrA = ((AvatarPragmaAuthenticity) pragma).getAttrA ();
- AvatarAttributeState attrB = ((AvatarPragmaAuthenticity) pragma).getAttrB ();
- if (attrA.getAttribute ().getBlock () == arg.block && attrA.getState ().getName ().equals (_asme.getName ())) {
- TraceManager.addDev ("DEBUG: " + attrA.getAttribute ());
+ AvatarAttributeState attrA = ((AvatarPragmaAuthenticity) pragma).getAttrA();
+ AvatarAttributeState attrB = ((AvatarPragmaAuthenticity) pragma).getAttrB();
+ if (attrA.getAttribute().getBlock() == arg.block && attrA.getState().getName().equals(_asme.getName())) {
+ //TraceManager.addDev("DEBUG: " + attrA.getAttribute());
//TraceManager.addDev ("DEBUG: " + attrA.getAttribute ().getBlock ());
//TraceManager.addDev ("DEBUG: " + arg.attributeCmp.get (attrA.getAttribute()));
- String sp = "authenticity" + ATTR_DELIM + AVATAR2ProVerif.makeAttrName (attrA.getAttribute ().getBlock ().getName (), attrA.getAttribute ().getName (), _asme.getName ()) + " (" + AVATAR2ProVerif.makeAttrName (attrA.getAttribute ().getBlock ().getName (), attrA.getAttribute ().getName (), arg.attributeCmp.get (attrA.getAttribute ()).toString ()) + ")";
- if (!authenticityEvents.contains (sp)) {
- authenticityEvents.add (sp);
- TraceManager.addDev("| | authenticity event " + sp + "added");
- _lastInstr = _lastInstr.setNextInstr (new ProVerifProcRaw ("event " + sp, true));
+ String sp = "authenticity" + ATTR_DELIM + AVATAR2ProVerif.makeAttrName(attrA.getAttribute().getBlock().getName(), attrA.getAttribute().getName(), _asme.getName()) + " (" + AVATAR2ProVerif.makeAttrName(attrA.getAttribute().getBlock().getName(), attrA.getAttribute().getName(), arg.attributeCmp.get(attrA.getAttribute()).toString()) + ")";
+ if (!authenticityEvents.contains(sp)) {
+ authenticityEvents.add(sp);
+ //TraceManager.addDev("| | authenticity event " + sp + "added");
+ _lastInstr = _lastInstr.setNextInstr(new ProVerifProcRaw("event " + sp, true));
}
}
- if (attrB.getAttribute ().getBlock () == arg.block && attrB.getState ().getName ().equals (_asme.getName ())) {
- String sp = "authenticity" + ATTR_DELIM + AVATAR2ProVerif.makeAttrName (attrB.getAttribute ().getBlock ().getName (), attrB.getAttribute ().getName (), _asme.getName ()) + " (" + AVATAR2ProVerif.makeAttrName (attrB.getAttribute ().getBlock ().getName (), attrB.getAttribute ().getName (), arg.attributeCmp.get (attrB.getAttribute ()).toString ()) + ")";
- if (!authenticityEvents.contains (sp)) {
- authenticityEvents.add (sp);
- TraceManager.addDev("| | authenticity event " + sp + "added");
- _lastInstr = _lastInstr.setNextInstr (new ProVerifProcRaw ("event " + sp, true));
+ if (attrB.getAttribute().getBlock() == arg.block && attrB.getState().getName().equals(_asme.getName())) {
+ String sp = "authenticity" + ATTR_DELIM + AVATAR2ProVerif.makeAttrName(attrB.getAttribute().getBlock().getName(), attrB.getAttribute().getName(), _asme.getName()) + " (" + AVATAR2ProVerif.makeAttrName(attrB.getAttribute().getBlock().getName(), attrB.getAttribute().getName(), arg.attributeCmp.get(attrB.getAttribute()).toString()) + ")";
+ if (!authenticityEvents.contains(sp)) {
+ authenticityEvents.add(sp);
+ //TraceManager.addDev("| | authenticity event " + sp + "added");
+ _lastInstr = _lastInstr.setNextInstr(new ProVerifProcRaw("event " + sp, true));
}
}
}
- int nbOfNexts = _asme.nbOfNexts ();
+ int nbOfNexts = _asme.nbOfNexts();
if (nbOfNexts == 0)
return;
if (nbOfNexts == 1) {
arg.lastInstr = _lastInstr;
arg.lastASME = _asme;
- this.translateNext (_asme.getNext(0), arg);
+ this.translateNext(_asme.getNext(0), arg);
} else if (_asme.hasElseChoiceType1()) {
- TraceManager.addDev("| | calling next ITE");
- ProVerifProcITE ite = new ProVerifProcITE (AVATAR2ProVerif.translateGuard (((AvatarTransition) _asme.getNext (0)).getGuard ().getRealGuard (_asme), arg.attributeCmp));
+ //TraceManager.addDev("| | calling next ITE");
+ ProVerifProcITE ite = new ProVerifProcITE(AVATAR2ProVerif.translateGuard(((AvatarTransition) _asme.getNext(0)).getGuard().getRealGuard(_asme), arg.attributeCmp));
- HashMap<AvatarAttribute, Integer> attributeCmp = new HashMap<AvatarAttribute, Integer> (arg.attributeCmp);
+ HashMap<AvatarAttribute, Integer> attributeCmp = new HashMap<AvatarAttribute, Integer>(arg.attributeCmp);
- arg.lastInstr = _lastInstr.setNextInstr (ite);
+ arg.lastInstr = _lastInstr.setNextInstr(ite);
arg.lastASME = _asme;
- this.translateNext (_asme.getNext (0), arg);
+ this.translateNext(_asme.getNext(0), arg);
arg.attributeCmp = attributeCmp;
- arg.lastInstr = ite.getElse ();
+ arg.lastInstr = ite.getElse();
arg.lastASME = _asme;
- this.translateNext (_asme.getNext (1), arg);
+ this.translateNext(_asme.getNext(1), arg);
} else {
- TraceManager.addDev("| | non deterministic next state");
- for (int i=0; i<nbOfNexts-1; i++) {
- String choice = "choice" + ATTR_DELIM + _asme.getName () + ATTR_DELIM + i;
- _lastInstr = _lastInstr.setNextInstr (new ProVerifProcNew (choice, "bitstring"));
- _lastInstr = _lastInstr.setNextInstr (new ProVerifProcRaw ("out (" + CH_MAINCH + ", " + choice + ");"));
+ //TraceManager.addDev("| | non deterministic next state");
+ for (int i = 0; i < nbOfNexts - 1; i++) {
+ String choice = "choice" + ATTR_DELIM + _asme.getName() + ATTR_DELIM + i;
+ _lastInstr = _lastInstr.setNextInstr(new ProVerifProcNew(choice, "bitstring"));
+ _lastInstr = _lastInstr.setNextInstr(new ProVerifProcRaw("out (" + CH_MAINCH + ", " + choice + ");"));
}
- _lastInstr = _lastInstr.setNextInstr (new ProVerifProcIn (CH_MAINCH, new ProVerifVar[] {new ProVerifVar ("choice" + ATTR_DELIM + _asme.getName (), "bitstring")}));
+ _lastInstr = _lastInstr.setNextInstr(new ProVerifProcIn(CH_MAINCH, new ProVerifVar[]{new ProVerifVar("choice" + ATTR_DELIM + _asme.getName(), "bitstring")}));
Map<AvatarAttribute, Integer> attributeCmp = arg.attributeCmp;
- for (int i=0; i<nbOfNexts-1; i++) {
- String choice = "choice" + ATTR_DELIM + _asme.getName () + ATTR_DELIM + i;
- ProVerifProcITE ite = new ProVerifProcITE ("choice" + ATTR_DELIM + _asme.getName () + " = " + choice);
+ for (int i = 0; i < nbOfNexts - 1; i++) {
+ String choice = "choice" + ATTR_DELIM + _asme.getName() + ATTR_DELIM + i;
+ ProVerifProcITE ite = new ProVerifProcITE("choice" + ATTR_DELIM + _asme.getName() + " = " + choice);
- arg.attributeCmp = new HashMap<AvatarAttribute, Integer> (attributeCmp);
+ arg.attributeCmp = new HashMap<AvatarAttribute, Integer>(attributeCmp);
arg.lastASME = _asme;
- arg.lastInstr = _lastInstr.setNextInstr (ite);
- this.translateNext (_asme.getNext (i), arg);
+ arg.lastInstr = _lastInstr.setNextInstr(ite);
+ this.translateNext(_asme.getNext(i), arg);
- _lastInstr = ite.getElse ();
+ _lastInstr = ite.getElse();
}
arg.attributeCmp = attributeCmp;
arg.lastInstr = _lastInstr;
arg.lastASME = _asme;
- this.translateNext (_asme.getNext (nbOfNexts-1), arg);
+ this.translateNext(_asme.getNext(nbOfNexts - 1), arg);
}
}
- public void translateRandom (AvatarRandom _asme, Object _arg) {
- TraceManager.addDev("| Random");
+ public void translateRandom(AvatarRandom _asme, Object _arg) {
+ //TraceManager.addDev("| Random");
ProVerifTranslatorParameter arg = (ProVerifTranslatorParameter) _arg;
ProVerifProcInstr _lastInstr = arg.lastInstr;
- AvatarTerm term = AvatarTerm.createFromString (arg.block, _asme.getVariable ());
- LinkedList<AvatarAttribute> names = new LinkedList<AvatarAttribute> ();
+ AvatarTerm term = AvatarTerm.createFromString(arg.block, _asme.getVariable());
+ LinkedList<AvatarAttribute> names = new LinkedList<AvatarAttribute>();
if (term instanceof AvatarAttribute)
- names.add ((AvatarAttribute) term);
+ names.add((AvatarAttribute) term);
else if (term instanceof AvatarTuple)
- for (AvatarTerm t: ((AvatarTuple) term).getComponents ())
+ for (AvatarTerm t : ((AvatarTuple) term).getComponents())
if (t instanceof AvatarAttribute)
- names.add ((AvatarAttribute) t);
+ names.add((AvatarAttribute) t);
- for (AvatarAttribute attr: names) {
- Integer c = arg.attributeCmp.get (attr) + 1;
- arg.attributeCmp.put (attr, c);
- _lastInstr = _lastInstr.setNextInstr (new ProVerifProcNew (AVATAR2ProVerif.translateTerm (attr, arg.attributeCmp), "bitstring"));
+ for (AvatarAttribute attr : names) {
+ Integer c = arg.attributeCmp.get(attr) + 1;
+ arg.attributeCmp.put(attr, c);
+ _lastInstr = _lastInstr.setNextInstr(new ProVerifProcNew(AVATAR2ProVerif.translateTerm(attr, arg.attributeCmp), "bitstring"));
}
arg.lastInstr = _lastInstr;
arg.lastASME = _asme;
- this.translateNext (_asme.getNext(0), _arg);
+ this.translateNext(_asme.getNext(0), _arg);
}
public void translateEmpty(AvatarEmpty _asme, Object _arg) {
- TraceManager.addDev("| Empty");
- this.translateNext (_asme.getNext(0), _arg);
+ //TraceManager.addDev("| Empty");
+ this.translateNext(_asme.getNext(0), _arg);
}
- public void translateStartState (AvatarStartState _asme, Object _arg) {
- this.translateNext (_asme.getNext(0), _arg);
+ public void translateStartState(AvatarStartState _asme, Object _arg) {
+ this.translateNext(_asme.getNext(0), _arg);
}
- public void translateTimerOperator (AvatarTimerOperator _asme, Object _arg) {
- this.translateNext (_asme.getNext(0), _arg);
+ public void translateTimerOperator(AvatarTimerOperator _asme, Object _arg) {
+ this.translateNext(_asme.getNext(0), _arg);
}
- public void translateStopState (AvatarStopState _asme, Object _arg) {
+ public void translateStopState(AvatarStopState _asme, Object _arg) {
}
public void translateLibraryFunctionCall(AvatarLibraryFunctionCall _asme, Object _arg) {
/* should not happen */
- this.translateNext (_asme.getNext(0), _arg);
+ this.translateNext(_asme.getNext(0), _arg);
}
public String modifyExprProVerif(String input) {
@@ -1503,4 +1482,12 @@ public class AVATAR2ProVerif implements AvatarTranslator {
return ret;
}
+
+ class ProVerifTranslatorParameter {
+ AvatarBlock block;
+ ProVerifProcInstr lastInstr;
+ Map<AvatarStateMachineElement, Integer> simplifiedElements;
+ Map<AvatarAttribute, Integer> attributeCmp;
+ AvatarStateMachineElement lastASME;
+ }
}
diff --git a/src/main/java/proverifspec/ProVerifOutputAnalyzer.java b/src/main/java/proverifspec/ProVerifOutputAnalyzer.java
index 6ed267771c96486a715874384cfe8e68e5ad1957..8417823e68c050bac5c7db554c80813a1f5c2428 100644
--- a/src/main/java/proverifspec/ProVerifOutputAnalyzer.java
+++ b/src/main/java/proverifspec/ProVerifOutputAnalyzer.java
@@ -112,8 +112,7 @@ public class ProVerifOutputAnalyzer {
this.listeners.remove(listener);
}
- private void notifyListeners()
- {
+ private void notifyListeners() {
for (ProVerifOutputListener listener: this.listeners)
listener.proVerifOutputChanged();
}
@@ -148,31 +147,25 @@ public class ProVerifOutputAnalyzer {
Matcher m = procPattern.matcher(str);
- if (isInTrace && (str.startsWith("A more detailed") || str.startsWith("Could not find")))
- {
+ if (isInTrace && (str.startsWith("A more detailed") || str.startsWith("Could not find"))) {
isInTrace = false;
resultTrace.finalizeMethod();
continue;
- }
- else if (!isInTrace && str.startsWith("1. "))
- {
+ } else if (!isInTrace && str.startsWith("1. ")) {
isInTrace = true;
}
// Found a trace step
- if (isInTrace)
- {
+ if (isInTrace) {
resultTrace.addTraceStep(str);
}
- else if (m.matches())
- {
+ else if (m.matches()) {
proverifProcess.add(m.group(1));
}
// Found a line with a RESULT
- else if (str.startsWith("RESULT "))
- {
+ else if (str.startsWith("RESULT ")) {
// Remove 'RESULT ' at the begining
str = str.substring(7);
@@ -180,15 +173,13 @@ public class ProVerifOutputAnalyzer {
ProVerifQueryResult result = new ProVerifQueryResult(true, true);
// This concerns an enteringState event
- if (str.startsWith(isTyped ? typedEvent : untypedEvent))
- {
+ if (str.startsWith(isTyped ? typedEvent : untypedEvent)) {
str = str.substring((isTyped ? typedEvent : untypedEvent).length());
String stateName = null;
previousAuthPragma = null;
- if (isTyped)
- {
+ if (isTyped) {
if (str.contains(typedTrue))
{
result.setSatisfied(false);
@@ -205,9 +196,7 @@ public class ProVerifOutputAnalyzer {
result.setTrace(resultTrace);
stateName = str.split(Pattern.quote(typedCannotBeProved))[0];
}
- }
- else
- {
+ } else {
stateName = str.split("\\(")[0];
if (str.contains(untypedTrue))
{
@@ -225,48 +214,45 @@ public class ProVerifOutputAnalyzer {
}
AvatarPragmaReachability reachabilityPragma = this.getAvatarPragmaReachabilityFromString(stateName);
- if (reachabilityPragma != null)
- {
+ if (reachabilityPragma != null) {
this.results.put(reachabilityPragma, result);
this.notifyListeners();
}
}
// This concerns a confidentiality check
- else if (str.contains(isTyped ? typedSecret : untypedSecret))
- {
+ else if (str.contains(isTyped ? typedSecret : untypedSecret)) {
+ TraceManager.addDev("Confidentiality of: " + str);
String attributeName = str.substring((isTyped ? typedSecret : untypedSecret).length()).split("\\[")[0];
previousAuthPragma = null;
- if (str.contains(isTyped ? typedFalse : untypedFalse))
- {
+ if (str.contains(isTyped ? typedFalse : untypedFalse)) {
+ TraceManager.addDev("Confidentiality: false");
result.setTrace(resultTrace);
result.setSatisfied(false);
}
- else if (str.contains(isTyped ? typedCannotBeProved : untypedCannotBeProved))
- {
+ else if (str.contains(isTyped ? typedCannotBeProved : untypedCannotBeProved)) {
+ TraceManager.addDev("Confidentiality: cannot be proved");
result.setTrace(resultTrace);
result.setProved(false);
}
AvatarAttribute attribute = this.getAvatarAttributeFromString(attributeName);
- if (attribute != null)
- {
- for (AvatarPragma pragma: pragmas)
- {
- if (pragma instanceof AvatarPragmaSecret)
- {
-
+ if (attribute != null) {
+ TraceManager.addDev("Confidentiality attribute is non null: " + attribute.toString());
+ for (AvatarPragma pragma: pragmas) {
+ if (pragma instanceof AvatarPragmaSecret) {
String trueName = this.avatar2proverif.getTrueName(((AvatarPragmaSecret) pragma).getArg());
-
- if (trueName != null && trueName.equals(attributeName))
- {
+ if (trueName != null && trueName.equals(attributeName)) {
+ TraceManager.addDev("Pragma: " + pragma.toString());
this.results.put(pragma, result);
this.notifyListeners();
}
}
}
+ } else {
+ TraceManager.addDev("Confidentiality attribute is NULL: " + attributeName);
}
}
@@ -331,18 +317,14 @@ public class ProVerifOutputAnalyzer {
state2 = this.getAvatarStateFromString(tmp[0] + AVATAR2ProVerif.ATTR_DELIM + tmp[2]);
}
- if (attribute1 != null && attribute2 != null && state1 != null && state2 != null)
- {
- for (AvatarPragma pragma: pragmas)
- {
- if (pragma instanceof AvatarPragmaAuthenticity)
- {
+ if (attribute1 != null && attribute2 != null && state1 != null && state2 != null) {
+ for (AvatarPragma pragma: pragmas) {
+ if (pragma instanceof AvatarPragmaAuthenticity) {
AvatarPragmaAuthenticity pragmaAuth = (AvatarPragmaAuthenticity) pragma;
if (pragmaAuth.getAttrA().getState() == state2
&& pragmaAuth.getAttrA().getAttribute() == attribute2
&& pragmaAuth.getAttrB().getState() == state1
- && pragmaAuth.getAttrB().getAttribute() == attribute1)
- {
+ && pragmaAuth.getAttrB().getAttribute() == attribute1) {
this.results.put(pragma, result);
this.notifyListeners();
break;
@@ -352,9 +334,8 @@ public class ProVerifOutputAnalyzer {
}
}
- // This concerns a satsified weak authenticity check
- else if (str.contains(isTyped ? typedWeakAuth : untypedWeakAuth))
- {
+ // This concerns a satisfied weak authenticity check
+ else if (str.contains(isTyped ? typedWeakAuth : untypedWeakAuth)) {
if (previousAuthPragma != null)
{
@@ -365,8 +346,7 @@ public class ProVerifOutputAnalyzer {
}
// This concerns a failed weak authenticity check
- else if (str.contains(isTyped ? typedWeakNonAuth : untypedWeakNonAuth))
- {
+ else if (str.contains(isTyped ? typedWeakNonAuth : untypedWeakNonAuth)) {
if (previousAuthPragma != null)
{
@@ -407,8 +387,7 @@ public class ProVerifOutputAnalyzer {
}
}
- private AvatarAttribute getAvatarAttributeFromString(String name)
- {
+ private AvatarAttribute getAvatarAttributeFromString(String name) {
String[] tmp = name.split(AVATAR2ProVerif.ATTR_DELIM);
if (tmp.length != 2)
return null;
@@ -420,8 +399,7 @@ public class ProVerifOutputAnalyzer {
return block.getAvatarAttributeWithName(tmp[1]);
}
- private AvatarPragmaReachability getAvatarPragmaReachabilityFromString(String name)
- {
+ private AvatarPragmaReachability getAvatarPragmaReachabilityFromString(String name) {
String[] tmp = name.split(AVATAR2ProVerif.ATTR_DELIM);
if (tmp.length != 2)
return null;
@@ -437,8 +415,7 @@ public class ProVerifOutputAnalyzer {
return new AvatarPragmaReachability("reachability" + AVATAR2ProVerif.ATTR_DELIM + name, null, block, state);
}
- private AvatarState getAvatarStateFromString(String name)
- {
+ private AvatarState getAvatarStateFromString(String name) {
String[] tmp = name.split(AVATAR2ProVerif.ATTR_DELIM);
if (tmp.length != 2)
return null;
@@ -457,8 +434,7 @@ public class ProVerifOutputAnalyzer {
return this.results;
}
- public Map<AvatarPragmaSecret, ProVerifQueryResult> getConfidentialityResults()
- {
+ public Map<AvatarPragmaSecret, ProVerifQueryResult> getConfidentialityResults() {
if (this.results == null)
return null;
@@ -475,8 +451,7 @@ public class ProVerifOutputAnalyzer {
return resultMap;
}
- public Map<AvatarPragmaReachability, ProVerifQueryResult> getReachabilityResults()
- {
+ public Map<AvatarPragmaReachability, ProVerifQueryResult> getReachabilityResults() {
if (this.results == null)
return null;
@@ -493,8 +468,7 @@ public class ProVerifOutputAnalyzer {
return resultMap;
}
- public Map<AvatarPragmaAuthenticity, ProVerifQueryAuthResult> getAuthenticityResults()
- {
+ public Map<AvatarPragmaAuthenticity, ProVerifQueryAuthResult> getAuthenticityResults() {
if (this.results == null)
return null;
diff --git a/src/main/java/tmltranslator/TMLModeling.java b/src/main/java/tmltranslator/TMLModeling.java
index 6d865a15bf28e3d9b6f9afbd6777ceb67a84d4bf..981394732fb00894c75f0e659f3ef974a3d82e00 100755
--- a/src/main/java/tmltranslator/TMLModeling.java
+++ b/src/main/java/tmltranslator/TMLModeling.java
@@ -774,14 +774,15 @@ public class TMLModeling<E> {
Map<AvatarPragmaSecret, ProVerifQueryResult> confResults = pvoa.getConfidentialityResults();
for (AvatarPragmaSecret pragma : confResults.keySet()) {
- // System.out.println("pragma " +pragma);
+ //TraceManager.addDev("pragma " + pragma);
ProVerifQueryResult result = confResults.get(pragma);
+ //TraceManager.addDev("pragma " + pragma + " / result proved:" + result.isProved() + " result satisfied:" + result.isSatisfied());
if (!result.isProved())
continue;
int r = result.isSatisfied() ? 2 : 3;
- AvatarAttribute attr = pragma.getArg();
+ AvatarAttribute attr = pragma.getArg();
TMLChannel channel = getChannelByShortName(attr.getName().replaceAll("_chData", ""));
boolean invalidate = false;
@@ -796,12 +797,13 @@ public class TMLModeling<E> {
for (AvatarPragmaReachability reachPragma : reachResults.keySet()) {
if (reachPragma.getState().getName().equals("aftersignalstate_reachannel_" + channel.getName())) {
if (!reachResults.get(reachPragma).isSatisfied()) {
- invalidate = true;
+ TraceManager.addDev("invalidate = true ");
+ invalidate = true;
}
}
}
}
- //Next check if there exists a writechannel operator that sends unencrypted data
+ // Next check if there exists a writechannel operator that sends unencrypted data
boolean found = false;
for (TMLTask task : getTasks()) {
TMLActivity act = task.getActivityDiagram();
@@ -817,6 +819,7 @@ public class TMLModeling<E> {
}
}
if (!found) {
+ //TraceManager.addDev("not found, invalidate = true ");
invalidate = true;
}
for (TMLPortWithSecurityInformation port : channel.ports) {
@@ -831,6 +834,8 @@ public class TMLModeling<E> {
}
}
}
+ } else {
+ //TraceManager.addDev("Null channel for backtracing Confidentiality");
}
TMLRequest req = getRequestByName(attr.getName().replaceAll("_reqData", ""));
if (req != null) {
@@ -853,9 +858,11 @@ public class TMLModeling<E> {
}
}
+ //TraceManager.addDev("Attribute name to find channels: " + attr.getName());
List<String> channels = secChannelMap.get(attr.getName());
if (channels != null) {
for (String channelName : channels) {
+ //TraceManager.addDev("Handling channel " + channelName);
channel = getChannelByShortName(channelName);
if (channel != null) {
for (TMLPortWithSecurityInformation port : channel.ports) {
diff --git a/src/main/java/ui/GTURTLEModeling.java b/src/main/java/ui/GTURTLEModeling.java
index b657350360e1f6012bd6364e77280ea260226b55..5421ea11bae9f4f89ee8ae34a831049d79fdccab 100644
--- a/src/main/java/ui/GTURTLEModeling.java
+++ b/src/main/java/ui/GTURTLEModeling.java
@@ -2047,9 +2047,7 @@ public class GTURTLEModeling {
public boolean generateProVerifFromAVATAR(String _path, int _stateReachability, boolean _typed, boolean allowPrivateChannelDuplication, String loopLimit) {
//
- if (avatarspec != null) {
- //use avspec
- } else if (tmap != null) {
+ if (tmap != null) {
t2a = new TML2Avatar(tmap, false, true);
avatarspec = t2a.generateAvatarSpec(loopLimit);
if (mgui.isExperimentalOn()) {
diff --git a/src/main/java/ui/MainGUI.java b/src/main/java/ui/MainGUI.java
index 7b08781691a5e58032df6b50df1a02f71262057e..5232a0abf9a458dbd41bc12376f12c86a2cc3b53 100644
--- a/src/main/java/ui/MainGUI.java
+++ b/src/main/java/ui/MainGUI.java
@@ -4771,7 +4771,9 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener, Per
AvatarDesignPanel adp = (AvatarDesignPanel) tp;
adp.modelBacktracingProVerif(pvoa);
getCurrentTDiagramPanel().repaint();
+
} else if (tp instanceof TMLArchiPanel) {
+ TraceManager.addDev("Backtracing to TMLArchiPanel (" + getTabName(tp) + ")");
/*
* for (int i=0; i<tabs.size(); i++){ tp = (TURTLEPanel)(tabs.elementAt(i)); if
* (tp instanceof TMLComponentDesignPanel) {
@@ -4781,7 +4783,9 @@ public class MainGUI implements ActionListener, WindowListener, KeyListener, Per
gtm.getTMLMapping().getTMLModeling().backtrace(pvoa, getTabName(tp));
gtm.getTML2Avatar().backtraceReachability(pvoa.getReachabilityResults());
gtm.getTMLMapping().getTMLModeling().backtraceAuthenticity(pvoa, getTabName(tp));
+
} else if (tp instanceof TMLComponentDesignPanel) {
+ TraceManager.addDev("Backtracing to TMLComponentDesignPanel");
gtm.getTMLMapping().getTMLModeling().clearBacktracing();
gtm.getTMLMapping().getTMLModeling().backtrace(pvoa, "Default Mapping");
gtm.getTML2Avatar().backtraceReachability(pvoa.getReachabilityResults());
diff --git a/src/main/java/ui/tmlcompd/TMLCPrimitivePort.java b/src/main/java/ui/tmlcompd/TMLCPrimitivePort.java
index 17ff393066d067798d4c9f0dd25b825ca5727eef..af00092c2985b2c7da12193f9257bc4a68a9472a 100755
--- a/src/main/java/ui/tmlcompd/TMLCPrimitivePort.java
+++ b/src/main/java/ui/tmlcompd/TMLCPrimitivePort.java
@@ -83,17 +83,23 @@
public boolean isOrigin = true;
public int typep = 0;
public String commName;
+
+
+
//Security Verification
public int checkConfStatus;
public int checkSecConfStatus;
public String secName = "";
+
public int checkWeakAuthStatus;
public int checkStrongAuthStatus;
public boolean checkConf;
public boolean checkAuth;
public String mappingName = "???";
public int verification;
+
+
public String oldName;
protected Color myColor;
protected int orientation;
diff --git a/src/main/java/ui/window/JDialogProverifVerification.java b/src/main/java/ui/window/JDialogProverifVerification.java
index 70bb34aaeef552bac41be2e8c06440ae88f96cc8..4391c4f3582cf57aeea7a104f200daacf8409917 100644
--- a/src/main/java/ui/window/JDialogProverifVerification.java
+++ b/src/main/java/ui/window/JDialogProverifVerification.java
@@ -121,7 +121,8 @@ import ui.util.IconManager;
* @version 1.0 19/02/2017
*/
-public class JDialogProverifVerification extends JDialog implements ActionListener, ListSelectionListener, MouseListener, Runnable, MasterProcessInterface, ProVerifOutputListener {
+public class JDialogProverifVerification extends JDialog implements ActionListener, ListSelectionListener, MouseListener, Runnable,
+ MasterProcessInterface, ProVerifOutputListener {
private static final Insets insets = new Insets(0, 0, 0, 0);
private static final Insets WEST_INSETS = new Insets(0, 0, 0, 0);
@@ -1048,6 +1049,9 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
@Override
public void proVerifOutputChanged() {
+
+ //TraceManager.addDev("Proverif output changed");
+
JLabel label;
this.jta.removeAll();