ATTACK 1 -- (Id: 591) | |
Violated Constraints | Open Variables |
b1 < > B2 | b3 -> A3 sk3 -> k!10 sk2 -> k!20 a1 -> A3 ak1 -> k!20 b1 -> A3 bk1 -> k!10 |
Knowledge | Context |
{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)] |
Model | Intruder 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 |