mod INV is
  inc CONFIG .
  ***
  op authInit : Set{OVal} Prin Prin&Intrdr Prin&Intrdr Nonce PNat -> Bool .
  op randInConfirm : Set{OVal} Prin&Intrdr Prin&Intrdr Prin&Intrdr Prin&Intrdr Nonce -> Bool .
  op ciphInConfirm : Set{OVal} Prin Prin Nonce PNat -> Bool .
  op nonSec : Set{OVal} Nonce -> Bool .
  ***
  var C : Set{OVal} .
  var P Q : Prin .
  vars PI PI' PJ PK : Prin&Intrdr .
  var N : Nonce .
  var R : PNat .
  *** authInit
  eq authInit(C,Q,PI,PI',N,R)
     = m3(PI',PI,Q,c3(Q,n(Q,PI,R))) \in msgs(C) and
       m2(Q,Q,PI,c2(PI,N,n(Q,PI,R))) \in msgs(C) 
       implies
       m3(PI,PI,Q,c3(Q,n(Q,PI,R))) \in msgs(C) .
  *** randInConfirm
  eq randInConfirm(C,PI',PI,PJ,PK,N)
     = m3(PI',PI,PJ,c3(PK,N)) \in msgs(C)
       implies
       not(rand(N) = rand(C)) .
  *** ciphInConfirm
  eq ciphInConfirm(C,P,Q,N,R)
     = m2(Q,Q,P,c2(P,N,n(Q,P,R))) \in msgs(C) and
       c3(Q,n(Q,P,R)) \in msgs(C)
       implies
       m3(P,P,Q,c3(Q,n(Q,P,R))) \in msgs(C) .
  *** nonSec
  eq nonSec(C,N)
     = N \in nonces(C)
       implies
       (gen(N) = intrdr or forWhom(N) = intrdr) .
endm