--
-- Needham-Schroeder-Lowe Public-Key Authentication Protocol
-- (NSLPK Protocol)
--
-- 1. Init p --> q : E_q(n_p, p)
-- 2. Resp q --> p : E_p(n_p, n_q, q)
-- 3. Ack  p --> q : E_q(n_q)
--

--
-- One of the principals is the intruder denoted by constant intruder.
--
mod* PRINCIPAL principal-sort Principal {
  [Principal]
  op intruder : -> Principal
  op _=_ : Principal Principal -> Bool {comm}
  var P : Principal
  eq (P = P) = true .
}

--
-- Unguessable random numbers for nonces
--
mod* RANDOM principal-sort Random {
  [Random]
  op _=_ : Random Random -> Bool {comm}
  var R : Random
  eq (R = R) = true .
}

--
-- Given principals p,q and random value r, term n(p,q,r) denotes a
-- nonce created by principal p for authenticating p to principal q,
-- where r makes the nonce globally unique and unguessable.
--
mod* NONCE principal-sort Nonce {
  inc(PRINCIPAL)
  inc(RANDOM)
  [Nonce]
  op n : Principal Principal Random -> Nonce {constr}
  op creator : Nonce -> Principal
  op forwhom : Nonce -> Principal
  op random : Nonce -> Random
  op _=_ : Nonce Nonce -> Bool {comm}
  vars N1 N2 : Nonce
  var C : Principal
  var W : Principal
  var R : Random
  eq creator(n(C,W,R)) = C .
  eq forwhom(n(C,W,R)) = W .
  eq random(n(C,W,R)) = R .
  eq (N1 = N2)
     = (creator(N1) = creator(N2) and forwhom(N1) = forwhom(N2) and
        random(N1) = random(N2)) .
}

--
-- Given principals p,q and nonce n_p, term enc1(q,n_p,p) denotes
-- cipher E_q(n_p, p), nonce n_p and principal p encrypted with
-- the principal q's public key.
--
mod* CIPHER1 principal-sort Cipher1 {
  inc(PRINCIPAL)
  inc(NONCE)
  [Cipher1]
  op enc1 : Principal Nonce Principal -> Cipher1 {constr}
  op key : Cipher1 -> Principal
  op nonce : Cipher1 -> Nonce
  op principal : Cipher1 -> Principal
  op _=_ : Cipher1 Cipher1 -> Bool {comm}
  vars E11 E12 : Cipher1
  var K : Principal
  var N : Nonce 
  var P : Principal
  eq key(enc1(K,N,P)) = K .
  eq nonce(enc1(K,N,P)) = N .
  eq principal(enc1(K,N,P)) = P .
  eq (E11 = E12)
     = (key(E11) = key(E12) and nonce(E11) = nonce(E12) and
        principal(E11) = principal(E12)) .
}

--
-- Given principals p,q and nonces n_p,n_q term enc2(p,n_p,n_q,q)
-- denotes cipher E_p(n_p, n_q, q), nonces n_p,n_q and principal q
-- encrypted with the principal p's public key.
--
mod* CIPHER2 principal-sort Cipher2 {
  inc(PRINCIPAL)
  inc(NONCE)
  [Cipher2]
  op enc2 : Principal Nonce Nonce Principal -> Cipher2 {constr}
  op key : Cipher2 -> Principal
  op nonce1 : Cipher2 -> Nonce
  op nonce2 : Cipher2 -> Nonce
  op principal : Cipher2 -> Principal
  op _=_ : Cipher2 Cipher2 -> Bool {comm}
  vars E21 E22 : Cipher2
  var K : Principal
  var N1 : Nonce
  var N2 : Nonce
  var P : Principal
  eq key(enc2(K,N1,N2,P)) = K .
  eq nonce1(enc2(K,N1,N2,P)) = N1 .
  eq nonce2(enc2(K,N1,N2,P)) = N2 .
  eq principal(enc2(K,N1,N2,P)) = P .
  eq (E21 = E22)
     = (key(E21) = key(E22) and nonce1(E21) = nonce1(E22) and
        nonce2(E21) = nonce2(E22) and principal(E21) = principal(E22)) .
}

--
-- Given principals p,q and nonce n_p, term enc1(q,n_p,p) denotes
-- cipher E_q(n_p, p), nonce n_p and principal p encrypted with
-- the principal q's public key.
--
mod* CIPHER3 principal-sort Cipher3 {
  inc(PRINCIPAL)
  inc(NONCE)
  [Cipher3]
  op enc3 : Principal Nonce -> Cipher3 {constr}
  op key : Cipher3 -> Principal
  op nonce : Cipher3 -> Nonce
  op _=_ : Cipher3 Cipher3 -> Bool {comm}
  vars E31 E32 : Cipher3
  var K : Principal
  var N : Nonce
  eq key(enc3(K,N)) = K .
  eq nonce(enc3(K,N)) = N .
  eq (E31 = E32) = (key(E31) = key(E32) and nonce(E31) = nonce(E32)) .
}

--
-- Given principals c,s,r and cipheri ei (i = 1,2,3),
-- mi(c,s,r,ei) denotes a message created by principal c,
-- but it seems to be sent by principal s to principal r.
--
-- c may be the intruder, and c may be different from s.
-- If c is different from s, then c must be the intruder
-- and the message is faked by the intruder. 
--
mod* MESSAGE principal-sort Message {
  inc(CIPHER1)
  inc(CIPHER2)
  inc(CIPHER3)
  [Message1 Message2 Message3 < Message]
  --      creator   sender    receiver
  --    --------------------------------------------------
  op m1 : Principal Principal Principal Cipher1 -> Message1 {constr}
  op m2 : Principal Principal Principal Cipher2 -> Message2 {constr}
  op m3 : Principal Principal Principal Cipher3 -> Message3 {constr}
  --
  op creator : Message -> Principal
  op sender : Message -> Principal
  op receiver : Message -> Principal
  op cipher1 : Message1 -> Cipher1
  op cipher2 : Message2 -> Cipher2
  op cipher3 : Message3 -> Cipher3
  --
  op _=_ : Message Message -> Bool {comm}
  --
  var M : Message
  vars M11 M12 : Message1
  vars M21 M22 : Message2
  vars M31 M32 : Message3
  vars C S R : Principal
  var E1 : Cipher1
  var E2 : Cipher2
  var E3 : Cipher3
  --
  eq creator(m1(C,S,R,E1)) = C .
  eq creator(m2(C,S,R,E2)) = C .
  eq creator(m3(C,S,R,E3)) = C .
  eq sender(m1(C,S,R,E1)) = S .
  eq sender(m2(C,S,R,E2)) = S .
  eq sender(m3(C,S,R,E3)) = S .
  eq receiver(m1(C,S,R,E1)) = R .
  eq receiver(m2(C,S,R,E2)) = R .
  eq receiver(m3(C,S,R,E3)) = R .
  eq cipher1(m1(C,S,R,E1)) = E1 .
  eq cipher2(m2(C,S,R,E2)) = E2 .
  eq cipher3(m3(C,S,R,E3)) = E3 .
  --
  eq (M = M) = true .
  eq (M11 = M12)
     = (creator(M11) = creator(M12) and sender(M11) = sender(M12) and
        receiver(M11) = receiver(M12) and cipher1(M11) = cipher1(M12)) .
  eq (M21 = M22)
     = (creator(M21) = creator(M22) and sender(M21) = sender(M22) and
        receiver(M21) = receiver(M22) and cipher2(M21) = cipher2(M22)) .
  eq (M31 = M32)
     = (creator(M31) = creator(M32) and sender(M31) = sender(M32) and
        receiver(M31) = receiver(M32) and cipher3(M31) = cipher3(M32)) .
  eq (M11 = M21) = false .
  eq (M11 = M31) = false .
  eq (M21 = M31) = false .
}

--
-- Formal parameter for the following prameterized module.
--
mod* EQTRIV principal-sort Elt {
  [Elt]
  op _=_ : Elt Elt -> Bool {comm}
  eq (E:Elt = E) = true .
}

--
-- Generic bags (multisets)
--
mod* BAG (D :: EQTRIV) principal-sort Bag {
  [Elt.D < Bag]
  op empty : -> Bag {constr}
  op _ _ : Bag Bag -> Bag {constr assoc comm id: empty}
  op _\in_ : Elt.D Bag -> Bool
  var S : Bag
  vars E1 E2 : Elt.D
  --
  eq E1 \in empty = false .
  eq E1 \in (E2 S) = (E1 = E2) or E1 \in S .
}

--
-- The baheviors of NSLPK
--
mod* NSLPK {
  inc(BAG(MESSAGE)*{sort Bag -> Network})
  inc(BAG(NONCE)*{sort Bag -> NonceBag})
  inc(BAG(RANDOM)*{sort Bag -> RandBag})
  [System]
  -- an arbitrary initial state
  op init : -> System {constr}
  -- observers
  op network : System -> Network      -- Network (bags of messages)
  op rands : System -> RandBag        -- used random numbers
  op nonces : System -> NonceBag      -- nonces gleaned by the intruder
  -- transitions
  -- sending messages according to the protocol
  op sdm1 : System Principal Principal Random -> System {constr}
  op sdm2 : System Principal Principal Principal
                                 Random Nonce -> System {constr}
  op sdm3 : System Principal Principal Principal
                                  Nonce Nonce -> System {constr}
  -- faking messages based on the gleaned info
  op fkm11 : System Principal Principal Message1    -> System {constr}
  op fkm12 : System Principal Principal Nonce       -> System {constr}
  op fkm21 : System Principal Principal Message2    -> System {constr}
  op fkm22 : System Principal Principal Nonce Nonce -> System {constr}
  op fkm31 : System Principal Principal Message3    -> System {constr}
  op fkm32 : System Principal Principal Nonce       -> System {constr}
  -- CafeOBJ variables
  var S : System
  vars P Q Q? : Principal
  var R : Random
  vars N N1 N2 : Nonce
  var M1 : Message1
  var M2 : Message2
  var M3 : Message3
  -- init
  eq network(init) = empty .
  eq rands(init) = empty .
  eq nonces(init) = empty .
  -- sdm1
  op c-sdm1 : System Principal Principal Random -> Bool
  eq c-sdm1(S,P,Q,R) = not(R \in rands(S)) .
  --
  ceq network(sdm1(S,P,Q,R))  = m1(P,P,Q,enc1(Q,n(P,Q,R),P)) network(S)
      if c-sdm1(S,P,Q,R) .
  ceq rands(sdm1(S,P,Q,R))    = R rands(S) if c-sdm1(S,P,Q,R) .
  ceq nonces(sdm1(S,P,Q,R))
      = (if Q = intruder then n(P,Q,R) nonces(S) else nonces(S) fi)
      if c-sdm1(S,P,Q,R) .
  ceq sdm1(S,P,Q,R)           = S if not c-sdm1(S,P,Q,R) .
  -- sdm2
  op c-sdm2 : System Principal Principal Principal Random Nonce -> Bool
  eq c-sdm2(S,Q?,P,Q,R,N)
     = (m1(Q?,Q,P,enc1(P,N,Q)) \in network(S) and not(R \in rands(S))) .
  --
  ceq network(sdm2(S,Q?,P,Q,R,N))  = m2(P,P,Q,enc2(Q,N,n(P,Q,R),P)) network(S)
      if c-sdm2(S,Q?,P,Q,R,N) .
  ceq rands(sdm2(S,Q?,P,Q,R,N))    = R rands(S) if c-sdm1(S,P,Q,R) .
  ceq nonces(sdm2(S,Q?,P,Q,R,N))
      = (if Q = intruder then N n(P,Q,R) nonces(S) else nonces(S) fi)
      if c-sdm2(S,Q?,P,Q,R,N) .
  ceq sdm2(S,Q?,P,Q,R,N)           = S if not c-sdm2(S,Q?,P,Q,R,N) .
  -- sdm3
  op c-sdm3 : System Principal Principal Principal Nonce Nonce -> Bool
  eq c-sdm3(S,Q?,P,Q,N1,N2) = m1(P,P,Q,enc1(Q,N1,P)) \in network(S) and
                              m2(Q?,Q,P,enc2(P,N1,N2,Q)) \in network(S) .
  --
  ceq network(sdm3(S,Q?,P,Q,N1,N2))  = m3(P,P,Q,enc3(Q,N2)) network(S)
      if c-sdm3(S,Q?,P,Q,N1,N2) .
   eq rands(sdm3(S,Q?,P,Q,N1,N2))    = rands(S) .
  ceq nonces(sdm3(S,Q?,P,Q,N1,N2))
      = (if Q = intruder then N2 nonces(S) else nonces(S) fi)
      if c-sdm3(S,Q?,P,Q,N1,N2) .
  ceq sdm3(S,Q?,P,Q,N1,N2)           = S if not c-sdm3(S,Q?,P,Q,N1,N2) .
  -- fkm11
  op c-fkm11 : System Principal Principal Message1 -> Bool
  eq c-fkm11(S,P,Q,M1) = M1 \in network(S) .
  --
  ceq network(fkm11(S,P,Q,M1))  = m1(intruder,P,Q,cipher1(M1)) network(S)
      if c-fkm11(S,P,Q,M1) .
   eq rands(fkm11(S,P,Q,M1))    = rands(S) .
   eq nonces(fkm11(S,P,Q,M1))   = nonces(S) .
  ceq fkm11(S,P,Q,M1)           = S if not c-fkm11(S,P,Q,M1) .
  -- fkm12
  op c-fkm12 : System Principal Principal Nonce -> Bool
  eq c-fkm12(S,P,Q,N) = N \in nonces(S) .
  --
  ceq network(fkm12(S,P,Q,N))  = m1(intruder,P,Q,enc1(Q,N,P)) network(S)
      if c-fkm12(S,P,Q,N) .
   eq rands(fkm12(S,P,Q,N))    = rands(S) .
   eq nonces(fkm12(S,P,Q,N))   = nonces(S) .
  ceq fkm12(S,P,Q,N)           = S if not c-fkm12(S,P,Q,N) .
  -- fkm21
  op c-fkm21 : System Principal Principal Message2 -> Bool
  eq c-fkm21(S,P,Q,M2) = M2 \in network(S) .
  --
  ceq network(fkm21(S,P,Q,M2))  = m2(intruder,P,Q,cipher2(M2)) network(S)
      if c-fkm21(S,P,Q,M2) .
   eq rands(fkm21(S,P,Q,M2))    = rands(S) .
   eq nonces(fkm21(S,P,Q,M2))   = nonces(S) .
  ceq fkm21(S,P,Q,M2)           = S if not c-fkm21(S,P,Q,M2) .
  -- fkm22
  op c-fkm22 : System Principal Principal Nonce Nonce -> Bool
  eq c-fkm22(S,P,Q,N1,N2) = N1 \in nonces(S) and N2 \in nonces(S) .
  --
  ceq network(fkm22(S,P,Q,N1,N2))  = m2(intruder,P,Q,enc2(Q,N1,N2,P)) network(S)
      if c-fkm22(S,P,Q,N1,N2) .
   eq rands(fkm22(S,P,Q,N1,N2))    = rands(S) .
   eq nonces(fkm22(S,P,Q,N1,N2))   = nonces(S) .
  ceq fkm22(S,P,Q,N1,N2)           = S if not c-fkm22(S,P,Q,N1,N2) .
  -- fkm31
  op c-fkm31 : System Principal Principal Message3 -> Bool
  eq c-fkm31(S,P,Q,M3) = M3 \in network(S) .
  --
  ceq network(fkm31(S,P,Q,M3))  = m3(intruder,P,Q,cipher3(M3)) network(S)
      if c-fkm31(S,P,Q,M3) .
   eq rands(fkm31(S,P,Q,M3))    = rands(S) .
   eq nonces(fkm31(S,P,Q,M3))   = nonces(S) .
  ceq fkm31(S,P,Q,M3)           = S if not c-fkm31(S,P,Q,M3) .
  -- fkm32
  op c-fkm32 : System Principal Principal Nonce -> Bool
  eq c-fkm32(S,P,Q,N) = N \in nonces(S) .
  --
  ceq network(fkm32(S,P,Q,N))  = m3(intruder,P,Q,enc3(Q,N)) network(S)
      if c-fkm32(S,P,Q,N) .
   eq rands(fkm32(S,P,Q,N))    = rands(S) .
   eq nonces(fkm32(S,P,Q,N))   = nonces(S) .
  ceq fkm32(S,P,Q,N)           = S if not c-fkm32(S,P,Q,N) .
}