-- Case analyses

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

-- 2) sdm2(s,p10,r10,m10)
mod EICASE2 { pr(ICASE2)
-- Basic predicates  
  op bp1 : -> Bool 
  #define bp1 ::= (r = r10) .
-- Exhaustiveness check
  op check : -> Bool 
  eq check = bp1 or not bp1 .
}
-- Case splitting
mod ICASE2-1 { pr(EICASE2)
  -- eq bp1 = true .
  eq r = r10 .
}
--
mod ICASE2-2 { pr(EICASE2)
  eq bp1 = false .
}

-- 3) sdm3(s,p10,r10,m10,m20)
mod EICASE3 { pr(ICASE3)
-- Basic predicates  
  ops bp1 bp2 bp3 bp4 : -> Bool 
  #define bp1 ::= (sender(m20) = intruder) .
  #define bp2 ::= (enc3(sender(m20),nonce2(cipher2(m20))) = enc3(q,n(q,p,r))) .
  #define bp3 ::= r \in ur(s) .
  #define bp4 ::= (p10 = intruder) .
-- Exhaustiveness check
  op check : -> Bool 
  eq check = bp1 or (not bp1 and not bp2) or (not bp1 and bp2 and bp3) or 
             (not bp1 and bp2 and not bp3 and bp4) or 
             (not bp1 and bp2 and not bp3 and not bp4) .
}
-- Case splitting
mod ICASE3-1 { pr(EICASE3)
  eq bp1 = true .
}
--
mod ICASE3-2 { pr(EICASE3)
  eq bp1 = false .
  eq bp2 = false .
}
--
mod ICASE3-3 { pr(EICASE3)
  eq bp1 = false .
  eq bp2 = true .
  eq bp3 = true .
}
--
mod ICASE3-4 { pr(EICASE3)
  eq bp1 = false .
  -- eq bp2 = true .
  eq q = sender(m20) .
  eq nonce2(cipher2(m20)) = n(q,p,r) .
  --
  eq bp3 = false .
  eq bp4 = true .
}
--
mod ICASE3-5 { pr(EICASE3)
  eq bp1 = false .
  -- eq bp2 = true .
  eq q = sender(m20) .
  eq nonce2(cipher2(m20)) = n(q,p,r) .
  --
  eq bp3 = false .
  eq bp4 = 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 ::= (enc3(q,n(q,p,r)) = e30) .
-- 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 .
  eq enc3(q,n(q,p,r)) = e30 .
}

-- 9) fkm32(s,p10,q10,n10)
mod EICASE9 { pr(ICASE9)
-- Basic predicates  
  ops bp1 bp2 bp3 : -> Bool 
  #define bp1 ::= (q10 = intruder) .
  #define bp2 ::= (enc3(q10,n10) = enc3(q,n(q,p,r))) .
  #define bp3 ::= r \in ur(s) .
-- Exhaustiveness check
  op check : -> Bool 
  eq check = bp1 or (not bp1 and not bp2) or (not bp1 and bp2 and bp3) or 
             (not bp1 and bp2 and not bp3) .
}
-- Case splitting
mod ICASE9-1 { pr(EICASE9)
  eq bp1 = true .
}
--
mod ICASE9-2 { pr(EICASE9)
  eq bp1 = false .
  eq bp2 = false .
}
--
mod ICASE9-3 { pr(EICASE9)
  eq bp1 = false .
  eq bp2 = true .
  eq bp3 = true .
}
--
mod ICASE9-4 { pr(EICASE9)
  eq bp1 = false .
  -- eq bp2 = true .
  eq q = q10 .
  eq n(q10,p,r) = n10 .
  --
  eq bp3 = 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 : inv240(init,p,q,r) .
-- II) Inductive cases
  red in ICASE1-1 : istep240(p,q,r) .
  red in ICASE1-2 : istep240(p,q,r) .
  red in ICASE2-1 : istep240(p,q,r) .
  red in ICASE2-2 : istep240(p,q,r) .
  red in ICASE3-1 : istep240(p,q,r) .
  red in ICASE3-2 : istep240(p,q,r) .
  red in ICASE3-3 : istep240(p,q,r) .
  red in ICASE3-4 : inv210(s,q,p,r) implies istep240(p,q,r) .
  red in ICASE3-5 : inv250(s,p10,p,q,r,nonce1(cipher2(m20))) implies istep240(p,q,r) .
  red in ICASE4-1 : istep240(p,q,r) .
  red in ICASE5-1 : istep240(p,q,r) .
  red in ICASE6-1 : istep240(p,q,r) .
  red in ICASE7-1 : istep240(p,q,r) .
  red in ICASE8-1 : istep240(p,q,r) .
  red in ICASE8-2 : istep240(p,q,r) .
  red in ICASE9-1 : istep240(p,q,r) .
  red in ICASE9-2 : istep240(p,q,r) .
  red in ICASE9-3 : istep240(p,q,r) .
  red in ICASE9-4 : inv210(s,q,p,r) implies istep240(p,q,r) .
-- Q.E.D.