--- Author: ic, some corrections by mos
--- Date: 10/14/03
---
--- Full Needham-Schroeder Public Key Protocol
---
---       A -> S: A, B
---       S -> A: [kB, B]kS
---       A -> B: {nA, A}kB
---       B -> S: B, A
---       S -> B: [kA, A]kS
---       B -> A: {nA, nB}kA
---       A -> B: {nB}kB

(
module protocols
export * .

msg   : type.

princ : type.                           princ  <: msg.
pubK  : princ -> type.                  pubK A <: msg.
prvK  : pubK A -> type.
verK  : princ -> type.
sigK  : verK A -> type.                 sigK k <: msg.
nonce : type.                           nonce  <: msg.

enc : pubK A -> msg -> msg.
sig : sigK k -> msg -> msg.

net : msg -> state.



module fullNSPK
import protocols * .
export * .

%% Server and its keys:

S: princ.
kS  : verK S.
kS' : sigK kS.


%% Key database

keyDB : <A: princ>pubK A -> state.


%% Initiator's role with all declarations explicit:

forall A:princ.
{
  exists L1: princ * princ -> state.
  exists L2: princ * <B: princ>pubK B * nonce -> state.

  forall B: princ.
     empty
  => net (A & B),
     L1 (A, B).

  forall B: princ.
  forall KB: pubK B.
     net (sig kS' (KB & B)),
     L1 (A, B)
  => exists nA: nonce.
     net (enc KB (nA & A)),
     L2 (A, B, KB, nA).

  forall B: princ.
  forall KB: pubK B.
  forall KA: pubK A.
  forall KA': prvK KA.
  forall NA: nonce.
  forall NB: nonce.
     net (enc KA (NA & NB)),
     L2 (A, B, KB, NA)
  => net (enc KB NB).
}

%%% Initiator role with omission of types that can be reconstructed on the
%   basis of the declarations alone.
%
%forall A.
%{
%  exists L1: princ * princ -> state.
%  exists L2: princ * <B: princ>pubK B * nonce -> state.
%
%     empty
%  => net (A & B),
%     L1 (A, B).
%
%     net (sig kS' (KB & B)),
%     L1 (A, B)
%  => exists nA.
%     net (enc KB (nA & A)),
%     L2 (A, B, KB, nA).
%
%  forall KB: pubK B.
%  forall KA: pubK A.
%  forall KA': prvK KA.
%  forall NB: nonce.
%     net (enc KA (NA & NB)),
%     L2 (A, B, KB, NA)
%  => net (enc KB NB).
%}
%
%%% Initiator role with omission of types that can be reconstructed on the
%   basis of the declarations and DAS.
%
%forall A.
%{
%  exists L1: princ * princ -> state.
%  exists L2: princ * <B: princ>pubK B * nonce -> state.
%
%     empty
%  => net (A & B),
%     L1 (A, B).
%
%     net (sig kS' (KB & B)),
%     L1 (A, B)
%  => exists nA.
%     net (enc KB (nA & A)),
%     L2 (A, B, KB, nA).
%
%  forall NB: nonce.
%     net (enc KA (NA & NB)),
%     L2 (A, B, KB, NA)
%  => net (enc KB NB).
%}


%% Responder role (with some typing information omitted):

forall B:princ.
{
  exists L1: princ * princ * nonce -> state.
  exists L2: princ * nonce -> state.

  forall KB : pubK B.
  forall KB': prvK KB.
     net (enc KB (NA & A))
  => net (B & A),
     L1 (B, A, NA).

     net (sig kS' (KA & A)),
     L1 (B, A, NA)
  => exists nB: nonce.
     net (enc KB (NA & nB)),
     L2 (B, nB).

     net (enc KB NB),
     L2 (B, NB)
  => empty.
}


%% Server role (with some typing information omitted):

for S.
{

     keyDB B KB
   ;
     net (A & B)
  => net (sig kS' (KB & B))
}
)