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