# Privacy-Preserving Solution for European Union Digital Vaccine Certificates
## 6 Security Analysis  
In this section, the security analysis of the cryptographic core takes place. In particular, we provide the proof of correctness, unforgeability, anonymity, and key-parameter consistency of our proposal. Note that the equality \(t\stackrel{{? }}{{=}}t_{verify}\), i.e., Equations (1) and (2), has been proven in [21]. Therefore, the correctness of our proposal is proven as follows:  
**Theorem 2** (Correctness). : _The Verification process in Section 5.2, point 3, is correct._  
Proof. : Since a symmetric cryptographic scheme is used to encrypt the attributes, at first, we show that the VER can reconstruct the USR's encryption key. In fact,  
\[j^{\prime}=u^{sk_{V}}=(g_{1}^{e})^{sk_{V}}=pk_{V}^{e}=j\] \[k_{enc}^{\prime}=KDF(j^{\prime})=KDF(j)=k_{enc} \tag{3}\]  
and, therefore, \(m_{i}^{\prime}=Dec_{SYM}(c_{i},k_{enc}^{\prime})=Dec_{SYM}(c_{i},k_{enc})=m_{i}\) for all \(m_{i}\in D\). Accordingly, the decryption process is correct as shown in Equation (3). Once the message is correctly decrypted, we need to show that \(\mathbf{e}(t_{verify},g_{2})\) is equal to \(\mathbf{e}(\hat{\sigma},\alpha)\cdot\mathbf{e}(g_{1}^{s_{\sigma}},g_{2})\). Note that \(e^{\prime}\) is equal to \(\mathcal{H}(t_{verify},\hat{\sigma},nonce)=e\). The pairing equality can be proven as shown in Equations (4) and (5):  
\[\mathbf{e}(\hat{\sigma},\alpha) =\mathbf{e}(g_{1}^{(\frac{1}{s_{0}+m_{1}x_{1}+\cdots+m_{n}x_{n}}) \rho},h_{0}^{-\epsilon}\cdot\prod_{i\in D}h_{i}^{s_{n_{i}}}\prod_{i\in D}h_{i }^{-cm_{i}})\] \[=\mathbf{e}(g_{1}^{(\frac{1}{s_{0}+m_{1}x_{1}+\cdots+m_{n}x_{n}}) \rho},g_{2}^{-ex_{0}+\prod_{i\in D}(\rho_{m_{i}}-m_{i})x_{i}+\prod_{i\in D}-m _{i}x_{i}})\] \[=\mathbf{e}(g_{1}^{(\frac{1}{s_{0}+m_{1}x_{1}+\cdots+m_{i}x_{i}}) \rho},g_{2}^{-ex_{0}+(x_{1}+\sum_{i=1}^{n}m_{i}x_{i})+\prod_{i\in D}\rho_{m_{i }}x_{i}})\] \[=\mathbf{e}(g_{1},g_{2})^{-\epsilon\rho+(\frac{1}{s_{0}+\sum_{i=1 }^{n}m_{i}x_{i}})\prod_{i\in D}\rho_{m_{i}}x_{i}\rho} \tag{4}\]  
and, therefore,  
\[\mathbf{e}(\hat{\sigma},\alpha)\cdot\mathbf{e}(g_{1}^{s_{\sigma}},g_{2}) =\mathbf{e}(g_{1},g_{2})^{-\epsilon\rho+(\frac{1}{s_{0}+\sum_{i=1 }^{n}m_{i}x_{i}})\prod_{i\in D}\rho_{m_{i}}x_{i}\rho}\cdot\mathbf{e}(g_{1},g_{ 2})^{\epsilon\
u+\epsilon\rho}\] \[=\mathbf{e}(g_{1},g_{2})^{\epsilon\
u+(\frac{1}{s_{0}+\sum_{i=1 }^{n}m_{i}x_{i}})\prod_{i\in D}\rho_{m_{i}}x_{i}\rho}\] \[=\mathbf{e}(g_{1}^{\epsilon\
u}\xi_{1}^{(\frac{1}{s_{0}+\sum_{i=1 }^{n}m_{i}x_{i}})\prod_{i\in D}\rho_{m_{i}}x_{i}\rho},g_{2})\] \[=\mathbf{e}(g_{1}^{\epsilon\
u}\sigma^{\prod_{i\in D}\rho_{m_{i}}x _{i}\rho},g_{2})\] \[k_{enc}^{\prime}=KDF(j^{\prime})=KDF(j)=k_{enc} \tag{3}\]0  
**Theorem 3** (Unforgeability). : _Our scheme is \((t,\epsilon,q_{H})\)-unforgeable if the n-SCDHI problem (see Theorem 2 for more details) is \((2t,e^{\prime})\)-hard, where \(q_{H}\) is the maximum number of random oracle queries and \(e^{\prime}=\epsilon(\frac{\epsilon}{qH}-\frac{1}{q})\)._  
Proof. : Since no modifications are made on the Issue protocol, the proof follows directly from the unforgeability of the KVAC protocol [21]. We recall the definition of anonymity:  
**Definition 3** ([21]). : _A keyed-verification credential system is anonymous if for all PPT adversaries \(\mathcal{A}\), there exists an efficient algorithm SimShow such that for all \(\kappa\), for all \(\phi\in\Phi\) and \((m_{1},\dots,m_{n})\in\) such that \((\phi(m_{1},\dots,m_{n})=1\), and for all \((sk_{1},pk_{1},params_{1},pk_{v},sk_{v})\)\(\leftarrow\)Setup\((1^{\kappa})\): \(\textit{Show}(params_{I},A,(m_{1},\dots,m_{n}),\phi)\leftrightarrow\mathcal{A} \rightarrow\approx\textit{SimShow}(params_{I},sk_{1},\phi)\), i.e., the adversary's view given the proof can be simulated by SimShow given only \(\phi\) and a valid secret key corresponding to \(params_{1}\)._  
**Theorem 4** (Anonymity). : _Our scheme is anonymous, as defined in Definition 3, in the random oracle model._  
Proof.