mod ICASE1 {
  pr(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 .
-- successor state
  eq s' = sdm1(s,p10,q10,r10) .
}

mod ICASE2 {
  pr(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 .
-- successor state
  eq s' = sdm2(s,p10,r10,m10) .
}

mod ICASE3 {
  pr(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) .
}

mod ICASE4 {
  pr(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 .
-- successor state
  eq s' = fkm11(s,p10,q10,e10) .
}

mod ICASE5 {
  pr(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 .
-- successor state
  eq s' = fkm12(s,p10,q10,n10) .
}

mod ICASE6 {
  pr(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 .
-- successor state
  eq s' = fkm21(s,p10,q10,e20) .
}

mod ICASE7 {
  pr(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 .
-- successor state
  eq s' = fkm22(s,p10,q10,n10,n20) .
}

mod ICASE8 {
  pr(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) .
}

mod ICASE9 {
  pr(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) .
}