ATTACK 1 -- (Id: 130) | |
Violated Constraints | Open Variables |
K :> nb2 z2 < > I0 T | |
Knowledge | Context |
nb1, nb2, {nb2,I0}B1+, B2, B2+, B1, B1+, I0, I0+, I0-, . | B2: () [in({I0,B1}B2-).out({nb2,I0}B1+).in({nb2}B2-)] B1: () [in({nb2,I0}B1-).out({nb1,nb2}I0+).in({nb1}B1-)] |
Model | Intruder process |
u2(K:10:nr) -> I0 z2(K:10:*) -> B1 | I -> B2: {I0,B1}B2+ B2 -> I: {nb2,I0}B1+ I -> B1: {nb2,I0}B1+ B1 -> I: {nb1,nb2}I0+ I -> B1: {nb1}B1+ I -> B2: {nb2}B2+ |
ATTACK 2 -- (Id: 133) | |
Violated Constraints | Open Variables |
K :> nb2 z2 < > I0 T | |
Knowledge | Context |
nb1, nb2, {nb2,I0}B1+, B2, B2+, B1, B1+, I0, I0+, I0-, . | B2: () [in({I0,B1}B2-).out({nb2,I0}B1+).in({nb2}B2-)] B1: () [in({nb2,I0}B1-).out({nb1,nb2}I0+).in({nb1}B1-)] |
Model | Intruder process |
u2(K:10:nr) -> I0 z2(K:10:*) -> B1 | I -> B2: {I0,B1}B2+ B2 -> I: {nb2,I0}B1+ I -> B1: {nb2,I0}B1+ B1 -> I: {nb1,nb2}I0+ I -> B2: {nb2}B2+ I -> B1: {nb1}B1+ |
ATTACK 3 -- (Id: 164) | |
Violated Constraints | Open Variables |
K :> nb1 z1 < > I0 T | |
Knowledge | Context |
nb2, nb1, {nb1,I0}B2+, B2, B2+, B1, B1+, I0, I0+, I0-, . | B2: () [in({nb1,I0}B2-).out({nb2,nb1}I0+).in({nb2}B2-)] B1: () [in({I0,B2}B1-).out({nb1,I0}B2+).in({nb1}B1-)] |
Model | Intruder process |
u1(K:10:nr) -> I0 z1(K:10:*) -> B2 | I -> B1: {I0,B2}B1+ B1 -> I: {nb1,I0}B2+ I -> B2: {nb1,I0}B2+ B2 -> I: {nb2,nb1}I0+ I -> B2: {nb2}B2+ I -> B1: {nb1}B1+ |
ATTACK 4 -- (Id: 167) | |
Violated Constraints | Open Variables |
K :> nb1 z1 < > I0 T | |
Knowledge | Context |
nb2, nb1, {nb1,I0}B2+, B2, B2+, B1, B1+, I0, I0+, I0-, . | B2: () [in({nb1,I0}B2-).out({nb2,nb1}I0+).in({nb2}B2-)] B1: () [in({I0,B2}B1-).out({nb1,I0}B2+).in({nb1}B1-)] |
Model | Intruder process |
u1(K:10:nr) -> I0 z1(K:10:*) -> B2 | I -> B1: {I0,B2}B1+ B1 -> I: {nb1,I0}B2+ I -> B2: {nb1,I0}B2+ B2 -> I: {nb2,nb1}I0+ I -> B1: {nb1}B1+ I -> B2: {nb2}B2+ |