ATTACK 1 -- (Id: 2364)
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:2354:*) -> nmb2
ma2(K:2352:*) -> nma3
mb3(K:2369:*) -> 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: 2373)
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:2352:*) -> nma3
ma2(K:2374:*) -> nmb1
mb3(K:2377:*) -> 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: 2624)
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:2612:*) -> nmb2
ma2(K:2610:*) -> nma3
mb3(K:2627:*) -> 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: 2633)
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:2610:*) -> nma3
ma2(K:2632:*) -> nmb1
mb3(K:2635:*) -> 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: 3091)
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:3076:*) -> nmb2
ma2(K:3074:*) -> nma3
mb3(K:3091:*) -> 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 6 -- (Id: 3100)
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:3074:*) -> nma3
ma2(K:3096:*) -> nmb1
mb3(K:3099:*) -> 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