ATTACK 1 -- (Id: 2918)
Violated ConstraintsOpen Variables
b3 = B2
u2 = A3
tk3 = tk2
mb3 < > nmb2

b3 -> B2
sk3 -> k!20
tk3 -> k!30
sk2 -> k!20
tk2 -> k!30
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+, {B2,A3,k!20}k!30, {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:2908:*) -> nmb2
ma2(K:2906:*) -> nma3
mb3(K:2923:*) -> 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: 2927)
Violated ConstraintsOpen Variables
b3 = B2
u2 = A3
tk3 = tk2
ma2 < > nma3

b3 -> B2
sk3 -> k!20
tk3 -> k!30
sk2 -> k!20
tk2 -> k!30
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+, {B2,A3,k!20}k!30, {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:2906:*) -> nma3
ma2(K:2928:*) -> nmb1
mb3(K:2931:*) -> 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: 3068)
Violated ConstraintsOpen Variables
b3 = B1
u1 = A3
tk3 = tk1
ma1 < > nma3

b3 -> B1
sk3 -> k!20
tk3 -> k!10
sk2 -> k!20
tk2 -> k!30
sk1 -> k!20
tk1 -> k!10
KnowledgeContext
{nmb1}k!20, {nmb2}k!20, nmb1, {nma3}k!20, nmb2,
{B1,A3,k!20}k!10, nma3, A3, A3+, B2,
B2+, B1, B1+, {B2,A3,k!20}k!30, {B1,A3,k!20}k!10,
I0, .
A3: () [out(nma3,{B1,A3,k!20}k!10).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:3056:*) -> nmb2
ma2(K:3054:*) -> nma3
mb3(K:3071:*) -> nmb1

A3 -> I: nma3,{B1,A3,k!20}k!10
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 4 -- (Id: 3077)
Violated ConstraintsOpen Variables
b3 = B1
u1 = A3
tk3 = tk1
mb3 < > nmb1

b3 -> B1
sk3 -> k!20
tk3 -> k!10
sk2 -> k!20
tk2 -> k!30
sk1 -> k!20
tk1 -> k!10
KnowledgeContext
{nmb2}k!20, {nmb1}k!20, nmb2, {nma3}k!20, nmb1,
{B1,A3,k!20}k!10, nma3, A3, A3+, B2,
B2+, B1, B1+, {B2,A3,k!20}k!30, {B1,A3,k!20}k!10,
I0, .
A3: () [out(nma3,{B1,A3,k!20}k!10).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:3054:*) -> nma3
ma2(K:3076:*) -> nmb1
mb3(K:3079:*) -> nmb2

A3 -> I: nma3,{B1,A3,k!20}k!10
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 5 -- (Id: 3737)
Violated ConstraintsOpen Variables
b3 = B2
u2 = A3
tk3 = tk2
mb3 < > nmb2

b3 -> B2
sk3 -> k!20
tk3 -> k!20
sk2 -> k!20
tk2 -> k!20
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+, {B2,A3,k!20}k!20, {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:3723:*) -> nmb2
ma2(K:3721:*) -> nma3
mb3(K:3738:*) -> 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 6 -- (Id: 3746)
Violated ConstraintsOpen Variables
b3 = B2
u2 = A3
tk3 = tk2
ma2 < > nma3

b3 -> B2
sk3 -> k!20
tk3 -> k!20
sk2 -> k!20
tk2 -> k!20
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+, {B2,A3,k!20}k!20, {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:3721:*) -> nma3
ma2(K:3743:*) -> nmb1
mb3(K:3746:*) -> 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 7 -- (Id: 3802)
Violated ConstraintsOpen Variables
b3 = B1
u1 = A3
tk3 = tk1
ma1 < > nma3

b3 -> B1
sk3 -> k!20
tk3 -> k!10
sk2 -> k!20
tk2 -> k!20
sk1 -> k!20
tk1 -> k!10
KnowledgeContext
{nmb1}k!20, {nmb2}k!20, nmb1, {nma3}k!20, nmb2,
{B1,A3,k!20}k!10, nma3, A3, A3+, B2,
B2+, B1, B1+, {B2,A3,k!20}k!20, {B1,A3,k!20}k!10,
I0, .
A3: () [out(nma3,{B1,A3,k!20}k!10).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:3786:*) -> nmb2
ma2(K:3784:*) -> nma3
mb3(K:3801:*) -> nmb1

A3 -> I: nma3,{B1,A3,k!20}k!10
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 8 -- (Id: 3811)
Violated ConstraintsOpen Variables
b3 = B1
u1 = A3
tk3 = tk1
mb3 < > nmb1

b3 -> B1
sk3 -> k!20
tk3 -> k!10
sk2 -> k!20
tk2 -> k!20
sk1 -> k!20
tk1 -> k!10
KnowledgeContext
{nmb2}k!20, {nmb1}k!20, nmb2, {nma3}k!20, nmb1,
{B1,A3,k!20}k!10, nma3, A3, A3+, B2,
B2+, B1, B1+, {B2,A3,k!20}k!20, {B1,A3,k!20}k!10,
I0, .
A3: () [out(nma3,{B1,A3,k!20}k!10).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:3784:*) -> nma3
ma2(K:3806:*) -> nmb1
mb3(K:3809:*) -> nmb2

A3 -> I: nma3,{B1,A3,k!20}k!10
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 9 -- (Id: 4443)
Violated ConstraintsOpen Variables
b3 = B2
u2 = A3
tk3 = tk2
mb3 < > nmb2

b3 -> B2
sk3 -> k!20
tk3 -> k!10
sk2 -> k!20
tk2 -> k!10
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+, {B2,A3,k!20}k!10, {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:4425:*) -> nmb2
ma2(K:4423:*) -> nma3
mb3(K:4440:*) -> 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 10 -- (Id: 4452)
Violated ConstraintsOpen Variables
b3 = B1
u1 = A3
tk3 = tk1
mb3 < > nmb1

b3 -> B1
sk3 -> k!20
tk3 -> k!10
sk2 -> k!20
tk2 -> k!10
sk1 -> k!20
tk1 -> k!10
KnowledgeContext
{nmb2}k!20, {nmb1}k!20, nmb2, {nma3}k!20, nmb1,
{B1,A3,k!20}k!10, nma3, A3, A3+, B2,
B2+, B1, B1+, {B2,A3,k!20}k!10, {B1,A3,k!20}k!10,
I0, .
A3: () [out(nma3,{B1,A3,k!20}k!10).in(nmb2,{nma3}k!20).out({nmb2}k!20)]
B2: () [in(nmb1,{B2,A3,k!20}k!10).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:4423:*) -> nma3
ma2(K:4445:*) -> nmb1
mb3(K:4448:*) -> nmb2

A3 -> I: nma3,{B1,A3,k!20}k!10
I -> B1: nma3,{B1,A3,k!20}k!10
B1 -> I: nmb1,{nma3}k!20
I -> B2: nmb1,{B2,A3,k!20}k!10
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 11 -- (Id: 5206)
Violated ConstraintsOpen Variables
b3 = B2
u2 = A3
tk3 = tk2
mb3 < > nmb2

b3 -> B2
sk3 -> k!10
tk3 -> k!20
sk2 -> k!10
tk2 -> k!20
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+, {B2,A3,k!10}k!20, {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:5186:*) -> nmb2
ma2(K:5184:*) -> nma3
mb3(K:5201:*) -> 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 12 -- (Id: 5215)
Violated ConstraintsOpen Variables
b3 = B2
u2 = A3
tk3 = tk2
ma2 < > nma3

b3 -> B2
sk3 -> k!10
tk3 -> k!20
sk2 -> k!10
tk2 -> k!20
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+, {B2,A3,k!10}k!20, {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:5184:*) -> nma3
ma2(K:5206:*) -> nmb1
mb3(K:5209:*) -> 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 13 -- (Id: 5271)
Violated ConstraintsOpen Variables
b3 = B1
u1 = A3
tk3 = tk1
ma1 < > nma3

b3 -> B1
sk3 -> k!10
tk3 -> k!10
sk2 -> k!10
tk2 -> k!20
sk1 -> k!10
tk1 -> k!10
KnowledgeContext
{nmb1}k!10, {nmb2}k!10, nmb1, {nma3}k!10, nmb2,
{B1,A3,k!10}k!10, nma3, A3, A3+, B2,
B2+, B1, B1+, {B2,A3,k!10}k!20, {B1,A3,k!10}k!10,
I0, .
A3: () [out(nma3,{B1,A3,k!10}k!10).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:5249:*) -> nmb2
ma2(K:5247:*) -> nma3
mb3(K:5264:*) -> nmb1

A3 -> I: nma3,{B1,A3,k!10}k!10
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 14 -- (Id: 5280)
Violated ConstraintsOpen Variables
b3 = B1
u1 = A3
tk3 = tk1
mb3 < > nmb1

b3 -> B1
sk3 -> k!10
tk3 -> k!10
sk2 -> k!10
tk2 -> k!20
sk1 -> k!10
tk1 -> k!10
KnowledgeContext
{nmb2}k!10, {nmb1}k!10, nmb2, {nma3}k!10, nmb1,
{B1,A3,k!10}k!10, nma3, A3, A3+, B2,
B2+, B1, B1+, {B2,A3,k!10}k!20, {B1,A3,k!10}k!10,
I0, .
A3: () [out(nma3,{B1,A3,k!10}k!10).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:5247:*) -> nma3
ma2(K:5269:*) -> nmb1
mb3(K:5272:*) -> nmb2

A3 -> I: nma3,{B1,A3,k!10}k!10
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 15 -- (Id: 5562)
Violated ConstraintsOpen Variables
b3 = B2
u2 = A3
tk3 = tk2
mb3 < > nmb2

b3 -> B2
sk3 -> k!10
tk3 -> k!10
sk2 -> k!10
tk2 -> k!10
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+, {B2,A3,k!10}k!10, {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:5538:*) -> nmb2
ma2(K:5536:*) -> nma3
mb3(K:5553:*) -> 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



ATTACK 16 -- (Id: 5571)
Violated ConstraintsOpen Variables
b3 = B1
u1 = A3
tk3 = tk1
mb3 < > nmb1

b3 -> B1
sk3 -> k!10
tk3 -> k!10
sk2 -> k!10
tk2 -> k!10
sk1 -> k!10
tk1 -> k!10
KnowledgeContext
{nmb2}k!10, {nmb1}k!10, nmb2, {nma3}k!10, nmb1,
{B1,A3,k!10}k!10, nma3, A3, A3+, B2,
B2+, B1, B1+, {B2,A3,k!10}k!10, {B1,A3,k!10}k!10,
I0, .
A3: () [out(nma3,{B1,A3,k!10}k!10).in(nmb2,{nma3}k!10).out({nmb2}k!10)]
B2: () [in(nmb1,{B2,A3,k!10}k!10).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:5536:*) -> nma3
ma2(K:5558:*) -> nmb1
mb3(K:5561:*) -> nmb2

A3 -> I: nma3,{B1,A3,k!10}k!10
I -> B1: nma3,{B1,A3,k!10}k!10
B1 -> I: nmb1,{nma3}k!10
I -> B2: nmb1,{B2,A3,k!10}k!10
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