# SPCL: A Smart Access Control System That Supports Blockchain
## 4 Security Analysis  
### Provable Security of SPCL Protocol  
The eCK model [26] is used to conduct a provable security proof for the SPCL protocol. The practical reasons for each step in the proof process are based on the formal proof process followed by the NAXOS protocol.  
Theorem 4.1: _The SPCL protocol eCK-security if \(\mathcal{H}_{2}\) is modeled as independent random oracles and \(GDH\) and DLOG problems are hard in \(G\)._  
_For any PPT adversary \(\mathcal{M}\) against SPCL that runs in time at most \(t\), involves at most \(n\) honest parties, and activates at most \(k\) sessions, there exists a \(GDH\) problem solver \(\mathcal{S}\) and a DLOG problem solver \(\mathcal{T}\) such that_  
\[\mathbf{Adv}_{\mathcal{M}}^{\text{SPCL}}\leq max\Big{\{}k^{2},nk\Big{\}} \left(2\mathbf{Adv}_{\mathcal{S}}^{GDH}+2n\cdot\mathbf{Adv}_{\mathcal{T}}^{ DLOG}+O\left(\frac{k^{2}}{2^{\lambda}}\right)\right)\]  
_where \(\mathcal{S}\) runs in time \(O(tk)\) and \(\mathcal{T}\) runs in time \(O(t)\)._  
Proof: Let \(\mathcal{M}\) be any AKE adversary against SPCL protocol. The session key of the _Test_ session is computed as \(sk=H_{2}(\gamma)\) for a 4-tuple \(\gamma\). We will demonstrate how to use \(\mathcal{M}\)'s ability to construct a solver \(\mathcal{S}\) for solving the \(GDH\) problem. \(\mathcal{S}\) first selects the system parameter \(params=\left\{E(F_{q}),G,H_{2}\right\},\) and then sends _params_ to \(\mathcal{M}\). As \(\mathcal{H}_{2}\) is a random oracle, \(\mathcal{M}\) can distinguish a session key \(sk=H_{2}(\gamma)\) from a random string with a significantly higher probability than \(\frac{1}{2}\) in one of the following events:  
\(E_{1}\): Guessing attack: \(\mathcal{M}\) correctly guesses the \(sk\). The probability of guessing \(sk\) is \(\mathcal{O}\left(\frac{1}{2^{\lambda}}\right)\), which is negligible. \(E_{2}\): Key replication: If an adversary \(\mathcal{M}\) forces two distinct non-matching sessions to have the same session key, it can select one of the sessions as the _Test_ session and query the key of the other session. This is because two non-matching sessions cannot have the same communicating parties and ephemeral public keys. The replication of keys is equivalent to finding a collision for the hash function \(\mathcal{H}_{2}\). Therefore, the probability of **Event**\(E_{2}\) occurring is \(\mathcal{O}\left(\frac{s(\lambda)^{2}}{2^{\lambda}}\right)\), which is negligible. \(E_{3}\): Forging attack: Adversary \(\mathcal{M}\) queries \(\mathcal{H}_{2}\) on the value \((N_{\mathcal{A}},N_{\mathcal{B}},x_{\mathcal{A}},y_{\mathcal{A}})\) (\(K_{\mathcal{A}}=(x_{\mathcal{A}},y_{\mathcal{A}})\)) in the _Test_ session owned by \(\mathcal{A}\) communicating with \(\mathcal{B}\). We will construct a \(GDH\) solver using an adversary \(\mathcal{M}\) that succeeds in a forging attack with non-negligible probability. \(\mathcal{S}\) simulates the game outlined above. During the game, \(\mathcal{S}\) has to answer all queries of the adversary \(\mathcal{M}\). The following two sub-events should be considered. \(E_{3.1}\): The _Test_ session has a matching session owned by another honest party. \(E_{3.2}\): No honest party owns a session matching with the _Test_ session.