ATTACK 1 -- (Id: 3001)
Violated ConstraintsOpen Variables
b3 = B2
a2 = A3
mb3 < > nmb2

b3 -> B2
sk3 -> k!20
tk3 -> k!30
a2 -> A3
sk2 -> k!20
tk2 -> k!30
a1 -> A3
sk1 -> k!20
tk1 -> k!10
KnowledgeContext
{nmb1}k!20, {nmb2}k!20, nmb1, {nma3}k!20, nmb2,
{B2,A3,k!20}k!30, nma3, A3, A3+, B2,
B2+, B1, B1+, {B1,A3,k!20}k!10, I0,
.
A3: () [out(nma3,{B2,A3,k!20}k!30).in(nmb1,{nma3}k!20).out({nmb1}k!20)]
B2: () [in(nma3,{B2,A3,k!20}k!30).out(nmb2,{nma3}k!20).in({nmb2}k!20)]
B1: () [in(nmb2,{B1,A3,k!20}k!10).out(nmb1,{nmb2}k!20).in({nmb1}k!20)]

ModelIntruder process
ma1(K:2991:*) -> nmb2
ma2(K:2989:*) -> nma3
mb3(K:3006:*) -> nmb1

A3 -> I: nma3,{B2,A3,k!20}k!30
I -> B2: nma3,{B2,A3,k!20}k!30
B2 -> I: nmb2,{nma3}k!20
I -> B1: nmb2,{B1,A3,k!20}k!10
B1 -> I: nmb1,{nmb2}k!20
I -> B2: {nmb2}k!20
I -> A3: nmb1,{nma3}k!20
A3 -> I: {nmb1}k!20
I -> B1: {nmb1}k!20



ATTACK 2 -- (Id: 3010)
Violated ConstraintsOpen Variables
b3 = B2
a2 = A3
ma2 < > nma3

b3 -> B2
sk3 -> k!20
tk3 -> k!30
a2 -> A3
sk2 -> k!20
tk2 -> k!30
a1 -> A3
sk1 -> k!20
tk1 -> k!10
KnowledgeContext
{nmb2}k!20, {nmb1}k!20, nmb2, {nma3}k!20, nmb1,
{B2,A3,k!20}k!30, nma3, A3, A3+, B2,
B2+, B1, B1+, {B1,A3,k!20}k!10, I0,
.
A3: () [out(nma3,{B2,A3,k!20}k!30).in(nmb2,{nma3}k!20).out({nmb2}k!20)]
B2: () [in(nmb1,{B2,A3,k!20}k!30).out(nmb2,{nmb1}k!20).in({nmb2}k!20)]
B1: () [in(nma3,{B1,A3,k!20}k!10).out(nmb1,{nma3}k!20).in({nmb1}k!20)]

ModelIntruder process
ma1(K:2989:*) -> nma3
ma2(K:3011:*) -> nmb1
mb3(K:3014:*) -> nmb2

A3 -> I: nma3,{B2,A3,k!20}k!30
I -> B1: nma3,{B1,A3,k!20}k!10
B1 -> I: nmb1,{nma3}k!20
I -> B2: nmb1,{B2,A3,k!20}k!30
B2 -> I: nmb2,{nmb1}k!20
I -> B1: {nmb1}k!20
I -> A3: nmb2,{nma3}k!20
A3 -> I: {nmb2}k!20
I -> B2: {nmb2}k!20



ATTACK 3 -- (Id: 3261)
Violated ConstraintsOpen Variables
b3 = B2
a2 = A3
mb3 < > nmb2

b3 -> B2
sk3 -> k!20
tk3 -> k!20
a2 -> A3
sk2 -> k!20
tk2 -> k!20
a1 -> A3
sk1 -> k!20
tk1 -> k!10
KnowledgeContext
{nmb1}k!20, {nmb2}k!20, nmb1, {nma3}k!20, nmb2,
{B2,A3,k!20}k!20, nma3, A3, A3+, B2,
B2+, B1, B1+, {B1,A3,k!20}k!10, I0,
.
A3: () [out(nma3,{B2,A3,k!20}k!20).in(nmb1,{nma3}k!20).out({nmb1}k!20)]
B2: () [in(nma3,{B2,A3,k!20}k!20).out(nmb2,{nma3}k!20).in({nmb2}k!20)]
B1: () [in(nmb2,{B1,A3,k!20}k!10).out(nmb1,{nmb2}k!20).in({nmb1}k!20)]

ModelIntruder process
ma1(K:3249:*) -> nmb2
ma2(K:3247:*) -> nma3
mb3(K:3264:*) -> nmb1

A3 -> I: nma3,{B2,A3,k!20}k!20
I -> B2: nma3,{B2,A3,k!20}k!20
B2 -> I: nmb2,{nma3}k!20
I -> B1: nmb2,{B1,A3,k!20}k!10
B1 -> I: nmb1,{nmb2}k!20
I -> B2: {nmb2}k!20
I -> A3: nmb1,{nma3}k!20
A3 -> I: {nmb1}k!20
I -> B1: {nmb1}k!20



ATTACK 4 -- (Id: 3270)
Violated ConstraintsOpen Variables
b3 = B2
a2 = A3
ma2 < > nma3

b3 -> B2
sk3 -> k!20
tk3 -> k!20
a2 -> A3
sk2 -> k!20
tk2 -> k!20
a1 -> A3
sk1 -> k!20
tk1 -> k!10
KnowledgeContext
{nmb2}k!20, {nmb1}k!20, nmb2, {nma3}k!20, nmb1,
{B2,A3,k!20}k!20, nma3, A3, A3+, B2,
B2+, B1, B1+, {B1,A3,k!20}k!10, I0,
.
A3: () [out(nma3,{B2,A3,k!20}k!20).in(nmb2,{nma3}k!20).out({nmb2}k!20)]
B2: () [in(nmb1,{B2,A3,k!20}k!20).out(nmb2,{nmb1}k!20).in({nmb2}k!20)]
B1: () [in(nma3,{B1,A3,k!20}k!10).out(nmb1,{nma3}k!20).in({nmb1}k!20)]

ModelIntruder process
ma1(K:3247:*) -> nma3
ma2(K:3269:*) -> nmb1
mb3(K:3272:*) -> nmb2

A3 -> I: nma3,{B2,A3,k!20}k!20
I -> B1: nma3,{B1,A3,k!20}k!10
B1 -> I: nmb1,{nma3}k!20
I -> B2: nmb1,{B2,A3,k!20}k!20
B2 -> I: nmb2,{nmb1}k!20
I -> B1: {nmb1}k!20
I -> A3: nmb2,{nma3}k!20
A3 -> I: {nmb2}k!20
I -> B2: {nmb2}k!20



ATTACK 5 -- (Id: 3491)
Violated ConstraintsOpen Variables
b3 = B2
a2 = A3
mb3 < > nmb2

b3 -> B2
sk3 -> k!20
tk3 -> k!10
a2 -> A3
sk2 -> k!20
tk2 -> k!10
a1 -> A3
sk1 -> k!20
tk1 -> k!10
KnowledgeContext
{nmb1}k!20, {nmb2}k!20, nmb1, {nma3}k!20, nmb2,
{B2,A3,k!20}k!10, nma3, A3, A3+, B2,
B2+, B1, B1+, {B1,A3,k!20}k!10, I0,
.
A3: () [out(nma3,{B2,A3,k!20}k!10).in(nmb1,{nma3}k!20).out({nmb1}k!20)]
B2: () [in(nma3,{B2,A3,k!20}k!10).out(nmb2,{nma3}k!20).in({nmb2}k!20)]
B1: () [in(nmb2,{B1,A3,k!20}k!10).out(nmb1,{nmb2}k!20).in({nmb1}k!20)]

ModelIntruder process
ma1(K:3477:*) -> nmb2
ma2(K:3475:*) -> nma3
mb3(K:3492:*) -> nmb1

A3 -> I: nma3,{B2,A3,k!20}k!10
I -> B2: nma3,{B2,A3,k!20}k!10
B2 -> I: nmb2,{nma3}k!20
I -> B1: nmb2,{B1,A3,k!20}k!10
B1 -> I: nmb1,{nmb2}k!20
I -> B2: {nmb2}k!20
I -> A3: nmb1,{nma3}k!20
A3 -> I: {nmb1}k!20
I -> B1: {nmb1}k!20



ATTACK 6 -- (Id: 3743)
Violated ConstraintsOpen Variables
b3 = B2
a2 = A3
mb3 < > nmb2

b3 -> B2
sk3 -> k!10
tk3 -> k!20
a2 -> A3
sk2 -> k!10
tk2 -> k!20
a1 -> A3
sk1 -> k!10
tk1 -> k!10
KnowledgeContext
{nmb1}k!10, {nmb2}k!10, nmb1, {nma3}k!10, nmb2,
{B2,A3,k!10}k!20, nma3, A3, A3+, B2,
B2+, B1, B1+, {B1,A3,k!10}k!10, I0,
.
A3: () [out(nma3,{B2,A3,k!10}k!20).in(nmb1,{nma3}k!10).out({nmb1}k!10)]
B2: () [in(nma3,{B2,A3,k!10}k!20).out(nmb2,{nma3}k!10).in({nmb2}k!10)]
B1: () [in(nmb2,{B1,A3,k!10}k!10).out(nmb1,{nmb2}k!10).in({nmb1}k!10)]

ModelIntruder process
ma1(K:3728:*) -> nmb2
ma2(K:3726:*) -> nma3
mb3(K:3743:*) -> nmb1

A3 -> I: nma3,{B2,A3,k!10}k!20
I -> B2: nma3,{B2,A3,k!10}k!20
B2 -> I: nmb2,{nma3}k!10
I -> B1: nmb2,{B1,A3,k!10}k!10
B1 -> I: nmb1,{nmb2}k!10
I -> B2: {nmb2}k!10
I -> A3: nmb1,{nma3}k!10
A3 -> I: {nmb1}k!10
I -> B1: {nmb1}k!10



ATTACK 7 -- (Id: 3752)
Violated ConstraintsOpen Variables
b3 = B2
a2 = A3
ma2 < > nma3

b3 -> B2
sk3 -> k!10
tk3 -> k!20
a2 -> A3
sk2 -> k!10
tk2 -> k!20
a1 -> A3
sk1 -> k!10
tk1 -> k!10
KnowledgeContext
{nmb2}k!10, {nmb1}k!10, nmb2, {nma3}k!10, nmb1,
{B2,A3,k!10}k!20, nma3, A3, A3+, B2,
B2+, B1, B1+, {B1,A3,k!10}k!10, I0,
.
A3: () [out(nma3,{B2,A3,k!10}k!20).in(nmb2,{nma3}k!10).out({nmb2}k!10)]
B2: () [in(nmb1,{B2,A3,k!10}k!20).out(nmb2,{nmb1}k!10).in({nmb2}k!10)]
B1: () [in(nma3,{B1,A3,k!10}k!10).out(nmb1,{nma3}k!10).in({nmb1}k!10)]

ModelIntruder process
ma1(K:3726:*) -> nma3
ma2(K:3748:*) -> nmb1
mb3(K:3751:*) -> nmb2

A3 -> I: nma3,{B2,A3,k!10}k!20
I -> B1: nma3,{B1,A3,k!10}k!10
B1 -> I: nmb1,{nma3}k!10
I -> B2: nmb1,{B2,A3,k!10}k!20
B2 -> I: nmb2,{nmb1}k!10
I -> B1: {nmb1}k!10
I -> A3: nmb2,{nma3}k!10
A3 -> I: {nmb2}k!10
I -> B2: {nmb2}k!10



ATTACK 8 -- (Id: 3872)
Violated ConstraintsOpen Variables
b3 = B2
a2 = A3
mb3 < > nmb2

b3 -> B2
sk3 -> k!10
tk3 -> k!10
a2 -> A3
sk2 -> k!10
tk2 -> k!10
a1 -> A3
sk1 -> k!10
tk1 -> k!10
KnowledgeContext
{nmb1}k!10, {nmb2}k!10, nmb1, {nma3}k!10, nmb2,
{B2,A3,k!10}k!10, nma3, A3, A3+, B2,
B2+, B1, B1+, {B1,A3,k!10}k!10, I0,
.
A3: () [out(nma3,{B2,A3,k!10}k!10).in(nmb1,{nma3}k!10).out({nmb1}k!10)]
B2: () [in(nma3,{B2,A3,k!10}k!10).out(nmb2,{nma3}k!10).in({nmb2}k!10)]
B1: () [in(nmb2,{B1,A3,k!10}k!10).out(nmb1,{nmb2}k!10).in({nmb1}k!10)]

ModelIntruder process
ma1(K:3855:*) -> nmb2
ma2(K:3853:*) -> nma3
mb3(K:3870:*) -> nmb1

A3 -> I: nma3,{B2,A3,k!10}k!10
I -> B2: nma3,{B2,A3,k!10}k!10
B2 -> I: nmb2,{nma3}k!10
I -> B1: nmb2,{B1,A3,k!10}k!10
B1 -> I: nmb1,{nmb2}k!10
I -> B2: {nmb2}k!10
I -> A3: nmb1,{nma3}k!10
A3 -> I: {nmb1}k!10
I -> B1: {nmb1}k!10