
initiator(A,B,Na,Klt,Kst,[ 
   send([pk(A),[Na,[pk(A),B]+Klt]]),
   recv([Kst*pk(A),[sha(Kst),[A,Na]]+Klt]),
   end(A,B,init,Na,Klt,Kst)
 ]).

responder(A,B,Na,Klt,Kst,[
   recv([pk(A),[Na,[pk(A),B]+Klt]]),
   send([Kst*pk(A),[sha(Kst),[A,Na]]+Klt]),
   end(A,B,init,Na,Klt,Kst)
 ]).

leak(X,[send(X)]).

ik([a,b,e]).

% perfect forward secrecy
scenario([[a,Init1],[b,Resp1],[l,Leak]],
              all(A,all(B,all(N,all(Klt,learn(Klt) and yest (once ([_,end(A,B,init,N,Klt,kst)] and neg learn(kst))) 
                    imp neg learn(kst)))))
             ) :-
   initiator(a,b,na,klt,Kst,Init1),
   responder(a,b,Na,klt,kst,Resp1),
   leak(klt,Leak). 
                         

