ATTACK 1 -- (Id: 67)
Violated ConstraintsOpen Variables
K :> nb1
z1 < > I0
z1 = A2
x2 < > B1

x2 -> I0
KnowledgeContext
nb1, {na2,nb1}A2+, na2, A2, A2+,
B1, B1+, I0, I0+, I0-,
.
A2: () [out({A2,na2}I0+).in({na2,nb1}A2-).out({nb1}I0+)]
B1: () [in({A2,na2}B1-).out({na2,nb1}A2+).in({nb1}B1-)]

ModelIntruder process
u1(K:56:*) -> na2
z1(K:56:*) -> A2
x2(K:5:nr) -> I0

A2 -> I: {A2,na2}I0+
I -> B1: {A2,na2}B1+
B1 -> I: {na2,nb1}A2+
I -> A2: {na2,nb1}A2+
A2 -> I: {nb1}I0+
I -> B1: {nb1}B1+



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

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

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

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



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

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

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

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



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

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

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

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



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

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

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

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