ATTACK 1 -- (Id: 2918) | |
Violated Constraints | Open 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 |
Knowledge | Context |
{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)] |
Model | Intruder 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 Constraints | Open 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 |
Knowledge | Context |
{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)] |
Model | Intruder 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 Constraints | Open 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 |
Knowledge | Context |
{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)] |
Model | Intruder 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 Constraints | Open 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 |
Knowledge | Context |
{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)] |
Model | Intruder 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 Constraints | Open 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 |
Knowledge | Context |
{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)] |
Model | Intruder 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 Constraints | Open 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 |
Knowledge | Context |
{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)] |
Model | Intruder 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 Constraints | Open 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 |
Knowledge | Context |
{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)] |
Model | Intruder 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 Constraints | Open 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 |
Knowledge | Context |
{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)] |
Model | Intruder 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 Constraints | Open 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 |
Knowledge | Context |
{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)] |
Model | Intruder 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 Constraints | Open 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 |
Knowledge | Context |
{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)] |
Model | Intruder 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 Constraints | Open 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 |
Knowledge | Context |
{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)] |
Model | Intruder 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 Constraints | Open 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 |
Knowledge | Context |
{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)] |
Model | Intruder 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 Constraints | Open 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 |
Knowledge | Context |
{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)] |
Model | Intruder 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 Constraints | Open 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 |
Knowledge | Context |
{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)] |
Model | Intruder 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 Constraints | Open 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 |
Knowledge | Context |
{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)] |
Model | Intruder 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 Constraints | Open 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 |
Knowledge | Context |
{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)] |
Model | Intruder 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 |