-- Case analyses

-- 1) sdm1(s,p10,q10,r10)
mod EICASE1 { pr(ICASE1)
-- Basic predicates  
  ops bp1 bp2 : -> Bool 
  #define bp1 ::= (q10 = intruder) .
  #define bp2 ::= (nonce2(e2) = 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 bp4 bp5 bp6 : -> Bool 
  #define bp1 ::= 
   (e2 = enc2(sender(m10),nonce(cipher1(m10)),n(p10,sender(m10),r10),p10)) .
  #define bp2 ::= (sender(m10) = intruder) .
  #define bp3 ::= (nonce2(e2) = nonce(cipher1(m10))) .
  #define bp4 ::= (nonce2(e2) = n(p10,sender(m10),r10)) .
  #define bp5 ::= (p10 = intruder) .
  #define bp6 ::= n(p10,sender(m10),r10) \in cnonce(m10 , nw10) .
-- Exhaustiveness check
  op check : -> Bool 
  eq check = (not bp1 and not bp2) or (not bp1 and bp2 and bp3) or 
             (not bp1 and bp2 and bp4) or (not bp1 and bp2 and not bp3 and not bp4) or 
             (bp1 and bp2) or (bp1 and not bp2 and not bp5) or
             (bp1 and not bp2 and bp5 and bp6) or(bp1 and not bp2 and bp5 and not bp6) .
}
-- Case splitting
mod ICASE2-1 { pr(EICASE2)
  eq bp1 = false .
  eq bp2 = false .
}
--
mod ICASE2-2 { pr(EICASE2)
  eq bp1 = false .
  eq bp2 = true .
  eq bp3 = true .
}
--
mod ICASE2-3 { pr(EICASE2)
  eq bp1 = false .
  eq bp2 = true .
  eq bp4 = true .
}
--
mod ICASE2-4 { pr(EICASE2)
  eq bp1 = false .
  eq bp2 = true .
  eq bp3 = false .
  eq bp4 = false .
}
--
mod ICASE2-5 { pr(EICASE2)
  -- eq bp1 = true .
  eq e2 = enc2(sender(m10),nonce(cipher1(m10)),n(p10,sender(m10),r10),p10) .
  --
  eq bp2 = true .
}
--
mod ICASE2-6 { pr(EICASE2)
  -- eq bp1 = true .
  eq e2 = enc2(sender(m10),nonce(cipher1(m10)),n(p10,sender(m10),r10),p10) .
  --
  eq bp2 = false .
  eq bp5 = false .
}
--
mod ICASE2-7 { pr(EICASE2)
  -- eq bp1 = true .
  eq e2 = enc2(sender(m10),nonce(cipher1(m10)),n(p10,sender(m10),r10),p10) .
  --
  eq bp2 = false .
  eq bp5 = true .
  eq bp6 = true .
}
--
mod ICASE2-8 { pr(EICASE2)
  -- eq bp1 = true .
  eq e2 = enc2(sender(m10),nonce(cipher1(m10)),n(p10,sender(m10),r10),p10) .
  --
  eq bp2 = false .
  eq bp5 = true .
  eq bp6 = 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 ::= (nonce2(e2) = 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 ::= (nonce2(e2) = 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  
  ops bp1 bp2 : -> Bool 
  #define bp1 ::= (key(e20) = intruder) .
  #define bp2 ::= (e2 = e20) .
-- Exhaustiveness check
  op check : -> Bool 
  eq check = (not bp1 and not bp2) or (not bp1 and bp2) or bp1 .
}
-- Case splitting
mod ICASE6-1 { pr(EICASE6)
  eq bp1 = false .
  eq bp2 = false .
}
--
mod ICASE6-2 { pr(EICASE6)
  eq bp1 = false .
  -- eq bp2 = true .
  eq e2 = e20 .
}
--
mod ICASE6-3 { pr(EICASE6)
  eq bp1 = true .
}

-- 7) fkm22(s,p10,q10,n10,n20)
mod EICASE7 { pr(ICASE7)
-- Basic predicates  
  ops bp1 bp2 bp3 bp4 bp5 : -> Bool 
  #define bp1 ::= (e2 = enc2(q10,n10,n20,p10)) .
  #define bp2 ::= (p10 = intruder) .
  #define bp3 ::= (q10 = intruder) .
  #define bp4 ::= (nonce2(e2) = n10) .
  #define bp5 ::= (nonce2(e2) = n20) .
-- Exhaustiveness check
  op check : -> Bool 
  eq check = (bp1 and not bp2) or (bp1 and bp2 and bp3) or 
             (bp1 and bp2 and not bp3) or (not bp1 and not bp3) or 
             (not bp1 and bp3 and bp4) or (not bp1 and bp3 and bp5) or 
             (not bp1 and bp3 and not bp4 and not bp5) .
}
-- Case splitting
mod ICASE7-1 { pr(EICASE7)
  -- eq bp1 = true .
  eq e2 = enc2(q10,n10,n20,p10) .
  --
  eq bp2 = false .
}
--
mod ICASE7-2 { pr(EICASE7)
  -- eq bp1 = true .
  eq e2 = enc2(q10,n10,n20,p10) .
  --
  eq bp2 = true .
  eq bp3 = true .
}
--
mod ICASE7-3 { pr(EICASE7)
  -- eq bp1 = true .
  eq e2 = enc2(q10,n10,n20,p10) .
  --
  eq bp2 = true .
  eq bp3 = false .
}
--
mod ICASE7-4 { pr(EICASE7)
  eq bp1 = false .
  eq bp3 = false .
}
--
mod ICASE7-5 { pr(EICASE7)
  eq bp1 = false .
  eq bp3 = true .
  eq bp4 = true .
}
--
mod ICASE7-6 { pr(EICASE7)
  eq bp1 = false .
  eq bp3 = true .
  eq bp5 = true .
}
--
mod ICASE7-7 { pr(EICASE7)
  eq bp1 = false .
  eq bp3 = true .
  eq bp4 = false .
  eq bp5 = 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 ::= (nonce2(e2) = 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 : inv150(init,e2) .
-- II) Inductive cases
  red in ICASE1-1 : istep150(e2) .
  red in ICASE1-2 : istep150(e2) .
  red in ICASE1-3 : istep150(e2) .
  red in ICASE2-1 : istep150(e2) .
  red in ICASE2-2 : istep150(e2) .
  red in ICASE2-3 : istep150(e2) .
  red in ICASE2-4 : istep150(e2) .
  red in ICASE2-5 : istep150(e2) .
  red in ICASE2-6 : istep150(e2) .
  red in ICASE2-7 : istep150(e2) .
  red in ICASE2-8 : inv160(s,n(p10,sender(m10),r10)) implies istep150(e2) .
  red in ICASE3-1 : istep150(e2) .
  red in ICASE3-2 : istep150(e2) .
  red in ICASE3-3 : istep150(e2) .
  red in ICASE4-1 : istep150(e2) .
  red in ICASE4-2 : inv100(s,e10) implies istep150(e2) .
  red in ICASE5-1 : istep150(e2) .
  red in ICASE5-2 : istep150(e2) .
  red in ICASE5-3 : istep150(e2) .
  red in ICASE6-1 : istep150(e2) .
  red in ICASE6-2 : istep150(e2) .
  red in ICASE6-3 : inv110(s,e20) implies istep150(e2) .
  red in ICASE7-1 : istep150(e2) .
  red in ICASE7-2 : istep150(e2) .
  red in ICASE7-3 : istep150(e2) .
  red in ICASE7-4 : istep150(e2) .
  red in ICASE7-5 : istep150(e2) .
  red in ICASE7-6 : istep150(e2) .
  red in ICASE7-7 : istep150(e2) .
  red in ICASE8-1 : istep150(e2) .
  red in ICASE8-2 : inv120(s,e30) implies istep150(e2) .
  red in ICASE9-1 : istep150(e2) .
  red in ICASE9-2 : istep150(e2) .
  red in ICASE9-3 : istep150(e2) .
-- Q.E.D.