ATTACK 1 -- (Id: 67) | |
Violated Constraints | Open Variables |
K :> nb1 z1 < > I0 z1 = A2 x2 < > B1 | x2 -> I0 |
Knowledge | Context |
nb1, {na2,nb1}A2+, na2, A2, A2+, B1, B1+, I0, I0+, I0-, . | A2: () [out({A2,na2}I0+).in({na2,nb1}A2-).out({nb1}I0+)] B1: () [in({A2,na2}B1-).out({na2,nb1}A2+).in({nb1}B1-)] |
Model | Intruder process |
u1(K:56:*) -> na2 z1(K:56:*) -> A2 x2(K:5:nr) -> I0 | A2 -> I: {A2,na2}I0+ I -> B1: {A2,na2}B1+ B1 -> I: {na2,nb1}A2+ I -> A2: {na2,nb1}A2+ A2 -> I: {nb1}I0+ I -> B1: {nb1}B1+ |
ATTACK 2 -- (Id: 97) | |
Violated Constraints | Open Variables |
K :> nb2 z2 < > I0 T | |
Knowledge | Context |
nb2, nb1, {I0,nb2}B1+, B2, B2+, B1, B1+, I0, I0+, I0-, . | B2: () [in({B1,I0}B2-).out({I0,nb2}B1+).in({nb2}B2-)] B1: () [in({I0,nb2}B1-).out({nb2,nb1}I0+).in({nb1}B1-)] |
Model | Intruder process |
u2(K:10:nr) -> I0 z2(K:10:*) -> B1 | I -> B2: {B1,I0}B2+ B2 -> I: {I0,nb2}B1+ I -> B1: {I0,nb2}B1+ B1 -> I: {nb2,nb1}I0+ I -> B1: {nb1}B1+ I -> B2: {nb2}B2+ |
ATTACK 3 -- (Id: 100) | |
Violated Constraints | Open Variables |
K :> nb2 z2 < > I0 T | |
Knowledge | Context |
nb2, nb1, {I0,nb2}B1+, B2, B2+, B1, B1+, I0, I0+, I0-, . | B2: () [in({B1,I0}B2-).out({I0,nb2}B1+).in({nb2}B2-)] B1: () [in({I0,nb2}B1-).out({nb2,nb1}I0+).in({nb1}B1-)] |
Model | Intruder process |
u2(K:10:nr) -> I0 z2(K:10:*) -> B1 | I -> B2: {B1,I0}B2+ B2 -> I: {I0,nb2}B1+ I -> B1: {I0,nb2}B1+ B1 -> I: {nb2,nb1}I0+ I -> B2: {nb2}B2+ I -> B1: {nb1}B1+ |
ATTACK 4 -- (Id: 131) | |
Violated Constraints | Open Variables |
K :> nb1 z1 < > I0 T | |
Knowledge | Context |
nb1, nb2, {I0,nb1}B2+, B2, B2+, B1, B1+, I0, I0+, I0-, . | B2: () [in({I0,nb1}B2-).out({nb1,nb2}I0+).in({nb2}B2-)] B1: () [in({B2,I0}B1-).out({I0,nb1}B2+).in({nb1}B1-)] |
Model | Intruder process |
u1(K:10:nr) -> I0 z1(K:10:*) -> B2 | I -> B1: {B2,I0}B1+ B1 -> I: {I0,nb1}B2+ I -> B2: {I0,nb1}B2+ B2 -> I: {nb1,nb2}I0+ I -> B2: {nb2}B2+ I -> B1: {nb1}B1+ |
ATTACK 5 -- (Id: 134) | |
Violated Constraints | Open Variables |
K :> nb1 z1 < > I0 T | |
Knowledge | Context |
nb1, nb2, {I0,nb1}B2+, B2, B2+, B1, B1+, I0, I0+, I0-, . | B2: () [in({I0,nb1}B2-).out({nb1,nb2}I0+).in({nb2}B2-)] B1: () [in({B2,I0}B1-).out({I0,nb1}B2+).in({nb1}B1-)] |
Model | Intruder process |
u1(K:10:nr) -> I0 z1(K:10:*) -> B2 | I -> B1: {B2,I0}B1+ B1 -> I: {I0,nb1}B2+ I -> B2: {I0,nb1}B2+ B2 -> I: {nb1,nb2}I0+ I -> B1: {nb1}B1+ I -> B2: {nb2}B2+ |