ATTACK 1 -- (Id: 33) | |
Violated Constraints | Open Variables |
b2 = B1 a1 < > A2 | b2 -> B1 s2 -> k!10 s1 -> k!10 |
Knowledge | Context |
{B1,{B1}k!10}kab1, {kab1}A2+, {A2}k!10, A2, A2+, B1, B1+, {A3}k!10, I0, A3, . | A2: () [out(A2,{A2}k!10,A2+).in({kab1}A2-).in({B1,{B1}k!10}kab1)] B1: () [in(A3,{A3}k!10,A2+).out({kab1}A2+).out({B1,{B1}k!10}kab1)] |
Model | Intruder process |
a1(K:8:*) -> A3 ak1(K:8:*) -> A2+ | A2 -> I: A2,{A2}k!10,A2+ I -> B1: A3,{A3}k!10,A2+ B1 -> I: {kab1}A2+ B1 -> I: {B1,{B1}k!10}kab1 I -> A2: {kab1}A2+ I -> A2: {B1,{B1}k!10}kab1 |