-- Case analyses

-- 1) sdm1(s,p10,q10,r10)
mod EICASE1 { pr(ICASE1)
-- Basic predicates  
-- Exhaustiveness check
  op check : -> Bool 
  eq check = true .
}
-- Case splitting
mod ICASE1-1 { pr(EICASE1) }

-- 2) sdm2(s,p10,r10,m10)
mod EICASE2 { pr(ICASE2)
-- Basic predicates  
  op bp1 : -> Bool 
  #define bp1 ::= 
    (m2(p,p,q,enc2(q,n1,n2,p))
     = m2(p10,p10,sender(m10),
         enc2(sender(m10),nonce(cipher1(m10)),n(p10,sender(m10),r10),p10))) .
-- Exhaustiveness check
  op check : -> Bool 
  eq check = bp1 or not bp1 .
}
-- Case splitting
mod ICASE2-1 { pr(EICASE2)
  eq bp1 = false .
}
--
mod ICASE2-2 { pr(EICASE2)
  -- eq bp1 = true .
  eq p = p10 .
  eq q = sender(m10) .
  eq n1 = nonce(cipher1(m10)) .
  eq n2 = n(p10,sender(m10),r10) .
}

-- 3) sdm3(s,p10,r10,m10,m20)
mod EICASE3 { pr(ICASE3)
-- Basic predicates  
-- Exhaustiveness check
  op check : -> Bool 
  eq check = true .
}
-- Case splitting
mod ICASE3-1 { pr(EICASE3) }

-- 4) fkm11(s,p10,q10,e10)
mod EICASE4 { pr(ICASE4)
-- Basic predicates  
-- Exhaustiveness check
  op check : -> Bool 
  eq check = true .
}
-- Case splitting
mod ICASE4-1 { pr(EICASE4) }

-- 5) fkm12(s,p10,q10,n10)
mod EICASE5 { pr(ICASE5)
-- Basic predicates  
-- Exhaustiveness check
  op check : -> Bool 
  eq check = true .
}
-- Case splitting
mod ICASE5-1 { pr(EICASE5) }

-- 6) fkm21(s,p10,q10,e20)
mod EICASE6 { pr(ICASE6)
-- Basic predicates  
  op bp1 : -> Bool
  #define bp1 ::= (p = intruder) .
-- Exhaustiveness check
  op check : -> Bool 
  eq check = bp1 or not bp1 .
}
-- Case splitting
mod ICASE6-1 { pr(EICASE6)
  eq bp1 = true .
}
--
mod ICASE6-2 { pr(EICASE6)
  eq bp1 = false .
}

-- 7) fkm22(s,p10,q10,n10,n20)
mod EICASE7 { pr(ICASE7)
-- Basic predicates  
  op bp1 : -> Bool
  #define bp1 ::= (p = intruder) .
-- Exhaustiveness check
  op check : -> Bool 
  eq check = bp1 or not bp1 .
}
-- Case splitting
mod ICASE7-1 { pr(EICASE7)
  eq bp1 = true .
}
--
mod ICASE7-2 { pr(EICASE7)
  eq bp1 = false .
}

-- 8) fkm31(s,p10,q10,e30)
mod EICASE8 { pr(ICASE8)
-- Basic predicates  
-- Exhaustiveness check
  op check : -> Bool 
  eq check = true .
}
-- Case splitting
mod ICASE8-1 { pr(EICASE8) }

-- 9) fkm32(s,p10,q10,n10)
mod EICASE9 { pr(ICASE9)
-- Basic predicates  
-- Exhaustiveness check
  op check : -> Bool 
  eq check = true .
}
-- Case splitting
mod ICASE9-1 { pr(EICASE9) }

-- Exhaustiveness Check 
  red in EICASE1 : check .
  red in EICASE2 : check .
  red in EICASE3 : check .
  red in EICASE4 : check .
  red in EICASE5 : check .
  red in EICASE6 : check .
  red in EICASE7 : check .
  red in EICASE8 : check .
  red in EICASE9 : check .
-- End of Exhaustiveness Check 

-- Proof
-- I) Base case
  red in INV : inv260(init,p,q,n1,n2) .
-- II) Inductive cases
  red in ICASE1-1 : istep260(p,q,n1,n2) .
  red in ICASE2-1 : istep260(p,q,n1,n2) .
  red in ICASE2-2 : istep260(p,q,n1,n2) .
  red in ICASE3-1 : istep260(p,q,n1,n2) .
  red in ICASE4-1 : istep260(p,q,n1,n2) .
  red in ICASE5-1 : istep260(p,q,n1,n2) .
  red in ICASE6-1 : istep260(p,q,n1,n2) .
  red in ICASE6-2 : istep260(p,q,n1,n2) .
  red in ICASE7-1 : istep260(p,q,n1,n2) .
  red in ICASE7-2 : istep260(p,q,n1,n2) .
  red in ICASE8-1 : istep260(p,q,n1,n2) .
  red in ICASE9-1 : istep260(p,q,n1,n2) .
-- Q.E.D.