-- 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  
-- Exhaustiveness check
  op check : -> Bool 
  eq check = true .
}
-- Case splitting
mod ICASE2-1 { pr(EICASE2) }

-- 3) sdm3(s,p10,r10,m10,m20)
mod EICASE3 { pr(ICASE3)
-- Basic predicates  
  ops bp1 bp2 : -> Bool
  #define bp1 ::= (e3 = enc3(sender(m20),nonce2(cipher2(m20)))) .
  #define bp2 ::= (sender(m20) = intruder) .
-- Exhaustiveness check
  op check : -> Bool 
  eq check = not bp1 or (bp1 and bp2) or (bp1 and not bp2) .
}
-- Case splitting
mod ICASE3-1 { pr(EICASE3)
  eq bp1 = false .
}
--
mod ICASE3-2 { pr(EICASE3)
  eq bp1 = true .
  eq bp2 = true .
}
--
mod ICASE3-3 { pr(EICASE3)
  -- eq bp1 = true .
  eq e3 = enc3(sender(m20),nonce2(cipher2(m20))) .
  -- 
  eq bp2 = false .
}

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

-- 7) fkm22(s,p10,q10,n10,n20)
mod EICASE7 { pr(ICASE7)
-- Basic predicates  
-- Exhaustiveness check
  op check : -> Bool 
  eq check = true .
}
-- Case splitting
mod ICASE7-1 { pr(EICASE7) }

-- 8) fkm31(s,p10,q10,e30)
mod EICASE8 { pr(ICASE8)
-- Basic predicates  
  op bp1 : -> Bool
  #define bp1 ::= (e3 = e30)  .
-- Exhaustiveness check
  op check : -> Bool 
  eq check = bp1 or not bp1 .
}
-- Case splitting
mod ICASE8-1 { pr(EICASE8)
  -- eq bp1 = true .
  eq e3 = e30 .
}
--
mod ICASE8-2 { pr(EICASE8)
  eq bp1 = false .
}

--> 9) fkm32(s,p10,q10,n10)
mod EICASE9 { pr(ICASE9)
-- Basic predicates  
  ops bp1 bp2 : -> Bool
  #define bp1 ::= (e3 = enc3(q10,n10)) .
  #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 ICASE9-1 { pr(EICASE9)
  eq bp1 = false .
}
--
mod ICASE9-2 { pr(EICASE9)
  eq bp1 = true .
  eq bp2 = true .
}
--
mod ICASE9-3 { pr(EICASE9)
  -- eq bp1 = true .
  eq e3 = enc3(q10,n10) .
  --
  eq bp2 = false .
}

-- 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 : inv120(init,e3) .
-- II) Inductive cases
  red in ICASE1-1 : istep120(e3) .
  red in ICASE2-1 : istep120(e3) .
  red in ICASE3-1 : istep120(e3) .
  red in ICASE3-2 : istep120(e3) .
  red in ICASE3-3 : istep120(e3) .
  red in ICASE4-1 : istep120(e3) .
  red in ICASE5-1 : istep120(e3) .
  red in ICASE6-1 : istep120(e3) .
  red in ICASE7-1 : istep120(e3) .
  red in ICASE8-1 : istep120(e3) .
  red in ICASE8-2 : istep120(e3) .
  red in ICASE9-1 : istep120(e3) .
  red in ICASE9-2 : istep120(e3) .
  red in ICASE9-3 : istep120(e3) .
-- Q.E.D.