ATTACK 1 -- (Id: 591)
Violated ConstraintsOpen Variables
b1 < > B2

b3 -> A3
sk3 -> k!10
sk2 -> k!20
a1 -> A3
ak1 -> k!20
b1 -> A3
bk1 -> k!10
KnowledgeContext
{nc2}kab1, {nt2,A3,kab1}kbb2, {na3}kab1, tka2(K:606:*), nc2,
{na3,A3,kab1}k!10, {nb2,A3,kab1}k!20, na3, A3, nb2,
na3, A3, A3+, B2, B2+,
S1, S1+, I0, .
A3: () [out(na3,A3).in({na3,A3,kab1}k!10,tkb3(K:608:*),nc2,{na3}kab1).out({nc2}kab1)]
B2: () [in(na3,A3).out(na3,A3,nb2,B2).in({nb2,A3,kab1}k!20,tka2(K:606:*)).out(tka2(K:606:*),{nt2,A3,kab1}kbb2,nc2,{na3}kab1).in({nc2}kab1)]
S1: () [in(nb2,A3,na3,A3).out({na3,A3,kab1}k!10,{nb2,A3,kab1}k!20)]

ModelIntruder process
b1(K:16:n \> B2
a1(K:16:n -> A3
b1(K:16:n -> A3
cna1(K:604:*) -> nb2
cnb1(K:604:*) -> na3
cn2(K:602:*) -> na3
bn3(K:608:*) -> nc2

A3 -> I: na3,A3
I -> B2: na3,A3
B2 -> I: na3,A3,nb2,B2
I -> S1: nb2,A3,na3,A3
S1 -> I: {na3,A3,kab1}k!10,{nb2,A3,kab1}k!20
I -> B2: {nb2,A3,kab1}k!20,tka2(K:606:*)
B2 -> I: tka2(K:606:*),{nt2,A3,kab1}kbb2,nc2,{na3}kab1
I -> A3: {na3,A3,kab1}k!10,tkb3(K:608:*),nc2,{na3}kab1
A3 -> I: {nc2}kab1
I -> B2: {nc2}kab1