mod* PRED-NSPK {
  inc(NSPK)
  -- declare invariants to prove
  op inv1 : System Principal Principal Principal Random Nonce -> Bool
  op inv2 : System Principal Principal Principal Random Nonce -> Bool
  op inv3 : System Message2 -> Bool
  op inv4 : System Principal Principal Nonce Random Message2 -> Bool
  op inv5 : System Nonce -> Bool
  op inv6 : System Message3 -> Bool
  op inv7 : System Principal Principal Nonce Random Message3 -> Bool
  op inv8 : System Message1 -> Bool
  op inv9 : System Nonce -> Bool
  op inv10 : System Principal Principal Random Message2 -> Bool
  op inv11 : System Principal Nonce Message1 -> Bool
  op inv12 : System Principal Nonce Nonce Message2 -> Bool
  op inv13 : System Principal Principal Principal Random Message1 -> Bool
  op inv14 : System Principal Principal Nonce Nonce -> Bool
  -- CafeOBJ variables
  var S : System
  var R : Random
  vars N N1 N2 : Nonce
  vars P Q P? Q? : Principal
  var M1 : Message1
  var M2 : Message2
  var M3 : Message3
  -- define invariants to prove
  eq inv1(S,P,Q,Q?,R,N)
     = (not(P = intruder) and
        m1(P,P,Q,enc1(Q,n(P,Q,R),P)) \in network(S) and
        m2(Q?,Q,P,enc2(P,n(P,Q,R),N)) \in network(S)
        implies
        m2(Q,Q,P,enc2(P,n(P,Q,R),N)) \in network(S)) .
  eq inv2(S,P,Q,P?,R,N)
     = (not(Q = intruder) and
        m2(Q,Q,P,enc2(P,N,n(Q,P,R))) \in network(S) and
        m3(P?,P,Q,enc3(Q,n(Q,P,R))) \in network(S)
        implies
        m3(P,P,Q,enc3(Q,n(Q,P,R))) \in network(S)) .
  eq inv3(S,M2)
     = (M2 \in network(S)
        implies
        random(nonce1(cipher2(M2))) \in rands(S) and
        random(nonce2(cipher2(M2))) \in rands(S)) .
  eq inv4(S,P,Q,N,R,M2)
     = (not(P = intruder) and not(Q = intruder) and
        m1(P,P,Q,enc1(Q,n(P,Q,R),P)) \in network(S) and
        M2 \in network(S) and cipher2(M2) = enc2(P,n(P,Q,R),N)
        implies
        m2(Q,Q,P,enc2(P,n(P,Q,R),N)) \in network(S)) .
  eq inv5(S,N)
     = (N \in nonces(S)
        implies creator(N) = intruder or forwhom(N) = intruder) .
  eq inv6(S,M3)
     = (M3 \in network(S)
        implies random(nonce(cipher3(M3))) \in rands(S)) .
  eq inv7(S,P,Q,N,R,M3)
     = (not(P = intruder) and not(Q = intruder) and
        m2(Q,Q,P,enc2(P,N,n(Q,P,R))) \in network(S) and
        M3 \in network(S) and cipher3(M3) = enc3(Q,n(Q,P,R))
        implies
        m3(P,P,Q,enc3(Q,n(Q,P,R))) \in network(S)) .
  eq inv8(S,M1)
     = (M1 \in network(S)
        implies random(nonce(cipher1(M1))) \in rands(S)) .
  eq inv9(S,N)
     = (N \in nonces(S) implies random(N) \in rands(S)) .
  eq inv10(S,P,Q,R,M2)
     = (not(P = intruder) and not(Q = intruder) and
        M2 \in network(S) and nonce2(cipher2(M2)) = n(Q,P,R)
        implies
        key(cipher2(M2)) = P) .
  eq inv11(S,P,N,M1)
     = (M1 \in network(S) and cipher1(M1) = enc1(P,N,intruder)
        implies
        creator(N) = intruder or forwhom(N) = intruder) .
  eq inv12(S,P,N1,N2,M2)
     = (M2 \in network(S) and cipher2(M2) = enc2(P,N1,N2)
        implies
        creator(N2) = intruder or forwhom(N2) = intruder) .
  eq inv13(S,P?,P,Q,R,M1)
     = (M1 \in network(S) and cipher1(M1) = enc1(P?,n(P,Q,R),P)
        implies
        P? = Q or P = intruder or n(P,Q,R) \in nonces(S)) .
  eq inv14(S,Q?,P,N1,N2)
     = (m1(P,P,intruder,enc1(intruder,N1,P)) \in network(S) and
        m2(Q?,intruder,P,enc2(P,N1,N2)) \in network(S)
        implies
        N2 \in nonces(S) or creator(N2) = intruder or forwhom(N2) = intruder) .
}

mod* BASE-NSPK {
  inc(PRED-NSPK)
  -- fresh constants
  ops s s' : -> System
  op r : -> Random
  ops n n1 n2 : -> Nonce
  ops p q p? q? : -> Principal
  op m1 : -> Message1 
  op m2 : -> Message2 
  op m3 : -> Message3 
}

mod* ISTEP-NSPK {
  inc(BASE-NSPK)
  -- declare formula to prove in inductive step
  op istep1 : -> Bool
  op istep2 : -> Bool
  op istep3 : -> Bool
  op istep4 : -> Bool
  op istep5 : -> Bool
  op istep6 : -> Bool
  op istep7 : -> Bool
  op istep8 : -> Bool
  op istep9 : -> Bool
  op istep10 : -> Bool
  op istep11 : -> Bool
  op istep12 : -> Bool
  op istep13 : -> Bool
  op istep14 : -> Bool
  -- CafeOBJ variables
  var R : Random
  vars N N1 N2 : Nonce
  vars P Q P? Q? : Principal
  var M1 : Message1
  var M2 : Message2
  var M3 : Message3
  -- define formula to prove in inductive step
  eq istep1 = inv1(s,p,q,q?,r,n) implies inv1(s',p,q,q?,r,n) .
  eq istep2 = inv2(s,p,q,p?,r,n) implies inv2(s',p,q,p?,r,n) .
  eq istep3 = inv3(s,m2) implies inv3(s',m2) .
  eq istep4 = inv4(s,p,q,n,r,m2) implies inv4(s',p,q,n,r,m2) .
  eq istep5 = inv5(s,n) implies inv5(s',n) .
  eq istep6 = inv6(s,m3) implies inv6(s',m3) .
  eq istep7 = inv7(s,p,q,n,r,m3) implies inv7(s',p,q,n,r,m3) .
  eq istep8 = inv8(s,m1) implies inv8(s',m1) .
  eq istep9 = inv9(s,n) implies inv9(s',n) .
  eq istep10 = inv10(s,p,q,r,m2) implies inv10(s',p,q,r,m2) .
  eq istep11 = inv11(s,p,n,m1) implies inv11(s',p,n,m1) .
  eq istep12 = inv12(s,p,n1,n2,m2) implies inv12(s',p,n1,n2,m2) .
  eq istep13 = inv13(s,p?,p,q,r,m1) implies inv13(s',p?,p,q,r,m1) .
  eq istep14 = inv14(s,q?,p,n1,n2) implies inv14(s',q?,p,n1,n2) .
  -- Induction Hypotheses
  -- eq inv1(s,P,Q,Q?,R,N) = true .
  -- eq inv2(s,P,Q,P?,R,N) = true .
  -- eq inv3(s,M2) = true .
  -- eq inv4(s,P,Q,N,R,M2) = true .
  -- eq inv5(s,N) = true .
  -- eq inv6(s,M3) = true .
  -- eq inv7(s,P,Q,N,R,M3) = true .
  -- eq inv8(s,M1) = true .
  -- eq inv9(s,N) = true .
  -- eq inv10(s,P,Q,R,M2) = true .
  -- eq inv11(s,P,N,M1) = true .
  -- eq inv12(s,P,N1,N2,M2) = true .
  -- eq inv13(s,P?,P,Q,R,M1) = true .
  -- eq inv14(s,Q?,P,N1,N2) = true .
}