## 4 Security Proofs
### Secure Mutual Authentication
If \((r_{1},r_{4})\) are valid, the state of \(\Pi^{u}_{MS_{i},V_{j}}\) will be changed as \"accepted\". The proof model of this case is depicted in Figure 12. In the proof model, we will construct a simulator \(\mathcal{S}_{MA}\) who will simulate the communication environment to \(E\) and try to break the IND-CCA defined in Definition 7. Assume that there are \(q_{1}\) entities \(MS_{i}\)'s and \(q_{2}\) entities \(V_{j}\)'s in the communication environment and \(E\) will perform \(\mathit{Send}(\Pi^{u}_{MS_{i},V_{j}},\mathcal{N})\) at most \(q_{3}\) times with \(i\in\{1,\ldots,q_{1}\}\) and \(j\in\{1,\ldots,q_{2}\}\) where \(q_{1}\), \(q_{2}\), and \(q_{3}\) are polynomials of security parameter \(k\). There also exists an oracle \(\mathcal{O}_{T}\) who will play the role of \(H\) to run the protocol of Section 3.3 to issue tickets. In order to set up the communication environment, \(\mathcal{S}_{MA}\) first randomly selects four strings, \((\bar{r}_{1},r_{1}^{\prime},\bar{r}_{2},\bar{r}_{3})\), and sets \(m_{0}=(\bar{r}_{1},\bar{r}_{2},\bar{r}_{3})\) and \(m_{1}=(\bar{r}_{1}^{\prime},\bar{r}_{2},\bar{r}_{3})\). Then, \(\mathcal{S}_{MA}\) sends \((m_{0},m_{1})\) to \(\mathcal{C}\) and gets \(\pi=E_{pk}(m_{b})\) from \(\mathcal{C}\) where \(b\in_{R}\{0,1\}\) and \(pk\) is the public key in the IND-CCA game. \(S_{R}\) denotes the set of the outputs of \(Send(\Pi_{V_{j},M_{S}}^{u},(\alpha,\beta_{1},T,\theta_{2}))\) queries, _i.e._, the second flow \((r_{1},r_{4})\)'s. \(\mathcal{S}_{MA}\) randomly chooses two integers \(\lambda\) and \(j^{\prime}\) and guesses that \(\Pi_{M_{S},V_{j}}^{u}\) will accept after \(E\) makes \(Send(\Pi_{M_{S},V_{j}}^{u},(r_{1},r_{4}))\) query where \((r_{1},r_{4})\
otin S_{R}\) and the session \(u\) was started by the \(\lambda\)th \(Send(\Pi_{M_{S},V_{j}}^{u},\mathcal{N})\) query. Then, \(\mathcal{S}_{MA}\) sets up the public/private keys \((pk_{V_{j}},sk_{V_{j}})\) for entity \(V_{j}\), where \(j=\{1,\ldots,q_{2}\}\) and \(j\
eq j^{\prime}\), and assigns the public key \(pk\) to entity \(V_{j}\) and generates public/private keys \((e_{H},n_{H},d_{H})\) and \((pk_{I},sk_{I})\) for \(H\) and the judge. When \(E\) makes \(Execute(\Pi_{M_{S},V_{j}}^{u},\Pi_{V_{j},M_{S}}^{u})\) query, \(\Pi_{M_{S},V_{j}}^{u}\) will perform the protocol of Section 3.3 with \(\mathcal{O}_{T}\) and get \((t,\rho,\gamma)\). Then, \(\Pi_{M_{S},V_{j}}^{u}\) prepares \(T=(F_{1}(m),\delta,\sigma,\gamma,s)\) and runs the protocol of Section 3.4 with \(\Pi_{V_{j},M_{S}}^{u}\) in the presence of \(E\). If \(V_{j}\) is involved in the execution query, \(S_{MA}\) can simulate it by running the protocol of Section 3.4 with querying \(\mathcal{O}_{E}\) for encryption and querying \(\mathcal{O}_{D}\) for decryption. Besides, \(\mathcal{S}_{MA}\) initializes two global parameters \(i_{guess}=0\) and \(f_{guess}=0\) and empties four lists \(L_{T_{MS}}\), \(L_{K_{MS}}\), \(L_{T_{V}}\), and \(L_{K_{V}}\). When \(E\) makes \(Send(\[PERSON]_{M_{S},V_{j}}^{u},\mathcal{M})\) and \(Send(\[PERSON]_{V_{j},M_{S}}^{u},\mathcal{M})\) queries, the actions of \(\[PERSON]_{M_{S},V_{j}}^{u}\) and \(\[PERSON]_{V_{j},M_{S}}^{u}\) are defined in Figure 13.  
Figure 12: The proof model of Case 1. Figure 13: The actions of \(\[PERSON]_{M_{S},V_{j}}^{u}\) and \(\Pi_{V_{j},M_{S}}^{u}\) for \(Send(\Pi_{M_{S},V_{j}}^{u},\mathcal{M})\) and \(Send(\Pi_{V_{j},M_{S}}^{u},\mathcal{M})\) queries, respectively. In Line 22 of \(\Pi^{u}_{MS_{i},V_{j}}\) in Figure 13, \(\mathcal{S}_{MA}\) tries to break IND-CCA as follows. If \(f_{guess}=0\), \(\mathcal{S}_{MA}\) will guess \(b^{\prime}=0\) when \(r^{\prime}_{1}=r_{1}\), guess \(b^{\prime}=1\) when \(r^{\prime}_{1}=r^{\prime}_{1}\), and randomly guess \(b^{\prime}\in\{0,1\}\) when \(r^{\prime}_{1}\
eq r_{1}\) and \(r^{\prime}_{1}\
eq r^{\prime}_{1}\). If \(f_{guess}=1\), \(\mathcal{S}_{MA}\) will randomly guess \(b^{\prime}\in\{0,1\}\).