diff --git a/doc/SysMLSec/fig/autogen2_t1.svg b/doc/SysMLSec/fig/autogen2_t1.svg
new file mode 100644
index 0000000000000000000000000000000000000000..bc04d9e8254e0c7038fb70ae39149c4815782b93
--- /dev/null
+++ b/doc/SysMLSec/fig/autogen2_t1.svg
@@ -0,0 +1,565 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<svg
+ xmlns:dc="http://purl.org/dc/elements/1.1/"
+ xmlns:cc="http://creativecommons.org/ns#"
+ xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
+ xmlns:svg="http://www.w3.org/2000/svg"
+ xmlns="http://www.w3.org/2000/svg"
+ xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
+ xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
+ version="1.1"
+ width="246.33398"
+ height="305.09903"
+ viewbox="348 46 133 324"
+ id="svg2"
+ inkscape:version="0.48.4 r9939"
+ sodipodi:docname="autogen2_t1.svg">
+ <metadata
+ id="metadata160">
+ <rdf:RDF>
+ <cc:Work
+ rdf:about="">
+ <dc:format>image/svg+xml</dc:format>
+ <dc:type
+ rdf:resource="http://purl.org/dc/dcmitype/StillImage" />
+ </cc:Work>
+ </rdf:RDF>
+ </metadata>
+ <defs
+ id="defs158" />
+ <sodipodi:namedview
+ pagecolor="#ffffff"
+ bordercolor="#666666"
+ borderopacity="1"
+ objecttolerance="10"
+ gridtolerance="10"
+ guidetolerance="10"
+ inkscape:pageopacity="0"
+ inkscape:pageshadow="2"
+ inkscape:window-width="2048"
+ inkscape:window-height="1086"
+ id="namedview156"
+ showgrid="false"
+ fit-margin-top="0"
+ fit-margin-left="0"
+ fit-margin-right="0"
+ fit-margin-bottom="0"
+ inkscape:zoom="0.89086634"
+ inkscape:cx="-290.68141"
+ inkscape:cy="268.80033"
+ inkscape:window-x="0"
+ inkscape:window-y="27"
+ inkscape:window-maximized="1"
+ inkscape:current-layer="svg2" />
+ <line
+ x1="91.5"
+ y1="245.59904"
+ x2="91.5"
+ y2="279.59903"
+ id="line4"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <polygon
+ points="414,340 409,331 418,331 "
+ id="polygon6"
+ style="fill:#000000"
+ transform="translate(-322.5,-60.400961)" />
+ <polygon
+ points="414,340 409,331 418,331 "
+ id="polygon8"
+ style="fill:none;stroke:#000000;stroke-width:1"
+ transform="translate(-322.5,-60.400961)" />
+ <line
+ x1="91.5"
+ y1="10.599039"
+ x2="91.5"
+ y2="58.599037"
+ id="line10"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <polygon
+ points="414,119 409,110 418,110 "
+ id="polygon12"
+ style="fill:#000000"
+ transform="translate(-322.5,-60.400961)" />
+ <polygon
+ points="414,119 409,110 418,110 "
+ id="polygon14"
+ style="fill:none;stroke:#000000;stroke-width:1"
+ transform="translate(-322.5,-60.400961)" />
+ <ellipse
+ cx="414"
+ cy="58"
+ rx="7"
+ ry="7"
+ id="ellipse16"
+ sodipodi:cx="414"
+ sodipodi:cy="58"
+ sodipodi:rx="7"
+ sodipodi:ry="7"
+ transform="translate(-322.07906,-51)"
+ style="fill:#000000" />
+ <line
+ x1="91.5"
+ y1="5.5990386"
+ x2="91.5"
+ y2="10.599039"
+ id="line18"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <polygon
+ points="437,301 382,301 382,281 437,281 447,291 "
+ id="polygon20"
+ style="fill:#68e5ff"
+ transform="translate(-322.5,-60.400961)" />
+ <line
+ x1="91.5"
+ y1="220.59904"
+ x2="91.5"
+ y2="215.59904"
+ id="line22"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="91.5"
+ y1="240.59904"
+ x2="91.5"
+ y2="245.59904"
+ id="line24"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="60.5"
+ y1="221.59904"
+ x2="115.5"
+ y2="221.59904"
+ id="line26"
+ style="fill:none;stroke:#68e5ff;stroke-width:1" />
+ <line
+ x1="60.5"
+ y1="241.59904"
+ x2="115.5"
+ y2="241.59904"
+ id="line28"
+ style="fill:none;stroke:#68e5ff;stroke-width:1" />
+ <line
+ x1="60.5"
+ y1="221.59904"
+ x2="60.5"
+ y2="241.59904"
+ id="line30"
+ style="fill:none;stroke:#68e5ff;stroke-width:1" />
+ <line
+ x1="115.5"
+ y1="221.59904"
+ x2="125.5"
+ y2="231.59904"
+ id="line32"
+ style="fill:none;stroke:#68e5ff;stroke-width:1" />
+ <line
+ x1="115.5"
+ y1="241.59904"
+ x2="125.5"
+ y2="231.59904"
+ id="line34"
+ style="fill:none;stroke:#68e5ff;stroke-width:1" />
+ <line
+ x1="59.5"
+ y1="220.59904"
+ x2="114.5"
+ y2="220.59904"
+ id="line36"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="59.5"
+ y1="240.59904"
+ x2="114.5"
+ y2="240.59904"
+ id="line38"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="59.5"
+ y1="220.59904"
+ x2="59.5"
+ y2="240.59904"
+ id="line40"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="114.5"
+ y1="220.59904"
+ x2="124.5"
+ y2="230.59904"
+ id="line42"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="114.5"
+ y1="240.59904"
+ x2="124.5"
+ y2="230.59904"
+ id="line44"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <text
+ x="58.745453"
+ y="218.86275"
+ style="font-size:12px;font-family:SansSerif"
+ id="text46">chl</text>
+ <text
+ x="64.5"
+ y="235.59904"
+ style="font-size:12px;font-family:SansSerif"
+ id="text48">comm(1)</text>
+ <text
+ x="99.165833"
+ y="254.60689"
+ style="font-size:12px;font-family:SansSerif"
+ id="text50">sec:autoEncrypt_comm</text>
+ <line
+ x1="29.5"
+ y1="217.59904"
+ x2="44.5"
+ y2="217.59904"
+ id="line52"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <polygon
+ points="367,278 358,282 358,273 "
+ id="polygon54"
+ style="fill:#000000"
+ transform="translate(-322.5,-60.400961)" />
+ <polygon
+ points="367,278 358,282 358,273 "
+ id="polygon56"
+ style="fill:none;stroke:#000000;stroke-width:1"
+ transform="translate(-322.5,-60.400961)" />
+ <ellipse
+ cx="374"
+ cy="275"
+ rx="3"
+ ry="4"
+ id="ellipse58"
+ sodipodi:cx="374"
+ sodipodi:cy="275"
+ sodipodi:rx="3"
+ sodipodi:ry="4"
+ style="fill:none;stroke:#000000;stroke-width:1"
+ transform="translate(-322.5,-60.400961)" />
+ <rect
+ x="47.5"
+ y="213.59904"
+ width="9.240202"
+ height="7.5378509"
+ id="rect60"
+ style="fill:#00ff00" />
+ <rect
+ x="47.5"
+ y="213.59904"
+ width="9"
+ height="7"
+ id="rect62"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <ellipse
+ cx="414"
+ cy="355"
+ rx="8"
+ ry="8"
+ id="ellipse64"
+ sodipodi:cx="414"
+ sodipodi:cy="355"
+ sodipodi:rx="8"
+ sodipodi:ry="8"
+ style="fill:#000000"
+ transform="translate(-322.5,-60.400961)" />
+ <ellipse
+ cx="414"
+ cy="355"
+ rx="10"
+ ry="10"
+ id="ellipse66"
+ sodipodi:cx="414"
+ sodipodi:cy="355"
+ sodipodi:rx="10"
+ sodipodi:ry="10"
+ style="fill:none;stroke:#000000;stroke-width:1"
+ transform="translate(-322.5,-60.400961)" />
+ <line
+ x1="91.5"
+ y1="284.59903"
+ x2="91.5"
+ y2="279.59903"
+ id="line68"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <polygon
+ points="353,144 363,134 353,124 476,124 476,144 "
+ id="polygon70"
+ style="fill:#68e5ff"
+ transform="translate(-322.5,-60.400961)" />
+ <line
+ x1="91.5"
+ y1="63.599037"
+ x2="91.5"
+ y2="58.599037"
+ id="line72"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="91.5"
+ y1="83.599037"
+ x2="91.5"
+ y2="88.599037"
+ id="line74"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="31.5"
+ y1="64.599037"
+ x2="154.5"
+ y2="64.599037"
+ id="line76"
+ style="fill:none;stroke:#68e5ff;stroke-width:1" />
+ <line
+ x1="154.5"
+ y1="64.599037"
+ x2="154.5"
+ y2="84.599037"
+ id="line78"
+ style="fill:none;stroke:#68e5ff;stroke-width:1" />
+ <line
+ x1="31.5"
+ y1="84.599037"
+ x2="154.5"
+ y2="84.599037"
+ id="line80"
+ style="fill:none;stroke:#68e5ff;stroke-width:1" />
+ <line
+ x1="31.5"
+ y1="64.599037"
+ x2="41.5"
+ y2="74.599037"
+ id="line82"
+ style="fill:none;stroke:#68e5ff;stroke-width:1" />
+ <line
+ x1="31.5"
+ y1="84.599037"
+ x2="41.5"
+ y2="74.599037"
+ id="line84"
+ style="fill:none;stroke:#68e5ff;stroke-width:1" />
+ <line
+ x1="30.5"
+ y1="63.599037"
+ x2="153.5"
+ y2="63.599037"
+ id="line86"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="153.5"
+ y1="63.599037"
+ x2="153.5"
+ y2="83.599037"
+ id="line88"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="30.5"
+ y1="83.599037"
+ x2="153.5"
+ y2="83.599037"
+ id="line90"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="30.5"
+ y1="63.599037"
+ x2="40.5"
+ y2="73.599037"
+ id="line92"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="30.5"
+ y1="83.599037"
+ x2="40.5"
+ y2="73.599037"
+ id="line94"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <text
+ x="35.5"
+ y="63.599037"
+ style="font-size:12px;font-family:SansSerif"
+ id="text96">chl</text>
+ <text
+ x="42.5"
+ y="78.599037"
+ style="font-size:12px;font-family:SansSerif"
+ id="text98">nonceChT2_T1(1)</text>
+ <text
+ x="122.5"
+ y="98.599037"
+ style="font-size:12px;font-family:SansSerif"
+ id="text100">sec:nonce_T2_T1</text>
+ <line
+ x1="0.5"
+ y1="60.599037"
+ x2="15.5"
+ y2="60.599037"
+ id="line102"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <polygon
+ points="338,121 329,125 329,116 "
+ id="polygon104"
+ style="fill:#000000"
+ transform="translate(-322.5,-60.400961)" />
+ <polygon
+ points="338,121 329,125 329,116 "
+ id="polygon106"
+ style="fill:none;stroke:#000000;stroke-width:1"
+ transform="translate(-322.5,-60.400961)" />
+ <ellipse
+ cx="345"
+ cy="118"
+ rx="3"
+ ry="4"
+ id="ellipse108"
+ sodipodi:cx="345"
+ sodipodi:cy="118"
+ sodipodi:rx="3"
+ sodipodi:ry="4"
+ style="fill:none;stroke:#000000;stroke-width:1"
+ transform="translate(-322.5,-60.400961)" />
+ <rect
+ x="18.78064"
+ y="56.879654"
+ width="8.5612516"
+ height="6.9821901"
+ id="rect110"
+ style="fill:#00ff00" />
+ <rect
+ x="18.5"
+ y="56.599037"
+ width="9"
+ height="7"
+ id="rect112"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="91.5"
+ y1="88.599037"
+ x2="91.5"
+ y2="139.59904"
+ id="line114"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <polygon
+ points="414,200 409,191 418,191 "
+ id="polygon116"
+ style="fill:#000000"
+ transform="translate(-322.5,-60.400961)" />
+ <polygon
+ points="414,200 409,191 418,191 "
+ id="polygon118"
+ style="fill:none;stroke:#000000;stroke-width:1"
+ transform="translate(-322.5,-60.400961)" />
+ <rect
+ x="84.5"
+ y="144.59904"
+ width="14.892945"
+ height="35.140987"
+ id="rect120"
+ style="fill:#c7f369" />
+ <polygon
+ points="407,240 422,240 414,245 "
+ id="polygon122"
+ style="fill:#c7f369"
+ transform="translate(-322.5,-60.400961)" />
+ <line
+ x1="84.5"
+ y1="144.59904"
+ x2="99.5"
+ y2="144.59904"
+ id="line124"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="84.5"
+ y1="144.59904"
+ x2="84.5"
+ y2="179.59904"
+ id="line126"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="99.5"
+ y1="144.59904"
+ x2="99.5"
+ y2="179.59904"
+ id="line128"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="84.5"
+ y1="179.59904"
+ x2="91.5"
+ y2="184.59904"
+ id="line130"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="91.5"
+ y1="184.59904"
+ x2="99.5"
+ y2="179.59904"
+ id="line132"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="91.5"
+ y1="144.59904"
+ x2="91.5"
+ y2="139.59904"
+ id="line134"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="91.5"
+ y1="184.59904"
+ x2="91.5"
+ y2="189.59904"
+ id="line136"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="87.5"
+ y1="155.59904"
+ x2="87.5"
+ y2="167.59904"
+ id="line138"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="96.5"
+ y1="155.59904"
+ x2="96.5"
+ y2="167.59904"
+ id="line140"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="87.5"
+ y1="155.59904"
+ x2="91.5"
+ y2="167.59904"
+ id="line142"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="96.5"
+ y1="155.59904"
+ x2="91.5"
+ y2="167.59904"
+ id="line144"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <text
+ x="106.5"
+ y="161.59904"
+ style="font-size:12px;font-family:SansSerif"
+ id="text146">sec:autoEncrypt_comm</text>
+ <text
+ x="106.5"
+ y="169.59904"
+ style="font-size:12px;font-family:SansSerif"
+ id="text148">nonce:nonce_T2_T1</text>
+ <line
+ x1="91.5"
+ y1="189.59904"
+ x2="91.5"
+ y2="215.59904"
+ id="line150"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <polygon
+ points="414,276 409,267 418,267 "
+ id="polygon152"
+ style="fill:#000000"
+ transform="translate(-322.5,-60.400961)" />
+ <polygon
+ points="414,276 409,267 418,267 "
+ id="polygon154"
+ style="fill:none;stroke:#000000;stroke-width:1"
+ transform="translate(-322.5,-60.400961)" />
+</svg>
diff --git a/doc/SysMLSec/fig/autogen2_t2.svg b/doc/SysMLSec/fig/autogen2_t2.svg
new file mode 100644
index 0000000000000000000000000000000000000000..779dde55b5643db9b917005eb6b47a4bd3c9ea3b
--- /dev/null
+++ b/doc/SysMLSec/fig/autogen2_t2.svg
@@ -0,0 +1,649 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<svg
+ xmlns:dc="http://purl.org/dc/elements/1.1/"
+ xmlns:cc="http://creativecommons.org/ns#"
+ xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
+ xmlns:svg="http://www.w3.org/2000/svg"
+ xmlns="http://www.w3.org/2000/svg"
+ xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
+ xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
+ version="1.1"
+ width="246.33398"
+ height="405.09109"
+ viewbox="350 63 129 421"
+ id="svg2"
+ inkscape:version="0.48.4 r9939"
+ sodipodi:docname="autogen2_t2.svg">
+ <metadata
+ id="metadata184">
+ <rdf:RDF>
+ <cc:Work
+ rdf:about="">
+ <dc:format>image/svg+xml</dc:format>
+ <dc:type
+ rdf:resource="http://purl.org/dc/dcmitype/StillImage" />
+ </cc:Work>
+ </rdf:RDF>
+ </metadata>
+ <defs
+ id="defs182" />
+ <sodipodi:namedview
+ pagecolor="#ffffff"
+ bordercolor="#666666"
+ borderopacity="1"
+ objecttolerance="10"
+ gridtolerance="10"
+ guidetolerance="10"
+ inkscape:pageopacity="0"
+ inkscape:pageshadow="2"
+ inkscape:window-width="2048"
+ inkscape:window-height="1086"
+ id="namedview180"
+ showgrid="false"
+ fit-margin-top="0"
+ fit-margin-left="0"
+ fit-margin-right="0"
+ fit-margin-bottom="0"
+ inkscape:zoom="0.97520661"
+ inkscape:cx="-135.77847"
+ inkscape:cy="94.251186"
+ inkscape:window-x="0"
+ inkscape:window-y="27"
+ inkscape:window-maximized="1"
+ inkscape:current-layer="svg2" />
+ <line
+ x1="89.5"
+ y1="228.59109"
+ x2="89.5"
+ y2="271.59109"
+ id="line4"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <polygon
+ points="414,346 409,337 418,337 "
+ id="polygon6"
+ style="fill:#000000"
+ transform="translate(-324.5,-74.408898)" />
+ <polygon
+ points="414,346 409,337 418,337 "
+ id="polygon8"
+ style="fill:none;stroke:#000000;stroke-width:1"
+ transform="translate(-324.5,-74.408898)" />
+ <line
+ x1="89.5"
+ y1="13.591102"
+ x2="89.5"
+ y2="40.591103"
+ id="line10"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <polygon
+ points="414,115 409,106 418,106 "
+ id="polygon12"
+ style="fill:#000000"
+ transform="translate(-324.5,-74.408898)" />
+ <polygon
+ points="414,115 409,106 418,106 "
+ id="polygon14"
+ style="fill:none;stroke:#000000;stroke-width:1"
+ transform="translate(-324.5,-74.408898)" />
+ <ellipse
+ cx="414"
+ cy="75"
+ rx="7"
+ ry="7"
+ id="ellipse16"
+ sodipodi:cx="414"
+ sodipodi:cy="75"
+ sodipodi:rx="7"
+ sodipodi:ry="7"
+ transform="translate(-325.14089,-68)"
+ style="fill:#000000" />
+ <line
+ x1="89.5"
+ y1="8.5911016"
+ x2="89.5"
+ y2="13.591102"
+ id="line18"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <polygon
+ points="380,298 390,288 380,278 449,278 449,298 "
+ id="polygon20"
+ style="fill:#68e5ff"
+ transform="translate(-324.5,-74.408898)" />
+ <line
+ x1="89.5"
+ y1="203.59109"
+ x2="89.5"
+ y2="198.59109"
+ id="line22"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="89.5"
+ y1="223.59109"
+ x2="89.5"
+ y2="228.59109"
+ id="line24"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="56.5"
+ y1="204.59109"
+ x2="125.5"
+ y2="204.59109"
+ id="line26"
+ style="fill:none;stroke:#68e5ff;stroke-width:1" />
+ <line
+ x1="125.5"
+ y1="204.59109"
+ x2="125.5"
+ y2="224.59109"
+ id="line28"
+ style="fill:none;stroke:#68e5ff;stroke-width:1" />
+ <line
+ x1="56.5"
+ y1="224.59109"
+ x2="125.5"
+ y2="224.59109"
+ id="line30"
+ style="fill:none;stroke:#68e5ff;stroke-width:1" />
+ <line
+ x1="56.5"
+ y1="204.59109"
+ x2="66.5"
+ y2="214.59109"
+ id="line32"
+ style="fill:none;stroke:#68e5ff;stroke-width:1" />
+ <line
+ x1="56.5"
+ y1="224.59109"
+ x2="66.5"
+ y2="214.59109"
+ id="line34"
+ style="fill:none;stroke:#68e5ff;stroke-width:1" />
+ <line
+ x1="55.5"
+ y1="203.59109"
+ x2="124.5"
+ y2="203.59109"
+ id="line36"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="124.5"
+ y1="203.59109"
+ x2="124.5"
+ y2="223.59109"
+ id="line38"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="55.5"
+ y1="223.59109"
+ x2="124.5"
+ y2="223.59109"
+ id="line40"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="55.5"
+ y1="203.59109"
+ x2="65.5"
+ y2="213.59109"
+ id="line42"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="55.5"
+ y1="223.59109"
+ x2="65.5"
+ y2="213.59109"
+ id="line44"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <text
+ x="60.5"
+ y="203.59109"
+ style="font-size:12px;font-family:SansSerif"
+ id="text46">chl</text>
+ <text
+ x="67.5"
+ y="218.59109"
+ style="font-size:12px;font-family:SansSerif"
+ id="text48">comm(1)</text>
+ <text
+ x="106.5"
+ y="238.59109"
+ style="font-size:12px;font-family:SansSerif"
+ id="text50">sec:autoEncrypt_comm</text>
+ <line
+ x1="25.5"
+ y1="200.59109"
+ x2="40.5"
+ y2="200.59109"
+ id="line52"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <polygon
+ points="365,275 356,279 356,270 "
+ id="polygon54"
+ style="fill:#000000"
+ transform="translate(-324.5,-74.408898)" />
+ <polygon
+ points="365,275 356,279 356,270 "
+ id="polygon56"
+ style="fill:none;stroke:#000000;stroke-width:1"
+ transform="translate(-324.5,-74.408898)" />
+ <ellipse
+ cx="372"
+ cy="272"
+ rx="3"
+ ry="4"
+ id="ellipse58"
+ sodipodi:cx="372"
+ sodipodi:cy="272"
+ sodipodi:rx="3"
+ sodipodi:ry="4"
+ style="fill:none;stroke:#000000;stroke-width:1"
+ transform="translate(-324.5,-74.408898)" />
+ <rect
+ x="43.5"
+ y="196.59109"
+ width="9.2817793"
+ height="6.9613347"
+ id="rect60"
+ style="fill:#00ff00" />
+ <rect
+ x="43.5"
+ y="196.59109"
+ width="9"
+ height="7"
+ id="rect62"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <ellipse
+ cx="414"
+ cy="469"
+ rx="8"
+ ry="8"
+ id="ellipse64"
+ sodipodi:cx="414"
+ sodipodi:cy="469"
+ sodipodi:rx="8"
+ sodipodi:ry="8"
+ style="fill:#000000"
+ transform="translate(-324.5,-74.408898)" />
+ <ellipse
+ cx="414"
+ cy="469"
+ rx="10"
+ ry="10"
+ id="ellipse66"
+ sodipodi:cx="414"
+ sodipodi:cy="469"
+ sodipodi:rx="10"
+ sodipodi:ry="10"
+ style="fill:none;stroke:#000000;stroke-width:1"
+ transform="translate(-324.5,-74.408898)" />
+ <line
+ x1="89.5"
+ y1="384.59109"
+ x2="89.5"
+ y2="379.59109"
+ id="line68"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <rect
+ x="82.5"
+ y="45.591103"
+ width="15.345869"
+ height="34.640892"
+ id="rect70"
+ style="fill:#c7f369" />
+ <polygon
+ points="422,155 414,160 407,155 "
+ id="polygon72"
+ transform="matrix(1,0,0,1.1025424,-324.5,-90.815678)"
+ style="fill:#c7f369" />
+ <line
+ x1="82.5"
+ y1="45.591103"
+ x2="97.5"
+ y2="45.591103"
+ id="line74"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="82.5"
+ y1="45.591103"
+ x2="82.5"
+ y2="80.591103"
+ id="line76"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="97.5"
+ y1="45.591103"
+ x2="97.5"
+ y2="80.591103"
+ id="line78"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="82.5"
+ y1="80.591103"
+ x2="89.5"
+ y2="85.591103"
+ id="line80"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="89.5"
+ y1="85.591103"
+ x2="97.5"
+ y2="80.591103"
+ id="line82"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="89.5"
+ y1="45.591103"
+ x2="89.5"
+ y2="40.591103"
+ id="line84"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="89.5"
+ y1="85.591103"
+ x2="89.5"
+ y2="90.591103"
+ id="line86"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="86.5"
+ y1="56.591103"
+ x2="86.5"
+ y2="68.591103"
+ id="line88"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="92.5"
+ y1="56.591103"
+ x2="92.5"
+ y2="68.591103"
+ id="line90"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="86.5"
+ y1="56.591103"
+ x2="92.5"
+ y2="68.591103"
+ id="line92"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <text
+ x="104.5"
+ y="62.591103"
+ style="font-size:12px;font-family:SansSerif"
+ id="text94">sec:nonce_T2_T1</text>
+ <polygon
+ points="464,222 355,222 355,202 464,202 474,212 "
+ id="polygon96"
+ style="fill:#68e5ff"
+ transform="translate(-324.5,-74.408898)" />
+ <line
+ x1="89.5"
+ y1="127.5911"
+ x2="89.5"
+ y2="122.5911"
+ id="line98"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="89.5"
+ y1="147.59109"
+ x2="89.5"
+ y2="152.59109"
+ id="line100"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="31.5"
+ y1="128.59109"
+ x2="140.5"
+ y2="128.59109"
+ id="line102"
+ style="fill:none;stroke:#68e5ff;stroke-width:1" />
+ <line
+ x1="31.5"
+ y1="148.59109"
+ x2="140.5"
+ y2="148.59109"
+ id="line104"
+ style="fill:none;stroke:#68e5ff;stroke-width:1" />
+ <line
+ x1="31.5"
+ y1="128.59109"
+ x2="31.5"
+ y2="148.59109"
+ id="line106"
+ style="fill:none;stroke:#68e5ff;stroke-width:1" />
+ <line
+ x1="140.5"
+ y1="128.59109"
+ x2="150.5"
+ y2="138.59109"
+ id="line108"
+ style="fill:none;stroke:#68e5ff;stroke-width:1" />
+ <line
+ x1="140.5"
+ y1="148.59109"
+ x2="150.5"
+ y2="138.59109"
+ id="line110"
+ style="fill:none;stroke:#68e5ff;stroke-width:1" />
+ <line
+ x1="30.5"
+ y1="127.5911"
+ x2="139.5"
+ y2="127.5911"
+ id="line112"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="30.5"
+ y1="147.59109"
+ x2="139.5"
+ y2="147.59109"
+ id="line114"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="30.5"
+ y1="127.5911"
+ x2="30.5"
+ y2="147.59109"
+ id="line116"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="139.5"
+ y1="127.5911"
+ x2="149.5"
+ y2="137.59109"
+ id="line118"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="139.5"
+ y1="147.59109"
+ x2="149.5"
+ y2="137.59109"
+ id="line120"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <text
+ x="30.152496"
+ y="125.77839"
+ style="font-size:12px;font-family:SansSerif"
+ id="text122">chl</text>
+ <text
+ x="35.5"
+ y="142.59109"
+ style="font-size:12px;font-family:SansSerif"
+ id="text124">nonceChT2_T1(1)</text>
+ <text
+ x="119.5"
+ y="162.59109"
+ style="font-size:12px;font-family:SansSerif"
+ id="text126">sec:nonce_T2_T1</text>
+ <line
+ x1="0.5"
+ y1="124.5911"
+ x2="15.5"
+ y2="124.5911"
+ id="line128"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <polygon
+ points="340,199 331,203 331,194 "
+ id="polygon130"
+ style="fill:#000000"
+ transform="translate(-324.5,-74.408898)" />
+ <polygon
+ points="340,199 331,203 331,194 "
+ id="polygon132"
+ style="fill:none;stroke:#000000;stroke-width:1"
+ transform="translate(-324.5,-74.408898)" />
+ <ellipse
+ cx="347"
+ cy="196"
+ rx="3"
+ ry="4"
+ id="ellipse134"
+ sodipodi:cx="347"
+ sodipodi:cy="196"
+ sodipodi:rx="3"
+ sodipodi:ry="4"
+ style="fill:none;stroke:#000000;stroke-width:1"
+ transform="translate(-324.5,-74.408898)" />
+ <rect
+ x="18.953186"
+ y="120.95365"
+ width="8.1812706"
+ height="6.4531775"
+ id="rect136"
+ style="fill:#00ff00" />
+ <rect
+ x="18.5"
+ y="120.5911"
+ width="9"
+ height="7"
+ id="rect138"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="89.5"
+ y1="90.591103"
+ x2="89.5"
+ y2="122.5911"
+ id="line140"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <polygon
+ points="414,197 409,188 418,188 "
+ id="polygon142"
+ style="fill:#000000"
+ transform="translate(-324.5,-74.408898)" />
+ <polygon
+ points="414,197 409,188 418,188 "
+ id="polygon144"
+ style="fill:none;stroke:#000000;stroke-width:1"
+ transform="translate(-324.5,-74.408898)" />
+ <line
+ x1="89.5"
+ y1="152.59109"
+ x2="89.5"
+ y2="198.59109"
+ id="line146"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <polygon
+ points="414,273 409,264 418,264 "
+ id="polygon148"
+ style="fill:#000000"
+ transform="translate(-324.5,-74.408898)" />
+ <polygon
+ points="414,273 409,264 418,264 "
+ id="polygon150"
+ style="fill:none;stroke:#000000;stroke-width:1"
+ transform="translate(-324.5,-74.408898)" />
+ <rect
+ x="82.5"
+ y="276.59109"
+ width="15.089513"
+ height="34.76907"
+ id="rect152"
+ style="fill:#c7f369" />
+ <polygon
+ points="422,386 414,391 407,386 "
+ id="polygon154"
+ transform="matrix(1,0,0,1.1538136,-324.5,-134.55)"
+ style="fill:#c7f369" />
+ <line
+ x1="82.5"
+ y1="276.59109"
+ x2="97.5"
+ y2="276.59109"
+ id="line156"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="82.5"
+ y1="276.59109"
+ x2="82.5"
+ y2="311.59109"
+ id="line158"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="97.5"
+ y1="276.59109"
+ x2="97.5"
+ y2="311.59109"
+ id="line160"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="82.5"
+ y1="311.59109"
+ x2="89.5"
+ y2="316.59109"
+ id="line162"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="89.5"
+ y1="316.59109"
+ x2="97.5"
+ y2="311.59109"
+ id="line164"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="89.5"
+ y1="276.59109"
+ x2="89.5"
+ y2="271.59109"
+ id="line166"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="89.5"
+ y1="316.59109"
+ x2="89.5"
+ y2="321.59109"
+ id="line168"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="87.5"
+ y1="283.59109"
+ x2="87.5"
+ y2="303.59109"
+ id="line170"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <text
+ x="104.5"
+ y="293.59109"
+ style="font-size:12px;font-family:SansSerif"
+ id="text172">sec:autoEncrypt_comm</text>
+ <line
+ x1="89.5"
+ y1="321.59109"
+ x2="89.5"
+ y2="379.59109"
+ id="line174"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <polygon
+ points="414,454 409,445 418,445 "
+ id="polygon176"
+ style="fill:#000000"
+ transform="translate(-324.5,-74.408898)" />
+ <polygon
+ points="414,454 409,445 418,445 "
+ id="polygon178"
+ style="fill:none;stroke:#000000;stroke-width:1"
+ transform="translate(-324.5,-74.408898)" />
+ <path
+ style="fill:none;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
+ d="m 86.3759,283.6321 c 9.46153,-1.13712 9.72864,19.92324 0.75368,19.73573"
+ id="path3019"
+ inkscape:connector-curvature="0"
+ sodipodi:nodetypes="cc" />
+</svg>
diff --git a/doc/SysMLSec/fig/autogen_fv.svg b/doc/SysMLSec/fig/autogen_fv.svg
new file mode 100644
index 0000000000000000000000000000000000000000..72910a6b02240b6cf6fba78af39a49627e93c839
--- /dev/null
+++ b/doc/SysMLSec/fig/autogen_fv.svg
@@ -0,0 +1,223 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<svg
+ xmlns:dc="http://purl.org/dc/elements/1.1/"
+ xmlns:cc="http://creativecommons.org/ns#"
+ xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
+ xmlns:svg="http://www.w3.org/2000/svg"
+ xmlns="http://www.w3.org/2000/svg"
+ xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
+ xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
+ version="1.1"
+ width="560"
+ height="151.6954"
+ viewbox="201 125 569 162"
+ id="svg2"
+ inkscape:version="0.48.4 r9939"
+ sodipodi:docname="autogen_fv.svg">
+ <metadata
+ id="metadata72">
+ <rdf:RDF>
+ <cc:Work
+ rdf:about="">
+ <dc:format>image/svg+xml</dc:format>
+ <dc:type
+ rdf:resource="http://purl.org/dc/dcmitype/StillImage" />
+ </cc:Work>
+ </rdf:RDF>
+ </metadata>
+ <defs
+ id="defs70" />
+ <sodipodi:namedview
+ pagecolor="#ffffff"
+ bordercolor="#666666"
+ borderopacity="1"
+ objecttolerance="10"
+ gridtolerance="10"
+ guidetolerance="10"
+ inkscape:pageopacity="0"
+ inkscape:pageshadow="2"
+ inkscape:window-width="2048"
+ inkscape:window-height="1086"
+ id="namedview68"
+ showgrid="false"
+ fit-margin-top="0"
+ fit-margin-left="0"
+ fit-margin-right="0"
+ fit-margin-bottom="0"
+ inkscape:zoom="4.4520178"
+ inkscape:cx="374.26159"
+ inkscape:cy="109.23576"
+ inkscape:window-x="0"
+ inkscape:window-y="27"
+ inkscape:window-maximized="1"
+ inkscape:current-layer="svg2" />
+ <rect
+ x="359.48895"
+ y="0.26354519"
+ width="199.00992"
+ height="150.80428"
+ id="rect32"
+ style="fill:#c9f3bc" />
+ <rect
+ x="0.26460266"
+ y="0.62308049"
+ width="200.18837"
+ height="150.68413"
+ id="rect6"
+ style="fill:#c9f3bc" />
+ <rect
+ x="0.5"
+ y="1.1954072"
+ width="200"
+ height="150"
+ id="rect4"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <text
+ x="91.5"
+ y="21.659958"
+ style="font-size:14px;font-family:SansSerif"
+ id="text8">T1</text>
+ <rect
+ x="187.5"
+ y="53.5"
+ width="25.952971"
+ height="25.873556"
+ id="rect10"
+ style="fill:#68e5ff" />
+ <rect
+ x="187.5"
+ y="53.5"
+ width="26"
+ height="26"
+ id="rect12"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <polygon
+ points="396,188 396,208 416,198 "
+ id="polygon14"
+ style="fill:none;stroke:#000000;stroke-width:1"
+ transform="translate(-205.5,-131.5)" />
+ <polygon
+ points="396,188 396,208 416,198 "
+ id="polygon16"
+ style="fill:#000000"
+ transform="translate(-205.5,-131.5)" />
+ <line
+ x1="211.29413"
+ y1="76.579407"
+ x2="211.29413"
+ y2="56.579407"
+ id="line18"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <text
+ x="187.5"
+ y="52.5"
+ style="font-size:8px;font-family:SansSerif"
+ id="text20">comm</text>
+ <rect
+ x="359.27539"
+ y="0.49999997"
+ width="200.22462"
+ height="150.67384"
+ id="rect30"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <text
+ x="450.5"
+ y="29.5"
+ style="font-size:14px;font-family:SansSerif"
+ id="text34">T2</text>
+ <rect
+ x="346.5"
+ y="53.5"
+ width="25.730005"
+ height="26.235395"
+ id="rect36"
+ style="fill:#68e5ff" />
+ <rect
+ x="346.5"
+ y="53.5"
+ width="26"
+ height="26"
+ id="rect38"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <polygon
+ points="555,188 555,208 575,198 "
+ id="polygon40"
+ style="fill:none;stroke:#000000;stroke-width:1"
+ transform="translate(-205.5,-131.5)" />
+ <polygon
+ points="555,188 555,208 575,198 "
+ id="polygon42"
+ style="fill:#000000"
+ transform="translate(-205.5,-131.5)" />
+ <line
+ x1="369.5"
+ y1="76.5"
+ x2="369.5"
+ y2="56.5"
+ id="line44"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <text
+ x="346.5"
+ y="52.5"
+ style="font-size:8px;font-family:SansSerif"
+ id="text46">comm</text>
+ <text
+ x="277.3349"
+ y="99.01107"
+ style="font-size:8px;font-family:SansSerif"
+ id="text48">autoEncrypt_comm</text>
+ <ellipse
+ cx="539"
+ cy="204"
+ rx="5"
+ ry="7"
+ id="ellipse50"
+ sodipodi:cx="539"
+ sodipodi:cy="204"
+ sodipodi:rx="5"
+ sodipodi:ry="7"
+ transform="translate(-204.93846,-127.34458)"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <polygon
+ points="532,219 548,219 532,203 "
+ id="polygon52"
+ transform="translate(-204.93846,-127.34458)"
+ style="fill:#ff0000" />
+ <polygon
+ points="548,203 532,203 548,219 "
+ id="polygon54"
+ transform="translate(-204.93846,-127.34458)"
+ style="fill:#00ff00" />
+ <polygon
+ points="532,219 548,219 532,203 "
+ id="polygon56"
+ transform="translate(-204.93846,-127.34458)"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <polygon
+ points="548,203 532,203 548,219 "
+ id="polygon58"
+ transform="translate(-204.93846,-127.34458)"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <text
+ x="328.06152"
+ y="87.655426"
+ style="font-size:8px;font-family:SansSerif"
+ id="text60">S</text>
+ <text
+ x="335.06152"
+ y="84.655426"
+ style="font-size:8px;font-family:SansSerif"
+ id="text62">W</text>
+ <text
+ x="261.5"
+ y="66.5"
+ style="font-size:12px;font-family:SansSerif"
+ id="text64">comm</text>
+ <line
+ x1="213.5"
+ y1="66.5"
+ x2="346.5"
+ y2="66.5"
+ id="line66"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+</svg>
diff --git a/doc/SysMLSec/fig/autogen_fv2.svg b/doc/SysMLSec/fig/autogen_fv2.svg
new file mode 100644
index 0000000000000000000000000000000000000000..721b64d9b24c92e6f0c35bab77fb677810026fc5
--- /dev/null
+++ b/doc/SysMLSec/fig/autogen_fv2.svg
@@ -0,0 +1,283 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<svg
+ xmlns:dc="http://purl.org/dc/elements/1.1/"
+ xmlns:cc="http://creativecommons.org/ns#"
+ xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
+ xmlns:svg="http://www.w3.org/2000/svg"
+ xmlns="http://www.w3.org/2000/svg"
+ xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
+ xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
+ version="1.1"
+ width="560"
+ height="153"
+ viewbox="5 5 775 292"
+ id="svg2"
+ inkscape:version="0.48.4 r9939"
+ sodipodi:docname="autogen_fv2.svg">
+ <metadata
+ id="metadata102">
+ <rdf:RDF>
+ <cc:Work
+ rdf:about="">
+ <dc:format>image/svg+xml</dc:format>
+ <dc:type
+ rdf:resource="http://purl.org/dc/dcmitype/StillImage" />
+ </cc:Work>
+ </rdf:RDF>
+ </metadata>
+ <defs
+ id="defs100" />
+ <sodipodi:namedview
+ pagecolor="#ffffff"
+ bordercolor="#666666"
+ borderopacity="1"
+ objecttolerance="10"
+ gridtolerance="10"
+ guidetolerance="10"
+ inkscape:pageopacity="0"
+ inkscape:pageshadow="2"
+ inkscape:window-width="2048"
+ inkscape:window-height="1086"
+ id="namedview98"
+ showgrid="false"
+ fit-margin-top="0"
+ fit-margin-left="0"
+ fit-margin-right="0"
+ fit-margin-bottom="0"
+ inkscape:zoom="0.77692308"
+ inkscape:cx="146.01142"
+ inkscape:cy="148.87138"
+ inkscape:window-x="0"
+ inkscape:window-y="27"
+ inkscape:window-maximized="1"
+ inkscape:current-layer="svg2" />
+ <rect
+ x="359.37378"
+ y="2.4139862"
+ width="200.60521"
+ height="150.16681"
+ id="rect40"
+ style="fill:#c9f3bc" />
+ <rect
+ x="0.85643005"
+ y="0.69554138"
+ width="199.93069"
+ height="150.73515"
+ id="rect6"
+ style="fill:#c9f3bc" />
+ <rect
+ x="0.5"
+ y="0.5"
+ width="200"
+ height="150"
+ id="rect4"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <text
+ x="91.5"
+ y="29.5"
+ style="font-size:14px;font-family:SansSerif"
+ id="text8">T1</text>
+ <rect
+ x="187.5"
+ y="8.5"
+ width="26.137672"
+ height="25.910137"
+ id="rect10"
+ style="fill:#68e5ff" />
+ <rect
+ x="187.5"
+ y="8.5"
+ width="26"
+ height="26"
+ id="rect12"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <polygon
+ points="416,141 416,161 396,151 "
+ id="polygon14"
+ style="fill:none;stroke:#000000;stroke-width:1"
+ transform="translate(-205.5,-129.5)" />
+ <polygon
+ points="416,141 416,161 396,151 "
+ id="polygon16"
+ style="fill:#000000"
+ transform="translate(-205.5,-129.5)" />
+ <rect
+ x="187.5"
+ y="55.5"
+ width="26.422091"
+ height="26.308323"
+ id="rect18"
+ style="fill:#68e5ff" />
+ <rect
+ x="187.5"
+ y="55.5"
+ width="26"
+ height="26"
+ id="rect20"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <polygon
+ points="396,188 396,208 416,198 "
+ id="polygon22"
+ style="fill:none;stroke:#000000;stroke-width:1"
+ transform="translate(-205.5,-129.5)" />
+ <polygon
+ points="396,188 396,208 416,198 "
+ id="polygon24"
+ style="fill:#000000"
+ transform="translate(-205.5,-129.5)" />
+ <line
+ x1="210.5"
+ y1="78.5"
+ x2="210.5"
+ y2="58.5"
+ id="line26"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <text
+ x="187.5"
+ y="54.5"
+ style="font-size:8px;font-family:SansSerif"
+ id="text28">comm</text>
+ <rect
+ x="359.5"
+ y="2.5"
+ width="200"
+ height="150"
+ id="rect38"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <text
+ x="450.5"
+ y="31.5"
+ style="font-size:14px;font-family:SansSerif"
+ id="text42">T2</text>
+ <rect
+ x="346.5"
+ y="8.5"
+ width="25.967022"
+ height="26.251438"
+ id="rect44"
+ style="fill:#68e5ff" />
+ <rect
+ x="346.5"
+ y="8.5"
+ width="26"
+ height="26"
+ id="rect46"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <polygon
+ points="575,141 575,161 555,151 "
+ id="polygon48"
+ style="fill:none;stroke:#ff0000;stroke-width:1"
+ transform="translate(-205.5,-129.5)" />
+ <polygon
+ points="575,141 575,161 555,151 "
+ id="polygon50"
+ style="fill:#000000;stroke:#000000"
+ transform="translate(-205.5,-129.5)" />
+ <rect
+ x="346.5"
+ y="55.5"
+ width="26.126238"
+ height="26.568687"
+ id="rect62"
+ style="fill:#68e5ff" />
+ <rect
+ x="346.5"
+ y="55.5"
+ width="26"
+ height="26"
+ id="rect64"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <polygon
+ points="555,188 555,208 575,198 "
+ id="polygon66"
+ style="fill:none;stroke:#8b4f0b;stroke-width:1"
+ transform="translate(-205.5,-129.5)" />
+ <polygon
+ points="555,188 555,208 575,198 "
+ id="polygon68"
+ style="fill:#000000;stroke:#000000"
+ transform="translate(-205.5,-129.5)" />
+ <line
+ x1="370.30444"
+ y1="78.580444"
+ x2="370.30444"
+ y2="58.580444"
+ id="line70"
+ style="fill:#000000;stroke:#000000;stroke-width:1" />
+ <text
+ x="346.5"
+ y="54.5"
+ style="font-size:8px;font-family:SansSerif"
+ id="text72">comm</text>
+ <text
+ x="279.71658"
+ y="99.056931"
+ style="font-size:8px;font-family:SansSerif"
+ id="text74">autoEncrypt_comm</text>
+ <ellipse
+ cx="539"
+ cy="204"
+ rx="5"
+ ry="7"
+ id="ellipse76"
+ style="fill:none;stroke:#000000;stroke-width:1"
+ sodipodi:cx="539"
+ sodipodi:cy="204"
+ sodipodi:rx="5"
+ sodipodi:ry="7"
+ transform="translate(-205.8413,-126.31452)" />
+ <polygon
+ points="532,219 548,219 532,203 "
+ id="polygon78"
+ style="fill:#00ff00;stroke:#000000"
+ transform="translate(-205.8413,-126.31452)" />
+ <polygon
+ points="548,203 532,203 548,219 "
+ id="polygon80"
+ transform="translate(-205.8413,-126.31452)"
+ style="fill:#00ff00" />
+ <polygon
+ points="532,219 548,219 532,203 "
+ id="polygon82"
+ style="fill:none;stroke:#000000;stroke-width:1"
+ transform="translate(-205.8413,-126.31452)" />
+ <polygon
+ points="548,203 532,203 548,219 "
+ id="polygon84"
+ style="fill:none;stroke:#000000;stroke-width:1"
+ transform="translate(-205.8413,-126.31452)" />
+ <text
+ x="327.15869"
+ y="88.685486"
+ style="font-size:8px;font-family:SansSerif"
+ id="text86">S</text>
+ <text
+ x="334.15869"
+ y="85.685486"
+ style="font-size:8px;font-family:SansSerif"
+ id="text88">W</text>
+ <text
+ x="261.5"
+ y="68.5"
+ style="font-size:12px;font-family:SansSerif"
+ id="text90">comm</text>
+ <line
+ x1="213.5"
+ y1="68.5"
+ x2="346.5"
+ y2="68.5"
+ id="line92"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <text
+ x="235.06311"
+ y="16.592819"
+ style="font-size:12px;font-family:SansSerif"
+ id="text94">nonceChT2_T1</text>
+ <line
+ x1="346.5"
+ y1="21.5"
+ x2="213.5"
+ y2="21.5"
+ id="line96"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+</svg>
diff --git a/doc/SysMLSec/fig/autogen_t1.svg b/doc/SysMLSec/fig/autogen_t1.svg
new file mode 100644
index 0000000000000000000000000000000000000000..8a87dd9f7c47db5b64aa3f365d6390596ac8074c
--- /dev/null
+++ b/doc/SysMLSec/fig/autogen_t1.svg
@@ -0,0 +1,396 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<svg
+ xmlns:dc="http://purl.org/dc/elements/1.1/"
+ xmlns:cc="http://creativecommons.org/ns#"
+ xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
+ xmlns:svg="http://www.w3.org/2000/svg"
+ xmlns="http://www.w3.org/2000/svg"
+ xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
+ xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
+ version="1.1"
+ width="218.33398"
+ height="247.32095"
+ viewbox="377 46 75 264"
+ id="svg2"
+ inkscape:version="0.48.4 r9939"
+ sodipodi:docname="autogen_t1.svg">
+ <metadata
+ id="metadata108">
+ <rdf:RDF>
+ <cc:Work
+ rdf:about="">
+ <dc:format>image/svg+xml</dc:format>
+ <dc:type
+ rdf:resource="http://purl.org/dc/dcmitype/StillImage" />
+ </cc:Work>
+ </rdf:RDF>
+ </metadata>
+ <defs
+ id="defs106" />
+ <sodipodi:namedview
+ pagecolor="#ffffff"
+ bordercolor="#666666"
+ borderopacity="1"
+ objecttolerance="10"
+ gridtolerance="10"
+ guidetolerance="10"
+ inkscape:pageopacity="0"
+ inkscape:pageshadow="2"
+ inkscape:window-width="2048"
+ inkscape:window-height="1086"
+ id="namedview104"
+ showgrid="false"
+ fit-margin-top="0"
+ fit-margin-left="0"
+ fit-margin-right="0"
+ fit-margin-bottom="0"
+ inkscape:zoom="1.340708"
+ inkscape:cx="-82.153241"
+ inkscape:cy="-9.3739663"
+ inkscape:window-x="0"
+ inkscape:window-y="27"
+ inkscape:window-maximized="1"
+ inkscape:current-layer="svg2" />
+ <line
+ x1="62.5"
+ y1="187.82095"
+ x2="62.5"
+ y2="221.82095"
+ id="line4"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <polygon
+ points="414,280 409,271 418,271 "
+ id="polygon6"
+ style="fill:#000000"
+ transform="translate(-351.5,-58.17904)" />
+ <polygon
+ points="414,280 409,271 418,271 "
+ id="polygon8"
+ style="fill:none;stroke:#000000;stroke-width:1"
+ transform="translate(-351.5,-58.17904)" />
+ <line
+ x1="62.5"
+ y1="12.82096"
+ x2="62.5"
+ y2="50.820961"
+ id="line10"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <polygon
+ points="414,109 409,100 418,100 "
+ id="polygon12"
+ style="fill:#000000"
+ transform="translate(-351.5,-58.17904)" />
+ <polygon
+ points="414,109 409,100 418,100 "
+ id="polygon14"
+ style="fill:none;stroke:#000000;stroke-width:1"
+ transform="translate(-351.5,-58.17904)" />
+ <ellipse
+ cx="414"
+ cy="58"
+ rx="7"
+ ry="7"
+ id="ellipse16"
+ sodipodi:cx="414"
+ sodipodi:cy="58"
+ sodipodi:rx="7"
+ sodipodi:ry="7"
+ transform="translate(-350.94059,-51)"
+ style="fill:#000000" />
+ <line
+ x1="62.5"
+ y1="7.82096"
+ x2="62.5"
+ y2="12.82096"
+ id="line18"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <polygon
+ points="437,221 447,231 437,241 382,241 382,221 "
+ id="polygon20"
+ style="fill:#68e5ff"
+ transform="translate(-351.5,-58.17904)" />
+ <line
+ x1="62.5"
+ y1="162.82095"
+ x2="62.5"
+ y2="157.82095"
+ id="line22"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="62.5"
+ y1="182.82095"
+ x2="62.5"
+ y2="187.82095"
+ id="line24"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="31.5"
+ y1="163.82095"
+ x2="86.5"
+ y2="163.82095"
+ id="line26"
+ style="fill:none;stroke:#68e5ff;stroke-width:1" />
+ <line
+ x1="31.5"
+ y1="183.82095"
+ x2="86.5"
+ y2="183.82095"
+ id="line28"
+ style="fill:none;stroke:#68e5ff;stroke-width:1" />
+ <line
+ x1="31.5"
+ y1="163.82095"
+ x2="31.5"
+ y2="183.82095"
+ id="line30"
+ style="fill:none;stroke:#68e5ff;stroke-width:1" />
+ <line
+ x1="86.5"
+ y1="163.82095"
+ x2="96.5"
+ y2="173.82095"
+ id="line32"
+ style="fill:none;stroke:#68e5ff;stroke-width:1" />
+ <line
+ x1="86.104431"
+ y1="183.6891"
+ x2="96.104431"
+ y2="173.6891"
+ id="line34"
+ style="fill:none;stroke:#68e5ff;stroke-width:1" />
+ <line
+ x1="30.5"
+ y1="162.82095"
+ x2="85.5"
+ y2="162.82095"
+ id="line36"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="30.5"
+ y1="182.82095"
+ x2="85.5"
+ y2="182.82095"
+ id="line38"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="30.5"
+ y1="162.82095"
+ x2="30.5"
+ y2="182.82095"
+ id="line40"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="85.5"
+ y1="162.82095"
+ x2="95.5"
+ y2="172.82095"
+ id="line42"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="85.5"
+ y1="182.82095"
+ x2="95.5"
+ y2="172.82095"
+ id="line44"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <text
+ x="31.544403"
+ y="161.63428"
+ style="font-size:12px;font-family:SansSerif"
+ id="text46">chl</text>
+ <text
+ x="35.5"
+ y="177.82095"
+ style="font-size:12px;font-family:SansSerif"
+ id="text48">comm(1)</text>
+ <text
+ x="78.5"
+ y="197.82095"
+ style="font-size:12px;font-family:SansSerif"
+ id="text50">sec:autoEncrypt_comm</text>
+ <line
+ x1="0.5"
+ y1="159.82095"
+ x2="15.5"
+ y2="159.82095"
+ id="line52"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <polygon
+ points="367,218 358,222 358,213 "
+ id="polygon54"
+ style="fill:#000000"
+ transform="translate(-351.5,-58.17904)" />
+ <polygon
+ points="367,218 358,222 358,213 "
+ id="polygon56"
+ style="fill:none;stroke:#000000;stroke-width:1"
+ transform="translate(-351.5,-58.17904)" />
+ <ellipse
+ cx="374"
+ cy="215"
+ rx="3"
+ ry="4"
+ id="ellipse58"
+ sodipodi:cx="374"
+ sodipodi:cy="215"
+ sodipodi:rx="3"
+ sodipodi:ry="4"
+ style="fill:none;stroke:#000000;stroke-width:1"
+ transform="translate(-351.5,-58.17904)" />
+ <rect
+ x="18.966187"
+ y="156.28712"
+ width="8"
+ height="6"
+ id="rect60"
+ style="fill:#00ff00" />
+ <rect
+ x="18.5"
+ y="155.82095"
+ width="9"
+ height="7"
+ id="rect62"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <ellipse
+ cx="414"
+ cy="295"
+ rx="8"
+ ry="8"
+ id="ellipse64"
+ sodipodi:cx="414"
+ sodipodi:cy="295"
+ sodipodi:rx="8"
+ sodipodi:ry="8"
+ style="fill:#000000"
+ transform="translate(-351.5,-58.17904)" />
+ <ellipse
+ cx="414"
+ cy="295"
+ rx="10"
+ ry="10"
+ id="ellipse66"
+ sodipodi:cx="414"
+ sodipodi:cy="295"
+ sodipodi:rx="10"
+ sodipodi:ry="10"
+ style="fill:none;stroke:#000000;stroke-width:1"
+ transform="translate(-351.5,-58.17904)" />
+ <line
+ x1="62.5"
+ y1="226.82095"
+ x2="62.5"
+ y2="221.82095"
+ id="line68"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <rect
+ x="55.5"
+ y="55.820961"
+ width="14.419555"
+ height="35.165428"
+ id="rect70"
+ style="fill:#c7f369" />
+ <polygon
+ points="422,149 414,154 407,149 "
+ id="polygon72"
+ transform="matrix(1.0155391,0,0,1.0932343,-358.05748,-72.53713)"
+ style="fill:#c7f369" />
+ <line
+ x1="55.5"
+ y1="55.820961"
+ x2="70.5"
+ y2="55.820961"
+ id="line74"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="55.5"
+ y1="55.820961"
+ x2="55.5"
+ y2="90.820961"
+ id="line76"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="70.5"
+ y1="55.820961"
+ x2="70.5"
+ y2="90.820961"
+ id="line78"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="55.5"
+ y1="90.820961"
+ x2="62.5"
+ y2="95.820961"
+ id="line80"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="62.5"
+ y1="95.820961"
+ x2="70.5"
+ y2="90.820961"
+ id="line82"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="62.5"
+ y1="55.820961"
+ x2="62.5"
+ y2="50.820961"
+ id="line84"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="62.5"
+ y1="95.820961"
+ x2="62.5"
+ y2="100.82096"
+ id="line86"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="58.5"
+ y1="66.820961"
+ x2="58.5"
+ y2="78.820961"
+ id="line88"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="67.5"
+ y1="66.820961"
+ x2="67.5"
+ y2="78.820961"
+ id="line90"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="58.5"
+ y1="66.820961"
+ x2="62.5"
+ y2="78.820961"
+ id="line92"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="67.5"
+ y1="66.820961"
+ x2="62.5"
+ y2="78.820961"
+ id="line94"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <text
+ x="77.5"
+ y="72.820961"
+ style="font-size:12px;font-family:SansSerif"
+ id="text96">sec:autoEncrypt_comm</text>
+ <line
+ x1="62.5"
+ y1="100.82096"
+ x2="62.5"
+ y2="157.82095"
+ id="line98"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <polygon
+ points="414,216 409,207 418,207 "
+ id="polygon100"
+ style="fill:#000000"
+ transform="translate(-351.5,-58.17904)" />
+ <polygon
+ points="414,216 409,207 418,207 "
+ id="polygon102"
+ style="fill:none;stroke:#000000;stroke-width:1"
+ transform="translate(-351.5,-58.17904)" />
+</svg>
diff --git a/doc/SysMLSec/fig/autogen_t2.svg b/doc/SysMLSec/fig/autogen_t2.svg
new file mode 100644
index 0000000000000000000000000000000000000000..d8145c4771519677472078fafeb7bbc43413f893
--- /dev/null
+++ b/doc/SysMLSec/fig/autogen_t2.svg
@@ -0,0 +1,381 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<svg
+ xmlns:dc="http://purl.org/dc/elements/1.1/"
+ xmlns:cc="http://creativecommons.org/ns#"
+ xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
+ xmlns:svg="http://www.w3.org/2000/svg"
+ xmlns="http://www.w3.org/2000/svg"
+ xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
+ xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
+ version="1.1"
+ width="221.33398"
+ height="221.38107"
+ viewbox="377 49 79 237"
+ id="svg2"
+ inkscape:version="0.48.4 r9939"
+ sodipodi:docname="autogen_t2.svg">
+ <metadata
+ id="metadata102">
+ <rdf:RDF>
+ <cc:Work
+ rdf:about="">
+ <dc:format>image/svg+xml</dc:format>
+ <dc:type
+ rdf:resource="http://purl.org/dc/dcmitype/StillImage" />
+ </cc:Work>
+ </rdf:RDF>
+ </metadata>
+ <defs
+ id="defs100" />
+ <sodipodi:namedview
+ pagecolor="#ffffff"
+ bordercolor="#666666"
+ borderopacity="1"
+ objecttolerance="10"
+ gridtolerance="10"
+ guidetolerance="10"
+ inkscape:pageopacity="0"
+ inkscape:pageshadow="2"
+ inkscape:window-width="2048"
+ inkscape:window-height="1086"
+ id="namedview98"
+ showgrid="false"
+ fit-margin-top="0"
+ fit-margin-left="0"
+ fit-margin-right="0"
+ fit-margin-bottom="0"
+ inkscape:zoom="1.8794154"
+ inkscape:cx="-2.0295745"
+ inkscape:cy="90.913221"
+ inkscape:window-x="0"
+ inkscape:window-y="27"
+ inkscape:window-maximized="1"
+ inkscape:current-layer="svg2" />
+ <line
+ x1="64.5"
+ y1="82.881073"
+ x2="64.5"
+ y2="108.88107"
+ id="line4"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <polygon
+ points="416,169 411,160 420,160 "
+ id="polygon6"
+ style="fill:#000000"
+ transform="translate(-351.5,-60.118924)" />
+ <polygon
+ points="416,169 411,160 420,160 "
+ id="polygon8"
+ style="fill:none;stroke:#000000;stroke-width:1"
+ transform="translate(-351.5,-60.118924)" />
+ <line
+ x1="64.5"
+ y1="13.881076"
+ x2="64.5"
+ y2="52.881077"
+ id="line10"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <polygon
+ points="416,113 411,104 420,104 "
+ id="polygon12"
+ style="fill:#000000"
+ transform="translate(-351.5,-60.118924)" />
+ <polygon
+ points="416,113 411,104 420,104 "
+ id="polygon14"
+ style="fill:none;stroke:#000000;stroke-width:1"
+ transform="translate(-351.5,-60.118924)" />
+ <ellipse
+ cx="416"
+ cy="61"
+ rx="7"
+ ry="7"
+ id="ellipse16"
+ sodipodi:cx="416"
+ sodipodi:cy="61"
+ sodipodi:rx="7"
+ sodipodi:ry="7"
+ transform="translate(-351.5,-54)"
+ style="fill:#000000" />
+ <line
+ x1="64.5"
+ y1="8.8810759"
+ x2="64.5"
+ y2="13.881076"
+ id="line18"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <polygon
+ points="382,138 392,128 382,118 451,118 451,138 "
+ id="polygon20"
+ style="fill:#68e5ff"
+ transform="translate(-351.5,-60.118924)" />
+ <line
+ x1="64.5"
+ y1="57.881077"
+ x2="64.5"
+ y2="52.881077"
+ id="line22"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="64.5"
+ y1="77.881073"
+ x2="64.5"
+ y2="82.881073"
+ id="line24"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="31.5"
+ y1="58.881077"
+ x2="100.5"
+ y2="58.881077"
+ id="line26"
+ style="fill:none;stroke:#68e5ff;stroke-width:1" />
+ <line
+ x1="100.5"
+ y1="58.881077"
+ x2="100.5"
+ y2="78.881073"
+ id="line28"
+ style="fill:none;stroke:#68e5ff;stroke-width:1" />
+ <line
+ x1="31.5"
+ y1="78.881073"
+ x2="100.5"
+ y2="78.881073"
+ id="line30"
+ style="fill:none;stroke:#68e5ff;stroke-width:1" />
+ <line
+ x1="31.5"
+ y1="58.881077"
+ x2="41.5"
+ y2="68.881073"
+ id="line32"
+ style="fill:none;stroke:#68e5ff;stroke-width:1" />
+ <line
+ x1="31.5"
+ y1="78.881073"
+ x2="41.5"
+ y2="68.881073"
+ id="line34"
+ style="fill:none;stroke:#68e5ff;stroke-width:1" />
+ <line
+ x1="30.5"
+ y1="57.881077"
+ x2="99.5"
+ y2="57.881077"
+ id="line36"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="99.5"
+ y1="57.881077"
+ x2="99.5"
+ y2="77.881073"
+ id="line38"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="30.5"
+ y1="77.881073"
+ x2="99.5"
+ y2="77.881073"
+ id="line40"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="30.5"
+ y1="57.881077"
+ x2="40.5"
+ y2="67.881073"
+ id="line42"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="30.5"
+ y1="77.881073"
+ x2="40.5"
+ y2="67.881073"
+ id="line44"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <text
+ x="30.044556"
+ y="56.093945"
+ style="font-size:12px;font-family:SansSerif"
+ id="text46">chl</text>
+ <text
+ x="42.5"
+ y="72.881073"
+ style="font-size:12px;font-family:SansSerif"
+ id="text48">comm(1)</text>
+ <text
+ x="81.5"
+ y="92.881073"
+ style="font-size:12px;font-family:SansSerif"
+ id="text50">sec:autoEncrypt_comm</text>
+ <line
+ x1="0.5"
+ y1="54.881077"
+ x2="15.5"
+ y2="54.881077"
+ id="line52"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <polygon
+ points="367,115 358,119 358,110 "
+ id="polygon54"
+ style="fill:#000000"
+ transform="translate(-351.5,-60.118924)" />
+ <polygon
+ points="367,115 358,119 358,110 "
+ id="polygon56"
+ style="fill:none;stroke:#000000;stroke-width:1"
+ transform="translate(-351.5,-60.118924)" />
+ <ellipse
+ cx="374"
+ cy="112"
+ rx="3"
+ ry="4"
+ id="ellipse58"
+ sodipodi:cx="374"
+ sodipodi:cy="112"
+ sodipodi:rx="3"
+ sodipodi:ry="4"
+ style="fill:none;stroke:#000000;stroke-width:1"
+ transform="translate(-351.5,-60.118924)" />
+ <rect
+ x="18.5"
+ y="50.881077"
+ width="9.1287127"
+ height="6.9405942"
+ id="rect60"
+ style="fill:#00ff00" />
+ <rect
+ x="18.5"
+ y="50.881077"
+ width="9"
+ height="7"
+ id="rect62"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <ellipse
+ cx="416"
+ cy="271"
+ rx="8"
+ ry="8"
+ id="ellipse64"
+ sodipodi:cx="416"
+ sodipodi:cy="271"
+ sodipodi:rx="8"
+ sodipodi:ry="8"
+ style="fill:#000000"
+ transform="translate(-351.5,-60.118924)" />
+ <ellipse
+ cx="416"
+ cy="271"
+ rx="10"
+ ry="10"
+ id="ellipse66"
+ sodipodi:cx="416"
+ sodipodi:cy="271"
+ sodipodi:rx="10"
+ sodipodi:ry="10"
+ style="fill:none;stroke:#000000;stroke-width:1"
+ transform="translate(-351.5,-60.118924)" />
+ <line
+ x1="64.5"
+ y1="200.88107"
+ x2="64.5"
+ y2="195.88107"
+ id="line68"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <rect
+ x="57.5"
+ y="113.88107"
+ width="14.997651"
+ height="35.596241"
+ id="rect70"
+ style="fill:#c7f369" />
+ <polygon
+ points="409,209 424,209 416,214 "
+ id="polygon72"
+ style="fill:#c7f369"
+ transform="translate(-351.5,-60.118924)" />
+ <line
+ x1="57.5"
+ y1="113.88107"
+ x2="72.5"
+ y2="113.88107"
+ id="line74"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="57.5"
+ y1="113.88107"
+ x2="57.5"
+ y2="148.88107"
+ id="line76"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="72.5"
+ y1="113.88107"
+ x2="72.5"
+ y2="148.88107"
+ id="line78"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="57.5"
+ y1="148.88107"
+ x2="64.5"
+ y2="153.88107"
+ id="line80"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="64.5"
+ y1="153.88107"
+ x2="72.5"
+ y2="148.88107"
+ id="line82"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="64.5"
+ y1="113.88107"
+ x2="64.5"
+ y2="108.88107"
+ id="line84"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="64.5"
+ y1="153.88107"
+ x2="64.5"
+ y2="158.88107"
+ id="line86"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="62.5"
+ y1="120.88107"
+ x2="62.5"
+ y2="140.88107"
+ id="line88"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <text
+ x="79.5"
+ y="130.88107"
+ style="font-size:12px;font-family:SansSerif"
+ id="text90">sec:autoEncrypt_comm</text>
+ <line
+ x1="64.5"
+ y1="158.88107"
+ x2="64.5"
+ y2="195.88107"
+ id="line92"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <polygon
+ points="416,256 411,247 420,247 "
+ id="polygon94"
+ style="fill:#000000"
+ transform="translate(-351.5,-60.118924)" />
+ <polygon
+ points="416,256 411,247 420,247 "
+ id="polygon96"
+ style="fill:none;stroke:#000000;stroke-width:1"
+ transform="translate(-351.5,-60.118924)" />
+ <path
+ style="fill:none;stroke:#000000;stroke-width:1px;stroke-linecap:butt;stroke-linejoin:miter;stroke-opacity:1"
+ d="m 61.34714,120.47046 c 9.46153,-1.13712 9.72864,19.92324 0.75368,19.73573"
+ id="path3019"
+ inkscape:connector-curvature="0"
+ sodipodi:nodetypes="cc" />
+</svg>
diff --git a/doc/SysMLSec/fig/automaticgeneration.png b/doc/SysMLSec/fig/automaticgeneration.png
new file mode 100644
index 0000000000000000000000000000000000000000..23229151f1a89940273842662b3de229d74834e8
Binary files /dev/null and b/doc/SysMLSec/fig/automaticgeneration.png differ
diff --git a/doc/SysMLSec/fig/mappedkeys.svg b/doc/SysMLSec/fig/mappedkeys.svg
new file mode 100644
index 0000000000000000000000000000000000000000..fb45b4d60804b3fc17f539a48eb14641c3c12b81
--- /dev/null
+++ b/doc/SysMLSec/fig/mappedkeys.svg
@@ -0,0 +1,988 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<svg
+ xmlns:dc="http://purl.org/dc/elements/1.1/"
+ xmlns:cc="http://creativecommons.org/ns#"
+ xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
+ xmlns:svg="http://www.w3.org/2000/svg"
+ xmlns="http://www.w3.org/2000/svg"
+ xmlns:sodipodi="http://sodipodi.sourceforge.net/DTD/sodipodi-0.dtd"
+ xmlns:inkscape="http://www.inkscape.org/namespaces/inkscape"
+ version="1.1"
+ width="1143.5387"
+ height="566.56683"
+ viewbox="50 49 1240 588"
+ id="svg2"
+ inkscape:version="0.48.4 r9939"
+ sodipodi:docname="mappedkeys.svg">
+ <metadata
+ id="metadata286">
+ <rdf:RDF>
+ <cc:Work
+ rdf:about="">
+ <dc:format>image/svg+xml</dc:format>
+ <dc:type
+ rdf:resource="http://purl.org/dc/dcmitype/StillImage" />
+ </cc:Work>
+ </rdf:RDF>
+ </metadata>
+ <defs
+ id="defs284" />
+ <sodipodi:namedview
+ pagecolor="#ffffff"
+ bordercolor="#666666"
+ borderopacity="1"
+ objecttolerance="10"
+ gridtolerance="10"
+ guidetolerance="10"
+ inkscape:pageopacity="0"
+ inkscape:pageshadow="2"
+ inkscape:window-width="2048"
+ inkscape:window-height="1086"
+ id="namedview282"
+ showgrid="true"
+ inkscape:snap-global="false"
+ fit-margin-top="0"
+ fit-margin-left="0"
+ fit-margin-right="0"
+ fit-margin-bottom="0"
+ inkscape:zoom="0.66435149"
+ inkscape:cx="930.32123"
+ inkscape:cy="605.36302"
+ inkscape:window-x="0"
+ inkscape:window-y="27"
+ inkscape:window-maximized="1"
+ inkscape:current-layer="svg2">
+ <inkscape:grid
+ type="xygrid"
+ id="grid3263"
+ empspacing="5"
+ visible="true"
+ enabled="true"
+ snapvisiblegridlinesonly="true"
+ originx="-140.57457px"
+ originy="-4.5px" />
+ </sodipodi:namedview>
+ <line
+ x1="342.42542"
+ y1="261.06683"
+ x2="428.42542"
+ y2="315.06683"
+ id="line6"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="737.68323"
+ y1="268.43268"
+ x2="680.68323"
+ y2="312.43268"
+ id="line8"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <rect
+ x="798.24036"
+ y="9.208374"
+ width="249.46349"
+ height="49.862621"
+ id="rect234"
+ style="fill:#d7bc80" />
+ <rect
+ x="940.77478"
+ y="77.141846"
+ width="200.19522"
+ height="200.12872"
+ id="rect256"
+ style="fill:#acead3" />
+ <rect
+ x="669.90778"
+ y="74.88913"
+ width="249.97757"
+ height="199.91577"
+ id="rect60"
+ style="fill:#c6ebf9" />
+ <rect
+ x="212.83632"
+ y="76.701736"
+ width="249.66306"
+ height="199.99567"
+ id="rect22"
+ style="fill:#c6ebf9" />
+ <rect
+ x="0.18292236"
+ y="77.558243"
+ width="200.51448"
+ height="200.43654"
+ id="rect196"
+ style="fill:#acead3" />
+ <rect
+ x="77.583603"
+ y="3.7473907"
+ width="250.06969"
+ height="49.317074"
+ id="rect174"
+ style="fill:#d7bc80" />
+ <line
+ x1="553.42542"
+ y1="427.06683"
+ x2="553.42542"
+ y2="387.06683"
+ id="line4"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <rect
+ x="212.90068"
+ y="76.5"
+ width="250"
+ height="200"
+ id="rect10"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="212.90068"
+ y1="76.5"
+ x2="214.90068"
+ y2="73.5"
+ id="line12"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="462.90063"
+ y1="76.5"
+ x2="464.90063"
+ y2="73.5"
+ id="line14"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="214.90068"
+ y1="73.5"
+ x2="464.90063"
+ y2="73.5"
+ id="line16"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="462.90063"
+ y1="276.5"
+ x2="464.90063"
+ y2="273.5"
+ id="line18"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="464.90063"
+ y1="73.5"
+ x2="464.90063"
+ y2="273.5"
+ id="line20"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <text
+ x="296.9007"
+ y="91.5"
+ style="font-size:12px;font-family:SansSerif"
+ id="text24"><<CPURR>></text>
+ <text
+ x="320.9007"
+ y="106.5"
+ style="font-size:12px;font-family:SansSerif"
+ id="text26">CPU1</text>
+ <rect
+ x="264.9007"
+ y="145.5"
+ width="171"
+ height="40"
+ id="rect28"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <rect
+ x="265.9007"
+ y="146.5"
+ width="169"
+ height="38"
+ id="rect30"
+ style="fill:#c6e3f9" />
+ <line
+ x1="410.90063"
+ y1="150.5"
+ x2="410.90063"
+ y2="175.5"
+ id="line32"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="410.90063"
+ y1="150.5"
+ x2="425.90063"
+ y2="150.5"
+ id="line34"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="425.90063"
+ y1="150.5"
+ x2="430.90063"
+ y2="155.5"
+ id="line36"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="430.90063"
+ y1="155.5"
+ x2="430.90063"
+ y2="175.5"
+ id="line38"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="430.90063"
+ y1="175.5"
+ x2="410.90063"
+ y2="175.5"
+ id="line40"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="425.90063"
+ y1="150.5"
+ x2="425.90063"
+ y2="155.5"
+ id="line42"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="425.90063"
+ y1="155.5"
+ x2="430.90063"
+ y2="155.5"
+ id="line44"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <text
+ x="269.9007"
+ y="160.5"
+ style="font-size:12px;font-family:SansSerif"
+ id="text46">NonSecureFV_enc::T1</text>
+ <rect
+ x="670.03864"
+ y="75.206207"
+ width="250"
+ height="200"
+ id="rect48"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="670.03864"
+ y1="75.206207"
+ x2="672.03864"
+ y2="72.206207"
+ id="line50"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="920.0387"
+ y1="75.206207"
+ x2="922.0387"
+ y2="72.206207"
+ id="line52"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="672.03864"
+ y1="72.206207"
+ x2="922.0387"
+ y2="72.206207"
+ id="line54"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="920.0387"
+ y1="275.20621"
+ x2="922.0387"
+ y2="272.20621"
+ id="line56"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="922.0387"
+ y1="72.206207"
+ x2="922.0387"
+ y2="272.20621"
+ id="line58"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <text
+ x="754.03864"
+ y="90.206207"
+ style="font-size:12px;font-family:SansSerif"
+ id="text62"><<CPURR>></text>
+ <text
+ x="778.03864"
+ y="105.20621"
+ style="font-size:12px;font-family:SansSerif"
+ id="text64">CPU2</text>
+ <rect
+ x="712.03864"
+ y="157.20621"
+ width="171"
+ height="40"
+ id="rect66"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <rect
+ x="713.03864"
+ y="158.20621"
+ width="169"
+ height="38"
+ id="rect68"
+ style="fill:#c6e3f9" />
+ <line
+ x1="858.03864"
+ y1="162.20621"
+ x2="858.03864"
+ y2="187.20621"
+ id="line70"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="858.03864"
+ y1="162.20621"
+ x2="873.03864"
+ y2="162.20621"
+ id="line72"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="873.03864"
+ y1="162.20621"
+ x2="878.03864"
+ y2="167.20621"
+ id="line74"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="878.03864"
+ y1="167.20621"
+ x2="878.03864"
+ y2="187.20621"
+ id="line76"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="878.03864"
+ y1="187.20621"
+ x2="858.03864"
+ y2="187.20621"
+ id="line78"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="873.03864"
+ y1="162.20621"
+ x2="873.03864"
+ y2="167.20621"
+ id="line80"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="873.03864"
+ y1="167.20621"
+ x2="878.03864"
+ y2="167.20621"
+ id="line82"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <text
+ x="717.03864"
+ y="172.20621"
+ style="font-size:12px;font-family:SansSerif"
+ id="text84">NonSecureFV_enc::T2</text>
+ <rect
+ x="428.42542"
+ y="291.06683"
+ width="250"
+ height="96"
+ id="rect86"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="428.42542"
+ y1="291.06683"
+ x2="430.42542"
+ y2="288.06683"
+ id="line88"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="678.42542"
+ y1="291.06683"
+ x2="680.42542"
+ y2="288.06683"
+ id="line90"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="430.42542"
+ y1="288.06683"
+ x2="680.42542"
+ y2="288.06683"
+ id="line92"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="678.42542"
+ y1="387.06683"
+ x2="680.42542"
+ y2="384.06683"
+ id="line94"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="680.42542"
+ y1="288.06683"
+ x2="680.42542"
+ y2="384.06683"
+ id="line96"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <rect
+ x="429.42542"
+ y="292.06683"
+ width="248"
+ height="94"
+ id="rect98"
+ style="fill:#d7bc80" />
+ <text
+ x="510.42542"
+ y="306.06683"
+ style="font-size:12px;font-family:SansSerif"
+ id="text100"><<BUS-RR>></text>
+ <text
+ x="527.42542"
+ y="321.06683"
+ style="font-size:12px;font-family:SansSerif"
+ id="text102">MainBus</text>
+ <rect
+ x="468.42542"
+ y="332.06683"
+ width="193"
+ height="40"
+ id="rect104"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="636.42542"
+ y1="337.06683"
+ x2="636.42542"
+ y2="362.06683"
+ id="line106"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="636.42542"
+ y1="337.06683"
+ x2="651.42542"
+ y2="337.06683"
+ id="line108"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="651.42542"
+ y1="337.06683"
+ x2="656.42542"
+ y2="342.06683"
+ id="line110"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="656.42542"
+ y1="342.06683"
+ x2="656.42542"
+ y2="362.06683"
+ id="line112"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="656.42542"
+ y1="362.06683"
+ x2="636.42542"
+ y2="362.06683"
+ id="line114"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="651.42542"
+ y1="337.06683"
+ x2="651.42542"
+ y2="342.06683"
+ id="line116"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="651.42542"
+ y1="342.06683"
+ x2="656.42542"
+ y2="342.06683"
+ id="line118"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <text
+ x="473.42542"
+ y="347.06683"
+ style="font-size:12px;font-family:SansSerif"
+ id="text120">NonSecureFV_enc::comm</text>
+ <text
+ x="473.42542"
+ y="367.06683"
+ style="font-size:12px;font-family:SansSerif"
+ id="text122">channel</text>
+ <rect
+ x="451.42542"
+ y="427.06683"
+ width="205"
+ height="139"
+ id="rect124"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="451.42542"
+ y1="427.06683"
+ x2="453.42542"
+ y2="424.06683"
+ id="line126"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="656.42542"
+ y1="427.06683"
+ x2="658.42542"
+ y2="424.06683"
+ id="line128"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="453.42542"
+ y1="424.06683"
+ x2="658.42542"
+ y2="424.06683"
+ id="line130"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="656.42542"
+ y1="566.06683"
+ x2="658.42542"
+ y2="563.06683"
+ id="line132"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="658.42542"
+ y1="424.06683"
+ x2="658.42542"
+ y2="563.06683"
+ id="line134"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <rect
+ x="452.42542"
+ y="428.06683"
+ width="203"
+ height="137"
+ id="rect136"
+ style="fill:#acead3" />
+ <text
+ x="507.42542"
+ y="442.06683"
+ style="font-size:12px;font-family:SansSerif"
+ id="text138"><<MEMORY>></text>
+ <text
+ x="508.42542"
+ y="457.06683"
+ style="font-size:12px;font-family:SansSerif"
+ id="text140">MainMemory</text>
+ <rect
+ x="463.42542"
+ y="479.06683"
+ width="193"
+ height="40"
+ id="rect142"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="631.42542"
+ y1="484.06683"
+ x2="631.42542"
+ y2="509.06683"
+ id="line144"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="631.42542"
+ y1="484.06683"
+ x2="646.42542"
+ y2="484.06683"
+ id="line146"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="646.42542"
+ y1="484.06683"
+ x2="651.42542"
+ y2="489.06683"
+ id="line148"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="651.42542"
+ y1="489.06683"
+ x2="651.42542"
+ y2="509.06683"
+ id="line150"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="651.42542"
+ y1="509.06683"
+ x2="631.42542"
+ y2="509.06683"
+ id="line152"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="646.42542"
+ y1="484.06683"
+ x2="646.42542"
+ y2="489.06683"
+ id="line154"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="646.42542"
+ y1="489.06683"
+ x2="651.42542"
+ y2="489.06683"
+ id="line156"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <text
+ x="468.42542"
+ y="494.06683"
+ style="font-size:12px;font-family:SansSerif"
+ id="text158">NonSecureFV_enc::comm</text>
+ <text
+ x="468.42542"
+ y="514.06683"
+ style="font-size:12px;font-family:SansSerif"
+ id="text160">channel</text>
+ <rect
+ x="77.900681"
+ y="3.5"
+ width="250"
+ height="50"
+ id="rect162"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="77.900681"
+ y1="3.5"
+ x2="79.900681"
+ y2="0.5"
+ id="line164"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="327.9007"
+ y1="3.5"
+ x2="329.9007"
+ y2="0.5"
+ id="line166"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="79.900681"
+ y1="0.5"
+ x2="329.9007"
+ y2="0.5"
+ id="line168"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="327.9007"
+ y1="53.5"
+ x2="329.9007"
+ y2="50.5"
+ id="line170"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="329.9007"
+ y1="0.5"
+ x2="329.9007"
+ y2="50.5"
+ id="line172"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <text
+ x="159.90068"
+ y="18.5"
+ style="font-size:12px;font-family:SansSerif"
+ id="text176"><<BUS-RR>></text>
+ <text
+ x="186.90068"
+ y="33.5"
+ style="font-size:12px;font-family:SansSerif"
+ id="text178">Bus1</text>
+ <polygon
+ points="177,76 180,76 183,72 183,89 174,97 165,89 165,72 168,76 171,76 174,72 "
+ id="polygon180"
+ transform="translate(-83.099322,-50.499999)"
+ style="fill:#00ff00" />
+ <polygon
+ points="177,76 180,76 183,72 183,89 174,97 165,89 165,72 168,76 171,76 174,72 "
+ id="polygon182"
+ transform="translate(-83.099322,-50.499999)"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <rect
+ x="0.5"
+ y="77.489548"
+ width="200"
+ height="200"
+ id="rect184"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="0.5"
+ y1="77.489548"
+ x2="2.5"
+ y2="74.489548"
+ id="line186"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="200.49998"
+ y1="77.489548"
+ x2="202.49998"
+ y2="74.489548"
+ id="line188"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="2.5"
+ y1="74.489548"
+ x2="202.49998"
+ y2="74.489548"
+ id="line190"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="200.49998"
+ y1="277.48953"
+ x2="202.49998"
+ y2="274.48953"
+ id="line192"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="202.49998"
+ y1="74.489548"
+ x2="202.49998"
+ y2="274.48953"
+ id="line194"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <text
+ x="54.5"
+ y="92.489548"
+ style="font-size:12px;font-family:SansSerif"
+ id="text198"><<MEMORY>></text>
+ <text
+ x="68.5"
+ y="107.48955"
+ style="font-size:12px;font-family:SansSerif"
+ id="text200">Memory1</text>
+ <rect
+ x="24.5"
+ y="133.48955"
+ width="144"
+ height="40"
+ id="rect202"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <rect
+ x="25.5"
+ y="134.48955"
+ width="142"
+ height="38"
+ id="rect204"
+ style="fill:#ace2d3" />
+ <ellipse
+ cx="209"
+ cy="198"
+ rx="6"
+ ry="6"
+ id="ellipse206"
+ sodipodi:cx="209"
+ sodipodi:cy="198"
+ sodipodi:rx="6"
+ sodipodi:ry="6"
+ transform="translate(-54.500003,-53.510453)"
+ style="fill:#000000" />
+ <rect
+ x="153.49998"
+ y="138.48955"
+ width="2"
+ height="24"
+ id="rect208"
+ style="fill:#000000" />
+ <rect
+ x="153.49998"
+ y="163.48955"
+ width="7"
+ height="2"
+ id="rect210"
+ style="fill:#000000" />
+ <rect
+ x="153.49998"
+ y="159.48955"
+ width="7"
+ height="2"
+ id="rect212"
+ style="fill:#000000" />
+ <text
+ x="29.5"
+ y="148.48955"
+ style="font-size:12px;font-family:SansSerif"
+ id="text214">autoEncrypt_comm</text>
+ <text
+ x="29.5"
+ y="168.48955"
+ style="font-size:12px;font-family:SansSerif"
+ id="text216">key</text>
+ <line
+ x1="122.08882"
+ y1="74.102783"
+ x2="139.90068"
+ y2="53.5"
+ id="line218"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="272.45471"
+ y1="73.301392"
+ x2="264.9007"
+ y2="53.5"
+ id="line220"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <rect
+ x="798.03864"
+ y="9.2062073"
+ width="250"
+ height="50"
+ id="rect222"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="798.03864"
+ y1="9.2062073"
+ x2="800.03864"
+ y2="6.2062073"
+ id="line224"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="1048.0387"
+ y1="9.2062073"
+ x2="1050.0387"
+ y2="6.2062073"
+ id="line226"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="800.03864"
+ y1="6.2062073"
+ x2="1050.0387"
+ y2="6.2062073"
+ id="line228"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="1048.0387"
+ y1="59.206207"
+ x2="1050.0387"
+ y2="56.206207"
+ id="line230"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="1050.0387"
+ y1="6.2062073"
+ x2="1050.0387"
+ y2="56.206207"
+ id="line232"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <text
+ x="880.03864"
+ y="24.206207"
+ style="font-size:12px;font-family:SansSerif"
+ id="text236"><<BUS-RR>></text>
+ <text
+ x="907.0387"
+ y="39.206207"
+ style="font-size:12px;font-family:SansSerif"
+ id="text238">Bus2</text>
+ <polygon
+ points="958,93 961,93 964,89 964,106 955,114 946,106 946,89 949,93 952,93 955,89 "
+ id="polygon240"
+ transform="translate(-143.96133,-61.793791)"
+ style="fill:#00ff00" />
+ <polygon
+ points="958,93 961,93 964,89 964,106 955,114 946,106 946,89 949,93 952,93 955,89 "
+ id="polygon242"
+ transform="translate(-143.96133,-61.793791)"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <rect
+ x="941.0387"
+ y="77.206207"
+ width="200"
+ height="200"
+ id="rect244"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="941.0387"
+ y1="77.206207"
+ x2="943.0387"
+ y2="74.206207"
+ id="line246"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="1141.0387"
+ y1="77.206207"
+ x2="1143.0387"
+ y2="74.206207"
+ id="line248"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="943.0387"
+ y1="74.206207"
+ x2="1143.0387"
+ y2="74.206207"
+ id="line250"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="1141.0387"
+ y1="277.20621"
+ x2="1143.0387"
+ y2="274.20621"
+ id="line252"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="1143.0387"
+ y1="74.206207"
+ x2="1143.0387"
+ y2="274.20621"
+ id="line254"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <text
+ x="995.0387"
+ y="92.206207"
+ style="font-size:12px;font-family:SansSerif"
+ id="text258"><<MEMORY>></text>
+ <text
+ x="1009.0387"
+ y="107.20621"
+ style="font-size:12px;font-family:SansSerif"
+ id="text260">Memory2</text>
+ <rect
+ x="965.0387"
+ y="151.20621"
+ width="144"
+ height="40"
+ id="rect262"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <rect
+ x="966.0387"
+ y="152.20621"
+ width="142"
+ height="38"
+ id="rect264"
+ style="fill:#ace2d3" />
+ <ellipse
+ cx="1239"
+ cy="224"
+ rx="6"
+ ry="6"
+ id="ellipse266"
+ sodipodi:cx="1239"
+ sodipodi:cy="224"
+ sodipodi:rx="6"
+ sodipodi:ry="6"
+ transform="translate(-143.96133,-61.793791)"
+ style="fill:#000000" />
+ <rect
+ x="1093.9722"
+ y="158.73405"
+ width="2"
+ height="24"
+ id="rect268"
+ style="fill:#000000" />
+ <rect
+ x="1094.0387"
+ y="181.20621"
+ width="7"
+ height="2"
+ id="rect270"
+ style="fill:#000000" />
+ <rect
+ x="1094.0387"
+ y="177.20621"
+ width="7"
+ height="2"
+ id="rect272"
+ style="fill:#000000" />
+ <text
+ x="970.0387"
+ y="166.20621"
+ style="font-size:12px;font-family:SansSerif"
+ id="text274">autoEncrypt_comm</text>
+ <text
+ x="970.0387"
+ y="186.20621"
+ style="font-size:12px;font-family:SansSerif"
+ id="text276">key</text>
+ <line
+ x1="857.03864"
+ y1="71.880096"
+ x2="860.03864"
+ y2="59.206207"
+ id="line278"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+ <line
+ x1="990.77258"
+ y1="74.412277"
+ x2="985.0387"
+ y2="59.206207"
+ id="line280"
+ style="fill:none;stroke:#000000;stroke-width:1" />
+</svg>
diff --git a/doc/SysMLSec/sysmlsec_documentation.tex b/doc/SysMLSec/sysmlsec_documentation.tex
index 15944adab5fa7166d90f37a1a946c2a8008897bb..6b1a16bec0228f9dfb321714a968c982da9e3ea0 100644
--- a/doc/SysMLSec/sysmlsec_documentation.tex
+++ b/doc/SysMLSec/sysmlsec_documentation.tex
@@ -352,6 +352,69 @@ Without taking into account penalties of the hardware platform (e.g. cache miss,
\caption{Excerpt of the simulation of the secure application mapped on the non secure architecture} \label{fig:simu_mapping3}
\end{figure*}
+\subsection{Automatic Security Generation}
+
+Given security requirements and an unsecured model, our toolkit magically adds security elements. It can 1) add the security operators to a functional view, 2) Add an HSM performing all security operations, and 3) Automatically map keys securely. See the thesis of Letitia Li, `Safe and Secure Model-Driven Design for Embedded Systems' for the detailed algorithms on how to add security.
+
+\begin{figure*}[htbp]
+\centering
+\includegraphics[width=0.99\textwidth]{fig/automaticgeneration.png}
+\caption{Window for Automatic Generation of Security} \label{fig:autogen}
+\end{figure*}
+
+First, each security-critical channel should be marked with whether the data across it should be checked for Confidentiality or Authenticity. It is assumed that the security properties to be checked are the ones that should be ensured for each channel.
+
+\subsubsection{Adding Security Operators}
+
+When the option to add security operators is selected, there are multiple options of the type of security operators to be added. The user should select if confidentiality, weak authenticity, and/or strong authenticity should be ensured for the model. For example, if the user only wishes to add operators to ensure confidentiality, then the toolkit will ignore the requirements on authenticity and only add the encryption operators to channels marked with the security annotation indicating that the data on them must be confidential.
+
+ In addition, for the operators being added, estimated times to perform encryption, decryption, calculate a MAC, etc, and the overhead, can be manually set in lieu of using the default options.
+
+\begin{figure*}[htbp]
+\centering
+\includegraphics[width=0.2\textwidth]{build/autogen_t1-svg.pdf}
+\includegraphics[width=0.4\textwidth]{build/autogen_fv-svg.pdf}
+\includegraphics[width=0.2\textwidth]{build/autogen_t2-svg.pdf}
+\caption{Functional view with automatically generated security operators to ensure weak authenticity} \label{fig:secfv1}
+\end{figure*}
+
+ For example, using the insecure architecture and functional model from Figure \ref{fig:fv1} and \ref{fig:mapping1}, if the communication channel is marked that it should be authentic, and if we choose to ensure weak authenticity only, then the toolkit generates the functional model shown in Figure \ref{fig:secfv1}. The Message Authentication Code concatenated onto the message can only be calculated with the given key and message, and if T2 detects that they do not match, then it discards the message as it was not an authentic message sent by T1.
+
+ If instead we chose to add weak and strong authenticity, then the tasks should exchange a nonce to avoid replay attacks, and the functional model in Figure \ref{fig:secfv2} is generated.
+
+\begin{figure*}[htbp]
+\centering
+\includegraphics[width=0.2\textwidth]{build/autogen2_t1-svg.pdf}
+\includegraphics[width=0.4\textwidth]{build/autogen_fv2-svg.pdf}
+\includegraphics[width=0.2\textwidth]{build/autogen2_t2-svg.pdf}
+\caption{Functional view with automatically generated security operators to ensure strong authenticity} \label{fig:secfv2}
+\end{figure*}
+
+\subsubsection{Adding Hardware Security Modules}
+
+ After a designer models a system, our toolkit can automatically add
+HSMs to designated tasks, including making all of the modifications to the
+diagrams relating to sending the data to the HSM, generating the HSM's activity
+diagram, etc. A single Hardware Security Module is added to each processor which executes at least one of the designated tasks. If multiple tasks mapped to a single CPU are designated to have a HSM added to them, then only a single HSM will be added.
+
+For each HSM to be added to perform security operations for one or more tasks, first, the architectural diagram is modified to add a Hardware Accelerator and memory, with a connecting private bus.
+
+Next, each task is modified, so that before each instance of sending a message which should be secure, the task first sends the data to the HSM. The HSM then performs the security operations, and returns the secured message to the task, which then sends the secured message to the receiving task. When a task receives data to be decrypted, it similarly sends the messages to the HSM, which then decrypts it and sends the message back, and which point the receiving task can understand the contents of the message.
+
+\subsubsection{Mapping Keys}
+
+With multiple Cryptographic Configurations, it may become tedious to the map all of the keys to memory. Our toolkit therefore can find every Cryptographic Configuration used by a task, and then, depending on the type of the Cryptographic Configuration, map each applicable key to a memory that the task can securely access. For Cryptographic Configurations of type symmetric encryption or MAC, both the sending and receiving task will need to be able to access the key. For asymmetric encryption, however, all the sending tasks will need the public key while only the receiving task will need to access the private key.
+
+If a key is sent along a bus accessible to an attacker, then the key would be known to the attacker, so we wish to avoid sending keys along public buses. For each task which needs the key, the algorithm searches for securely accessible memories from the processor to which it is mapped. The algorithm traverses all possible private buses and bridges using breadth-first search, until it finds a memory. The key is then mapped to that memory. If all possible secure paths are searched and no memories are found, then a warning is issued saying it is impossible to map keys for that task.
+
+For example, for the automatically secured model in Figure \ref{fig:secfv1}, the keys for autoEncrypt\_comm are mapped as shown in Figure \ref{fig:mapkey}, where there is a secure path to the memory. If they keys were mapped to MainMemory, then the attacker could recover the key when it was read over the public bus MainBus.
+
+\begin{figure*}[htbp]
+\centering
+\includegraphics[width=0.99\textwidth]{build/mappedkeys-svg.pdf}
+\caption{Mapping model with mapped keys} \label{fig:mapkey}
+\end{figure*}
+
\subsection{Designing security protocols}
During the HW/SW partitioning stage, security mechanisms have been modeled at a high level of abstraction, mostly to place them correctly in the system, and to evaluate their impact on the system performance. During the software design stage, security protocols can be designed in a more precise way.
@@ -386,4 +449,6 @@ The security formal verification can be performed from these diagrams. Just like
\end{figure*}
+
+
\end{document}
diff --git a/src/main/java/proverifspec/ProVerifOutputAnalyzer.java b/src/main/java/proverifspec/ProVerifOutputAnalyzer.java
index f1233297aab0137129bf4bdb21896e1b8797053f..5fc74b117ca48ce1025509fc5edb0236c83efceb 100644
--- a/src/main/java/proverifspec/ProVerifOutputAnalyzer.java
+++ b/src/main/java/proverifspec/ProVerifOutputAnalyzer.java
@@ -136,7 +136,7 @@ public class ProVerifOutputAnalyzer {
{
if (str.isEmpty())
continue;
-
+ // System.out.println("OUTPUT " + str);
Matcher m = procPattern.matcher(str);
if (isInTrace && (str.startsWith("A more detailed") || str.startsWith("Could not find")))
diff --git a/src/main/java/tmltranslator/TMLModeling.java b/src/main/java/tmltranslator/TMLModeling.java
index 05ec17d08fc5f6b4746864f94d8c764ee09a9951..f21759b5baecfcc83ea890ca77fe560e8c442449 100755
--- a/src/main/java/tmltranslator/TMLModeling.java
+++ b/src/main/java/tmltranslator/TMLModeling.java
@@ -1085,15 +1085,15 @@ public class TMLModeling<E> {
}
}*/
signalName=signalName.split("__")[1];
- System.out.println("secpattern " + signalName);
+ // System.out.println("secpattern " + signalName);
List<String> channels=secChannelMap.get(signalName);
- System.out.println("secpattern channels " + channels);
+ // System.out.println("secpattern channels " + channels);
if (channels!=null) {
for (String channelName: channels) {
channel = getChannelByShortName(channelName);
if (channel!=null){
for (TMLCPrimitivePort port:channel.ports){
- System.out.println("adding to port " + channelName);
+ // System.out.println("adding to port " + channelName);
if (port.checkAuth){
port.checkStrongAuthStatus = 2;
port.secName= signalName;
diff --git a/src/main/java/tmltranslator/toavatar/TML2Avatar.java b/src/main/java/tmltranslator/toavatar/TML2Avatar.java
index 30980565bc26b1bc7c3b8f2901bdda7fd31c2f6b..36e334fb51add223da79c9815e986bc03a136166 100644
--- a/src/main/java/tmltranslator/toavatar/TML2Avatar.java
+++ b/src/main/java/tmltranslator/toavatar/TML2Avatar.java
@@ -103,8 +103,9 @@ import java.util.regex.Pattern;
for (TMLTask t1:tmlmodel.getTasks()){
List<SecurityPattern> keys = new ArrayList<SecurityPattern>();
accessKeys.put(t1, keys);
+
HwExecutionNode node1 = (HwExecutionNode) tmlmap.getHwNodeOf(t1);
- //Try to find memory using only private buses
+ //Try to find memory using only private buses from origin
List<HwNode> toVisit = new ArrayList<HwNode>();
//List<HwNode> toMemory = new ArrayList<HwNode>();
List<HwNode> complete = new ArrayList<HwNode>();
@@ -132,13 +133,16 @@ import java.util.regex.Pattern;
}
}
else if (curr == link.hwnode){
- if (!complete.contains(link.bus) && !toVisit.contains(link.bus)){
+ if (!complete.contains(link.bus) && !toVisit.contains(link.bus) && link.bus.privacy==1){
toVisit.add(link.bus);
}
}
}
complete.add(curr);
}
+
+ //Find path to secure memory from destination node
+
// System.out.println("Memory found ?"+ memory);
for (TMLTask t2:tmlmodel.getTasks()){
HwExecutionNode node2 = (HwExecutionNode) tmlmap.getHwNodeOf(t2);
@@ -147,6 +151,7 @@ import java.util.regex.Pattern;
originDestMap.put(t1.getName()+"__"+t2.getName(), channelPublic);
}
else if (node1==node2){
+
originDestMap.put(t1.getName()+"__"+t2.getName(), channelPrivate);
}
else {
@@ -165,7 +170,7 @@ import java.util.regex.Pattern;
pathMap.put(link.bus, tmp);
}
}
-outerloop:
+ outerloop:
while (found.size()>0){
HwNode curr = found.remove(0);
for (HwLink link: links){
@@ -213,9 +218,11 @@ outerloop:
}
}
}
+ //System.out.println(originDestMap);
}
- public void checkChannels(){
+
+ /* public void checkChannels(){
List<TMLChannel> channels = tmlmodel.getChannels();
List<TMLTask> destinations = new ArrayList<TMLTask>();
TMLTask a;
@@ -234,6 +241,11 @@ outerloop:
//List<HwBus> buses = new ArrayList<HwBus>();
HwNode node2 = tmlmap.getHwNodeOf(t);
+ //Check if each node has a secure path to memory
+
+
+
+
if (node1==node2){
channelMap.put(channel, channelPrivate);
}
@@ -255,7 +267,7 @@ outerloop:
pathMap.put(link.bus, tmp);
}
}
-outerloop:
+ outerloop:
while (found.size()>0){
HwNode curr = found.remove(0);
for (HwLink link: links){
@@ -307,7 +319,8 @@ outerloop:
}
}
}
- }
+ System.out.println(channelMap);
+ }*/
public List<AvatarStateMachineElement> translateState(TMLActivityElement ae, AvatarBlock block){
@@ -1250,6 +1263,7 @@ outerloop:
if (ae.securityPattern!=null){
//send nonce
if (ae.securityPattern.type.equals("Nonce")){
+ block.addAttribute(new AvatarAttribute(ae.securityPattern.name, AvatarType.INTEGER, block,null));
as.addValue(ae.securityPattern.name);
}
//send encrypted key
@@ -1561,7 +1575,7 @@ outerloop:
}
checkConnections();
- checkChannels();
+ // checkChannels();
distributeKeys();
diff --git a/src/main/java/ui/GTURTLEModeling.java b/src/main/java/ui/GTURTLEModeling.java
index 0e17581850c5a654c38a845c05032270f8ee672f..490eb32ad0a38aeffafb8b8b7d8e732bfdf3ad8f 100644
--- a/src/main/java/ui/GTURTLEModeling.java
+++ b/src/main/java/ui/GTURTLEModeling.java
@@ -1361,7 +1361,7 @@ public class GTURTLEModeling {
} else if (tmap != null) {
t2a = new TML2Avatar(tmap, false, true);
avatarspec = t2a.generateAvatarSpec(loopLimit);
- drawPanel(avatarspec, mgui.getFirstAvatarDesignPanelFound());
+ // drawPanel(avatarspec, mgui.getFirstAvatarDesignPanelFound());
} else if (tmlm != null) {
//Generate default mapping
diff --git a/src/main/java/ui/HSMGeneration.java b/src/main/java/ui/HSMGeneration.java
index e081057a123823befab08f2202a9f9675734a276..2820c30edd6a42278341c611688fc5d4e3f045d1 100644
--- a/src/main/java/ui/HSMGeneration.java
+++ b/src/main/java/ui/HSMGeneration.java
@@ -75,7 +75,7 @@ public class HSMGeneration implements Runnable {
avatar2proverif = new AVATAR2ProVerif(avatarspec);
try {
- proverif = avatar2proverif.generateProVerif(true, true, 3, true, false);
+ proverif = avatar2proverif.generateProVerif(true, true, 3, true, true);
//warnings = avatar2proverif.getWarnings();
if (!avatar2proverif.saveInFile("pvspec")) {
@@ -90,6 +90,10 @@ public class HSMGeneration implements Runnable {
ProVerifOutputAnalyzer pvoa = avatar2proverif.getOutputAnalyzer();
pvoa.analyzeOutput(data, true);
+ if (pvoa.getResults().size() ==0){
+ TraceManager.addDev("ERROR: No security results");
+ }
+
Map<AvatarPragmaSecret, ProVerifQueryResult> confResults = pvoa.getConfidentialityResults();
for (AvatarPragmaSecret pragma : confResults.keySet()) {
if (confResults.get(pragma).isProved() && !confResults.get(pragma).isSatisfied()) {
@@ -131,6 +135,8 @@ public class HSMGeneration implements Runnable {
}
public void run(){
+ Map<String, Integer> channelIndexMap = new HashMap<String, Integer>();
+ int channelIndex=0;
TraceManager.addDev("Adding HSM");
String encComp = "100";
@@ -171,8 +177,8 @@ public class HSMGeneration implements Runnable {
for (String cpuName : selectedCpuTasks.keySet()) {
Map<String, HSMChannel> hsmChannels = new HashMap<String, HSMChannel>();
TMLCPrimitiveComponent hsm = new TMLCPrimitiveComponent(0, 500, tcdp.getMinX(), tcdp.getMaxX(), tcdp.getMinY(), tcdp.getMaxY(), false, null, tcdp);
- //TAttribute isEnc = new TAttribute(2, "isEnc", "true", 4);
- //hsm.getAttributeList().add(isEnc);
+ TAttribute index = new TAttribute(2, "channelIndex", "0", 0);
+ hsm.getAttributeList().add(index);
tcdp.addComponent(hsm, 0, 500, false, true);
hsm.setValueWithChange("HSM_" + cpuName);
//Find all associated components
@@ -240,6 +246,10 @@ public class HSMGeneration implements Runnable {
if (type != -1) {
compChannels.put(writeChannel.getChannelName(), ch);
channelInstances.add(tg);
+ if (!channelIndexMap.containsKey(writeChannel.getChannelName())){
+ channelIndexMap.put(writeChannel.getChannelName(),channelIndex);
+ channelIndex++;
+ }
}
}
} else {
@@ -261,6 +271,10 @@ public class HSMGeneration implements Runnable {
HSMChannel ch = new HSMChannel(writeChannel.getChannelName(), compName, type);
ch.securityContext = writeChannel.getSecurityContext();
compChannels.put(writeChannel.getChannelName(), ch);
+ if (!channelIndexMap.containsKey(writeChannel.getChannelName())){
+ channelIndexMap.put(writeChannel.getChannelName(),channelIndex);
+ channelIndex++;
+ }
//chanNames.add(writeChannel.getChannelName()+compName);
}
}
@@ -275,6 +289,10 @@ public class HSMGeneration implements Runnable {
HSMChannel ch = new HSMChannel(readChannel.getChannelName(), compName, HSMChannel.DEC);
ch.securityContext = "hsmSec_" + readChannel.getChannelName();
compChannels.put(readChannel.getChannelName(), ch);
+ if (!channelIndexMap.containsKey(readChannel.getChannelName())){
+ channelIndexMap.put(readChannel.getChannelName(),channelIndex);
+ channelIndex++;
+ }
if (nonSecChans.contains(compName + "__" + readChannel.getChannelName() + "_chData") && nonAuthChans.contains(compName + "__" + readChannel.getChannelName())) {
ch.nonceName = "nonce_" + readChannel.getChannelName();
}
@@ -287,6 +305,10 @@ public class HSMGeneration implements Runnable {
HSMChannel ch = new HSMChannel(readChannel.getChannelName(), compName, HSMChannel.DEC);
ch.securityContext = readChannel.getSecurityContext();
compChannels.put(readChannel.getChannelName(), ch);
+ if (!channelIndexMap.containsKey(readChannel.getChannelName())){
+ channelIndexMap.put(readChannel.getChannelName(),channelIndex);
+ channelIndex++;
+ }
}
}
}
@@ -301,6 +323,8 @@ public class HSMGeneration implements Runnable {
//}
}
}
+
+ // System.out.println("channelIndex " + channelIndexMap);
//System.out.println("compchannels " +compChannels);
List<ChannelData> hsmChans = new ArrayList<ChannelData>();
ChannelData chd = new ChannelData("startHSM_" + cpuName, false, false);
@@ -322,7 +346,7 @@ public class HSMGeneration implements Runnable {
if (!hsmChan.isChan) {
originPort.typep = 2;
destPort.typep = 2;
- // originPort.setParam(0, new TType(2));
+ originPort.setParam(0, new TType(1));
}
destPort.isOrigin = !hsmChan.isOrigin;
@@ -367,7 +391,11 @@ public class HSMGeneration implements Runnable {
TMLADSendRequest req = new TMLADSendRequest(xpos, ypos + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
req.setRequestName("startHSM_" + cpuName);
- // req.setParam(0, "isEnc");
+
+
+
+ req.setParam(0, Integer.toString(channelIndexMap.get(chanName)));
+ req.makeValue();
tad.addComponent(req, xpos, ypos + yShift, false, true);
fromStart.setP2(req.getTGConnectingPointAtIndex(0));
@@ -458,7 +486,9 @@ public class HSMGeneration implements Runnable {
yShift += 50;
TMLADSendRequest req = new TMLADSendRequest(xpos, ypos + yShift, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
req.setRequestName("startHSM_" + cpuName);
- // req.setParam(0, "isEnc");
+
+ req.setParam(0, Integer.toString(channelIndexMap.get(chanName)));
+
req.makeValue();
tad.addComponent(req, xpos, ypos + yShift, false, true);
@@ -534,9 +564,9 @@ public class HSMGeneration implements Runnable {
fromStart = new TGConnectorTMLAD(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector<Point>());
-/* TMLADReadRequestArg req = new TMLADReadRequestArg(300, 100, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+ TMLADReadRequestArg req = new TMLADReadRequestArg(300, 100, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
tad.addComponent(req, 300, 100, false, true);
- req.setParam(0, "isEnc");
+ req.setParam(0, "channelIndex");
req.makeValue();
//Connect start and readrequest
@@ -544,14 +574,14 @@ public class HSMGeneration implements Runnable {
fromStart.setP2(req.getTGConnectingPointAtIndex(0));
tad.addComponent(fromStart, 300, 200, false, true);
-*/
+
TMLADChoice choice = new TMLADChoice(300, 200, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
tad.addComponent(choice, 300, 200, false, true);
//Connect readrequest and choice
fromStart = new TGConnectorTMLAD(xpos, ypos, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad, null, null, new Vector<Point>());
- fromStart.setP1(start.getTGConnectingPointAtIndex(0));
+ fromStart.setP1(req.getTGConnectingPointAtIndex(1));
fromStart.setP2(choice.getTGConnectingPointAtIndex(0));
tad.addComponent(fromStart, 300, 200, false, true);
@@ -560,8 +590,9 @@ public class HSMGeneration implements Runnable {
//Allows 9 channels max to simplify the diagram
//If more than 3 channels, build 2 levels of choices
- TMLADChoice choice2 = new TMLADChoice(xc, 400, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
+
if (hsmChannels.keySet().size() > 3) {
+ TMLADChoice choice2 = new TMLADChoice(xc, 400, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
int i = 0;
for (String chan : hsmChannels.keySet()) {
HSMChannel ch = hsmChannels.get(chan);
@@ -661,6 +692,10 @@ public class HSMGeneration implements Runnable {
int i = 1;
for (String chan : hsmChannels.keySet()) {
+
+ //Add guard as channelindex
+ choice.setGuard("[channelIndex=="+channelIndexMap.get(chan)+"]",i-1);
+
HSMChannel ch = hsmChannels.get(chan);
TMLADReadChannel rd = new TMLADReadChannel(xc, 300, tad.getMinX(), tad.getMaxX(), tad.getMinY(), tad.getMaxY(), false, null, tad);
rd.setChannelName("data_" + chan + "_" + hsmChannels.get(chan).task);
diff --git a/src/main/java/ui/SecurityGeneration.java b/src/main/java/ui/SecurityGeneration.java
index bceba0449953637596a67a37b1782829b012af5c..89b0e253f43db26d158f30a3d0ac6131c9472fd2 100644
--- a/src/main/java/ui/SecurityGeneration.java
+++ b/src/main/java/ui/SecurityGeneration.java
@@ -85,7 +85,7 @@ public class SecurityGeneration implements Runnable {
avatar2proverif = new AVATAR2ProVerif(avatarspec);
try {
- proverif = avatar2proverif.generateProVerif(true, true, 3, true, false);
+ proverif = avatar2proverif.generateProVerif(true, true, 3, true, true);
//warnings = avatar2proverif.getWarnings();
if (!avatar2proverif.saveInFile("pvspec")) {
@@ -98,9 +98,17 @@ public class SecurityGeneration implements Runnable {
rshc.sendExecuteCommandRequest();
Reader data = rshc.getDataReaderFromProcess();
+
ProVerifOutputAnalyzer pvoa = avatar2proverif.getOutputAnalyzer();
pvoa.analyzeOutput(data, true);
+
+ if (pvoa.getResults().size() ==0){
+ TraceManager.addDev("ERROR: No security results");
+ }
+
+
Map<AvatarPragmaSecret, ProVerifQueryResult> confResults = pvoa.getConfidentialityResults();
+
for (AvatarPragmaSecret pragma : confResults.keySet()) {
if (confResults.get(pragma).isProved() && !confResults.get(pragma).isSatisfied()) {
nonSecChans.add(pragma.getArg().getBlock().getName() + "__" + pragma.getArg().getName());
@@ -111,6 +119,8 @@ public class SecurityGeneration implements Runnable {
}
}
}
+
+
Map<AvatarPragmaAuthenticity, ProVerifQueryAuthResult> authResults = pvoa.getAuthenticityResults();
for (AvatarPragmaAuthenticity pragma : authResults.keySet()) {
if (authResults.get(pragma).isProved() && !authResults.get(pragma).isSatisfied()) {
diff --git a/src/main/java/ui/window/JDialogCryptographicConfiguration.java b/src/main/java/ui/window/JDialogCryptographicConfiguration.java
index 6051a39a5e031267dac5fd2d7168c42cccdcce1c..dc0ed3bf6b7eeeb7d2e538620b0303f7358ca86f 100644
--- a/src/main/java/ui/window/JDialogCryptographicConfiguration.java
+++ b/src/main/java/ui/window/JDialogCryptographicConfiguration.java
@@ -42,6 +42,7 @@
package ui.window;
import ui.util.IconManager;
+import myutil.TraceManager;
import javax.swing.*;
import java.awt.*;
@@ -170,10 +171,12 @@ public class JDialogCryptographicConfiguration extends JDialogBase implements Ac
String command = evt.getActionCommand();
// Compare the action command to the known actions.
- if (command.equals("Save and Close")) {
- closeDialog();
- } else if (command.equals("Cancel")) {
- cancelDialog();
+ if (evt.getSource() == closeButton) {
+ TraceManager.addDev("Closing button");
+ closeDialog();
+ } else if (evt.getSource() == cancelButton) {
+ TraceManager.addDev("Cancel button");
+ cancelDialog();
} else if (inserts[0] != null) {
if (evt.getSource() == inserts[0]) {
texts[1].setText(helps.get(1).getSelectedItem().toString());
diff --git a/src/main/java/ui/window/JDialogProverifVerification.java b/src/main/java/ui/window/JDialogProverifVerification.java
index 4d9cd7e0196717744f759522d6d565336a90ae35..5c7ba105c696e11552be374237f2f29aec536bef 100644
--- a/src/main/java/ui/window/JDialogProverifVerification.java
+++ b/src/main/java/ui/window/JDialogProverifVerification.java
@@ -1034,6 +1034,9 @@ public class JDialogProverifVerification extends JDialog implements ActionListen
LinkedList<AvatarPragma> nonProved = new LinkedList<>();
this.results = this.pvoa.getResults();
+
+ //System.out.println(results);
+
for (AvatarPragma pragma : this.results.keySet()) {
if (pragma instanceof AvatarPragmaReachability) {
ProVerifQueryResult r = this.results.get(pragma);