--> I) Base cases
open INV
  red inv200(init,p,q,r) .
close

--> II) Inductive cases
--> 1 sdm1(s,p10,q10,r10)
-- 1.1 c-sdm1(s,p10,q10,r10) = true
open ISTEP
-- arbitrary objects
  op p10 : -> Principal .
  op q10 : -> Principal .
  op r10 : -> Random .
  op nw10 : -> Network .
-- assumptions
  -- eq c-sdm1(s,p10,q10,r10) = true .
  eq r10 \in ur(s) = false .
  --
  eq r = r10 .
-- successor
  eq s' = sdm1(s,p10,q10,r10) .
-- checking
  red istep200(p,q,r) .
close
--
open ISTEP
-- arbitrary objects
  op p10 : -> Principal .
  op q10 : -> Principal .
  op r10 : -> Random .
  op nw10 : -> Network .
-- assumptions
  -- eq c-sdm1(s,p10,q10,r10) = true .
  eq r10 \in ur(s) = false .
  --
  eq (r = r10) = false .
-- successor
  eq s' = sdm1(s,p10,q10,r10) .
-- checking
  red istep200(p,q,r) .
close
--
-- 1.2 c-sdm1(s,p10,q10,r10) = false
open ISTEP
-- arbitrary objects
  op p10 : -> Principal .
  op q10 : -> Principal .
  op r10 : -> Random .
  op nw10 : -> Network .
-- assumptions
  eq c-sdm1(s,p10,q10,r10) = false .
-- successor
  eq s' = sdm1(s,p10,q10,r10) .
-- checking
  red istep200(p,q,r) .
close

--> 2 sdm2(s,p10,r10,m10)
-- 2.1 c-sdm2(s,p10,r10,m10) = true
open ISTEP
-- arbitrary objects
  op p10 : -> Principal .
  op r10 : -> Random .
  op m10 : -> Message .
  op nw10 : -> Network .
  op nw20 : -> Network .
-- assumptions
  -- eq c-sdm2(s,p10,r10,m10) = true .
  eq nw(s) = m10 , nw10 .
  eq m1?(m10) = true .
  eq receiver(m10) = p10 .
  eq key(cipher1(m10)) = p10 .
  eq principal(cipher1(m10)) = sender(m10) .
  eq r10 \in ur(s) = false .
  --
  eq r = r10 .
-- successor
  eq s' = sdm2(s,p10,r10,m10) .
-- checking
  red istep200(p,q,r) .
close
--
open ISTEP
-- arbitrary objects
  op p10 : -> Principal .
  op r10 : -> Random .
  op m10 : -> Message .
  op nw10 : -> Network .
  op nw20 : -> Network .
-- assumptions
  -- eq c-sdm2(s,p10,r10,m10) = true .
  eq nw(s) = m10 , nw10 .
  eq m1?(m10) = true .
  eq receiver(m10) = p10 .
  eq key(cipher1(m10)) = p10 .
  eq principal(cipher1(m10)) = sender(m10) .
  eq r10 \in ur(s) = false .
  --
  eq (r = r10) = false .
-- successor
  eq s' = sdm2(s,p10,r10,m10) .
-- checking
  red istep200(p,q,r) .
close
--
-- 2.2 c-sdm2(s,p10,r10,m10) = false
open ISTEP
-- arbitrary objects
  op p10 : -> Principal .
  op r10 : -> Random .
  op m10 : -> Message .
  op nw10 : -> Network .
  op nw20 : -> Network .
-- assumptions
  eq c-sdm2(s,p10,r10,m10) = false .
-- successor
  eq s' = sdm2(s,p10,r10,m10) .
-- checking
  red istep200(p,q,r) .
close

--> 3 sdm3(s,p10,r10,m10,m20)
-- 3.1 c-sdm3(s,p10,r10,m10,m20) = true
open ISTEP
-- arbitrary objects
  op p10 : -> Principal .
  op r10 : -> Random .
  op m10 : -> Message .
  op m20 : -> Message .
  op nw10 : -> Network .
-- assumptions
  -- eq c-sdm3(s,p10,r10,m10,m20) = true .
  eq nw(s) = m10 , m20 , nw10 .
  eq m1?(m10) = true .
  eq m2?(m20) = true .
  eq creator(m10) = p10 .
  eq sender(m10) = p10  .
  eq receiver(m10) = sender(m20) .
  eq key(cipher1(m10)) = sender(m20) .
  eq nonce(cipher1(m10)) = n(p10,sender(m20),r10) .
  eq principal(cipher1(m10)) = p10  .
  eq receiver(m20) = p10 .
  eq key(cipher2(m20)) = p10 .
  eq nonce1(cipher2(m20)) = n(p10,sender(m20),r10) .
  eq principal(cipher2(m20)) = sender(m20) .
-- successor
  eq s' = sdm3(s,p10,r10,m10,m20) .
-- checking
  red istep200(p,q,r) .
close
--
-- 3.2 c-sdm3(s,p10,r10,m10,m20) = false
open ISTEP
-- arbitrary objects
  op p10 : -> Principal .
  op r10 : -> Random .
  op m10 : -> Message .
  op m20 : -> Message .
  op nw10 : -> Network .
-- assumptions
  eq c-sdm3(s,p10,r10,m10,m20) = false .
-- successor
  eq s' = sdm3(s,p10,r10,m10,m20) .
-- checking
  red istep200(p,q,r) .
close

--> 4 fkm11(s,p10,q10,e10)
-- 4.1 c-fkm11(s,p10,q10,e10) = true
open ISTEP
-- arbitrary objects
  op p10 : -> Principal .
  op q10 : -> Principal .
  op e10 : -> Cipher1 .
-- assumptions
  -- eq c-fkm11(s,p10,q10,e10) = true .
  eq e10 \in cenc1(nw(s)) = true .
  --
  eq enc1(q,n(p,q,r),p) = e10 .
-- successor
  eq s' = fkm11(s,p10,q10,e10) .
-- checking
  red istep200(p,q,r) .
close
--
open ISTEP
-- arbitrary objects
  op p10 : -> Principal .
  op q10 : -> Principal .
  op e10 : -> Cipher1 .
-- assumptions
  -- eq c-fkm11(s,p10,q10,e10) = true .
  eq e10 \in cenc1(nw(s)) = true .
  --
  eq (enc1(q,n(p,q,r),p) = e10) = false .
-- successor
  eq s' = fkm11(s,p10,q10,e10) .
-- checking
  red istep200(p,q,r) .
close
--
-- 4.2 c-fkm11(s,p10,q10,e10) = false
open ISTEP
-- arbitrary objects
  op p10 : -> Principal .
  op q10 : -> Principal .
  op e10 : -> Cipher1 .
-- assumptions
  eq c-fkm11(s,p10,q10,e10) = false .
-- successor
  eq s' = fkm11(s,p10,q10,e10) .
-- checking
  red istep200(p,q,r) .
close

--> 5 fkm12(s,p10,q10,n10)
-- 5.1 c-fkm12(s,p10,q10,n10) = true
open ISTEP
-- arbitrary objects
  op p10 : -> Principal .
  op q10 : -> Principal .
  op n10 : -> Nonce .
-- assumptions
  -- eq c-fkm12(s,p10,q10,n10) = true .
  eq n10 \in cnonce(nw(s)) = true .
  --
  eq q10 = intruder .
  eq r \in ur(s) = true .
  eq n(p,q,r) = n10 .
-- successor
  eq s' = fkm12(s,p10,q10,n10) .
-- checking
  red inv210(s,p,q,r) implies istep200(p,q,r) .
close
--
open ISTEP
-- arbitrary objects
  op p10 : -> Principal .
  op q10 : -> Principal .
  op n10 : -> Nonce .
-- assumptions
  -- eq c-fkm12(s,p10,q10,n10) = true .
  eq n10 \in cnonce(nw(s)) = true .
  --
  eq (q10 = intruder) = false .
  eq r \in ur(s) = true .
  eq n(p,q,r) = n10 .
-- successor
  eq s' = fkm12(s,p10,q10,n10) .
-- checking
  red inv210(s,p,q,r) implies istep200(p,q,r) .
close
--
open ISTEP
-- arbitrary objects
  op p10 : -> Principal .
  op q10 : -> Principal .
  op n10 : -> Nonce .
-- assumptions
  -- eq c-fkm12(s,p10,q10,n10) = true .
  eq n10 \in cnonce(nw(s)) = true .
  --
  eq q10 = intruder .
  eq r \in ur(s) = false .
  eq n(p,q,r) = n10 .
-- successor
  eq s' = fkm12(s,p10,q10,n10) .
-- checking
  red inv210(s,p,q,r) implies istep200(p,q,r) .
close
--
open ISTEP
-- arbitrary objects
  op p10 : -> Principal .
  op q10 : -> Principal .
  op n10 : -> Nonce .
-- assumptions
  -- eq c-fkm12(s,p10,q10,n10) = true .
  eq n10 \in cnonce(nw(s)) = true .
  --
  eq (q10 = intruder) = false .
  eq r \in ur(s) = false .
  eq n(p,q,r) = n10 .
-- successor
  eq s' = fkm12(s,p10,q10,n10) .
-- checking
  red inv210(s,p,q,r) implies istep200(p,q,r) .
close
--
open ISTEP
-- arbitrary objects
  op p10 : -> Principal .
  op q10 : -> Principal .
  op n10 : -> Nonce .
-- assumptions
  -- eq c-fkm12(s,p10,q10,n10) = true .
  eq n10 \in cnonce(nw(s)) = true .
  --
  eq q10 = intruder .
  eq r \in ur(s) = true .
  eq (n(p,q,r) = n10) = false .
-- successor
  eq s' = fkm12(s,p10,q10,n10) .
-- checking
  red inv210(s,p,q,r) implies istep200(p,q,r) .
close
--
open ISTEP
-- arbitrary objects
  op p10 : -> Principal .
  op q10 : -> Principal .
  op n10 : -> Nonce .
-- assumptions
  -- eq c-fkm12(s,p10,q10,n10) = true .
  eq n10 \in cnonce(nw(s)) = true .
  --
  eq (q10 = intruder) = false .
  eq r \in ur(s) = true .
  eq (n(p,q,r) = n10) = false .
-- successor
  eq s' = fkm12(s,p10,q10,n10) .
-- checking
  red inv210(s,p,q,r) implies istep200(p,q,r) .
close
--
open ISTEP
-- arbitrary objects
  op p10 : -> Principal .
  op q10 : -> Principal .
  op n10 : -> Nonce .
-- assumptions
  -- eq c-fkm12(s,p10,q10,n10) = true .
  eq n10 \in cnonce(nw(s)) = true .
  --
  eq q10 = intruder .
  eq r \in ur(s) = false .
  eq (n(p,q,r) = n10) = false .
-- successor
  eq s' = fkm12(s,p10,q10,n10) .
-- checking
  red inv210(s,p,q,r) implies istep200(p,q,r) .
close
--
open ISTEP
-- arbitrary objects
  op p10 : -> Principal .
  op q10 : -> Principal .
  op n10 : -> Nonce .
-- assumptions
  -- eq c-fkm12(s,p10,q10,n10) = true .
  eq n10 \in cnonce(nw(s)) = true .
  --
  eq (q10 = intruder) = false .
  eq r \in ur(s) = false .
  eq (n(p,q,r) = n10) = false .
-- successor
  eq s' = fkm12(s,p10,q10,n10) .
-- checking
  red inv210(s,p,q,r) implies istep200(p,q,r) .
close
--
-- 5.2 c-fkm12(s,p10,q10,n10) = false
open ISTEP
-- arbitrary objects
  op p10 : -> Principal .
  op q10 : -> Principal .
  op n10 : -> Nonce .
-- assumptions
  eq c-fkm12(s,p10,q10,n10) = false .
-- successor
  eq s' = fkm12(s,p10,q10,n10) .
-- checking
  red istep200(p,q,r) .
close

--> 6 fkm21(s,p10,q10,e20)
-- 6.1 c-fkm21(s,p10,q10,e20) = true
open ISTEP
-- arbitrary objects
  op p10 : -> Principal .
  op q10 : -> Principal .
  op e20 : -> Cipher2 .
-- assumptions
  -- eq c-fkm21(s,p10,q10,e20) = true .
  eq e20 \in cenc2(nw(s)) = true .
-- successor
  eq s' = fkm21(s,p10,q10,e20) .
-- checking
  red istep200(p,q,r) .
close
--
-- 6.2 c-fkm21(s,p10,q10,e20) = false
open ISTEP
-- arbitrary objects
  op p10 : -> Principal .
  op q10 : -> Principal .
  op e20 : -> Cipher2 .
-- assumptions
  eq c-fkm21(s,p10,q10,e20) = false .
-- successor
  eq s' = fkm21(s,p10,q10,e20) .
-- checking
  red istep200(p,q,r) .
close

--> 7 fkm22(s,p10,q10,n10,n20)
-- 7.1 c-fkm22(s,p10,q10,n10,n20) = true
open ISTEP
-- arbitrary objects
  op p10 : -> Principal .
  op q10 : -> Principal .
  op n10 : -> Nonce .
  op n20 : -> Nonce .
-- assumptions
  -- eq c-fkm22(s,p10,q10,n10,n20) = true .
  eq n10 \in cnonce(nw(s)) = true .
  eq n20 \in cnonce(nw(s)) = true .
-- successor
  eq s' = fkm22(s,p10,q10,n10,n20) .
-- checking
  red istep200(p,q,r) .
close
--
-- 7.2 c-fkm22(s,p10,q10,n10,n20) = false
open ISTEP
-- arbitrary objects
  op p10 : -> Principal .
  op q10 : -> Principal .
  op n10 : -> Nonce .
  op n20 : -> Nonce .
-- assumptions
  eq c-fkm22(s,p10,q10,n10,n20) = false .
-- successor
  eq s' = fkm22(s,p10,q10,n10,n20) .
-- checking
  red istep200(p,q,r) .
close

--> 8 fkm31(s,p10,q10,e30)
-- 8.1 c-fkm31(s,p10,q10,e30) = true
open ISTEP
-- arbitrary objects
  op p10 : -> Principal .
  op q10 : -> Principal .
  op e30 : -> Cipher3 .
-- assumptions
  -- eq c-fkm31(s,p10,q10,e30) = true .
  eq e30 \in cenc3(nw(s)) = true .
-- successor
  eq s' = fkm31(s,p10,q10,e30) .
-- checking
  red istep200(p,q,r) .
close
--
-- 8.2 c-fkm31(s,p10,q10,e30) = false
open ISTEP
-- arbitrary objects
  op p10 : -> Principal .
  op q10 : -> Principal .
  op e30 : -> Cipher3 .
-- assumptions
  eq c-fkm31(s,p10,q10,e30) = false .
-- successor
  eq s' = fkm31(s,p10,q10,e30) .
-- checking
  red istep200(p,q,r) .
close

--> 9 fkm32(s,p10,q10,n10)
-- 9.1 c-fkm32(s,p10,q10,n10) = true
open ISTEP
-- arbitrary objects
  op p10 : -> Principal .
  op q10 : -> Principal .
  op n10 : -> Nonce .
-- assumptions
  -- eq c-fkm32(s,p10,q10,n10) = true .
  eq n10 \in cnonce(nw(s)) = true .
-- successor
  eq s' = fkm32(s,p10,q10,n10) .
-- checking
  red istep200(p,q,r) .
close
--
-- 9.2 c-fkm32(s,p10,q10,n10) = false
open ISTEP
-- arbitrary objects
  op p10 : -> Principal .
  op q10 : -> Principal .
  op n10 : -> Nonce .
-- assumptions
  eq c-fkm32(s,p10,q10,n10) = false .
-- successor
  eq s' = fkm32(s,p10,q10,n10) .
-- checking
  red istep200(p,q,r) .
close

--> Q.E.D.