% ASLAN/IF model for On-the-Fly Execution (PRESTO) protocol
% test the model with the following command line: 
% cl-atse_i686-windows.exe --of if --lvl 1 -f avispa_if_exec.aslan

section signature:

state_adv: agent * nat * nat -> fact

state_usr: nat * agent * message * message * message  * message * message -> fact
state_car: nat * agent * message * message * message-> fact

grant_access: agent * message * message * message -> fact
sent_mac_response: nat -> fact
send_mac_request: agent * nat * nat -> fact


bind: agent * agent * message * nat -> fact
accept: agent * agent * message * nat -> fact
send: agent * message -> fact
inv: message -> message
reach: agent -> fact
flag: message -> fact

section types:

i, X, usr, car, A: agent
0,1,2,3,4,5,6,7,8,9,10,11,12,13, 14, 15: nat
SID, KSES, ACT, Role, Atr, open, start, role: message
sid, kses, act, sid1, sid2, sid3, sid4: message
hash: function
NC, NU: nonce
PkUsr, PkCarE, PkCar: public_key

section inits:
 initial_state init1 :=

iknows(i).
iknows(usr).
iknows(car).
iknows(open).
iknows(start).
%iknows(kses).

 
% allow the adversary i to start the protocol with the car 
state_car(0, i, sid, kses, open).
state_car(0, i, sid, kses, start).
state_car(0, i, sid, kses, open).
state_car(0, i, sid, kses, start)

% alternatively one can allow the user usr to start the protocol with the car 
%state_car(0, usr, sid, kses, open).
%state_car(0, usr, sid, kses, start).
%state_usr(0, usr, role, atr, sid, kses, open).
%state_usr(0, usr, role, atr, sid, kses, start)

%section hornClauses:

section rules:

%send request from user to car
step trans1(X, SID, KSES, ACT, Role, Atr, PkUsr):=
state_usr(0, X, Role, Atr, SID, KSES, ACT)
=[exists NU] => 
iknows(pair(NU, pair(Role, Atr))).
iknows(crypt(inv(PkUsr), pair(NU, pair(Role, Atr)))).
state_usr(1, X, Role, Atr, SID, KSES, ACT)

%car responds with challenge to user
step trans2(X, SID, KSES, ACT, Role, Atr, PkUsr, PkCarE, PkCar, NU):=
state_car(0, X, SID, KSES, ACT)
=[exists NC] => 
iknows(pair(PkCarE, pair(NC, pair(SID , crypt(inv(PkUsr), pair(NU, pair(Role, Atr))))))).
iknows(crypt(inv(PkCar), pair(PkCarE, pair(NC, pair(SID , crypt(inv(PkUsr), pair(NU, pair(Role, Atr)))))))).
state_car(1, X, SID, KSES, ACT)

% user responds to car
step trans3(X, SID, KSES, ACT, Role, Atr, NC, NU, PkUsr, PkCar, PkCarE):=
state_usr(1, X, Role, Atr, SID, KSES, ACT)
=> 
iknows(crypt(PkCar, KSES)).
iknows(scrypt(KSES, pair(ACT, crypt(inv(PkCar), pair(PkCarE, pair(NC, pair(SID , crypt(inv(PkUsr), pair(NU, pair(Role, Atr)))))))))).
state_usr(2, X, Role, Atr, SID, KSES, ACT)

% car grants access
step trans2(X, SID, KSES, ACT, Role, Atr, PkUsr, PkCarE, PkCar, NU, NC):=
state_car(1, X, SID, KSES, ACT).
iknows(scrypt(KSES, pair(ACT, crypt(inv(PkCar), pair(PkCarE, pair(NC, pair(SID , crypt(inv(PkUsr), pair(NU, pair(Role, Atr))))))))))
=> 
state_car(2, X, SID, KSES, ACT)


section goals:
   %checks that the adversary cannot start the car
   attack_state grant_access(A, SID, KSES, ACT) := state_car(2, i, SID, KSES, open)
   %attack_state grant_access(A, SID, KSES, ACT) := state_car(2, i, SID, KSES, start)
   %alternatively on can check that the user can open or start the car, also uncomment user facts at lines 40-43
   %attack_state grant_access(A, SID, KSES, ACT) := state_car(2, usr, SID, KSES, start)
   %attack_state grant_access(A, SID, KSES, ACT) := state_car(2, usr, SID, KSES, open)