-- Case analyses

-- 1) sdm1(s,p10,q10,r10)
mod EICASE1 { pr(ICASE1)
-- Basic predicates  
  ops bp1 bp2 : -> Bool 
  #define bp1 ::= (q10 = intruder) .
  #define bp2 ::= (n = n(p10,q10,r10)) .
-- Exhaustiveness check
  op check : -> Bool 
  eq check = not bp1 or (bp1 and bp2) or (bp1 and not bp2) .
}
-- Case splitting
mod ICASE1-1 { pr(EICASE1)
  eq bp1 = false .
}
--
mod ICASE1-2 { pr(EICASE1)
  eq bp1 = true .
  eq bp2 = true .
}
--
mod ICASE1-3 { pr(EICASE1)
  eq bp1 = true .
  eq bp2 = false .
}

-- 2) sdm2(s,p10,r10,m10)
mod EICASE2 { pr(ICASE2)
-- Basic predicates  
  ops bp1 bp2 bp3 : -> Bool 
  #define bp1 ::= (sender(m10) = intruder) .
  #define bp2 ::= (n = nonce(cipher1(m10))) .
  #define bp3 ::= (n = n(p10,sender(m10),r10)) .
-- Exhaustiveness check
  op check : -> Bool 
  eq check = not bp1 or (bp1 and bp2) or (bp1 and bp3) or
             (bp1 and not bp2 and not bp3) .
}
-- 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 bp3 = true .
}
--
mod ICASE2-4 { pr(EICASE2)
  eq bp1 = true .
  eq bp2 = false .
  eq bp3 = false .
}

-- 3) sdm3(s,p10,r10,m10,m20)
mod EICASE3 { pr(ICASE3)
-- Basic predicates  
  ops bp1 bp2 : -> Bool 
  #define bp1 ::= (sender(m20) = intruder) .
  #define bp2 ::= (n = nonce2(cipher2(m20))) .
-- 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 bp2 = false .
}

-- 4) fkm11(s,p10,q10,e10)
mod EICASE4 { pr(ICASE4)
-- Basic predicates  
  op bp1 : -> Bool 
  #define bp1 ::= (key(e10) = intruder) .
-- Exhaustiveness check
  op check : -> Bool 
  eq check = not bp1 or bp1 .
}
-- Case splitting
mod ICASE4-1 { pr(EICASE4)
  eq bp1 = false .
}
--
mod ICASE4-2 { pr(EICASE4)
  eq bp1 = true .
}

-- 5) fkm12(s,p10,q10,n10)
mod EICASE5 { pr(ICASE5)
-- Basic predicates  
  ops bp1 bp2 : -> Bool 
  #define bp1 ::= (q10 = intruder) .
  #define bp2 ::= (n = n10) .
-- Exhaustiveness check
  op check : -> Bool 
  eq check = not bp1 or (bp1 and bp2) or (bp1 and not bp2) .
}
-- Case splitting
mod ICASE5-1 { pr(EICASE5)
  eq bp1 = false .
}
--
mod ICASE5-2 { pr(EICASE5)
  eq bp1 = true .
  eq bp2 = true .
}
--
mod ICASE5-3 { pr(EICASE5)
  eq bp1 = true .
  eq bp2 = false .
}

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

-- 7) fkm22(s,p10,q10,n10,n20)
mod EICASE7 { pr(ICASE7)
-- Basic predicates  
  ops bp1 bp2 bp3 : -> Bool 
  #define bp1 ::= (q10 = intruder) .
  #define bp2 ::= (n = n10) .
  #define bp3 ::= (n = n20) .
-- Exhaustiveness check
  op check : -> Bool 
  eq check = not bp1 or (bp1 and bp2) or (bp1 and bp3) or (bp1 and not bp2 and not bp3) .
}
-- 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 bp3 = true .
}
--
mod ICASE7-4 { pr(EICASE7)
  eq bp1 = true .
  eq bp2 = false .
  eq bp3 = false .
}

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

-- 9) fkm32(s,p10,q10,n10)
mod EICASE9 { pr(ICASE9)
-- Basic predicates  
  ops bp1 bp2 : -> Bool 
  #define bp1 ::= (q10 = intruder) .
  #define bp2 ::= (n = n10) .
-- 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 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 : inv160(init,n) .
-- II) Inductive cases
  red in ICASE1-1 : istep160(n) .
  red in ICASE1-2 : istep160(n) .
  red in ICASE1-3 : istep160(n) .
  red in ICASE2-1 : istep160(n) .
  red in ICASE2-2 : istep160(n) .
  red in ICASE2-3 : istep160(n) .
  red in ICASE2-4 : istep160(n) .
  red in ICASE3-1 : istep160(n) .
  red in ICASE3-2 : istep160(n) .
  red in ICASE3-3 : istep160(n) .
  red in ICASE4-1 : istep160(n) .
  red in ICASE4-2 : inv100(s,e10) implies istep160(n) .
  red in ICASE5-1 : istep160(n) .
  red in ICASE5-2 : istep160(n) .
  red in ICASE5-3 : istep160(n) .
  red in ICASE6-1 : istep160(n) .
  red in ICASE6-2 : inv110(s,e20) implies istep160(n) .
  red in ICASE7-1 : istep160(n) .
  red in ICASE7-2 : istep160(n) .
  red in ICASE7-3 : istep160(n) .
  red in ICASE7-4 : istep160(n) .
  red in ICASE8-1 : istep160(n) .
  red in ICASE8-2 : inv120(s,e30) implies istep160(n) .
  red in ICASE9-1 : istep160(n) .
  red in ICASE9-2 : istep160(n) .
  red in ICASE9-3 : istep160(n) .
-- Q.E.D.