#base: inv170(init,p,q,q1,r,n)

#inductive: istep170(p,q,q1,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
#lemma: inv190(s,p,q,r,n)
#case: (p = intruder) = true
       (p = intruder) = false
#case: ## m1(p10,p10,q10,enc1(q10,n(p10,q10,r10),p10)) \
       ##  = m1(p,p,q,enc1(q,n(p,q,r),p))
       r = r10 &
       q10 = q &
       p10 = p
       (m1(p10,p10,q10,enc1(q10,n(p10,q10,r10),p10)) \
        = m1(p,p,q,enc1(q,n(p,q,r),p))) = false
#case: ## m2(q1,q,p,enc2(p,n(p,q,r10),n,q)) \in nw(s) = true
       nw(s) = m2(q1,q,p,enc2(p,n(p,q,r10),n,q)) , nw10
       m2(q1,q,p,enc2(p,n(p,q,r10),n,q)) \in nw(s) = 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
#case: (m2(q1,q,p,enc2(p,n(p,q,r),n,q)) \
        = m2(p10,p10,sender(m10), \
          enc2(sender(m10),nonce(cipher1(m10)),n(p10,sender(m10),r10),p10))) = false &
       (m2(q,q,p,enc2(p,n(p,q,r),n,q)) \
        = m2(p10,p10,sender(m10), \
           enc2(sender(m10),nonce(cipher1(m10)),n(p10,sender(m10),r10),p10))) = true
       (m2(q1,q,p,enc2(p,n(p,q,r),n,q)) \
        = m2(p10,p10,sender(m10), \
          enc2(sender(m10),nonce(cipher1(m10)),n(p10,sender(m10),r10),p10))) = false &
       (m2(q,q,p,enc2(p,n(p,q,r),n,q)) \
        = m2(p10,p10,sender(m10), \
           enc2(sender(m10),nonce(cipher1(m10)),n(p10,sender(m10),r10),p10))) = false
       ## (m2(q1,q,p,enc2(p,n(p,q,r),n,q)) \
       ##  = m2(p10,p10,sender(m10), \
       ##    enc2(sender(m10),nonce(cipher1(m10)),n(p10,sender(m10),r10),p10))) = true
       q1 = p10 &
       p = sender(m10) &
       nonce(cipher1(m10)) = n(p,q,r) &
       n = n(p10,sender(m10),r10) &
       q = p10

#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)

#action: fkm11(s,p10,q10,e10)
#constants: p10 : -> Principal
	    q10 : -> Principal
	    e10 : -> Cipher1
#effective: e10 \in cenc1(nw(s)) = true
#case: p = intruder
       (p = intruder) = false

#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
#case: p = intruder
       (p = intruder) = false

#action: fkm21(s,p10,q10,e20)
#constants: p10 : -> Principal
	    q10 : -> Principal
	    e20 : -> Cipher2
#effective: e20 \in cenc2(nw(s)) = true
#lemma: inv220(s,p,q,r,n)
#case: p = intruder
       (p = intruder) = false
#case: m1(p,p,q,enc1(q,n(p,q,r),p)) \in nw(s) = true
       m1(p,p,q,enc1(q,n(p,q,r),p)) \in nw(s) = false
#case: (m2(intruder,p10,q10,e20) = m2(q1,q,p,enc2(p,n(p,q,r),n,q))) = false &
       (m2(intruder,p10,q10,e20) = m2(q,q,p,enc2(p,n(p,q,r),n,q))) = false
       (m2(intruder,p10,q10,e20) = m2(q1,q,p,enc2(p,n(p,q,r),n,q))) = false &
       (m2(intruder,p10,q10,e20) = m2(q,q,p,enc2(p,n(p,q,r),n,q))) = true
       ## (m2(intruder,p10,q10,e20) = m2(q1,q,p,enc2(p,n(p,q,r),n,q))) = true
       q1 = intruder &
       p10 = q &
       q10 = p &
       e20 = enc2(p,n(p,q,r),n,q) &
       enc2(p,n(p,q,r),n,q) \in cenc2(nw(s)) = true 
#case: m2(q,q,p,enc2(p,n(p,q,r),n,q)) \in nw(s) = true
       m2(q,q,p,enc2(p,n(p,q,r),n,q)) \in nw(s) = false
#case: (m2(q,q,p,enc2(p,n(p,q,r),n,q)) = m2(intruder,q,p,enc2(p,n(p,q,r),n,q))) = true
       (m2(q,q,p,enc2(p,n(p,q,r),n,q)) = m2(intruder,q,p,enc2(p,n(p,q,r),n,q))) = 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: inv130(s,n10)
#case: (p = intruder) = true
       (p = intruder) = false
#case: (m2(q1,q,p,enc2(p,n(p,q,r),n,q)) \
        = m2(intruder,p10,q10,enc2(q10,n10,n20,p10))) = false &
       (m2(q,q,p,enc2(p,n(p,q,r),n,q)) \
        = m2(intruder,p10,q10,enc2(q10,n10,n20,p10))) = false
       (m2(q1,q,p,enc2(p,n(p,q,r),n,q)) \
        = m2(intruder,p10,q10,enc2(q10,n10,n20,p10))) = false &
       (m2(q,q,p,enc2(p,n(p,q,r),n,q))\
        = m2(intruder,p10,q10,enc2(q10,n10,n20,p10))) =  true
       ## (m2(q1,q,p,enc2(p,n(p,q,r),n,q)) \
       ##  = m2(intruder,p10,q10,enc2(q10,n10,n20,p10))) = true
       q1 = intruder &
       p10 = q &
       q10 = p &
       n10 = n(p,q,r) &
       n = n20 &
       n(p,q,r) \in cnonce(nw(s)) = true
#case: (q = intruder) = true
       (q = intruder) = false

#action: fkm31(s,p10,q10,e30)
#constants: p10 : -> Principal
	    q10 : -> Principal
	    e30 : -> Cipher3
#effective: e30 \in cenc3(nw(s)) = true

#action: fkm32(s,p10,q10,n10)
#constants: p10 : -> Principal
	    q10 : -> Principal
	    n10 : -> Nonce
#effective: n10 \in cnonce(nw(s)) = true