% Protocol Otway-Rees


% Trova due attacchi type flaw:

% 1- A ---> I(B): Trudy intercetta il primo messaggio spedito da Alice a Bob: N,A,B,{Na,N,A,B}_Kas
% 2- I(B) ---> A: Trudy impersona Bob e manda ad Alice il messaggio: N,{Na,N,A,B}_Kas
% 3- Alice crede sia stato Bob a rispondendergli ed accetta (N,A,B) come chiave di sessione terminando il protocollo.


% 1- A ---> B:    Alice contatta Bob e gli manda: N,A,B,{Na,N,A,B}_Kas  
% 2- B ---> I(S): Trudy intercetta il messaggio che Bob manda al server: N,A,B,{Na,N,A,B}_Kas,{Nb,N,A,B}_Kbs  
% 3- I(S) ---> B: Trudy impersona il server e spedisce a Bob: N,{Na,N,A,B}_Kas,{Nb,N,A,B}_Kbs 
% 4- B ---> A:    Bob termina mandando ad Alice il messaggio: N,{Na,N,A,B}_Kas   



init(K,L) :- f(K,WM,_,L,_,_),
             \+(member(agent(_,step1(_,_,_)),WM)),
             \+(member(agent(_,step2(_,_,_)),WM)),
             \+(member(agent(_,step3(_,_)),WM)),
             \+(member(agent(_,step4(_,_)),WM)),
             \+(member(net(_,_),WM)),
             \+(member(net(_,_,_),WM)),
             \+(member(mem(_),WM)),
             nl.



% Alice contatta Bob e gli manda: N,A,B,{Na,N,A,B}_Kas

rule([fresh(X)],
     [fresh(Y), agent(A,step1(B,nonce(N),NA)),
		  net(plain(cons(nonce(N),cons(A,B))),enc(sk(A,server),cons(NA,cons(nonce(N),cons(A,B))))),
			mem(plain(cons(nonce(N),cons(A,B)))),
		  mem(plain(nonce(N))), mem(plain(cons(A,B))), 
			mem(plain(A)), mem(plain(B)), %%%%%%% aggiunte
		  mem(enc(sk(A,server),cons(NA,cons(nonce(N),cons(A,B)))))],
     {Y>NA, NA>N, N>X}, alice_starts_protocol_with_Bob_(rule1)).


% Bob ha ricevuto la richiesta di inizio del protocollo e contatta il server spedendo il messaggio:
% N,A,B,{Na,N,A,B}_Kas,{Nb,N,A,B}_Kbs

rule([net(plain(cons(nonce(N),cons(A,B))),enc(sk(A,server),cons(NA,cons(nonce(N),cons(A,B))))), fresh(X)],
     [agent(B,step2(A,nonce(N),NB)), fresh(Y),
      net(plain(cons(nonce(N),cons(A,B))),enc(sk(A,server),cons(NA,cons(nonce(N),cons(A,B)))),enc(sk(B,server),cons(NB,cons(nonce(N),cons(A,B))))),
			mem(plain(cons(nonce(N),cons(A,B)))),
      mem(plain(nonce(N))), mem(plain(cons(A,B))), 
			mem(plain(A)), mem(plain(B)), %%%%%%% aggiunte
		  mem(enc(sk(A,server),cons(NA,cons(nonce(N),cons(A,B))))), 
			mem(enc(sk(B,server),cons(NB,cons(nonce(N),cons(A,B)))))],
     {Y>NB, NB>X}, bob_sends_a_message_to_server_(rule2)).


% Il server risponde a Bob: N,{Na,K_ab}_Kas,{Nb,K_ab}_Kbs

rule([net(plain(cons(nonce(N),cons(A,B))),enc(sk(A,server),cons(NA,cons(nonce(N),cons(A,B)))),enc(sk(B,server),cons(NB,cons(nonce(N),cons(A,B))))),
      fresh(X)],
     [net(plain(nonce(N)),enc(sk(A,server),cons(NA,KAB)),enc(sk(B,server),cons(NB,KAB))),
		  mem(plain(nonce(N))), mem(enc(sk(A,server),cons(NA,KAB))), mem(enc(sk(B,server),cons(NB,KAB)))],
     {}, server_sends_Kab_to_Bob_(rule3)).


% Bob contatta Alice terminando la sua fase del protocollo: N,{Na,K_ab}_Kas

rule([net(plain(nonce(N)),enc(sk(A,server),cons(NA,KAB)),enc(sk(B,server),cons(NB,KAB))), agent(B,step2(A,nonce(N),NB))],
     [agent(B,step3(A,KAB)), net(plain(nonce(N)),enc(sk(A,server),cons(NA,KAB))),
		  mem(plain(nonce(N))), mem(enc(sk(A,server),cons(NA,KAB)))],
     {}, bob_sends_Kab_to_Alice_(rule4)).


% Alice ha ricevuto la chiave di sessione e termina il protocollo

rule([net(plain(nonce(N)),enc(sk(A,server),cons(NA,KAB))), agent(A,step1(B,nonce(N),NA))],
     [agent(A,step4(B,KAB))],
     {}, alice_received_Kab_and_ends_protocol_(rule5)).


% Questa regola fa esplodere gli stati
%rule([mem(plain(X)), mem(plain(Y))],
%     [mem(plain(X)), mem(plain(Y)), mem(plain(cons(X,Y)))],
%     {}, trudy_create_a_message).


% Trudy usa le informazioni che ha in memoria per creare nuovi messaggi (una sola componente crittata)
% e metterli sulla rete

rule([mem(plain(X)), mem(enc(sk(K,server),Y))],
     [mem(plain(X)), mem(enc(sk(K,server),Y)), net(plain(X),enc(sk(K,server),Y))],
     {}, trudy_writes_a_message_on_the_net1).


% Trudy usa le informazioni che ha in memoria per creare nuovi messaggi (due componenti crittate) 
% e metterli sulla rete

rule([mem(plain(X)), mem(enc(sk(K,server),Y)), mem(enc(sk(H,server),W))],
     [mem(plain(X)), mem(enc(sk(K,server),Y)), mem(enc(sk(H,server),W)), net(plain(X),enc(sk(K,server),Y),enc(sk(H,server),W))],
     {}, trudy_writes_a_message_on_the_net2).    



% Unsafe states

unsafe([    unsafe([agent(A,step4(B,KAB)), mem(plain(KAB))], {})  % Trova il primo attacco
          % unsafe([agent(B,step3(A,KAB)), mem(plain(KAB))], {})  % Trova il secondo attacco
			]).


invariants([ inv([fresh(X), fresh(Y)], {}),

             inv([agent(_,step2(_,cons(_,_),_))], {}),
             inv([agent(_,step1(_,cons(_,_),_))], {}),
						 
             inv([fresh(A),net(_,enc(_,cons(B,_)))], {B-A>0}),
             inv([fresh(A), agent(_,step1(_,_,E))], {E-A>0}),
             inv([fresh(A), agent(_,step2(_,_,E))], {E-A>0})
 ]).