module security.
% A model for the Needham-Schroeder Public-Key Security Protocol
% [Needham-Schroeder 78]

kind principal type.

type alice A -> principal. 

type bob   A -> principal.

type trudy A -> principal.

type nomsg principal.

type c     A -> B -> C. 

type knows_key principal -> Msg -> o.

type knows     principal -> Msg -> o.

type keypair (A -> principal) -> SecretKey -> PublicKey -> o.

type announce PublicKey -> o.

type enc K -> M -> N. 

type state principal -> principal ->  principal -> principal -> list A -> o.

type go o.


% A -> B: Na

state   (alice 0) Bob     Network     Intruder  History:-
  announce PK,
  keypair alice SKA PKA,
  pi Na\ 
      (knows (alice 0) Na) => 
        (knows (alice 0) PK) => 
	     (term_to_string (enc PK (c Na PKA)) S,
	      state (alice 1) Bob (enc PK (c Na PKA))  Intruder (S::("A sends to B")::History)).

% B -> A: Na,Nb
  
state    Alice    (bob 0) (enc PK (c Na PKA)) Intruder History:-
   keypair bob SK PK,
   announce PKA,
   pi Nb \ 
    (knows (bob 0) Na) =>
      (knows (bob 1) Nb) =>
        (knows (bob 0) PKA) => 
         (term_to_string (enc PKA (c Na Nb)) S,
	  state  Alice  (bob 1) (enc PKA (c Na Nb)) Intruder (S::("B sends to A")::History)).

% A -> B: Nb

state   (alice 1) Bob       (enc PKA (c Na Nb)) Intruder History:-
  keypair alice SK PKA,
  knows (alice 0) Na,
  knows (alice 0) PKB,  
  ((knows (alice 1) Nb) =>
     (term_to_string (enc PKB Nb) S,
      state (alice 2) Bob   (enc PKB Nb)  Intruder (S::("A sends to B")::History))).

type  print_reverse list A -> o.

print_reverse (A::N):-
 print_reverse N,
 term_to_string A T,
 print "\n", 
 print T.
 
print_reverse nil.

% B: receives Nb

state    Alice    (bob 1)   (enc PK Nb) Intruder History :-
   keypair bob SK PK,
   knows (bob 1) Nb,
   knows (alice 0) Na,
   knows (trudy Any) Nb,
   knows (trudy Any1) Na,
   print "\n\nProtocol terminated successfully, however Trudy knows Na and Nb",
   print "\nTraccia:",
   print_reverse ("Bob recognizes the nonce"::History),
   read _.
   

% Intruder

 
type chooseMsgKey principal -> principal ->  principal -> Key -> list A -> o. 
type chooseMsgMsg principal -> principal ->  principal -> Key -> list A -> o. 

chooseMsgKey Alice Bob Trudy PK History:-
   knows_key (trudy 0) K,
   knows     (trudy 0) M,
   term_to_string  (enc PK (c M K)) S,
   state Alice Bob (enc PK (c M K)) Trudy (S::"[trudy] "::History). 
 
chooseMsgMsg Alice Bob Trudy PK History:-
   knows     (trudy 0) M1,
   knows     (trudy 0) M2,
   term_to_string  (enc PK (c M1 M2)) S,
   state Alice Bob (enc PK (c M1 M2)) Trudy (S::"[trudy] "::History). 
 

state  Alice Bob (enc PK (c M1 M2)) (trudy 0) History:-
 keypair trudy SK PK,
 announce PKB,
 pi Nt \
 ((knows_key (trudy 0) PK)   =>
  (knows_key (trudy 0) PKB)  =>
  (knows_key (trudy 0) M2)   =>
  (knows     (trudy 0) M1)   => 
  (knows     (trudy 0) Nt)   =>
  (chooseMsgKey Alice Bob (trudy 1) PKB History)).
   

state  Alice Bob (enc PK (c M1 M2)) (trudy 1) History:-
 keypair trudy SK PK,
 knows_key (trudy 0) PKA,
 ((knows (trudy 0) M1) => 
  (knows (trudy 0) M2) =>
  (chooseMsgMsg Alice Bob (trudy 2) PKA History)).
  
 
state  Alice Bob (enc PK M) (trudy 2) History:-
 keypair trudy SK PK,
 knows_key (trudy 0) PKB,
 (knows    (trudy 0) M)      => 
   (term_to_string (enc PKB M) S,
    state Alice Bob (enc PKB M) (trudy 3) 
        (S::("[trudy] ")::History)).  


go:- 
    (
    pi PKA \ pi SKA \ pi PKB \ pi SKB \ pi PKT \ pi SKT \    
    keypair trudy SKT PKT   =>
     keypair alice SKA PKA  =>
      keypair bob   SKB PKB =>
       announce PKB         => 
        announce PKA        => 
	  announce PKT      => 
            state (alice 0) (bob 0) nomsg (trudy 0) nil), 
    fail.