#base: inv180(init,p,q,p1,r,n) #inductive: istep180(p,q,p1,r,n) #successor: s' #action: sdm1(s,p10,q10,r10) #constants: p10 : -> Principal q10 : -> Principal r10 : -> Random nw10 : -> Network #effective: r10 \in ur(s) = false #action: sdm2(s,p10,r10,m10) #constants: p10 : -> Principal r10 : -> Random m10 : -> Message nw10 : -> Network nw20 : -> 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: inv240(s,p,q,r) #case: q = intruder (q = intruder) = false #case: (m2(p10,p10,sender(m10), \ enc2(sender(m10),nonce(cipher1(m10)),n(p10,sender(m10),r10),p10)) \ = m2(q,q,p,enc2(p,n,n(q,p,r),q))) = false ## (m2(p10,p10,sender(m10), \ ## enc2(sender(m10),nonce(cipher1(m10)),n(p10,sender(m10),r10),p10)) \ ## = m2(q,q,p,enc2(p,n,n(q,p,r),q))) = false p10 = q & sender(m10) = p & nonce(cipher1(m10)) = n & r = r10 & p10 = q #case: m3(p1,p,q,enc3(q,n(q,p,r10))) \in m10,nw10 = false ## m3(p1,p,q,enc3(q,n(q,p,r10))) \in m10,nw10 = true nw10 = m3(p1,p,q,enc3(q,n(q,p,r10))) , nw20 #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) #case: (m3(p1,p,q,enc3(q,n(q,p,r))) \ = m3(p10,p10,sender(m20),enc3(sender(m20),nonce2(cipher2(m20))))) = false & (m3(p,p,q,enc3(q,n(q,p,r))) \ = m3(p10,p10,sender(m20),enc3(sender(m20),nonce2(cipher2(m20))))) = false (m3(p1,p,q,enc3(q,n(q,p,r))) \ = m3(p10,p10,sender(m20),enc3(sender(m20),nonce2(cipher2(m20))))) = false & (m3(p,p,q,enc3(q,n(q,p,r))) \ = m3(p10,p10,sender(m20),enc3(sender(m20),nonce2(cipher2(m20))))) = true ## (m3(p1,p,q,enc3(q,n(q,p,r))) \ ## = m3(p10,p10,sender(m20),enc3(sender(m20),nonce2(cipher2(m20))))) = true p1 = p10 & p = p10 & sender(m20) = q & nonce2(cipher2(m20)) = n(q,p,r) #action: fkm11(s,p10,q10,e10) #constants: p10 : -> Principal q10 : -> Principal e10 : -> Cipher1 #effective: e10 \in cenc1(nw(s)) = true #action: fkm12(s,p10,q10,n10) #constants: p10 : -> Principal q10 : -> Principal n10 : -> Nonce #effective: n10 \in cnonce(nw(s)) = true #case: e1 = enc1(q10,n10,p10) (e1 = enc1(q10,n10,p10)) = false #action: fkm21(s,p10,q10,e20) #constants: p10 : -> Principal q10 : -> Principal e20 : -> Cipher2 #effective: e20 \in cenc2(nw(s)) = true #lemma: #case: (m2(q,q,p,enc2(p,n,n(q,p,r),q)) = m2(intruder,p10,q10,e20)) = false ## (m2(q,q,p,enc2(p,n,n(q,p,r),q)) = m2(intruder,p10,q10,e20)) = true q = intruder & p10 = q & q10 = p & e20 = enc2(p,n,n(intruder,p,r),intruder) #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: (m2(q,q,p,enc2(p,n,n(q,p,r),q)) = m2(intruder,p10,q10,enc2(q10,n10,n20,p10))) \ = false ## (m2(q,q,p,enc2(p,n,n(q,p,r),q)) = m2(intruder,p10,q10,enc2(q10,n10,n20,p10))) \ ## = true q = intruder & p10 = q & q10 = p & n = n10 & n(q,p,r) = n20 #action: fkm31(s,p10,q10,e30) #constants: p10 : -> Principal q10 : -> Principal e30 : -> Cipher3 #effective: e30 \in cenc3(nw(s)) = true #lemma: inv230(s,p,q,r) #case: (m3(p1,p,q,enc3(q,n(q,p,r))) = m3(intruder,p10,q10,e30)) = false & (m3(p,p,q,enc3(q,n(q,p,r))) = m3(intruder,p10,q10,e30)) = false (m3(p1,p,q,enc3(q,n(q,p,r))) = m3(intruder,p10,q10,e30)) = false & (m3(p,p,q,enc3(q,n(q,p,r))) = m3(intruder,p10,q10,e30)) = true ## (m3(p1,p,q,enc3(q,n(q,p,r))) = m3(intruder,p10,q10,e30)) = true p1 = intruder & p10 = p & q10 = q & e30 = enc3(q,n(q,p,r)) & enc3(q,n(q,p,r)) \in cenc3(nw(s)) = true #case: (p = intruder) = true (p = intruder) = false #case: (p = intruder) = true (p = intruder) = false #case: m3(p,p,q,enc3(q,n(q,p,r))) \in nw(s) = true m3(p,p,q,enc3(q,n(q,p,r))) \in nw(s) = false #action: fkm32(s,p10,q10,n10) #constants: p10 : -> Principal q10 : -> Principal n10 : -> Nonce #effective: n10 \in cnonce(nw(s)) = true #lemma: inv130(s,n(q,p,r)) #case: (m3(p1,p,q,enc3(q,n(q,p,r))) = m3(intruder,p10,q10,enc3(q10,n10))) = false & (m3(p,p,q,enc3(q,n(q,p,r))) = m3(intruder,p10,q10,enc3(q10,n10))) = false (m3(p1,p,q,enc3(q,n(q,p,r))) = m3(intruder,p10,q10,enc3(q10,n10))) = false & (m3(p,p,q,enc3(q,n(q,p,r))) = m3(intruder,p10,q10,enc3(q10,n10))) = true ## (m3(p1,p,q,enc3(q,n(q,p,r))) = m3(intruder,p10,q10,enc3(q10,n10))) = true p1 = intruder & p10 = p & q10 = q & n10 = n(q,p,r) & n(q,p,r) \in cnonce(nw(s)) = true #case: (q = intruder) = true (q = intruder) = false #case: (p = intruder) = true (p = intruder) = false