# EAIA: An Efficient and Anonymous Identity-Authentication Scheme in 5G-V2V
## 6 Security Evaluation
### Formal Proof by BAN Logic  
Burrows-Abadi-Needham logic (BAN logic), initially proposed by [PERSON] et al., is a formal method used to analyze and verify the security properties of authentication protocols. It has been employed to formally derive the logical correctness of security protocols. BAN logic provides a logical framework to describe the beliefs of trusted parties involved in an authentication protocol and the evolution of these beliefs. To perform verification, the protocol must first be translated into an idealized version. Assumptions and goals need to be stated. Then, derivation rules are manually applied toachieve the goals. The key elements of BAN logic include principles (entities such as users or servers); messages; and the beliefs, goals, and trust relationships of these principles. The symbols used in BAN logic are listed in Table 2.  
The derivation rules of BAN logic consist of 19 logical rules. Here we only list the rules used in this paper:  
Rule 1: Message Meaning Rule :  
\[\frac{P|\equiv\overset{K}{\rightarrow}Q,P\lhd X_{K^{-1}}}{P|\equiv Q|\sim X}\]  
This rule means that if \(P\) believes that the public key for user \(Q\) is \(K\), and \(P\) can see that the message \(X\) signed by the private key of \(Q\) is \(K^{-1}\), then \(P\) believes the message \(X\) is sent by \(Q\). Rule 2: Nonce Verification Rule:  
\[\frac{P|\equiv\#(X),P|\equiv Q|\sim X}{P|\equiv Q|\equiv X}\]  
This rule means if \(P\) believes \(X\) is fresh and \(P\) believes \(Q\) sent \(X\), then \(P\) believes \(Q\) believes \(X\). Rule 3: Jurisdiction Rule:  
\[\frac{P|\equiv Q\Rightarrow X,P|\equiv Q|\equiv X}{P|\equiv X}\]  
This rule means if \(P\) believes \(Q\) has jurisdiction on message \(X\), and \(P\) believes \(Q\) believes \(X\), then P believes \(X\). Rule 4: Freshness Rule:  
\[\frac{P|\equiv\#(X)}{P|\equiv\#(X,Y)}\]  
This rule means that if part of the formula is fresh, the entire formula is also fresh. It only makes sense to appear in ciphertext. If a part of the ciphertext is fresh, then the entire part is also fresh. Rule 5: Belief Rule:  
\[\frac{P|\equiv Q|\equiv(X,Y)}{P|\equiv Q|\equiv X}\]  
This rule reflects the consistency of beliefs in different operations of the concatenation and segmentation of messages and the transitivity of beliefs in such operations. The main steps for formal verification using BAN logic are as follows: (1) Idealization: convert the actual protocol messages into an abstract form that captures the essential security properties. (2) Assumptions: define the initial beliefs and assumptions about the principles and messages. (3) Derivations: apply BAN logic derivation rules to deduce new beliefs from the initial assumptions. (4) Verification: check whether the derived beliefs satisfy the required security properties, such as mutual authentication or key agreement. \begin{table}
\begin{tabular}{c c} \hline \hline
**Notation** & **Meaning** \\ \hline \(P|\equiv X\) & \(P\) believes the message \(X\) \\ \(P\lhd X\) & \(P\) saw the message \(X\) \\ \(P|\sim X\) & \(P\) said the message \(X\) \\ \(P\Rightarrow X\) & \(P\) has the message \(X\) jurisdiction \\ \(\#(X)\) & The message \(X\) is fresh \\ \(X_{K}\) & \(X\) is encrypted with key \(K\) \\ \(P\overset{K}{\longleftrightarrow}Q\) & \(K\) is the security key between \(P\) and \(Q\) \\ \hline \hline \end{tabular}
\end{table} 
Table 2: Notation and meaning of BAN logic. (1) The goals of EAIA: First, we establish our goals. In our model, the AMF is a trusted entity for both \(OBU_{i}\) and \(OBU_{j}\). Therefore, if \(OBU_{i}\) and \(OBU_{j}\) share the same session key with the AMF, we think that \(OBU_{i}\) and \(OBU_{j}\) share a session key. Additionally, the session key \(SK\) shared between \(OBU_{i}\) and \(OBU_{j}\) is generated using the random numbers \(a\) and \(b\). Finally, for simplicity in some parts of the expression, we denote the AMF public key, which is also the system public key, as \(pk\).