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