mod! INV {
  inc(CONFIG)
  op nonSec : Config Nonce -> Bool
  --
  var C : Config
  var N : Nonce
  -- nonSec
  eq nonSec(C,N)
     = N \in nonces(C)
       implies
       (gen(N) = intrdr or forWhom(N) = intrdr) .
}