#base: inv220(init,p,q,r,n)

#inductive: istep220(p,q,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
       (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))) = false
       ## (m1(p10,p10,q10,enc1(q10,n(p10,q10,r10),p10)) \
       ##  = m1(p,p,q,enc1(q,n(p,q,r),p))) = true
       r = r10 &
       q10 = q &
       p10 = p

#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
#case: (enc2(p,n(p,q,r),n,q) \
        = enc2(sender(m10),nonce(cipher1(m10)),n(p10,sender(m10),r10),p10)) = false 
       ## (enc2(p,n(p,q,r),n,q) \
       ##  = enc2(sender(m10),nonce(cipher1(m10)),n(p10,sender(m10),r10),p10)) = true
       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: 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
#case: p = intruder
       (p = intruder) = false
#case: e20 = enc2(p,n(p,q,r),n,q) &
       enc2(p,n(p,q,r),n,q) \in cenc2(nw(s)) = true
       (e20 = enc2(p,n(p,q,r),n,q)) = false 
#case: m2(intruder,p10,q10,enc2(p,n(p,q,r),n,q)) \
       = m2(q,q,p,enc2(p,n(p,q,r),n,q))
       (m2(intruder,p10,q10,enc2(p,n(p,q,r),n,q)) \
        = m2(q,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: (enc2(p,n(p,q,r),n,q) = enc2(q10,n10,n20,p10)) = false
       ## (enc2(p,n(p,q,r),n,q) = enc2(q10,n10,n20,p10)) = true
       q10 = p &
       n10 = n(p,q,r) &
       n = n20 &
       p10 = q &
       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