# SPCL: A Smart Access Control System That Supports Blockchain
## 4 Security Analysis
### Provable Security of SPCL Protocol
#### 4.1.2 The Analysis of Event \(E_{3.2}\)  
If \(\mathcal{M}\) selects a _Test_ session for which no matching session exists, \(\mathcal{S}\) modifies the experiment as follows.  
\(E_{3.2.1}\): \(\mathcal{S}\) randomly selects an eCK session in which \(\mathcal{B}\) is the owner.  
\(\mathcal{S}\) picks a random party \(\mathcal{B}\), and sets \(\mathcal{Q}_{B}\gets X_{B}\) as its long-term public key. Note that \(\mathcal{S}\) doesn't know long-term private key \(DLOG(X_{B})\) corresponding to \(X_{B}\). Therefore, it cannot effectively simulate eCK sessions executed by \(\mathcal{B}\). \(\mathcal{S}\) sets \(msg_{\mathcal{B}}=h_{\mathcal{B}}\cdot P\) instead of \((r_{\mathcal{B}}+DLOG(X_{B}))\times P\). \(\mathcal{S}\) sets a session key \(sk\) (\(\text{H}_{2}(CDH(r_{\mathcal{B}}\times P+X_{B},msg_{\mathcal{A}}),\cdot,\cdot)\)) to be a random value. \(\mathcal{S}\) can manage session key and ephemeral secret key reveals by making \(SessionKeyReveal(\cdot)\) and \(EphemeralKeyReveal(\cdot)\) queries.  
Assuming \(\mathcal{A}\) is an adversary-controlled party, \(\mathcal{M}\) can compute the session key, reveal the session key \(sk\), and detect that it is fake. To mitigate this issue, \(\mathcal{S}\) monitors \(\mathcal{M}\)'s random oracle queries, and if \(\mathcal{M}\) ever queries \((x,y,\cdot,\cdot)\) to \(H_{2}\) (for some \(Z\in G\), \(Z=(x,y)\)), \(\mathcal{S}\) checks if \(DDH(r_{\mathcal{B}}\times P+X_{B},msg_{\mathcal{A}},Z)=1\), and if yes, replies with the session key \(sk\). Similarly, while computing \(sk\), \(\mathcal{S}\) checks if \(sk\) matches any previous response from the random oracle. \(\mathcal{M}\) cannot detect that it is in the simulated eCK experiment unless it queries \(\mathcal{H}_{2}\) or reveals \(\mathcal{B}\)'s long-term private key using the \(LongTermKeyReveal(B)\) query. The first event reveals \(DLOG(X_{B})\), and allows \(\mathcal{S}\) to solve the \(CDH\) problem, which occurs with probability at most  
\[n\cdot\mathbf{Adv}_{\mathcal{T}}^{\text{DLOG}}\]  
\(E_{3.2.2}\): \(\mathcal{S}\) also randomly selects an eCK session in which \(\mathcal{B}\) is the peer.  
Let the owner of this session be denoted by \(\mathcal{A}\). \(\mathcal{S}\) normally generates \(d_{\mathcal{A}}\), \(r_{\mathcal{A}}\) and \(d_{\mathcal{B}}\), \(r_{\mathcal{B}}\). Then, \(\mathcal{S}\) sets \(msg_{\mathcal{A}}\gets X_{\mathcal{A}}\) (instead of \((r_{\mathcal{A}}+d_{\mathcal{A}})\times P\) and \(msg_{\mathcal{B}}\gets Y_{\mathcal{B}}\) (instead of \((r_{\mathcal{B}}+d_{\mathcal{B}})\times P\)). With probability at least \(\frac{1}{nk}\) (where \(\frac{1}{n}\) is to pick the correct party \(\mathcal{B}\), and \(\frac{1}{k}\) is to pick the correct session), \(\mathcal{M}\) picks the selected session as the _Test_ session and solves the \(CDH\) problem if it wins. \(\mathcal{M}\) is not allowed to reveal both \((r_{\mathcal{A}},d_{\mathcal{A}})\), and cannot corrupt \(\mathcal{B}\). In this event, the only way that \(\mathcal{M}\) can distinguish this simulated eCK experiment from a true eCK experiment is if \(\mathcal{M}\) queries \((r_{\mathcal{A}},d_{\mathcal{A}})\). By **Event**\(E_{3.1}\) it happens with probability at most  
\[n\cdot\mathbf{Adv}_{\mathcal{T}}^{\text{DLOG}}\]  
Overall, the success probability of \(\mathcal{S}\) is at most  
\[\mathbf{Adv}_{\mathcal{S}}^{\text{GDH}}\geq\frac{1}{nk}\cdot\mathbf{Adv}_{ \mathcal{M}}^{\text{SPCL}}-O\bigg{(}\frac{k^{2}}{2^{\lambda}}\bigg{)}-2n\cdot \mathbf{Adv}^{\text{DLOG}}(\mathcal{T})\]  
Therefore, we have:  
\[\mathbf{Adv}_{\mathcal{M}}^{\text{SPCL}}\leq max\Big{\{}k^{2},nk\Big{\}} \bigg{(}2\mathbf{Adv}_{\mathcal{S}}^{\text{GDH}}+2n\cdot\mathbf{Adv}_{ \mathcal{T}}^{\text{DLOG}}+O\bigg{(}\frac{k^{2}}{2^{\lambda}}\bigg{)}\bigg{)}\]  
Finally, under the GDH assumption, \(\mathbf{Adv}_{\mathcal{S}}^{\text{GDH}}\) is negligible. Therefore, \(\mathbf{Adv}_{\mathcal{M}}^{\text{SPCL}}\) is negligible, and SPCL protocol has eCK security.