245 lines
14 KiB
Plaintext
245 lines
14 KiB
Plaintext
digraph {
|
|
graph [ordering = out]
|
|
edge [arrowhead = none, penwidth = 1.6, fontsize = 30]
|
|
node [shape = point, width = 0, height = 0, fontsize = 30]
|
|
Trace [label = <A trace has been found.<br/>
|
|
>, shape = plaintext]
|
|
P0__0 [label = "Honest Process", shape = plaintext]
|
|
P__0 [label = "Attacker", shape = plaintext]
|
|
Trace -> P0__0 [label = "", style = invisible, weight = 100]{rank = same; P0__0 P__0}
|
|
P0__0 -> P0__1 [label = <>, weight = 100]
|
|
P0__1 -> P0__2 [label = <>, weight = 100]
|
|
P0__2 [shape = plaintext, label = <<TABLE BORDER="0" CELLBORDER="1" CELLSPACING="0" CELLPADDING="4"> <TR><TD><FONT COLOR="darkgreen">{1}</FONT><FONT COLOR="blue">new </FONT>ke1_1</TD></TR><TR><TD><FONT COLOR="darkgreen">{2}</FONT><FONT COLOR="blue">new </FONT>km1_1</TD></TR><TR><TD><FONT COLOR="darkgreen">{3}</FONT><FONT COLOR="blue">new </FONT>ke2_1</TD></TR><TR><TD><FONT COLOR="darkgreen">{4}</FONT><FONT COLOR="blue">new </FONT>km2_1</TD></TR><TR><TD><FONT COLOR="darkgreen">{5}</FONT><FONT COLOR="blue">new </FONT>d_1</TD></TR></TABLE>>]
|
|
P0__2 -> P0__3 [label = <>, weight = 100]
|
|
/*RPar */
|
|
P0__3 -> P0_5__3 [label = <>]
|
|
P0__3 -> P0_4__3 [label = <>]
|
|
P0__3 -> P0_3__3 [label = <>]
|
|
P0__3 -> P0_2__3 [label = <>]
|
|
P0__3 -> P0_1__3 [label = <>]
|
|
P0__3 -> P0_0__3 [label = <>]
|
|
P0__3 [label = "", fixedsize = false, width = 0, height = 0, shape = none]
|
|
{rank = same; P0_0__3 P0_1__3 P0_2__3 P0_3__3 P0_4__3 P0_5__3}
|
|
P0_1__3 -> P0_1__4 [label = <>, weight = 100]
|
|
P0_1__4 [shape = plaintext, label = <<TABLE BORDER="0" CELLBORDER="1" CELLSPACING="0" CELLPADDING="4"> <TR><TD>Beginning of process <FONT COLOR="darkgreen">passport</FONT></TD></TR></TABLE>>]
|
|
P0_1__4 -> P0_1__5 [label = <>, weight = 100]
|
|
P0_2__3 -> P0_2__4 [label = <>, weight = 100]
|
|
P0_2__4 [shape = plaintext, label = <<TABLE BORDER="0" CELLBORDER="1" CELLSPACING="0" CELLPADDING="4"> <TR><TD>Beginning of process <FONT COLOR="darkgreen">passport</FONT></TD></TR></TABLE>>]
|
|
P0_2__4 -> P0_2__5 [label = <>, weight = 100]
|
|
P0_5__3 [label = "!", shape = ellipse]
|
|
P0_5_0__3 [label = "", fixedsize = false, width = 0, height = 0, shape = none]
|
|
P0_5__3 -> P0_5_0__3 [label = <>, weight = 100]
|
|
P0_5_0__3 -> P0_5_0__4 [label = <>, weight = 100]
|
|
P0_5_0__4 [shape = plaintext, label = <<TABLE BORDER="0" CELLBORDER="1" CELLSPACING="0" CELLPADDING="4"> <TR><TD>Beginning of process <FONT COLOR="darkgreen">reader</FONT></TD></TR></TABLE>>]
|
|
P0_5_0__4 -> P0_5_0__5 [label = <>, weight = 100]
|
|
P0_5_0__5 -> P0_5_0__6 [label = <>, weight = 100]
|
|
P0_4__3 -> P0_4__4 [label = <>, weight = 100]
|
|
{rank = same; P0_4__4 P0_5_0__6}
|
|
P0_5_0__6 -> P0_5_0__7 [label = <>, weight = 100]
|
|
P0_4__4 -> P0_4__5 [label = <>, weight = 100]
|
|
{rank = same; P0_4__5 P0_5_0__7}
|
|
P0_5_0__7 -> P0_4__5 [label = <(ke1_1,km1_1)>, dir = back, arrowhead = normal]
|
|
P0_5_0__7 -> P0_5_0__8 [label = <>, weight = 100]
|
|
P0_4__5 -> P0_4__6 [label = <>, weight = 100]
|
|
{rank = same; P0_4__6 P0_5_0__8}
|
|
P0_4__7 [label = "", width = 0.3, height = 0.3]
|
|
P0_4__6 -> P0_4__7 [label = <>, weight = 100]
|
|
P0_5_0__8 -> P0_5_0__9 [label = <>, weight = 100]
|
|
P0_4__8 [label = "", style = invisible]
|
|
P0_4__7 -> P0_4__8 [label = <>, weight = 100, style = invisible]
|
|
P0_3__3 -> P0_3__4 [label = <>, weight = 100]
|
|
P0_2__5 -> P0_2__6 [label = <>, weight = 100]
|
|
P0_1__5 -> P0_1__6 [label = <>, weight = 100]
|
|
P0_0__3 -> P0_0__4 [label = <>, weight = 100]
|
|
P__0 -> P__1 [label = <>, weight = 100]
|
|
{rank = same; P__1 P0_0__4 P0_1__6 P0_2__6 P0_3__4 P0_4__8 P0_5_0__9}
|
|
P0_5_0__9 -> P0_5_0__10 [label = <>, weight = 100]
|
|
P__1 -> P__2 [label = <>, weight = 100]
|
|
{rank = same; P__2 P0_5_0__10}
|
|
P0_5_0__10 -> P__2 [label = <~M = GetC>, arrowhead = normal]
|
|
P0_5_0__10 -> P0_5_0__11 [label = <>, weight = 100]
|
|
P0_4__9 [label = "", style = invisible]
|
|
P0_4__8 -> P0_4__9 [label = <>, weight = 100, style = invisible]
|
|
P0_3__4 -> P0_3__5 [label = <>, weight = 100]
|
|
P0_2__6 -> P0_2__7 [label = <>, weight = 100]
|
|
P0_1__6 -> P0_1__7 [label = <>, weight = 100]
|
|
P0_0__4 -> P0_0__5 [label = <>, weight = 100]
|
|
P__2 -> P__3 [label = <>, weight = 100]
|
|
{rank = same; P__3 P0_0__5 P0_1__7 P0_2__7 P0_3__5 P0_4__9 P0_5_0__11}
|
|
P0_5_0__11 -> P0_5_0__12 [label = <>, weight = 100]
|
|
P0_4__10 [label = "", style = invisible]
|
|
P0_4__9 -> P0_4__10 [label = <>, weight = 100, style = invisible]
|
|
P0_3__5 -> P0_3__6 [label = <>, weight = 100]
|
|
P0_2__7 -> P0_2__8 [label = <>, weight = 100]
|
|
P0_1__7 -> P0_1__8 [label = <>, weight = 100]
|
|
P0_0__5 -> P0_0__6 [label = <>, weight = 100]
|
|
P__3 -> P__4 [label = <>, weight = 100]
|
|
{rank = same; P__4 P0_0__6 P0_1__8 P0_2__8 P0_3__6 P0_4__10 P0_5_0__12}
|
|
P0_5_0__12 -> P0_5_0__13 [label = <>, weight = 100]
|
|
P__4 -> P__5 [label = <>, weight = 100]
|
|
{rank = same; P__5 P0_5_0__13}
|
|
P0_5_0__13 -> P__5 [label = <a_1>, dir = back, arrowhead = normal]
|
|
P0_5_0__13 -> P0_5_0__14 [label = <>, weight = 100]
|
|
P0_4__11 [label = "", style = invisible]
|
|
P0_4__10 -> P0_4__11 [label = <>, weight = 100, style = invisible]
|
|
P0_3__6 -> P0_3__7 [label = <>, weight = 100]
|
|
P0_2__8 -> P0_2__9 [label = <>, weight = 100]
|
|
P0_1__8 -> P0_1__9 [label = <>, weight = 100]
|
|
P0_0__6 -> P0_0__7 [label = <>, weight = 100]
|
|
P__5 -> P__6 [label = <>, weight = 100]
|
|
{rank = same; P__6 P0_0__7 P0_1__9 P0_2__9 P0_3__7 P0_4__11 P0_5_0__14}
|
|
P0_5_0__14 -> P0_5_0__15 [label = <>, weight = 100]
|
|
P0_5_0__15 [shape = plaintext, label = <<TABLE BORDER="0" CELLBORDER="1" CELLSPACING="0" CELLPADDING="4"> <TR><TD><FONT COLOR="darkgreen">{10}</FONT><FONT COLOR="blue">new </FONT>nr_4</TD></TR><TR><TD><FONT COLOR="darkgreen">{11}</FONT><FONT COLOR="blue">new </FONT>kr_4</TD></TR></TABLE>>]
|
|
P0_5_0__15 -> P0_5_0__16 [label = <>, weight = 100]
|
|
P0_5_0__16 -> P0_5_0__17 [label = <>, weight = 100]
|
|
P0_4__12 [label = "", style = invisible]
|
|
P0_4__11 -> P0_4__12 [label = <>, weight = 100, style = invisible]
|
|
P0_3__7 -> P0_3__8 [label = <>, weight = 100]
|
|
P0_2__9 -> P0_2__10 [label = <>, weight = 100]
|
|
P0_1__9 -> P0_1__10 [label = <>, weight = 100]
|
|
P0_0__7 -> P0_0__8 [label = <>, weight = 100]
|
|
P__6 -> P__7 [label = <>, weight = 100]
|
|
{rank = same; P__7 P0_0__8 P0_1__10 P0_2__10 P0_3__8 P0_4__12 P0_5_0__17}
|
|
P0_5_0__17 -> P0_5_0__18 [label = <>, weight = 100]
|
|
P__7 -> P__8 [label = <>, weight = 100]
|
|
{rank = same; P__8 P0_5_0__18}
|
|
P0_5_0__18 -> P__8 [label = <~M_1 = sign(senc((nr_4,a_1,kr_4),ke1_1),km1_1)>, arrowhead = normal]
|
|
P0_5_0__18 -> P0_5_0__19 [label = <>, weight = 100]
|
|
P0_4__13 [label = "", style = invisible]
|
|
P0_4__12 -> P0_4__13 [label = <>, weight = 100, style = invisible]
|
|
P0_3__8 -> P0_3__9 [label = <>, weight = 100]
|
|
P0_2__10 -> P0_2__11 [label = <>, weight = 100]
|
|
P0_1__10 -> P0_1__11 [label = <>, weight = 100]
|
|
P0_0__8 -> P0_0__9 [label = <>, weight = 100]
|
|
P__8 -> P__9 [label = <>, weight = 100]
|
|
{rank = same; P__9 P0_0__9 P0_1__11 P0_2__11 P0_3__9 P0_4__13 P0_5_0__19}
|
|
P0_5_0__19 -> P0_5_0__20 [label = <>, weight = 100]
|
|
P0_4__14 [label = "", style = invisible]
|
|
P0_4__13 -> P0_4__14 [label = <>, weight = 100, style = invisible]
|
|
P0_3__9 -> P0_3__10 [label = <>, weight = 100]
|
|
P0_2__11 -> P0_2__12 [label = <>, weight = 100]
|
|
P0_1__11 -> P0_1__12 [label = <>, weight = 100]
|
|
P0_0__9 -> P0_0__10 [label = <>, weight = 100]
|
|
P__9 -> P__10 [label = <>, weight = 100]
|
|
{rank = same; P__10 P0_0__10 P0_1__12 P0_2__12 P0_3__10 P0_4__14 P0_5_0__20}
|
|
P0_5_0__20 -> P0_5_0__21 [label = <>, weight = 100]
|
|
P__10 -> P__11 [label = <>, weight = 100]
|
|
{rank = same; P__11 P0_5_0__21}
|
|
P0_5_0__21 -> P__11 [label = <Phase 1>, style = dotted]
|
|
P0_5_0__21 -> P0_5_0__22 [label = <>, weight = 100]
|
|
P0_4__15 [label = "", style = invisible]
|
|
P0_4__14 -> P0_4__15 [label = <>, weight = 100, style = invisible]
|
|
P0_3__10 -> P0_3__11 [label = <>, weight = 100]
|
|
P0_2__12 -> P0_2__13 [label = <>, weight = 100]
|
|
P0_1__12 -> P0_1__13 [label = <>, weight = 100]
|
|
P0_0__10 -> P0_0__11 [label = <>, weight = 100]
|
|
P__11 -> P__12 [label = <>, weight = 100]
|
|
{rank = same; P__12 P0_0__11 P0_1__13 P0_2__13 P0_3__11 P0_4__15 P0_5_0__22}
|
|
/*RPar */
|
|
P0_5_0__22 -> P0_5_0_1__22 [label = <>]
|
|
P0_5_0__22 -> P0_5_0_0__22 [label = <>]
|
|
P0_5_0__22 [label = "", fixedsize = false, width = 0, height = 0, shape = none]
|
|
{rank = same; P0_5_0_0__22 P0_5_0_1__22}
|
|
P0_5_0_1__22 -> P0_5_0_1__23 [label = <>, weight = 100]
|
|
P0_5_0_1__23 [shape = plaintext, label = <<TABLE BORDER="0" CELLBORDER="1" CELLSPACING="0" CELLPADDING="4"> <TR><TD>Beginning of process <FONT COLOR="darkgreen">passport</FONT></TD></TR></TABLE>>]
|
|
P0_5_0_1__23 -> P0_5_0_1__24 [label = <>, weight = 100]
|
|
P0_5_0_1__24 -> P0_5_0_1__25 [label = <>, weight = 100]
|
|
P0_5_0_0__22 -> P0_5_0_0__23 [label = <>, weight = 100]
|
|
{rank = same; P0_5_0_0__23 P0_5_0_1__25}
|
|
P0_5_0_1__25 -> P0_5_0_1__26 [label = <>, weight = 100]
|
|
P0_5_0_0__23 -> P0_5_0_0__24 [label = <>, weight = 100]
|
|
{rank = same; P0_5_0_0__24 P0_5_0_1__26}
|
|
P0_5_0_1__26 -> P0_5_0_0__24 [label = <<FONT COLOR="blue">choice</FONT>[(ke1_1,km1_1),(ke2_1,km2_1)]>, dir = back, arrowhead = normal]
|
|
P0_5_0_1__26 -> P0_5_0_1__27 [label = <>, weight = 100]
|
|
P0_5_0_0__24 -> P0_5_0_0__25 [label = <>, weight = 100]
|
|
{rank = same; P0_5_0_0__25 P0_5_0_1__27}
|
|
P0_5_0_0__26 [label = "", width = 0.3, height = 0.3]
|
|
P0_5_0_0__25 -> P0_5_0_0__26 [label = <>, weight = 100]
|
|
P0_5_0_1__27 -> P0_5_0_1__28 [label = <>, weight = 100]
|
|
P0_5_0_0__27 [label = "", style = invisible]
|
|
P0_5_0_0__26 -> P0_5_0_0__27 [label = <>, weight = 100, style = invisible]
|
|
P0_4__16 [label = "", style = invisible]
|
|
P0_4__15 -> P0_4__16 [label = <>, weight = 100, style = invisible]
|
|
P0_3__11 -> P0_3__12 [label = <>, weight = 100]
|
|
P0_2__13 -> P0_2__14 [label = <>, weight = 100]
|
|
P0_1__13 -> P0_1__14 [label = <>, weight = 100]
|
|
P0_0__11 -> P0_0__12 [label = <>, weight = 100]
|
|
P__12 -> P__13 [label = <>, weight = 100]
|
|
{rank = same; P__13 P0_0__12 P0_1__14 P0_2__14 P0_3__12 P0_4__16 P0_5_0_0__27 P0_5_0_1__28}
|
|
P0_5_0_1__28 -> P0_5_0_1__29 [label = <>, weight = 100]
|
|
P__13 -> P__14 [label = <>, weight = 100]
|
|
{rank = same; P__14 P0_5_0_1__29}
|
|
P0_5_0_1__29 -> P__14 [label = <GetC>, dir = back, arrowhead = normal]
|
|
P0_5_0_1__29 -> P0_5_0_1__30 [label = <>, weight = 100]
|
|
P0_5_0_0__28 [label = "", style = invisible]
|
|
P0_5_0_0__27 -> P0_5_0_0__28 [label = <>, weight = 100, style = invisible]
|
|
P0_4__17 [label = "", style = invisible]
|
|
P0_4__16 -> P0_4__17 [label = <>, weight = 100, style = invisible]
|
|
P0_3__12 -> P0_3__13 [label = <>, weight = 100]
|
|
P0_2__14 -> P0_2__15 [label = <>, weight = 100]
|
|
P0_1__14 -> P0_1__15 [label = <>, weight = 100]
|
|
P0_0__12 -> P0_0__13 [label = <>, weight = 100]
|
|
P__14 -> P__15 [label = <>, weight = 100]
|
|
{rank = same; P__15 P0_0__13 P0_1__15 P0_2__15 P0_3__13 P0_4__17 P0_5_0_0__28 P0_5_0_1__30}
|
|
P0_5_0_1__30 -> P0_5_0_1__31 [label = <>, weight = 100]
|
|
P0_5_0_1__31 [shape = plaintext, label = <<TABLE BORDER="0" CELLBORDER="1" CELLSPACING="0" CELLPADDING="4"> <TR><TD><FONT COLOR="darkgreen">{43}</FONT><FONT COLOR="blue">new </FONT>nt_4</TD></TR></TABLE>>]
|
|
P0_5_0_1__31 -> P0_5_0_1__32 [label = <>, weight = 100]
|
|
P0_5_0_1__32 -> P0_5_0_1__33 [label = <>, weight = 100]
|
|
P0_5_0_0__29 [label = "", style = invisible]
|
|
P0_5_0_0__28 -> P0_5_0_0__29 [label = <>, weight = 100, style = invisible]
|
|
P0_4__18 [label = "", style = invisible]
|
|
P0_4__17 -> P0_4__18 [label = <>, weight = 100, style = invisible]
|
|
P0_3__13 -> P0_3__14 [label = <>, weight = 100]
|
|
P0_2__15 -> P0_2__16 [label = <>, weight = 100]
|
|
P0_1__15 -> P0_1__16 [label = <>, weight = 100]
|
|
P0_0__13 -> P0_0__14 [label = <>, weight = 100]
|
|
P__15 -> P__16 [label = <>, weight = 100]
|
|
{rank = same; P__16 P0_0__14 P0_1__16 P0_2__16 P0_3__14 P0_4__18 P0_5_0_0__29 P0_5_0_1__33}
|
|
P0_5_0_1__33 -> P0_5_0_1__34 [label = <>, weight = 100]
|
|
P__16 -> P__17 [label = <>, weight = 100]
|
|
{rank = same; P__17 P0_5_0_1__34}
|
|
P0_5_0_1__34 -> P__17 [label = <~M_2 = nt_4>, arrowhead = normal]
|
|
P0_5_0_1__34 -> P0_5_0_1__35 [label = <>, weight = 100]
|
|
P0_5_0_0__30 [label = "", style = invisible]
|
|
P0_5_0_0__29 -> P0_5_0_0__30 [label = <>, weight = 100, style = invisible]
|
|
P0_4__19 [label = "", style = invisible]
|
|
P0_4__18 -> P0_4__19 [label = <>, weight = 100, style = invisible]
|
|
P0_3__14 -> P0_3__15 [label = <>, weight = 100]
|
|
P0_2__16 -> P0_2__17 [label = <>, weight = 100]
|
|
P0_1__16 -> P0_1__17 [label = <>, weight = 100]
|
|
P0_0__14 -> P0_0__15 [label = <>, weight = 100]
|
|
P__17 -> P__18 [label = <>, weight = 100]
|
|
{rank = same; P__18 P0_0__15 P0_1__17 P0_2__17 P0_3__15 P0_4__19 P0_5_0_0__30 P0_5_0_1__35}
|
|
P0_5_0_1__35 -> P0_5_0_1__36 [label = <>, weight = 100]
|
|
P0_5_0_0__31 [label = "", style = invisible]
|
|
P0_5_0_0__30 -> P0_5_0_0__31 [label = <>, weight = 100, style = invisible]
|
|
P0_4__20 [label = "", style = invisible]
|
|
P0_4__19 -> P0_4__20 [label = <>, weight = 100, style = invisible]
|
|
P0_3__15 -> P0_3__16 [label = <>, weight = 100]
|
|
P0_2__17 -> P0_2__18 [label = <>, weight = 100]
|
|
P0_1__17 -> P0_1__18 [label = <>, weight = 100]
|
|
P0_0__15 -> P0_0__16 [label = <>, weight = 100]
|
|
P__18 -> P__19 [label = <>, weight = 100]
|
|
{rank = same; P__19 P0_0__16 P0_1__18 P0_2__18 P0_3__16 P0_4__20 P0_5_0_0__31 P0_5_0_1__36}
|
|
P0_5_0_1__36 -> P0_5_0_1__37 [label = <>, weight = 100]
|
|
P__19 -> P__20 [label = <>, weight = 100]
|
|
{rank = same; P__20 P0_5_0_1__37}
|
|
P0_5_0_1__37 -> P__20 [label = <~M_1 = sign(senc((nr_4,a_1,kr_4),ke1_1),km1_1)>, dir = back, arrowhead = normal]
|
|
P0_5_0_1__37 -> P0_5_0_1__38 [label = <>, weight = 100]
|
|
P0_5_0_0__32 [label = "", style = invisible]
|
|
P0_5_0_0__31 -> P0_5_0_0__32 [label = <>, weight = 100, style = invisible]
|
|
P0_4__21 [label = "", style = invisible]
|
|
P0_4__20 -> P0_4__21 [label = <>, weight = 100, style = invisible]
|
|
P0_3__16 -> P0_3__17 [label = <>, weight = 100]
|
|
P0_2__18 -> P0_2__19 [label = <>, weight = 100]
|
|
P0_1__18 -> P0_1__19 [label = <>, weight = 100]
|
|
P0_0__16 -> P0_0__17 [label = <>, weight = 100]
|
|
P__20 -> P__21 [label = <>, weight = 100]
|
|
{rank = same; P__21 P0_0__17 P0_1__19 P0_2__19 P0_3__17 P0_4__21 P0_5_0_0__32 P0_5_0_1__38}
|
|
P0_5_0_1__38 -> P0_5_0_1__39 [label = <>, weight = 100]
|
|
P0_5_0_1__39 [color = red, shape = plaintext, label = <<TABLE BORDER="0" CELLBORDER="1" CELLSPACING="0" CELLPADDING="4"> <TR><TD><FONT COLOR="darkgreen">{46}</FONT><FONT COLOR="blue">let</FONT> x_3 = checksign(sign(senc((nr_4,a_1,kr_4),<br/>
|
|
ke1_1),km1_1),vk(<FONT COLOR="blue">choice</FONT>[km1_1,km2_1]))<br/>
|
|
This process performs a test that may succeed on<br/>
|
|
one side and not on the other.</TD></TR></TABLE>>]
|
|
P0_5_0_1__39 -> P0_5_0_1__40 [label = <>, weight = 100]
|
|
} |