## 4 Security Proofs
### Ticket Swinding Resistance
\(E\) can make the query \(\mathit{Send}(\[PERSON]^{u}_{\mathit{MS}_{i},V_{j}^{\prime}},\mathcal{N})\) to get a response of the first flow where \(\mathcal{N}\) is an empty string.
* \(\mathit{Reveal}(\[PERSON]^{u}_{\mathit{MS}_{i},V_{j}^{\prime}})\) or \(\mathit{Reveal}(\[PERSON]^{v}_{V_{j},\mathit{MS}_{i}})\): This query allows the adversary to get the session key of \(\[PERSON]^{u}_{\mathit{MS}_{i},V_{j}}\) or \(\[PERSON]^{v}_{V_{j},\mathit{MS}_{i}}\) after \(\[PERSON]^{u}_{\mathit{MS}_{i},V_{j}}\) and \(\[PERSON]^{v}_{V_{j},\mathit{MS}_{i}}\) have successfully finished mutual authentication and established a common session key.
* \(\mathit{Reveal}(T)\): This query allows the adversary to obtain the secret value \(m\) if \(T\) has been successfully consumed for authentication where \(T=(F_{1}(m),\delta,\sigma,\gamma,s)\).
* \(\mathit{Corrupt}(V_{j})\): This query reveals \(V_{j}\)'s long-term key \(\mathit{sk}_{V_{j}}\).  
In our protocol, once a mobile user consumes her/his \(T\) for authentication, \(T\) will be kept in the system's database for double-using checking. Hence, a successfully-used \(T\) cannot be consumed again by any eavesdropper. Any attacker can just try to swindle an eavesdropped \(T\) which has not been successfully used, _i.e._, the attacker has to interfere the authentication process after she/he obtains \(T\) in the first flow of the authentication protocol in Section 3.4. We define Ticket Swindling below.  
Definition 6 (The Ticket Swindling Game): Let \(k\in\mathbb{N}\) be the security parameter. \(\mathcal{A}_{\mathit{TS}}\) is a polynomial time adversary who tries to swindle an eavesdropped \(T\). Consider the following experiment:  
\[\begin{array}{l}\mathit{Experiment}\ \mathit{Exp}_{\mathcal{A}_{\mathit{TS}}}^{ TS}(k)\\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \  
**Definition 8** (Rsa-Sti).: _Let \(k\in\mathbb{N}\) be the security parameter. Let \(\mathcal{A}\) be a polynomial time adversary. Consider the following experiment:_  
\[\text{Experiment }Exp_{\mathcal{A}}^{RSA-STI}(k)\] \[\text{- }(N,e,d)\overset{R}{=}KeyGen(k)\] \[\text{- }y\overset{R}{\leftarrow}Z_{N}^{*};x\leftarrow\mathcal{A} (N,e,k,y)\] \[\text{If }x^{e}\equiv y\pmod{N}\text{ return 1 else return 0}\]  
_We define the advantage of \(\mathcal{A}\) as \(Adv_{\mathcal{A}}^{RSA-STI}(k)=Pr[Exp_{\mathcal{A}}^{RSA-STI}(k)=1]\)._  
**Theorem 4**. : _The proposed anonymous authentication protocol satisfies Ticket Swinding Resistance._  
Proof. : The proof model is illustrated in Figure 10. A simulator \(\mathcal{S}_{TS}\) will simulate the communication environment and help us to solve the RSA-STI problem. First, \(\mathcal{S}_{TS}\) obtains the parameters \((N,e,y)\) from the RSA-STI problem. \(\mathcal{S}_{TS}\) initializes the system parameters, which are the public-private key pairs of \(H\), \(V\)'s, and the judge, and constructs the oracles \(\Pi_{MS_{i},V_{j}}^{u}\) and \(\Pi_{V_{j},MS_{i}}^{v}\). \(\mathcal{S}_{TS}\) also controls three hash oracles \(\mathcal{O}_{F_{1}}\), \(\mathcal{O}_{F_{2}}\), and \(\mathcal{O}_{F_{3}}\) to simulate the hash functions \(F_{1}\), \(F_{2}\), and \(F_{3}\), respectively. When \(\mathcal{O}_{F_{1}}\) is queried with \(m\), it will return \(r_{f_{1}}\) retrieved from \(L_{F_{1}}\) via \(m\) if \(m\) exists in \(L_{F_{1}}\) or return \(r_{f_{1}}=(m^{e}\text{ mod }N)\) and records \((m,r_{f_{1}})\) in \(L_{F_{1}}\). If \(\mathcal{O}_{F_{2}}\) is queried with \((\delta,\sigma,\gamma)\), it will return \(r_{f_{2}}\) retrieved from \(L_{F_{2}}\) via \((\delta,\sigma,\gamma)\) if \((\delta,\sigma,\gamma)\) exists in \(L_{F_{2}}\) or return a randomly-selected string \(r_{f_{2}}\in\{0,1\}^{l_{r}}\) and record \((\delta,\sigma,\gamma,r_{f_{2}})\) in \(L_{F_{2}}\). When \(\mathcal{O}_{F_{3}}\) is queried with \((r_{2}||r_{4})\), it will return \(r_{f_{3}}\) retrieved from \(L_{F_{3}}\) if \((r_{2}||r_{4})\) exists in \(L_{F_{3}}\) or a randomly-chosen string \(r_{f_{3}}\in\{0,1\}^{l_{r}}\) and record \(((r_{2}||r_{4}),r_{f_{3}})\) in \(L_{F_{3}}\).