ATTACK 1 -- (Id: 130)
Violated ConstraintsOpen Variables
K :> nb2
z2 < > I0
T

KnowledgeContext
nb1, nb2, {nb2,I0}B1+, B2, B2+,
B1, B1+, I0, I0+, I0-,
.
B2: () [in({I0,B1}B2-).out({nb2,I0}B1+).in({nb2}B2-)]
B1: () [in({nb2,I0}B1-).out({nb1,nb2}I0+).in({nb1}B1-)]

ModelIntruder process
u2(K:10:nr) -> I0
z2(K:10:*) -> B1

I -> B2: {I0,B1}B2+
B2 -> I: {nb2,I0}B1+
I -> B1: {nb2,I0}B1+
B1 -> I: {nb1,nb2}I0+
I -> B1: {nb1}B1+
I -> B2: {nb2}B2+



ATTACK 2 -- (Id: 133)
Violated ConstraintsOpen Variables
K :> nb2
z2 < > I0
T

KnowledgeContext
nb1, nb2, {nb2,I0}B1+, B2, B2+,
B1, B1+, I0, I0+, I0-,
.
B2: () [in({I0,B1}B2-).out({nb2,I0}B1+).in({nb2}B2-)]
B1: () [in({nb2,I0}B1-).out({nb1,nb2}I0+).in({nb1}B1-)]

ModelIntruder process
u2(K:10:nr) -> I0
z2(K:10:*) -> B1

I -> B2: {I0,B1}B2+
B2 -> I: {nb2,I0}B1+
I -> B1: {nb2,I0}B1+
B1 -> I: {nb1,nb2}I0+
I -> B2: {nb2}B2+
I -> B1: {nb1}B1+



ATTACK 3 -- (Id: 164)
Violated ConstraintsOpen Variables
K :> nb1
z1 < > I0
T

KnowledgeContext
nb2, nb1, {nb1,I0}B2+, B2, B2+,
B1, B1+, I0, I0+, I0-,
.
B2: () [in({nb1,I0}B2-).out({nb2,nb1}I0+).in({nb2}B2-)]
B1: () [in({I0,B2}B1-).out({nb1,I0}B2+).in({nb1}B1-)]

ModelIntruder process
u1(K:10:nr) -> I0
z1(K:10:*) -> B2

I -> B1: {I0,B2}B1+
B1 -> I: {nb1,I0}B2+
I -> B2: {nb1,I0}B2+
B2 -> I: {nb2,nb1}I0+
I -> B2: {nb2}B2+
I -> B1: {nb1}B1+



ATTACK 4 -- (Id: 167)
Violated ConstraintsOpen Variables
K :> nb1
z1 < > I0
T

KnowledgeContext
nb2, nb1, {nb1,I0}B2+, B2, B2+,
B1, B1+, I0, I0+, I0-,
.
B2: () [in({nb1,I0}B2-).out({nb2,nb1}I0+).in({nb2}B2-)]
B1: () [in({I0,B2}B1-).out({nb1,I0}B2+).in({nb1}B1-)]

ModelIntruder process
u1(K:10:nr) -> I0
z1(K:10:*) -> B2

I -> B1: {I0,B2}B1+
B1 -> I: {nb1,I0}B2+
I -> B2: {nb1,I0}B2+
B2 -> I: {nb2,nb1}I0+
I -> B1: {nb1}B1+
I -> B2: {nb2}B2+