###keys
newmsg recmsg1 recmsg2 isFake newCen1 newCen2 newCen3 cenc1 cenc2 cenc3 nw m1 m2 m3 nwM1 nwM2 nwM3 rands urand nonces prins
###textDisplay
newmsg::::EXT
newmsg#0 newmsg#1 newmsg#2 newmsg#3#0 newmsg#3#3 newmsg#3#1#0 newmsg#3#1#1 newmsg#3#1#2 newmsg#3#2#0 newmsg#3#2#1 newmsg#3#2#2
###states
(newmsg: m1(p, p, intrdr , enc1(intrdr , n(p, intrdr , r1), p), true) recmsg1: empt recmsg2: empt isFake: false newCen1: empC1 newCen2: empC2 newCen3: empC3 cenc1: emp cenc2: emp cenc3: emp nw: m1(p, p, intrdr , enc1(intrdr , n(p, intrdr , r1), p), true) m1: m1(p, p, intrdr , enc1(intrdr , n(p, intrdr , r1), p), true) m2: empM2 m3: empM3 nwM1: m1(p, p, intrdr , enc1(intrdr , n(p, intrdr , r1), p), true) nwM2: emp nwM3: emp rands: r2 urand: r1 nonces: n(p, intrdr , r1) prins: (p q intrdr )) ||
(newmsg: m1(intrdr , p, q, enc1(q, n(p, intrdr , r1), p), false) recmsg1: empt recmsg2: empt isFake: true newCen1: enc1(q, n(p, intrdr , r1), p) newCen2: empC2 newCen3: empC3 cenc1: enc1(q, n(p, intrdr , r1), p) cenc2: emp cenc3: emp nw: (m1(p, p, intrdr , enc1(intrdr , n(p, intrdr , r1), p), true) m1(intrdr , p, q, enc1(q, n(p, intrdr , r1), p), false)) m1: m1(intrdr , p, q, enc1(q, n(p, intrdr , r1), p), false) m2: empM2 m3: empM3 nwM1: (m1(p, p, intrdr , enc1(intrdr , n(p, intrdr , r1), p), true) m1(intrdr , p, q, enc1(q, n(p, intrdr , r1), p), false)) nwM2: emp nwM3: emp rands: r2 urand: r1 nonces: n(p, intrdr , r1) prins: (p q intrdr )) ||
(newmsg: m2(q, q, p, enc2(p, n(p, intrdr , r1), n(q, p, r2)), true) recmsg1: m1(intrdr , p, q, enc1(q, n(p, intrdr , r1), p), false) recmsg2: empt isFake: false newCen1: empC1 newCen2: enc2(p, n(p, intrdr , r1), n(q, p, r2)) newCen3: empC3 cenc1: enc1(q, n(p, intrdr , r1), p) cenc2: enc2(p, n(p, intrdr , r1), n(q, p, r2)) cenc3: emp nw: (m1(p, p, intrdr , enc1(intrdr , n(p, intrdr , r1), p), true) m1(intrdr , p, q, enc1(q, n(p, intrdr , r1), p), false) m2(q, q, p, enc2(p, n(p, intrdr , r1), n(q, p, r2)), true)) m1: empM1 m2: m2(q, q, p, enc2(p, n(p, intrdr , r1), n(q, p, r2)), true) m3: empM3 nwM1: (m1(p, p, intrdr , enc1(intrdr , n(p, intrdr , r1), p), true) m1(intrdr , p, q, enc1(q, n(p, intrdr , r1), p), false)) nwM2: m2(q, q, p, enc2(p, n(p, intrdr , r1), n(q, p, r2)), true) nwM3: emp rands: emp urand: (r1 r2) nonces: n(p, intrdr , r1) prins: (p q intrdr )) ||
(newmsg: m2(intrdr , intrdr , p, enc2(p, n(p, intrdr , r1), n(q, p, r2)), false) recmsg1: empt recmsg2: empt isFake: true newCen1: empC1 newCen2: enc2(p, n(p, intrdr , r1), n(q, p, r2)) newCen3: empC3 cenc1: enc1(q, n(p, intrdr , r1), p) cenc2: enc2(p, n(p, intrdr , r1), n(q, p, r2)) cenc3: emp nw: (m1(p, p, intrdr , enc1(intrdr , n(p, intrdr , r1), p), true) m1(intrdr , p, q, enc1(q, n(p, intrdr , r1), p), false) m2(q, q, p, enc2(p, n(p, intrdr , r1), n(q, p, r2)), true) m2(intrdr , intrdr , p, enc2(p, n(p, intrdr , r1), n(q, p, r2)), false)) m1: empM1 m2: m2(intrdr , intrdr , p, enc2(p, n(p, intrdr , r1), n(q, p, r2)), false) m3: empM3 nwM1: (m1(p, p, intrdr , enc1(intrdr , n(p, intrdr , r1), p), true) m1(intrdr , p, q, enc1(q, n(p, intrdr , r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, intrdr , r1), n(q, p, r2)), true) m2(intrdr , intrdr , p, enc2(p, n(p, intrdr , r1), n(q, p, r2)), false)) nwM3: emp rands: emp urand: (r1 r2) nonces: n(p, intrdr , r1) prins: (p q intrdr )) ||
(newmsg: m3(p, p, intrdr , enc3(intrdr , n(q, p, r2)), true) recmsg1: m2(intrdr , intrdr , p, enc2(p, n(p, intrdr , r1), n(q, p, r2)), false) recmsg2: empt isFake: false newCen1: empC1 newCen2: empC2 newCen3: empC3 cenc1: enc1(q, n(p, intrdr , r1), p) cenc2: enc2(p, n(p, intrdr , r1), n(q, p, r2)) cenc3: emp nw: (m1(p, p, intrdr , enc1(intrdr , n(p, intrdr , r1), p), true) m1(intrdr , p, q, enc1(q, n(p, intrdr , r1), p), false) m2(q, q, p, enc2(p, n(p, intrdr , r1), n(q, p, r2)), true) m2(intrdr , intrdr , p, enc2(p, n(p, intrdr , r1), n(q, p, r2)), false) m3(p, p, intrdr , enc3(intrdr , n(q, p, r2)), true)) m1: empM1 m2: empM2 m3: m3(p, p, intrdr , enc3(intrdr , n(q, p, r2)), true) nwM1: (m1(p, p, intrdr , enc1(intrdr , n(p, intrdr , r1), p), true) m1(intrdr , p, q, enc1(q, n(p, intrdr , r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, intrdr , r1), n(q, p, r2)), true) m2(intrdr , intrdr , p, enc2(p, n(p, intrdr , r1), n(q, p, r2)), false)) nwM3: m3(p, p, intrdr , enc3(intrdr , n(q, p, r2)), true) rands: emp urand: (r1 r2) nonces: (n(p, intrdr , r1) n(q, p, r2)) prins: (p q intrdr )) ||
(newmsg: m3(intrdr, p, q, enc3(q, n(q, p, r2)), false) recmsg1: empt recmsg2: empt isFake: true newCen1: empC1 newCen2: empC2 newCen3: enc3(q, n(q, p, r2)) cenc1: enc1(q, n(p, intrdr, r1), p) cenc2: enc2(p, n(p, intrdr, r1), n(q, p, r2)) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, intrdr, enc1(intrdr, n(p, intrdr, r1), p), true) m1(intrdr, p, q, enc1(q, n(p, intrdr, r1), p), false) m2(q, q, p, enc2(p, n(p, intrdr, r1), n(q, p, r2)), true) m2(intrdr, intrdr, p, enc2(p, n(p, intrdr, r1), n(q, p, r2)), false) m3(p, p, intrdr, enc3(intrdr, n(q, p, r2)), true) m3(intrdr, p, q, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: empM2 m3: m3(intrdr, p, q, enc3(q, n(q, p, r2)), false) nwM1: (m1(p, p, intrdr, enc1(intrdr, n(p, intrdr, r1), p), true) m1(intrdr, p, q, enc1(q, n(p, intrdr, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, intrdr, r1), n(q, p, r2)), true) m2(intrdr, intrdr, p, enc2(p, n(p, intrdr, r1), n(q, p, r2)), false)) nwM3: (m3(p, p, intrdr, enc3(intrdr, n(q, p, r2)), true) m3(intrdr, p, q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: (n(p, intrdr, r1) n(q, p, r2)) prins: (p q intrdr))