help translating my protocol into Tamarin

[Hossein Geranfar]

Hello dears

I'm new to Tamarin and working on my thesis, trying to verify a protocol with Tamarin bug  I faced with numerous errors...would you plz help to translate my protocol in tamarin language?

I don't know exactly which part should be put in premise and which one to the conclusion? below is my written code

thanks a bunch

/*
* Author: Hossein
* Model Name:
* Status: DEVELOPMENTAL
*
* Comments:
*/


theory Thesis
begin


builtins: hashing, xor, asymmetric-encryption, diffie-hellman, symmetric-encryption

functions: puf/1 [private],h/1






// Initialize Role Vehicle
rule Vehicle:
[ Fr(~ID_V) ]
--[Create(V, ~ID_V), Role('Vehicle')]->
[ !Ltk(ID_V, ~ltkID_V),
!Pk(ID_V, pkID_V),
St_V_1(V, ~ID_V, ltkID_V, pkID_A, A)
]




// Initialize Role Aggregator
rule Aggregator:
[ Fr(~ID_A)
, !Ltk(A, ~ltkID_A)
, !Pk(A, pkID_A)
]
--[ Create(A, ~ID_A), Role('Aggregator') ]->
[ Out(pk(~ltkA)),
St_A_1(A, ~ID_A, ~ltkA, pkA, V)
]




// Initialize Role Server
rule Server:
[ Fr(~ID_S)
, !Ltk(S, ltkS)
, !Pk(S, pkS)
]
--[ Create(S, ~ID_S), Role('Server') ]->
[ Out(pk(~ltkS)),
St_A_1(A, ~ID_A, ltkA, pkA, A, pkV, V)
]


rule Vehicle1:
let
R_V = ~N_V * P
R_V2 = ~N_V * pkA
PID_V = h(<ID_V,K>) xor (R_V2)
in
[ Fr(~N_V), ID_V, K, R_V2 , PID_V ]


--[Message(Vehicle, Aggregator) ]->
[R_V, R_V2, PID_V , Out(PID_V,R_V) ]


rule Aggregator1:
let
R_V2=R_V*ltkA
h(ID_V,K)=(R_V2) XOR (PID_V)
R_A=puf(~C_A)
M_AS=aenc(<PID_V,N_A,ID_A>,R_A)
I_AS = h ( ID_A ,M_AS ,R_A ,N_A )
in
[In(<PID_V,R_V>),
Fr(~N_A)]
--[ Message(Aggregator, Server) ]->
[Out(<ID_A,M_AS,I_AS,PID_V>) ]




rule Server1:
let
Sk_SV=senc(PID_V xor (K)
in
[ID_V, adec(M_AS),R_A), Fr(~N_S) ]
--[ ]->
[Sk_SV=senc(<PID_V xor K>,k),
SK_SA=senc(<ID_A xor N_A xor K>,k)
T=senc(<ID_V,Sk_SV,N_S>,S ]
end