% 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_otf_exec.aslan

section signature:

state_adv: agent * nat * nat -> fact
state_usr: nat * agent * message * message * message * nonce -> fact
state_car: nat * agent * message * message * message * nonce -> fact
grant_access: agent * message * message * message -> fact


section types:

i, X, usr, car, A: agent
MAC: nat
0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15: nat
SID, KSES, ACT, open, start: message
sid, kses, act: message
NC, nc: nonce

section inits:
 initial_state init1 :=

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


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

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

% horn clauses not needed
%section hornClauses:

section rules:

%send request from user to car
step trans1(X, SID, KSES, ACT, NC):=
state_usr(0, X, SID, KSES, ACT, nc)
=> 
iknows(SID).
iknows(scrypt(KSES, ACT)).
iknows(scrypt(KSES, pair(SID, scrypt(KSES, ACT)))).
state_usr(1, X, SID, KSES, ACT, nc)

%car responds with challenge to user
step trans2(X, SID, KSES, ACT, NC):=
state_car(0, X, SID, KSES, ACT, nc)
=[exists NC] => 
iknows(pair(NC, scrypt(KSES, pair(SID, ACT)))).
iknows(scrypt(KSES, pair(NC, scrypt(KSES, pair(SID, ACT))))).
state_car(1, X, SID, KSES, ACT, NC)

% user responds to car
step trans3(X, SID, KSES, ACT, NC):=
state_usr(1, X, SID, KSES, ACT, nc).
iknows(pair(NC, scrypt(KSES, pair(SID, ACT)))).
iknows(scrypt(KSES, pair(NC, scrypt(KSES, pair(SID, ACT)))))
=> 
iknows(scrypt(KSES, scrypt(KSES, pair(NC, scrypt(KSES, pair(SID, ACT)))))).
state_usr(2, X, SID, KSES, ACT, NC)

% car grants access
step trans4(X, SID, KSES, ACT, NC):=
state_car(1, X, SID, KSES, ACT, NC).
iknows(scrypt(KSES, scrypt(KSES, pair(NC, scrypt(KSES, pair(SID, ACT))))))
=> 
state_car(2, X, SID, KSES, ACT, NC)


section goals:
   %checks that the adversary cannot start the car
   attack_state grant_access(A, SID, KSES, ACT, NC) := state_car(2, i, SID, KSES, start, NC)
   %checks that the adversary cannot open the car
   %attack_state grant_access(A, SID, KSES, ACT, NC) := state_car(2, i, SID, KSES, open, NC)
   %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, NC) := state_car(2, usr, SID, KSES, open, NC)
   %attack_state grant_access(A, SID, KSES, ACT, NC) := state_car(2, usr, SID, KSES, start, NC)