## 6 Security Analysis
### Formal Security Analysis through AVISPA
#### 6.2.1 Proposed Protocol's HLPSL Code  
The AVISPA uses the four back-ends, such as On-the-fly Model-Checker (OFMC) [32], CL-based Attack Searcher (CL-AtSe) [33], SAT-based Model-Checker (SATMC), and Tree Automate-based Protocol Analyser (TA4 SP) in order to verify security of a protocol. The code is translated into intermediate format (IF), and IF uses four back-ends to convert to output format (OF). Especially, OFMC and CL-AtSe are commonly used for verification. The proposed protocol has three basic _roles_ which denote entities: \(VI\) denotes a vehicle, \(RSU\) denotes a roadside unit and \(TA\) denotes a trusted authority. Roles of _session_ and _environments_ are illustrated in Figure 8. In _session_ and _environments_, we set up the intruder knowledge, five authentication goals and four secrecy goals. We briefly discuss HLPSL code for role \(VI\) shown in Figure 9.  
At transition \(1\), \(VI\) begins registration phase at \(0\) state value with start message, and \(VI\) updates the state to \(1\). \(VI\) sends message \(\{ID_{i},PW_{i},PE_{i},BE_{i}\}\) to \(TA\) through closed channels and declares the function \(secret(\{IDi,PWi,Bi^{\prime}\},sp1,\{VI\})\), which means that \(sp1\) denotes values \(\{IDi,PWi,Bi^{\prime}\}\) which are only known to \(VI\). At transition \(2\), \(VI\) receives the \(OBU_{i}\) from \(TA\) and updates the state to \(2\). At the state \(2\), \(VA\) generates a random number \(r_{i}\), sends the message \(\{Auth_{1},M_{1},HID_{i}\}\) to the \(RSU_{j}\) through an open channel, and declares function \(witness(VI,TA,vi\_ta\_ri,Ri^{\prime})\), which means that \(vi\_ta\_ri\) denotes a weakness authentication factor is used by \(VI\) to authenticate \(TA\). At transition \(3\), \(VI\) receives the message from \(RSU\). After that \(VI\) generates the session key \(SK\), performs message confirmation and declares \(witness(VI,RSU,vi\_rsu\_sig,SK^{\prime})\) and \(request(VI,TA,ta\_vi\_auth4,Rj^{\prime})\). The function \(request(VI,TA,ta\_vi\_auth4,Rj^{\prime})\) means that \(ta\_vi\_auth4\) represents a strong authentication factor. The codes of \(RSU\) and \(TA\) are similar to the code of \(VI\). role session(EV, OP, EAG: agent, SKevop: symmetric_key, H: hash_func) def= local SN1, SN2, SN3, RV1, RV2, RV3: channel(dy) composition vehicle(EV, EAG, OP, SKevop,H, SN1, RV1) \(\wedge\) operator(EV, EAG, OP, SKevop,H, SN2, RV2) \(\wedge\) agg(EV, EAG, OP, H, SN3, RV3) end role  
role environment() def= const ev, eag, op : agent, skewop: symmetric_key, h, mul, add: hash_func, idev, ideg: text, seq1, sp2, sp3, sp4: protocol_id, ev_eag_m2, eag_ev_md: protocol_id  
intruder_knowledge = {ev,eag,op,h,mul,add,idev,ideag} composition session(ev,eag,op,skewop, h) \(\wedge\)session(ev,i,op,skewop,h) \(\wedge\)session(ev,eag,skewop,h) end role  
goal secrecy_of sp1, sp2, sp3, sp4 authentication_on ev_eag_m2, eag_ev_md end goal  
environment()  
role vehicle(EV, OP, EAG: agent, SKevop: symmetric_key, H: hash_func, SND, RVV : channel(dy)) played, by EV def= local Suter: nat, MUL, ADD : hash_func, HDHD,I, PWi, AI, Rev, PKG, G, HDI, Kop, PKGop, Ai, Bi, Ci, Di, E1 : text, Dega, PKeg, M2, M3, Md, T1, T2, B1, SK : text const sp1, sp2, sp3, sp4_ev_eag_m2, eag_ev_md : protocol_id ini State = 0 \(\backslash\) RTVC(start) \(\Rightarrow\) State \(\Rightarrow\) \(\Delta\) At \(\doteq\) new() \(\backslash\) Rev \(\vee\) = new() \(\backslash\) PRV := MLUL(Rev:G) \(\backslash\) HID := HDHD(L:A1) \(\wedge\) SEND(HDHD(L:A1)) \(\wedge\) SEND(HDHD(L:A1)) \(\wedge\) Secure([ID, PWi, Rev\({}^{\prime}\)], sp1, [EV]) \(\wedge\) secure([A1],sp2,[EV, OP])  
2. State = 2 \(\backslash\) RCV(start(H(HD(L:A1)),AT),Kop),H(HD(L:A1),AT:Kop)]_S&Keyop= \(\backslash\) State \(\Rightarrow\) \(\Delta\) At \(\doteq\) Rev \(\Rightarrow\) \(\Delta\) \(\doteq\) zero(H(L:D1),PWi),A17 \(\doteq\) new() \(\backslash\) MZ := H(A1:HD(L:A1),T1) \(\wedge\) SENDMUL(Rev:G),ADD(A1:H(HD(L:A1),T1),MUL(Rev\({}^{\prime}\)], Keng)) \(\wedge\) witness(EV,EAG, ev_eag_m2, AI)  
3.