# A Lightweight and Practical Anonymous Authentication Protocol Based on Bit-Self-Test PUF
## 4 Formal Security Analysis
### Security Analysis
: If the adversary is unable to correlate two successful device authentication requests with two valid responses corresponding from the server, then the device is generally untraceable. This theory can be proved by modeling the game with adversary \(A\) by setting \(CH\) as the challenger of the RFID system. \(CH\) chooses a valid server unit \(S\) and two devices \(D_{1}\) and \(D_{2}\); \(A\) invokes the following queries, Transmit, Enquiry, Execute, and Blocking, on \(S\) and \(D_{1}\) and \(D_{2}\); After completing the invocation of the query, \(A\) notifies \(CH\); \(CH\) randomly selects one of the devices \(D\); \(A\) invokes the following queries on \(S\) and \(D\): Transmit, Enquiry, Execute, Blocking. In addition, \(A\) can invoke Reveal once; \(A\) predicts her guess \(D^{\prime}\), and if \(D^{\prime}=D\), \(A\) wins the game. Thus, the advantage of a successful guess is defined as \(Adv_{A}=2\times(Sel[D^{\prime}=D]-1/2)\). If adversary \(A\) does not have any advantage in random guessing, then \(Sel[D^{\prime}=D]=1/2\), and therefore \(Adv_{A}\) is zero, which means that it cannot be traced. In our proposed protocol, it is known from Lemma 2 that \(A\) cannot infer the PUF response \(r_{i}\) at round i of authentication, and thus cannot generate the important information key \(k_{1}\). From Lemma 3, we know that \(A\) cannot correlate the identities of the device at round i and i+1. Therefore, adversary \(A\) has only one choice, i.e., random guess \(Sel[D^{\prime}=D]\). Then, according to the above formula \(Adv_{A}=2\times(Sel[D^{\prime}=D]-1/2)\), it is known that \(Adv_{A=0}\) when \(Sel[D^{\prime}=D]=1/2\). Therefore, the proposed authentication protocol can ensure untraceability. The proposed authentication protocol can ensure forward confidentiality while supporting backward untraceability. Proof. : To ensure that the proposed protocol has forward secrecy supported by backward untraceability, we model a game in Theorem 1. The difference is that adversary \(A\) needs to call a Reveal query on the device to obtain the challenge \(c\) and the helper data \(h\), which are stored in the device memory, and finally, \(A\) outputs the guessed \(D\). By Lemma 2, \(A\) cannot launch the key information \(r_{i}\), and each CRP is randomly generated, so they are considered to be independent of each other. Since all the secret information used in the proposed protocol is one-time, if the attacker has access to challenge \(c\), the helper data \(h\), and a small quantity of CRPs, from Lemma 3, \(A\) still cannot track the device by using the compromised information. Thus, adversary \(A\) will not have any advantage over random guesses in predicting the device, and the proposed protocol can ensure forward secrecy with backward untraceability support. **Lemma 4**: _The proposed scheme can ensure resilience against DoS attacks._  
In a DOS attack, the adversary \(A\) tends to invoke the Blocking query to stop the device from receiving the message \(s_{4}^{\prime}\) in the third transmission; hence, the information on the device remains the \(ID_{1}\), \((c_{1},h_{1})\) and cannot be updated. To deal with this attack, we store the auxiliary key \(k_{old}\) and temporary ID \(ID_{old}\) at the server. If, in the next authentication, the server cannot find the correct \(ID\), it will use the \((ID_{old},k_{old})\) instead of \((ID_{1},k_{1})\) to perform the authentication. This will serve as a defense against DoS attacks. **Lemma 5**: _The proposed protocol can ensure security against a cloning attack._  
Most existing authentication protocols store the secret in the tag's NVM. However, this approach is prone to key leakage. In our proposed scheme, we do not store any keys in the tag, and the device's PUF is considered to be inseparable from the microprocessor. Therefore, even if an adversary has access to the device, it cannot compromise the security of the proposed protocol (Lemma 1).