ATTACK 1 -- (Id: 2364) | |
Violated Constraints | Open 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 |
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+, {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: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 Constraints | Open 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 |
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+, {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: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 Constraints | Open 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 |
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+, {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: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 Constraints | Open 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 |
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+, {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: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 Constraints | Open 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 |
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+, {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: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 Constraints | Open 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 |
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+, {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: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 |