-- 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  
  ops bp1 bp2 : -> Bool
  #define bp1 ::= (e2 = enc2(sender(m10),nonce(cipher1(m10)),n(p10,sender(m10),r10),p10)) .
  #define bp2 ::= (sender(m10) = intruder) .
-- Exhaustiveness check
  op check : -> Bool 
  eq check = true .
}
-- Case splitting
mod ICASE2-1 { pr(EICASE2)
  eq bp1 = false .
}
--
mod ICASE2-2 { pr(EICASE2)
  eq bp1 = true .
  eq bp2 = true .
}
--
mod ICASE2-3 { pr(EICASE2)
  -- eq bp1 = true .
  eq e2 = enc2(sender(m10),nonce(cipher1(m10)),n(p10,sender(m10),r10),p10) .
  --
  eq bp2 = false .
}

-- 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 ::= (e2 = e20) .
-- Exhaustiveness check
  op check : -> Bool 
  eq check = bp1 or not bp1 .
}
-- Case splitting
mod ICASE6-1 { pr(EICASE6)
  -- eq bp1 = true .
  eq e2 = e20 .
}
--
mod ICASE6-2 { pr(EICASE6)
  eq bp1 = false .
}

--> 7) fkm22(s,p10,q10,n10,n20)
mod EICASE7 { pr(ICASE7)
-- Basic predicates  
  ops bp1 bp2 : -> Bool
  #define bp1 ::= (e2 = enc2(q10,n10,n20,p10)) .
  #define bp2 ::= (q10 = intruder) .
-- Exhaustiveness check
  op check : -> Bool 
  eq check = not bp1 or (bp1 and bp2) or (bp1 and not bp2) .
}
-- Case splitting
mod ICASE7-1 { pr(EICASE7)
  eq bp1 = false .
}
--
mod ICASE7-2 { pr(EICASE7)
  eq bp1 = true .
  eq bp2 = true .
}
--
mod ICASE7-3 { pr(EICASE7)
  -- eq bp1 = true .
  eq e2 = enc2(q10,n10,n20,p10) .
  --
  eq bp2 = 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 : inv110(init,e2) .
-- II) Inductive cases
  red in ICASE1-1 : istep110(e2) .
  red in ICASE2-1 : istep110(e2) .
  red in ICASE2-2 : istep110(e2) .
  red in ICASE2-3 : istep110(e2) .
  red in ICASE3-1 : istep110(e2) .
  red in ICASE4-1 : istep110(e2) .
  red in ICASE5-1 : istep110(e2) .
  red in ICASE6-1 : istep110(e2) .
  red in ICASE6-2 : istep110(e2) .
  red in ICASE7-1 : istep110(e2) .
  red in ICASE7-2 : istep110(e2) .
  red in ICASE7-3 : istep110(e2) .
  red in ICASE8-1 : istep110(e2) .
  red in ICASE9-1 : istep110(e2) .
-- Q.E.D.