mod! INV {
  inc(CONFIG)
  op check : Bool Bool -> Bool
  --
  op isValid : Config -> Bool
  op nonSec : Config Nonce -> Bool
  op nonInCiph1 : Config Cipher1 -> Bool
  op nonInCiph2 : Config Cipher2 -> Bool
  --
  vars C C' : Config
  var N : Nonce
  var NS : NonceSet
  vars LEMS F2P : Bool
  var CIPH1 : Cipher1
  var CIPH2 : Cipher2
  -- check
  -- LEMS is lemmas and induction hypotheses, and
  -- F2P is a formula to prove
  eq check(LEMS,F2P)
     = if (LEMS implies F2P) == true
       then true else false fi .
  -- isValid
  eq isValid(C) 
     = (#nw(C) = s(z)) and (#rand(C) = s(z)) and
       (#nonces(C) = s(z)) and (#prins(C) = s(z)) .
  -- nonSec
  eq nonSec(C,N)
     = N \in nonces(C)
       implies
       (gen(N) = intrdr or forWhom(N) = intrdr) .
  -- nonInCiph1
  eq nonInCiph1(C,CIPH1)
     = (CIPH1 \in msgs(C) and gen(CIPH1) = intrdr)
       implies
       (gen(non(CIPH1)) = intrdr or forWhom(non(CIPH1)) = intrdr) .
  -- nonInCiph2
  eq nonInCiph2(C,CIPH2)
     = (CIPH2 \in msgs(C) and gen(CIPH2) = intrdr)
       implies
       (gen(non(CIPH2)) = intrdr or forWhom(non(CIPH2)) = intrdr) .
}