# PriSign, A Privacy-Preserving Single Sign-On System for Cloud Environments
## 4 System and Security Model
### Security Model  
In this section, we adopt a game-based model to define the security properties of the PriSign scheme, including its unforgeability, unlinkability, and token-hiding. All security definitions use the following global variables and oracles. There is a challenger \(\mathcal{C}\) and a PPT adversary \(\mathcal{A}\) in the game; \(\mathcal{C}\) is responsible for initializing the system, issuing keys for all policymakers, and controlling all global variables and oracles; and \(\mathcal{A}\) interacts with \(\mathcal{C}\) through the oracles to break the scheme. **Global Variables**. \(\mathcal{Q}_{\mathsf{HU}}\): a set storing \((uid,usk,upk,utk,\{m_{j}\}_{j\in[\mathsf{I},q]},ucred)\) each time \(\mathsf{CA}\) issues a credential for an honest user \(uid\). \(\mathcal{Q}_{\mathsf{CU}}\): a set of corrupt user identities \(uid\);  
\(\mathcal{Q}_{\mathsf{I}}\): a set storing \(isk\) when \(\mathsf{CA}\) issues a credential for the ticket issuer. \(\mathcal{Q}_{\mathsf{V}}\): a set storing \((vid,\vec{v},tk_{vid,\vec{v}})\) each time \(t\) policymakers cooperate to generate a policy key for a verifier \(vid\) with policy \(\vec{v}\). \(\mathcal{Q}_{\mathsf{TKT}}\): a set storing \((uid,pst,tkt,dsid,VP,\mathsf{CTX})\) each time \(\mathsf{I}\) issues a ticket for an honest user \(uid\). \(\mathcal{Q}_{\mathsf{TOK}}\): a set storing \((uid,tok,\vec{u},\vec{v},vid)\) each time \(\mathsf{U}\) create an access token to a designated verifier \(vid\) with a policy \(\vec{v}\). **Oracles**. \(-\)\(\mathcal{O}_{\mathsf{Reg}_{i}}()\): It is an oracle that can be used to issue a public key credential for the ticket issuer. It generates a key pair by running \((isk,ipk)\leftarrow\mathsf{PriSign.IssuerKeyGen}()\), and then issues a credential to the ticket issuer by running \(icred\leftarrow\mathsf{PriSign.IssuerKey}(\mathsf{I}(isk,ipk)\leftrightarrow \mathsf{CA}(msk,mpk))\). Finally, it adds \(isk\) to \(\mathcal{Q}_{\mathsf{I}}\) and returns \((ipk,icred)\). \(-\)\(\mathcal{O}_{\mathsf{Cor}_{\mathsf{I}}}()\): an oracle that can be used to corrupt the ticket issuer by returning \(isk\). \(-\)\(\mathcal{O}_{\mathsf{Reg}_{i}}(vid,\vec{v})\): an oracle that can be used to generate a policy key for a ticket verifier \(vid\) with a policy \(\vec{v}\). If \((vid,\vec{v})\in\mathcal{Q}_{\mathsf{V}}\), then it returns \(\bot\); otherwise, it runs \(\{tk_{vid,\vec{v},i}\leftarrow\mathsf{PriSign.IssuerKeyGen}()\), \(\mathsf{PriSign.IssuerKey}(psk_{vid,\vec{v}},id,\vec{v})\}_{i\in[\mathsf{I},t]}\), then runs \(tk_{vid,\vec{v}}\leftarrow\mathsf{PriSign.AsggrPolKey}(vid,\vec{v},\)  
\(\{tk_{vid,\vec{v},i},pvk_{i}\}_{i\in[\mathsf{I},t]})\), and finally adds \((vid,\vec{v},tk_{vid,\vec{v}})\) to \(\mathcal{Q}_{\mathsf{V}}\). \(-\)\(\mathcal{O}_{\mathsf{Cor}_{\mathsf{V}}}(vid,\vec{v})\): an oracle that can be used to corrupt a ticket verifier \(vid\) with the policy \(\vec{v}\) by returning \(tk_{vid,\vec{v}}\). \(-\)\(\mathcal{O}_{\mathsf{Reg}_{i}}(uid,\{m_{j}\}_{j\in[\mathsf{I},q]})\): an oracle that can be used to issue an attribute-based credential for an honest user \(uid\) with an attribute set \(\{m_{j}\}_{j\in[\mathsf{I},q]}\). If \(uid\in\mathcal{CU}\cup\mathcal{UU}\), then it returns \(\bot\); otherwise, it generates keys by running \((usk,upk,utk)\leftarrow\mathsf{PriSign.UserKeyGen}()\), then issues a credential to user \(uid\) by running \((ucred,\mathcal{L}^{\prime})\leftarrow\mathsf{PriSign.UserReg}(\mathsf{U}(uid, usk,upk,utk,\{m_{j}\}_{j\in[\mathsf{I},q]})\leftrightarrow\mathsf{CA}(msk,mpk, \mathcal{L}))\). Finally, it adds \((uid,usk,upk,utk,\{m_{j}\}_{j\in[\mathsf{I},q]}\)_{i\in[\mathsf{I},q]}\)_, \(ucred)\) to \(\mathcal{Q}_{\mathsf{HU}}\). \(-\mathcal{O}_{\mathsf{Cor}_{\mathsf{UI}}}(uid)\): an oracle that can be used to corrupt an honest user \(uid\). If \(uid\in\mathcal{Q}_{\mathsf{CU}}\), then it returns \(\bot\). If \(uid\in\mathcal{Q}_{\mathsf{HU}}\), then it returns \(\bot\).