-- I) Base case

open INV
  red inv170(init,p,q,q1,r,n) .
close

-- II) Inductive ceses

--> 1) sdm1(s,p10,q10,r10)
-- 1.1) c-sdm1(s,p10,q10,r10)
open ISTEP
-- arbitrary objects
  ops p10 q10 : -> Principal .
  op r10 : -> Random .
-- assumptions
  -- eq c-sdm1(s,p10,q10,r10) = true .
  eq r10 \in ur(s) = false .
--
  eq p = intruder .
-- successor state
  eq s' = sdm1(s,p10,q10,r10) .
-- check if the predicate is true.
  red istep170(p,q,q1,r,n) .
close
--
open ISTEP
-- arbitrary objects
  ops p10 q10 : -> Principal .
  op r10 : -> Random .
-- assumptions
  -- eq c-sdm1(s,p10,q10,r10) = true .
  eq r10 \in ur(s) = false .
--
  eq (p = intruder) = false .
  eq (m1(p10,p10,q10,enc1(q10,n(p10,q10,r10),p10))
      = m1(p,p,q,enc1(q,n(p,q,r),p))) = false .
-- successor state
  eq s' = sdm1(s,p10,q10,r10) .
-- check if the predicate is true.
  red istep170(p,q,q1,r,n) .
close
--
open ISTEP
-- arbitrary objects
  ops p10 q10 : -> Principal .
  op r10 : -> Random .
-- assumptions
  -- eq c-sdm1(s,p10,q10,r10) = true .
  eq r10 \in ur(s) = false .
--
  eq (p = intruder) = false .
  -- eq m1(p10,p10,q10,enc1(q10,n(p10,q10,r10),p10))
  --    = m1(p,p,q,enc1(q,n(p,q,r),p)) .
  -- ***REWRITE*** -- Tip 2.d
  eq r = r10 .
  eq q10 = q .
  eq p10 = p .
  --
  eq m2(q1,q,p,enc2(p,n(p,q,r10),n,q)) \in nw(s) = false .
-- successor state
  eq s' = sdm1(s,p10,q10,r10) .
-- check if the predicate is true.
  red istep170(p,q,q1,r,n) .
close
--
open ISTEP
-- arbitrary objects
  ops p10 q10 : -> Principal .
  op r10 : -> Random .
  op nw10 : -> Network .
-- assumptions
  -- eq c-sdm1(s,p10,q10,r10) = true .
  eq r10 \in ur(s) = false .
--
  eq (p = intruder) = false .
  -- eq m1(p10,p10,q10,enc1(q10,n(p10,q10,r10),p10))
  --    = m1(p,p,q,enc1(q,n(p,q,r),p)) .
  -- ***REWRITE***
  eq r = r10 .
  eq q10 = q .
  eq p10 = p .
  --
  -- eq m2(q1,q,p,enc2(p,n(p,q,r10),n,q)) \in nw(s) = true .
  -- ***REWRITE***
  eq nw(s) = m2(q1,q,p,enc2(p,n(p,q,r10),n,q)) , nw10 .
-- successor state
  eq s' = sdm1(s,p10,q10,r10) .
-- check if the predicate is true.
  red inv190(s,p,q,r,n) implies istep170(p,q,q1,r,n) .
close
--
-- 1.2) not c-sdm1(s,p10,q10,r10)
open ISTEP
-- arbitrary objects
  ops p10 q10 : -> Principal .
  op r10 : -> Random .
-- assumptions
  eq c-sdm1(s,p10,q10,r10) = false .
-- successor state
  eq s' = sdm1(s,p10,q10,r10) .
-- check if the predicate is true.
  red istep170(p,q,q1,r,n) .
close

--> 2) sdm2(s,p10,r10,m10)
-- 2.1) c-sdm2(s,p10,r10,m10)
open ISTEP
-- arbitrary objects
  op p10 : -> Principal .
  op r10 : -> Random .
  op m10 : -> Message .
  op nw10 : -> 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 (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 .
  eq (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 .
-- successor state
  eq s' = sdm2(s,p10,r10,m10) .
-- check if the predicate is true.
  red istep170(p,q,q1,r,n) .
close
--
open ISTEP
-- arbitrary objects
  op p10 : -> Principal .
  op r10 : -> Random .
  op m10 : -> Message .
  op nw10 : -> 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 (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 .
  eq 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)) .
-- successor state
  eq s' = sdm2(s,p10,r10,m10) .
-- check if the predicate is true.
  red istep170(p,q,q1,r,n) .
close
--
open ISTEP
-- arbitrary objects
  op p10 : -> Principal .
  op r10 : -> Random .
  op m10 : -> Message .
  op nw10 : -> 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 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)) .
  -- ***REWRITE***
  eq q1 = p10 .
  eq p = sender(m10) .
  eq nonce(cipher1(m10)) = n(p,q,r) .
  eq n = n(p10,sender(m10),r10) .
  eq q = p10 .
-- successor state
  eq s' = sdm2(s,p10,r10,m10) .
-- check if the predicate is true.
  red istep170(p,q,q1,r,n) .
close
--
-- 2.2) not c-sdm2(s,p10,r10,m10)
open ISTEP
-- arbitrary objects
  op p10 : -> Principal .
  op r10 : -> Random .
  op m10 : -> Message .
-- assumptions
  eq c-sdm2(s,p10,r10,m10) = false .
-- successor state
  eq s' = sdm2(s,p10,r10,m10) .
-- check if the predicate is true.
  red istep170(p,q,q1,r,n) .
close

--> 3) sdm3(s,p10,r10,m10,m20)
-- 3.1) c-sdm3(s,p10,r10,m10,m20)
open ISTEP
-- arbitrary objects
  op p10 : -> Principal .
  op r10 : -> Random .
  ops m10 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 state
  eq s' = sdm3(s,p10,r10,m10,m20) .
-- check if the predicate is true.
  red istep170(p,q,q1,r,n) .
close
--
-- 3.2) not c-sdm3(s,p10,r10,m10,m20)
open ISTEP
-- arbitrary objects
  op p10 : -> Principal .
  op r10 : -> Random .
  ops m10 m20 : -> Message .
-- assumptions
  eq c-sdm3(s,p10,r10,m10,m20) = false .
-- successor state
  eq s' = sdm3(s,p10,r10,m10,m20) .
-- check if the predicate is true.
  red istep170(p,q,q1,r,n) .
close

--> 4) fkm11(s,p10,q10,e10)
-- 4.1) c-fkm11(s,p10,q10,e10)
open ISTEP
-- arbitrary objects
  ops p10 q10 : -> Principal .
  op e10 : -> Cipher1 .
-- assumptions
  -- eq c-fkm11(s,p10,q10,e10) = true .
  eq e10 \in cenc1(nw(s)) = true .
--
  eq p = intruder .
-- successor state
  eq s' = fkm11(s,p10,q10,e10) .
-- check if the predicate is true.
  red istep170(p,q,q1,r,n) .
close
--
open ISTEP
-- arbitrary objects
  ops p10 q10 : -> Principal .
  op e10 : -> Cipher1 .
-- assumptions
  -- eq c-fkm11(s,p10,q10,e10) = true .
  eq e10 \in cenc1(nw(s)) = true .
--
  eq (p = intruder) = false .
-- successor state
  eq s' = fkm11(s,p10,q10,e10) .
-- check if the predicate is true.
  red istep170(p,q,q1,r,n) .
close
--
-- 4.2) not c-fkm11(s,p10,q10,e10)
open ISTEP
-- arbitrary objects
  ops p10 q10 : -> Principal .
  op e10 : -> Cipher1 .
-- assumptions
  eq c-fkm11(s,p10,q10,e10) = false .
-- successor state
  eq s' = fkm11(s,p10,q10,e10) .
-- check if the predicate is true.
  red istep170(p,q,q1,r,n) .
close

--> 5) fkm12(s,p10,q10,n10)
-- 5.1) c-fkm12(s,p10,q10,n10)
open ISTEP
-- arbitrary objects
  ops p10 q10 : -> Principal .
  op n10 : -> Nonce .
-- assumptions
  -- eq c-fkm12(s,p10,q10,n10) = true .
  eq n10 \in cnonce(nw(s)) = true .
--
  eq p = intruder .
-- successor state
  eq s' = fkm12(s,p10,q10,n10) .
-- check if the predicate is true.
  red istep170(p,q,q1,r,n) .
close
--
open ISTEP
-- arbitrary objects
  ops p10 q10 : -> Principal .
  op n10 : -> Nonce .
-- assumptions
  -- eq c-fkm12(s,p10,q10,n10) = true .
  eq n10 \in cnonce(nw(s)) = true .
--
  eq (p = intruder) = false .
-- successor state
  eq s' = fkm12(s,p10,q10,n10) .
-- check if the predicate is true.
  red istep170(p,q,q1,r,n) .
close
--
-- 5.2) not c-fkm12(s,p10,q10,n10)
open ISTEP
-- arbitrary objects
  ops p10 q10 : -> Principal .
  op n10 : -> Nonce .
-- assumptions
  eq c-fkm12(s,p10,q10,n10) = false .
-- successor state
  eq s' = fkm12(s,p10,q10,n10) .
-- check if the predicate is true.
  red istep170(p,q,q1,r,n) .
close

--> 6) fkm21(s,p10,q10,e20)
-- 6.1) c-fkm21(s,p10,q10,e20)
open ISTEP
-- arbitrary objects
  ops p10 q10 : -> Principal .
  op e20 : -> Cipher2 .
-- assumptions
  -- eq c-fkm21(s,p10,q10,e20) = true .
  eq e20 \in cenc2(nw(s)) = true .
--
  eq p = intruder .
-- successor state
  eq s' = fkm21(s,p10,q10,e20) .
-- check if the predicate is true.
  red istep170(p,q,q1,r,n) .
close
--
open ISTEP
-- arbitrary objects
  ops p10 q10 : -> Principal .
  op e20 : -> Cipher2 .
-- assumptions
  -- eq c-fkm21(s,p10,q10,e20) = true .
  eq e20 \in cenc2(nw(s)) = true .
--
  eq (p = intruder) = false .
  eq m1(p,p,q,enc1(q,n(p,q,r),p)) \in nw(s) = false .
-- successor state
  eq s' = fkm21(s,p10,q10,e20) .
-- check if the predicate is true.
  red istep170(p,q,q1,r,n) .
close
--
open ISTEP
-- arbitrary objects
  ops p10 q10 : -> Principal .
  op e20 : -> Cipher2 .
-- assumptions
  -- eq c-fkm21(s,p10,q10,e20) = true .
  eq e20 \in cenc2(nw(s)) = true .
--
  eq (p = intruder) = false .
  eq m1(p,p,q,enc1(q,n(p,q,r),p)) \in nw(s) = true .
  eq (m2(intruder,p10,q10,e20) = m2(q1,q,p,enc2(p,n(p,q,r),n,q))) = false .
  eq (m2(intruder,p10,q10,e20) = m2(q,q,p,enc2(p,n(p,q,r),n,q))) = false .
-- successor state
  eq s' = fkm21(s,p10,q10,e20) .
-- check if the predicate is true.
  red istep170(p,q,q1,r,n) .
close
--
open ISTEP
-- arbitrary objects
  ops p10 q10 : -> Principal .
  op e20 : -> Cipher2 .
-- assumptions
  -- eq c-fkm21(s,p10,q10,e20) = true .
  eq e20 \in cenc2(nw(s)) = true .
--
  eq (p = intruder) = false .
  eq m1(p,p,q,enc1(q,n(p,q,r),p)) \in nw(s) = true .
  eq (m2(intruder,p10,q10,e20) = m2(q1,q,p,enc2(p,n(p,q,r),n,q))) = false .
  eq (m2(intruder,p10,q10,e20) = m2(q,q,p,enc2(p,n(p,q,r),n,q))) = true .
-- successor state
  eq s' = fkm21(s,p10,q10,e20) .
-- check if the predicate is true.
  red istep170(p,q,q1,r,n) .
close
--
open ISTEP
-- arbitrary objects
  ops p10 q10 : -> Principal .
  op e20 : -> Cipher2 .
-- assumptions
  -- eq c-fkm21(s,p10,q10,e20) = true .
  -- eq e20 \in cenc2(nw(s)) = true .
  -- ***REWRITE***
  eq enc2(p,n(p,q,r),n,q) \in cenc2(nw(s)) = true .
--
  eq (p = intruder) = false .
  eq m1(p,p,q,enc1(q,n(p,q,r),p)) \in nw(s) = true .
  -- eq m2(intruder,p10,q10,e20) = m2(q1,q,p,enc2(p,n(p,q,r),n,q)) .
  -- ***REWRITE***
  eq q1 = intruder .
  eq p10 = q .
  eq q10 = p .
  eq e20 = enc2(p,n(p,q,r),n,q) .
  --
  eq m2(q,q,p,enc2(p,n(p,q,r),n,q)) \in nw(s) = true .
  eq (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 .
-- successor state
  eq s' = fkm21(s,p10,q10,e20) .
-- check if the predicate is true.
  red istep170(p,q,q1,r,n) .
close
--
open ISTEP
-- arbitrary objects
  ops p10 q10 : -> Principal .
  op e20 : -> Cipher2 .
-- assumptions
  -- eq c-fkm21(s,p10,q10,e20) = true .
  -- eq e20 \in cenc2(nw(s)) = true .
  -- ***REWRITE***
  eq enc2(p,n(p,q,r),n,q) \in cenc2(nw(s)) = true .
--
  eq (p = intruder) = false .
  eq m1(p,p,q,enc1(q,n(p,q,r),p)) \in nw(s) = true .
  -- eq m2(intruder,p10,q10,e20) = m2(q1,q,p,enc2(p,n(p,q,r),n,q)) .
  -- ***REWRITE***
  eq q1 = intruder .
  eq p10 = q .
  eq q10 = p .
  eq e20 = enc2(p,n(p,q,r),n,q) .
  --
  eq m2(q,q,p,enc2(p,n(p,q,r),n,q)) \in nw(s) = true .
  eq (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 .
-- successor state
  eq s' = fkm21(s,p10,q10,e20) .
-- check if the predicate is true.
  red istep170(p,q,q1,r,n) .
close
--
open ISTEP
-- arbitrary objects
  ops p10 q10 : -> Principal .
  op e20 : -> Cipher2 .
-- assumptions
  -- eq c-fkm21(s,p10,q10,e20) = true .
  -- eq e20 \in cenc2(nw(s)) = true .
  -- ***REWRITE***
  eq enc2(p,n(p,q,r),n,q) \in cenc2(nw(s)) = true .
--
  eq (p = intruder) = false .
  eq m1(p,p,q,enc1(q,n(p,q,r),p)) \in nw(s) = true .
  -- eq m2(intruder,p10,q10,e20) = m2(q1,q,p,enc2(p,n(p,q,r),n,q)) .
  -- ***REWRITE***
  eq q1 = intruder .
  eq p10 = q .
  eq q10 = p .
  eq e20 = enc2(p,n(p,q,r),n,q) .
  --
  eq m2(q,q,p,enc2(p,n(p,q,r),n,q)) \in nw(s) = false .
  eq (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 .
-- successor state
  eq s' = fkm21(s,p10,q10,e20) .
-- check if the predicate is true.
  red istep170(p,q,q1,r,n) .
close
--
open ISTEP
-- arbitrary objects
  ops p10 q10 : -> Principal .
  op e20 : -> Cipher2 .
-- assumptions
  -- eq c-fkm21(s,p10,q10,e20) = true .
  -- eq e20 \in cenc2(nw(s)) = true .
  -- ***REWRITE***
  eq enc2(p,n(p,q,r),n,q) \in cenc2(nw(s)) = true .
--
  eq (p = intruder) = false .
  eq m1(p,p,q,enc1(q,n(p,q,r),p)) \in nw(s) = true .
  -- eq m2(intruder,p10,q10,e20) = m2(q1,q,p,enc2(p,n(p,q,r),n,q)) .
  -- ***REWRITE***
  eq q1 = intruder .
  eq p10 = q .
  eq q10 = p .
  eq e20 = enc2(p,n(p,q,r),n,q) .
  --
  eq m2(q,q,p,enc2(p,n(p,q,r),n,q)) \in nw(s) = false .
  eq (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 .
-- successor state
  eq s' = fkm21(s,p10,q10,e20) .
-- check if the predicate is true.
  red inv220(s,p,q,r,n) implies istep170(p,q,q1,r,n) .
close
--
-- 6.2) not c-fkm21(s,p10,q10,e20)
open ISTEP
-- arbitrary objects
  ops p10 q10 : -> Principal .
  op e20 : -> Cipher2 .
-- assumptions
  eq c-fkm21(s,p10,q10,e20) = false .
-- successor state
  eq s' = fkm21(s,p10,q10,e20) .
-- check if the predicate is true.
  red istep170(p,q,q1,r,n) .
close

--> 7) fkm22(s,p10,q10,n10,n20)
-- 7.1) c-fkm22(s,p10,q10,n10,n20)
open ISTEP
-- arbitrary objects
  ops p10 q10 : -> Principal .
  ops n10 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 .
--
  eq p = intruder .
-- successor state
  eq s' = fkm22(s,p10,q10,n10,n20) .
-- check if the predicate is true.
  red istep170(p,q,q1,r,n) .
close
--
open ISTEP
-- arbitrary objects
  ops p10 q10 : -> Principal .
  ops n10 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 .
--
  eq (p = intruder) = false .
  eq (m2(q1,q,p,enc2(p,n(p,q,r),n,q))
      = m2(intruder,p10,q10,enc2(q10,n10,n20,p10))) = false .
  eq (m2(q,q,p,enc2(p,n(p,q,r),n,q))
      = m2(intruder,p10,q10,enc2(q10,n10,n20,p10))) = false .
-- successor state
  eq s' = fkm22(s,p10,q10,n10,n20) .
-- check if the predicate is true.
  red istep170(p,q,q1,r,n) .
close
--
open ISTEP
-- arbitrary objects
  ops p10 q10 : -> Principal .
  ops n10 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 .
--
  eq (p = intruder) = false .
  eq (m2(q1,q,p,enc2(p,n(p,q,r),n,q))
      = m2(intruder,p10,q10,enc2(q10,n10,n20,p10))) = false .
  eq (m2(q,q,p,enc2(p,n(p,q,r),n,q))
      = m2(intruder,p10,q10,enc2(q10,n10,n20,p10))) = true .
-- successor state
  eq s' = fkm22(s,p10,q10,n10,n20) .
-- check if the predicate is true.
  red istep170(p,q,q1,r,n) .
close
--
open ISTEP
-- arbitrary objects
  ops p10 q10 : -> Principal .
  ops n10 n20 : -> Nonce .
-- assumptions
  -- eq c-fkm22(s,p10,q10,n10,n20) = true .
  -- eq n10 \in cnonce(nw(s)) = true .
  -- **REWRITE**
  eq n(p,intruder,r) \in cnonce(nw(s)) = true . -- Tip 2.c
  eq n20 \in cnonce(nw(s)) = true .
--
  eq (p = intruder) = false .
  -- eq m2(q1,q,p,enc2(p,n(p,q,r),n,q))
  --    = m2(intruder,p10,q10,enc2(q10,n10,n20,p10)) .
  -- ***REWRITE***
  eq q1 = intruder .
  eq p10 = q .
  eq q10 = p .
  eq n10 = n(p,q,r) .
  eq n = n20 .
  --
  eq q = intruder .
-- successor state
  eq s' = fkm22(s,p10,q10,n10,n20) .
-- check if the predicate is true.
  red istep170(p,q,q1,r,n) .
close
--
open ISTEP
-- arbitrary objects
  ops p10 q10 : -> Principal .
  ops n10 n20 : -> Nonce .
-- assumptions
  -- eq c-fkm22(s,p10,q10,n10,n20) = true .
  -- eq n10 \in cnonce(nw(s)) = true .
  -- **REWRITE**
  eq n(p,q,r) \in cnonce(nw(s)) = true .
  eq n20 \in cnonce(nw(s)) = true .
--
  eq (p = intruder) = false .
  -- eq m2(q1,q,p,enc2(p,n(p,q,r),n,q))
  --    = m2(intruder,p10,q10,enc2(q10,n10,n20,p10)) .
  -- ***REWRITE***
  eq q1 = intruder .
  eq p10 = q .
  eq q10 = p .
  eq n10 = n(p,q,r) .
  eq n = n20 .
  --
  eq (q = intruder) = false .
-- successor state
  eq s' = fkm22(s,p10,q10,n10,n20) .
-- check if the predicate is true.
  red inv130(s,n10) implies istep170(p,q,q1,r,n) .
close
--
-- 7.2) not c-fkm22(s,p10,q10,n10,n20)
open ISTEP
-- arbitrary objects
  ops p10 q10 : -> Principal .
  ops n10 n20 : -> Nonce .
-- assumptions
  eq c-fkm22(s,p10,q10,n10,n20) = false .
-- successor state
  eq s' = fkm22(s,p10,q10,n10,n20) .
-- check if the predicate is true.
  red istep170(p,q,q1,r,n) .
close

--> 8) fkm31(s,p10,q10,e30)
-- 8.1) c-fkm31(s,p10,q10,e30)
open ISTEP
-- arbitrary objects
  ops p10 q10 : -> Principal .
  op e30 : -> Cipher3 .
-- assumptions
  -- eq c-fkm31(s,p10,q10,e30) = true .
  eq e30 \in cenc3(nw(s)) = true .
-- successor state
  eq s' = fkm31(s,p10,q10,e30) .
-- check if the predicate is true.
  red istep170(p,q,q1,r,n) .
close
--
-- 8.2) not c-fkm31(s,p10,q10,e30)
open ISTEP
-- arbitrary objects
  ops p10 q10 : -> Principal .
  op e30 : -> Cipher3 .
-- assumptions
  eq c-fkm31(s,p10,q10,e30) = false .
-- successor state
  eq s' = fkm31(s,p10,q10,e30) .
-- check if the predicate is true.
  red istep170(p,q,q1,r,n) .
close

--> 9) fkm32(s,p10,q10,n10)
-- 9.1) c-fkm32(s,p10,q10,n10)
open ISTEP
-- arbitrary objects
  ops p10 q10 : -> Principal .
  op n10 : -> Nonce .
-- assumptions
  -- eq c-fkm32(s,p10,q10,n10) = true .
  eq n10 \in cnonce(nw(s)) = true .
-- successor state
  eq s' = fkm32(s,p10,q10,n10) .
-- check if the predicate is true.
  red istep170(p,q,q1,r,n) .
close
--
-- 9.2) not c-fkm32(s,p10,q10,n10)
open ISTEP
-- arbitrary objects
  ops p10 q10 : -> Principal .
  op n10 : -> Nonce .
-- assumptions
  eq c-fkm32(s,p10,q10,n10) = false .
-- successor state
  eq s' = fkm32(s,p10,q10,n10) .
-- check if the predicate is true.
  red istep170(p,q,q1,r,n) .
close

--> Q.E.D.