# A Traceable and Verifiable Tobacco Products Logistics System with GPS and RFID Technologies
## 4 Security Analysis  
### Mutual Authentication  
We used BAN logic to verify the mutual authentication in the authentication phase. The notation of BAN logic is described below.  
\begin{tabular}{l l} \hline \(\{X\}_{K}\) & The message \(X\) is encrypted by a key \(K\) \\ \(P\overset{SK}{\leftrightarrow}Q\) & \(P\) and \(Q\) use a shared key SK to communicate \\ \(P|\equiv X\) & \(P\) believes X (belief rule) \\ \(P\lhd X\) & \(P\) sees \(X\) (seeing rule) \\ \(P|\sim X\) & \(P\) once said \(X\) (message meaning rule) \\ \(P|\Rightarrow X\) & \(P\) has jurisdiction over \(X\) (jurisdiction rule) \\ \(\#(X)\) & The message \(X\) is new (freshness rule) \\ \hline \end{tabular}  
The goals of the authentication analysis are:  
\begin{tabular}{l l} \(G1\): \(A|\equiv A\overset{X_{A_{A}}}{\leftrightarrow}B\) \\ \(G2\): \(A|\equiv B|\equiv A\overset{X_{A_{A}}}{\leftrightarrow}B\) \\ \(G3\): \(B|\equiv A\overset{X_{B}}{\leftrightarrow}B\) \\ \(G4\): \(B|\equiv A|\equiv A\overset{X_{B_{1}}}{\leftrightarrow}B\) \\ \(G5\): \(A|\equiv ID_{B}\) \\ \(G6\): \(A|\equiv B|\equiv ID_{B}\) \\ \(G7\): \(B|\equiv ID_{A}\) \\ \(G8\): \(B|\equiv A|\equiv ID_{A}\) \\ \hline \end{tabular}  
Figure 14: The validation flow in the arbitration phase.  
According to the authentication algorithm, BAN logic was used to produce an idealized form as follows:  
_M1: UserA\(\rightarrow\)UserB \((\{ID_{A},ID_{B},T_{1}\}_{\mathit{P}uk_{B}},r_{A_{1}},s_{A_{1}})\)_  
_M2: UserB\(\rightarrow\)UserA \((\{ID_{B},ID_{A},T_{3}\}_{\mathit{P}uk_{A}},r_{B_{1}},s_{B_{1}})\)_  
To analyze the proposed scheme, the following assumptions were made:  
_A1: A\(|\equiv\#(T_{1})\)_  
_A2: B\(|\equiv\#(T_{1})\)_  
_A3: A\(|\equiv\#(T_{3})\)_  
_A4: B\(|\equiv\#(T_{3})\)_  
_A5: A\(|\equiv B|\Rightarrow\begin{smallmatrix}x_{B_{1}}\\ \leftrightarrow\\ x_{A}\end{smallmatrix}\)_  
_A6: B\(|\equiv A|\Rightarrow\begin{smallmatrix}x_{A1}\\ \leftrightarrow\\ x_{A1}\end{smallmatrix}\)_  
_A7: A\(|\equiv B|\Rightarrow ID_{B}\)_  
_A8: B\(|\equiv A|\Rightarrow ID_{A}\)_  
User B authenticates user A  
By \(M1\) and the seeing rule, derive:  
\(B\lhd\)\((\{ID_{A},ID_{B},T_{1}\}_{\mathit{P}uk_{B}}r_{A_{1}},s_{A_{1}})\) (_Statement 1_) By \(A2\) and the freshness rule, derive:  
\(B|\equiv\#(\{ID_{A},ID_{B},T_{1}\}_{\mathit{P}uk_{B}},r_{A_{1}},s_{A_{1}})\) (_Statement 2_) By (_Statement 1_) and the message meaning rule derive:  
\(B|\equiv A|\sim(ID_{A},ID_{B},T_{1},r_{A_{1}},s_{A_{1}})\) (_Statement 3_) By (_Statement 2_), (_Statement 3_) and the nonce verification rule, derive:  
\(B|\equiv A|\equiv(ID_{A},ID_{B},T_{1},r_{A_{1}},s_{A_{1}})\) (_Statement 4_) By (_Statement 4_) and the belief rule, derive (G4):  
\(B|\equiv A\stackrel{{ x_{A1}}}{{\leftrightarrow}}B\) (_Statement 5_) By (_Statement 5_), _A6_, and the jurisdiction rule, derive (G3):  
\(B|\equiv A\stackrel{{ x_{A1}}}{{\leftrightarrow}}B\) (_Statement 6_) By (_Statement 4_) and the belief rule, derive (G8):  
\(B|\equiv A|\Rightarrow ID_{A}\) (_Statement 7_) By (_Statement 7_), _A8_, and the belief rule, derive (G7):  
\(B|\equiv ID_{A}\) (_Statement 8_)  
User A authenticates user B  
By \(M1\) and the seeing rule, derive:  
\(A\lhd\)\((\{ID_{B},ID_{A},T_{3}\}_{\mathit{P}uk_{A}},r_{B_{1}},s_{B_{1}})\) (_Statement 9_) By \(A3\) and the freshness rule, derive:  
\(A|\equiv\#(\{ID_{B},ID_{A},T_{3}\}_{\mathit{P}uk_{A}},r_{B_{1}},s_{B_{1}})\) (_Statement 10_) By (_Statement 9_) and the message meaning rule derive:  
\(A|\equiv B|\sim(ID_{B},ID_{A},T_{3},r_{B_{1}},s_{B_{1}})\) (_Statement 11_) By (_Statement 12_) and the belief rule, derive (G2):  
\(A|\equiv B|\equiv B\stackrel{{