% Protocollo Otway-Rees Corretto



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
% Trudy memorizza le parti in chiaro e crittate.

rule([fresh(X)],
     [fresh(Y), agent(id(A),step1(id(B),nonce(N),nonce(NA))), 
		  net(plain(nonce(N),id(A),id(B)),enc(sk(id(A),server),tuple(nonce(NA),nonce(N),id(A),id(B)))),
			mem(nonce(N)), mem(enc(sk(id(A),server),tuple(nonce(NA),nonce(N),id(A),id(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
% Trudy memorizza le parti in chiaro e crittate.

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


% Il server risponde a Bob creando la chiave di sessione KAB: N,{Na,K_ab}_Kas,{Nb,K_ab}_Kbs
% Trudy memorizza le parti in chiaro e crittate.

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


% Bob contatta Alice terminando la sua fase del protocollo: N,{Na,K_ab}_Kas
% Trudy memorizza le parti in chiaro e crittate.

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


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

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




% Trudy usa le informazioni che ha in memoria per scrivere nuovi messaggi: crea a piacere A e B
% Scrive tre componenti in chiaro ed una crittata

rule([mem(nonce(N)), mem(enc(sk(id(K),server),Y))],
     [mem(nonce(N)), mem(enc(sk(id(K),server),Y)), 
		  net(plain(nonce(N),id(A),id(B)),enc(sk(id(K),server),Y))],
     {}, trudy_writes_a_message_on_the_net1).

% Scrive tre componenti in chiaro ed due crittate

rule([mem(nonce(N)), mem(enc(sk(id(K),server),Y)), mem(enc(sk(id(H),server),W))],
     [mem(nonce(N)), mem(enc(sk(id(K),server),Y)), mem(enc(sk(id(H),server),W)), 
		  net(plain(nonce(N),id(A),id(B)),enc(sk(id(K),server),Y),enc(sk(id(H),server),W))],
     {}, trudy_writes_a_message_on_the_net2).

% Scrive una componente in chiaro e due crittate

rule([mem(nonce(N)), mem(enc(sk(id(K),server),Y)), mem(enc(sk(id(H),server),W))],
     [mem(nonce(N)), mem(enc(sk(id(K),server),Y)), mem(enc(sk(id(H),server),W)), 
		  net(plain(nonce(N)),enc(sk(id(K),server),Y),enc(sk(id(H),server),W))],
     {}, trudy_writes_a_message_on_the_net3).    

% Scrive una componente in chiaro ed una crittata

rule([mem(nonce(N)), mem(enc(sk(id(K),server),Y))],
     [mem(nonce(N)), mem(enc(sk(id(K),server),Y)), net(plain(nonce(N)),enc(sk(id(K),server),Y))],
     {}, trudy_writes_a_message_on_the_net4).  




% Unsafe states

unsafe([  unsafe([agent(id(A),step4(id(B),key(KAB))), mem(key(KAB))], {})  
         % unsafe([agent(id(B),step3(id(A),key(KAB))), mem(key(KAB))], {})  
			]).


invariants([ 
             inv([fresh(_), fresh(_)], {}),
						 
             inv([fresh(A), net(plain(nonce(B)),_,_)], {B>A}),
						 inv([fresh(A), net(plain(nonce(B)),_)], {B>A}),
						 inv([fresh(D), net(_,_,enc(_,tuple(nonce(G),_)))], {G>D}),
						 
						 inv([fresh(A), agent(_,step1(_,nonce(H),_))], {H>A}),
						 inv([fresh(A), agent(_,step1(_,_,nonce(H)))], {H>A}),
						 
						 inv([fresh(E), mem(key(H))], {H>E}),
						 inv([fresh(E), mem(enc(_,tuple(_,key(H))))], {H>E})
	        ]).