#base: inv140(init,e1) #inductive: istep140(e1) #successor: s' #action: sdm1(s,p10,q10,r10) #constants: p10 : -> Principal q10 : -> Principal r10 : -> Random #effective: r10 \in ur(s) = false #lemma: inv160(s,nonce(e1)) #case: n = n(p10,q10,r10) (n = n(p10,q10,r10)) = false #case: e1 = enc1(q10,n(p10,q10,r10),p10) (e1 = enc1(q10,n(p10,q10,r10),p10)) = false #case: nonce(e1) = n(p10,intruder,r10) (nonce(e1) = n(p10,intruder,r10)) = false #case: (p10 = intruder) = true (p10 = intruder) = false #case: q10 = intruder (q10 = intruder) = false #action: sdm2(s,p10,r10,m10) #constants: p10 : -> Principal r10 : -> Random m10 : -> Message nw10 : -> Network #effective: nw(s) = m10 , nw10 m1?(m10) = true receiver(m10) = p10 key(cipher1(m10)) = p10 principal(cipher1(m10)) = sender(m10) r10 \in ur(s) = false #lemma: #case: sender(m10) = intruder (sender(m10) = intruder) = false #case: nonce(e1) = n(p10,intruder,r10) (nonce(e1) = n(p10,intruder,r10)) = false #case: nonce(e1) = nonce(cipher1(m10)) (nonce(e1) = nonce(cipher1(m10))) = false #action: sdm3(s,p10,r10,m10,m20) #constants: p10 : -> Principal r10 : -> Random m10 : -> Message m20 : -> Message nw10 : -> Network #effective: nw(s) = m10 , m20 , nw10 m1?(m10) = true m2?(m20) = true creator(m10) = p10 sender(m10) = p10 receiver(m10) = sender(m20) key(cipher1(m10)) = sender(m20) nonce(cipher1(m10)) = n(p10,sender(m20),r10) principal(cipher1(m10)) = p10 receiver(m20) = p10 key(cipher2(m20)) = p10 nonce1(cipher2(m20)) = n(p10,sender(m20),r10) principal(cipher2(m20)) = sender(m20) #lemma: #case: sender(m20) = intruder (sender(m20) = intruder) = false #case: nonce(e1) = nonce2(cipher2(m20)) (nonce(e1) = nonce2(cipher2(m20))) = false #action: fkm11(s,p10,q10,e10) #constants: p10 : -> Principal q10 : -> Principal e10 : -> Cipher1 #effective: e10 \in cenc1(nw(s)) = true #lemma: inv100(s,e10) #case: key(e10) = intruder (key(e10) = intruder) = false #case: e1 = e10 (e1 = e10) = false #action: fkm12(s,p10,q10,n10) #constants: p10 : -> Principal q10 : -> Principal n10 : -> Nonce #effective: n10 \in cnonce(nw(s)) = true #lemma: #case: e1 = enc1(q10,n10,p10) (e1 = enc1(q10,n10,p10)) = false #case: (p10 = intruder) = true (p10 = intruder) = false #case: (q10 = intruder) = true (q10 = intruder) = false #case: nonce(e1) = n10 (nonce(e1) = n10) = false #action: fkm21(s,p10,q10,e20) #constants: p10 : -> Principal q10 : -> Principal e20 : -> Cipher2 #effective: e20 \in cenc2(nw(s)) = true #lemma: inv110(s,e20) #case: key(e20) = intruder (key(e20) = intruder) = false #action: fkm22(s,p10,q10,n10,n20) #constants: p10 : -> Principal q10 : -> Principal n10 : -> Nonce n20 : -> Nonce #effective: n10 \in cnonce(nw(s)) = true n20 \in cnonce(nw(s)) = true #lemma: #case: (q10 = intruder) = true (q10 = intruder) = false #case: nonce(e1) = n10 (nonce(e1) = n10) = false #case: nonce(e1) = n20 (nonce(e1) = n20) = false #action: fkm31(s,p10,q10,e30) #constants: p10 : -> Principal q10 : -> Principal e30 : -> Cipher3 #effective: e30 \in cenc3(nw(s)) = true #lemma: inv120(s,e30) #case: key(e30) = intruder (key(e30) = intruder) = false #action: fkm32(s,p10,q10,n10) #constants: p10 : -> Principal q10 : -> Principal n10 : -> Nonce #effective: n10 \in cnonce(nw(s)) = true #lemma: #case: (q10 = intruder) = true (q10 = intruder) = false #case: nonce(e1) = n10 (nonce(e1) = n10) = false