###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, q, enc1(q, n(p, q, r1), p), true) recmsg1: empt recmsg2: empt isFake: false newCen1: enc1(q, n(p, q, r1), p) newCen2: empC2 newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: emp cenc3: emp nw: m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1: m1(p, p, q, enc1(q, n(p, q, r1), p), true) m2: empM2 m3: empM3 nwM1: m1(p, p, q, enc1(q, n(p, q, r1), p), true) nwM2: emp nwM3: emp rands: r2 urand: r1 nonces: emp prins: (p q intrdr )) ||
(newmsg: m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) recmsg1: empt recmsg2: empt isFake: true newCen1: enc1(q, n(p, q, r1), p) newCen2: empC2 newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: emp cenc3: emp nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false)) m1: m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m2: empM2 m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false)) nwM2: emp nwM3: emp rands: r2 urand: r1 nonces: emp prins: (p q intrdr )) ||
(newmsg: m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) recmsg1: m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) recmsg2: empt isFake: false newCen1: empC1 newCen2: enc2(p, n(p, q, r1), n(q, p, r2), q) newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: emp nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true)) m1: empM1 m2: m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false)) nwM2: m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) nwM3: emp rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) recmsg1: empt recmsg2: empt isFake: true newCen1: enc1(q, n(p, q, r1), p) newCen2: empC2 newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: emp nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true)) m1: m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m2: empM2 m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false)) nwM2: m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) nwM3: emp rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) recmsg1: empt recmsg2: empt isFake: true newCen1: enc1(q, n(p, q, r1), p) newCen2: empC2 newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: emp nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true)) m1: m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m2: empM2 m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false)) nwM2: m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) nwM3: emp rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) || (newmsg: m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) recmsg1: empt recmsg2: empt isFake: true newCen1: enc1(q, n(p, q, r1), p) newCen2: empC2 newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: emp nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true)) m1: m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m2: empM2 m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false)) nwM2: m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) nwM3: emp rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) || (newmsg: m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) recmsg1: empt recmsg2: empt isFake: true newCen1: empC1 newCen2: enc2(p, n(p, q, r1), n(q, p, r2), q) newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: emp nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) m1: empM1 m2: m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: emp rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) recmsg1: empt recmsg2: empt isFake: true newCen1: empC1 newCen2: enc2(p, n(p, q, r1), n(q, p, r2), q) newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: emp nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) m1: empM1 m2: m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: emp rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) recmsg1: empt recmsg2: empt isFake: true newCen1: empC1 newCen2: enc2(p, n(p, q, r1), n(q, p, r2), q) newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: emp nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) m1: empM1 m2: m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: emp rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) recmsg1: empt recmsg2: empt isFake: true newCen1: empC1 newCen2: enc2(p, n(p, q, r1), n(q, p, r2), q) newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: emp nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) m1: empM1 m2: m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: emp rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) recmsg1: empt recmsg2: empt isFake: true newCen1: empC1 newCen2: enc2(p, n(p, q, r1), n(q, p, r2), q) newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: emp nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) m1: empM1 m2: m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: emp rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) recmsg1: empt recmsg2: empt isFake: true newCen1: enc1(q, n(p, q, r1), p) newCen2: empC2 newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: emp nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) m1: m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m2: empM2 m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: emp rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) recmsg1: empt recmsg2: empt isFake: true newCen1: enc1(q, n(p, q, r1), p) newCen2: empC2 newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: emp nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) m1: m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2: empM2 m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: emp rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) recmsg1: empt recmsg2: empt isFake: true newCen1: enc1(q, n(p, q, r1), p) newCen2: empC2 newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: emp nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) m1: m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m2: empM2 m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: emp rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) recmsg1: empt recmsg2: empt isFake: true newCen1: empC1 newCen2: enc2(p, n(p, q, r1), n(q, p, r2), q) newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: emp nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) m1: empM1 m2: m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: emp rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m3(p, p, q, enc3(q, n(q, p, r2)), true) recmsg1: m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) recmsg2: empt isFake: false newCen1: empC1 newCen2: empC2 newCen3: enc3(q, n(q, p, r2)) cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true)) m1: empM1 m2: empM2 m3: m3(p, p, q, enc3(q, n(q, p, r2)), true) nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: m3(p, p, q, enc3(q, n(q, p, r2)), true) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) recmsg1: empt recmsg2: empt isFake: true newCen1: enc1(q, n(p, q, r1), p) newCen2: empC2 newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true)) m1: m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m2: empM2 m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: m3(p, p, q, enc3(q, n(q, p, r2)), true) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m3(p, p, q, enc3(q, n(q, p, r2)), true) recmsg1: m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) recmsg2: empt isFake: false newCen1: empC1 newCen2: empC2 newCen3: enc3(q, n(q, p, r2)) cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true)) m1: empM1 m2: empM2 m3: m3(p, p, q, enc3(q, n(q, p, r2)), true) nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: m3(p, p, q, enc3(q, n(q, p, r2)), true) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m3(intrdr , intrdr , p, 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, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: empM2 m3: m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) recmsg1: empt recmsg2: empt isFake: true newCen1: empC1 newCen2: enc2(p, n(p, q, r1), n(q, p, r2), q) newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) recmsg1: empt recmsg2: empt isFake: true newCen1: empC1 newCen2: enc2(p, n(p, q, r1), n(q, p, r2), q) newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m3(intrdr , intrdr , 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, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: empM2 m3: m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false) nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m3(p, p, q, enc3(q, n(q, p, r2)), true) recmsg1: m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) recmsg2: empt isFake: false newCen1: empC1 newCen2: empC2 newCen3: enc3(q, n(q, p, r2)) cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: empM2 m3: m3(p, p, q, enc3(q, n(q, p, r2)), true) nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) recmsg1: empt recmsg2: empt isFake: true newCen1: empC1 newCen2: enc2(p, n(p, q, r1), n(q, p, r2), q) newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) recmsg1: empt recmsg2: empt isFake: true newCen1: empC1 newCen2: enc2(p, n(p, q, r1), n(q, p, r2), q) newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m3(intrdr , intrdr , p, 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, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: empM2 m3: m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m3(intrdr , intrdr , 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, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: empM2 m3: m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false) nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m3(p, p, q, enc3(q, n(q, p, r2)), true) recmsg1: m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) recmsg2: empt isFake: false newCen1: empC1 newCen2: empC2 newCen3: enc3(q, n(q, p, r2)) cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: empM2 m3: m3(p, p, q, enc3(q, n(q, p, r2)), true) nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) recmsg1: empt recmsg2: empt isFake: true newCen1: enc1(q, n(p, q, r1), p) newCen2: empC2 newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m2: empM2 m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) recmsg1: empt recmsg2: empt isFake: true newCen1: empC1 newCen2: enc2(p, n(p, q, r1), n(q, p, r2), q) newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) recmsg1: empt recmsg2: empt isFake: true newCen1: enc1(q, n(p, q, r1), p) newCen2: empC2 newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m2: empM2 m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m3(intrdr , intrdr , p, 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, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: empM2 m3: m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) recmsg1: empt recmsg2: empt isFake: true newCen1: empC1 newCen2: enc2(p, n(p, q, r1), n(q, p, r2), q) newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) recmsg1: empt recmsg2: empt isFake: true newCen1: empC1 newCen2: enc2(p, n(p, q, r1), n(q, p, r2), q) newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) recmsg1: empt recmsg2: empt isFake: true newCen1: empC1 newCen2: enc2(p, n(p, q, r1), n(q, p, r2), q) newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp 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, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , 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, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) recmsg1: empt recmsg2: empt isFake: true newCen1: empC1 newCen2: enc2(p, n(p, q, r1), n(q, p, r2), q) newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) recmsg1: empt recmsg2: empt isFake: true newCen1: enc1(q, n(p, q, r1), p) newCen2: empC2 newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m2: empM2 m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m3(intrdr , intrdr , p, 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, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: empM2 m3: m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) recmsg1: empt recmsg2: empt isFake: true newCen1: empC1 newCen2: enc2(p, n(p, q, r1), n(q, p, r2), q) newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) recmsg1: empt recmsg2: empt isFake: true newCen1: enc1(q, n(p, q, r1), p) newCen2: empC2 newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2: empM2 m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) recmsg1: empt recmsg2: empt isFake: true newCen1: enc1(q, n(p, q, r1), p) newCen2: empC2 newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m2: empM2 m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m3(intrdr , intrdr , p, 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, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: empM2 m3: m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) recmsg1: empt recmsg2: empt isFake: true newCen1: enc1(q, n(p, q, r1), p) newCen2: empC2 newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2: empM2 m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m3(intrdr , intrdr , p, 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, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: empM2 m3: m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m3(intrdr , intrdr , 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, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: empM2 m3: m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false) nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) recmsg1: empt recmsg2: empt isFake: true newCen1: enc1(q, n(p, q, r1), p) newCen2: empC2 newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2: empM2 m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m3(p, p, q, enc3(q, n(q, p, r2)), true) recmsg1: m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) recmsg2: empt isFake: false newCen1: empC1 newCen2: empC2 newCen3: enc3(q, n(q, p, r2)) cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: empM2 m3: m3(p, p, q, enc3(q, n(q, p, r2)), true) nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) recmsg1: empt recmsg2: empt isFake: true newCen1: empC1 newCen2: enc2(p, n(p, q, r1), n(q, p, r2), q) newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) recmsg1: empt recmsg2: empt isFake: true newCen1: enc1(q, n(p, q, r1), p) newCen2: empC2 newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m2: empM2 m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) recmsg1: empt recmsg2: empt isFake: true newCen1: enc1(q, n(p, q, r1), p) newCen2: empC2 newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m2: empM2 m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m3(p, p, q, enc3(q, n(q, p, r2)), true) recmsg1: m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) recmsg2: empt isFake: false newCen1: empC1 newCen2: empC2 newCen3: enc3(q, n(q, p, r2)) cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: empM2 m3: m3(p, p, q, enc3(q, n(q, p, r2)), true) nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) recmsg1: empt recmsg2: empt isFake: true newCen1: empC1 newCen2: enc2(p, n(p, q, r1), n(q, p, r2), q) newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m3(intrdr , q, p, 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, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: empM2 m3: m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m3(intrdr , intrdr , p, 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, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: empM2 m3: m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) recmsg1: empt recmsg2: empt isFake: true newCen1: enc1(q, n(p, q, r1), p) newCen2: empC2 newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m2: empM2 m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp 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, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , 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, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m3(intrdr , intrdr , p, 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, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: empM2 m3: m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m3(p, p, q, enc3(q, n(q, p, r2)), true) recmsg1: m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) recmsg2: empt isFake: false newCen1: empC1 newCen2: empC2 newCen3: enc3(q, n(q, p, r2)) cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: empM2 m3: m3(p, p, q, enc3(q, n(q, p, r2)), true) nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m3(p, p, q, enc3(q, n(q, p, r2)), true) recmsg1: m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) recmsg2: empt isFake: false newCen1: empC1 newCen2: empC2 newCen3: enc3(q, n(q, p, r2)) cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: empM2 m3: m3(p, p, q, enc3(q, n(q, p, r2)), true) nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) recmsg1: empt recmsg2: empt isFake: true newCen1: enc1(q, n(p, q, r1), p) newCen2: empC2 newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m2: empM2 m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m3(p, p, q, enc3(q, n(q, p, r2)), true) recmsg1: m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) recmsg2: empt isFake: false newCen1: empC1 newCen2: empC2 newCen3: enc3(q, n(q, p, r2)) cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: empM2 m3: m3(p, p, q, enc3(q, n(q, p, r2)), true) nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) recmsg1: empt recmsg2: empt isFake: true newCen1: enc1(q, n(p, q, r1), p) newCen2: empC2 newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m2: empM2 m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m3(p, p, q, enc3(q, n(q, p, r2)), true) recmsg1: m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) recmsg2: empt isFake: false newCen1: empC1 newCen2: empC2 newCen3: enc3(q, n(q, p, r2)) cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: empM2 m3: m3(p, p, q, enc3(q, n(q, p, r2)), true) nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m3(intrdr , intrdr , p, 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, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: empM2 m3: m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) recmsg1: empt recmsg2: empt isFake: true newCen1: enc1(q, n(p, q, r1), p) newCen2: empC2 newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m2: empM2 m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) recmsg1: empt recmsg2: empt isFake: true newCen1: enc1(q, n(p, q, r1), p) newCen2: empC2 newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m2: empM2 m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m3(intrdr , intrdr , p, 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, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: empM2 m3: m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) recmsg1: empt recmsg2: empt isFake: true newCen1: empC1 newCen2: enc2(p, n(p, q, r1), n(q, p, r2), q) newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) recmsg1: empt recmsg2: empt isFake: true newCen1: empC1 newCen2: enc2(p, n(p, q, r1), n(q, p, r2), q) newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) recmsg1: empt recmsg2: empt isFake: true newCen1: empC1 newCen2: enc2(p, n(p, q, r1), n(q, p, r2), q) newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) recmsg1: empt recmsg2: empt isFake: true newCen1: enc1(q, n(p, q, r1), p) newCen2: empC2 newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m2: empM2 m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) recmsg1: empt recmsg2: empt isFake: true newCen1: enc1(q, n(p, q, r1), p) newCen2: empC2 newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m2: empM2 m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) recmsg1: empt recmsg2: empt isFake: true newCen1: enc1(q, n(p, q, r1), p) newCen2: empC2 newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m2: empM2 m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) recmsg1: empt recmsg2: empt isFake: true newCen1: enc1(q, n(p, q, r1), p) newCen2: empC2 newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m2: empM2 m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) recmsg1: empt recmsg2: empt isFake: true newCen1: enc1(q, n(p, q, r1), p) newCen2: empC2 newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m2: empM2 m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) recmsg1: empt recmsg2: empt isFake: true newCen1: enc1(q, n(p, q, r1), p) newCen2: empC2 newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2: empM2 m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) recmsg1: empt recmsg2: empt isFake: true newCen1: empC1 newCen2: enc2(p, n(p, q, r1), n(q, p, r2), q) newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m3(p, p, q, enc3(q, n(q, p, r2)), true) recmsg1: m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) recmsg2: empt isFake: false newCen1: empC1 newCen2: empC2 newCen3: enc3(q, n(q, p, r2)) cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: empM2 m3: m3(p, p, q, enc3(q, n(q, p, r2)), true) nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) recmsg1: empt recmsg2: empt isFake: true newCen1: empC1 newCen2: enc2(p, n(p, q, r1), n(q, p, r2), q) newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) recmsg1: empt recmsg2: empt isFake: true newCen1: enc1(q, n(p, q, r1), p) newCen2: empC2 newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2: empM2 m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m3(intrdr , intrdr , p, 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, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: empM2 m3: m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) recmsg1: empt recmsg2: empt isFake: true newCen1: enc1(q, n(p, q, r1), p) newCen2: empC2 newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m2: empM2 m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m3(intrdr , intrdr , 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, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: empM2 m3: m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false) nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) recmsg1: empt recmsg2: empt isFake: true newCen1: empC1 newCen2: enc2(p, n(p, q, r1), n(q, p, r2), q) newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m3(p, p, q, enc3(q, n(q, p, r2)), true) recmsg1: m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) recmsg2: empt isFake: false newCen1: empC1 newCen2: empC2 newCen3: enc3(q, n(q, p, r2)) cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: empM2 m3: m3(p, p, q, enc3(q, n(q, p, r2)), true) nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) recmsg1: empt recmsg2: empt isFake: true newCen1: enc1(q, n(p, q, r1), p) newCen2: empC2 newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m2: empM2 m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) recmsg1: empt recmsg2: empt isFake: true newCen1: empC1 newCen2: enc2(p, n(p, q, r1), n(q, p, r2), q) newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: empM1 m2: m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr )) ||
(newmsg: m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) recmsg1: empt recmsg2: empt isFake: true newCen1: enc1(q, n(p, q, r1), p) newCen2: empC2 newCen3: empC3 cenc1: enc1(q, n(p, q, r1), p) cenc2: enc2(p, n(p, q, r1), n(q, p, r2), q) cenc3: enc3(q, n(q, p, r2)) nw: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false) m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) m1: m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m2: empM2 m3: empM3 nwM1: (m1(p, p, q, enc1(q, n(p, q, r1), p), true) m1(intrdr , p, q, enc1(q, n(p, q, r1), p), false) m1(intrdr , q, p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , p, enc1(q, n(p, q, r1), p), false) m1(intrdr , intrdr , q, enc1(q, n(p, q, r1), p), false)) nwM2: (m2(q, q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), true) m2(intrdr , p, q, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , q, p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , p, enc2(p, n(p, q, r1), n(q, p, r2), q), false) m2(intrdr , intrdr , q, enc2(p, n(p, q, r1), n(q, p, r2), q), false)) nwM3: (m3(p, p, q, enc3(q, n(q, p, r2)), true) m3(intrdr , p, q, enc3(q, n(q, p, r2)), false) m3(intrdr , q, p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , p, enc3(q, n(q, p, r2)), false) m3(intrdr , intrdr , q, enc3(q, n(q, p, r2)), false)) rands: emp urand: (r1 r2) nonces: emp prins: (p q intrdr ))