# Detecting Colluding Inter-App Communication in Mobile Environment
## 2 Model Checking Background
* \([K]\phi\) and \(\langle K\rangle\phi\) are the modal operators (as shown by (17) and (18) in Table 2): \([K]\phi\) is satisfied by a state, which, for every performance of an action in \(K\), evolves in a state obeying \(\phi\); while \(\langle K\rangle\phi\) is satisfied by a state, which can evolve to a state obeying \(\phi\) by performing an action in \(K\). In Table 2 is reported the precise definition of the satisfaction of a closed formula \(\varphi\) by a state \(s\) (denoted \(s\models\varphi\)). where:  
* for each \(n\), \(\
u Z^{n}.\varphi\) and \(\mu Z^{n}.\varphi\) are defined as: \[ \begin{array}{ll}\
u Z^{0}.\varphi=\tttt&\mu Z^{0}.\varphi=\ff\\ \
u Z^{n+1}.\varphi=\varphi[\
u Z^{n}.\varphi/Z]&\mu Z^{n+1}.\varphi=\varphi[ \mu Z^{n}.\varphi/Z]\end{array} \] where the notation \(\varphi[\psi/Z]\) indicates the substitution of \(\psi\) for every free occurrence of the variable \(Z\) in \(\varphi\). \(\mu Z.\phi\) and \(\
u Z.\phi\) are the fixed point formulae, where \(\mu Z\) (\(\
u Z\)) (as shown by (19) and (20) in Table 2) _binds_ free occurrences of \(Z\) in \(\phi\). An occurrence of \(Z\) is free if it is not within the scope of a binder \(\mu Z\) (\(\
u Z\)). A formula is _closed_ if it contains no free variables. \(\mu Z.\phi\) is the least fix-point of the recursive equation \(Z=\phi\), while \(\
u Z.\phi\) is the greatest one. A transition system \(T\) satisfies a formula \(\phi\), denoted \(T\models\phi\), if and only if \(q\models\phi\), where \(q\) is the initial state of \(T\). A CCS process \(p\) satisfies \(\phi\) if \(S(p)\models\phi\). \begin{table}
\begin{tabular}{l l l l} \hline \hline \(p\) & \(\models\) & \(\tt ff\) & and & \(p\models\) & \(\tt tt\) & (14) \\ \(p\) & \(\models\) & \(\varphi\wedge\psi\) & iff & \(p\models\varphi\) and \(p\models\psi\) & (15) \\ \(p\) & \(\models\) & \(\varphi\vee\psi\) & iff & \(p\models\varphi\) or \(p\models\psi\) & (16) \\ \(p\) & \(\models\) &In (21)-(23), we consider the following abbreviations (where \(K\) ranges over sets of actions and \(\mathcal{A}\) is the set of all actions):  
\[\left\langle\alpha_{1},\,\ldots,\,\alpha_{n}\right\rangle\,\varphi \stackrel{{\text{def}}}{{=}} \left\langle\left\{\alpha_{1},\,\ldots,\,\alpha_{n}\right\} \right\rangle\,\varphi \tag{21}\] \[\left\langle-\right\rangle\varphi \stackrel{{\text{def}}}{{=}} \left\langle\mathcal{A}\right\rangle\,\varphi\] (22) \[\left\langle-K\right\rangle\varphi \stackrel{{\text{def}}}{{=}} \left\langle\mathcal{A}-K\right\rangle\,\varphi \tag{23}\]  
Finally, once defined the model and the temporal logic properties, we need something enabling us to check whether the model satisfies the defined properties. To this aim, formal verification is considered, a system process exploiting mathematical reasoning to verify if a system (i.e., the model) satisfies some requirement (i.e., the temporal logic properties). In recent years, several verification techniques were proposed, e.g., in [22], model checking is considered. In the model checking technique, the properties are formulated in temporal logic: each property is evaluated against the system i.e., the Labeled Transition System (LTS)-based model. The model checker accepts as input a model and a property, it returns \"true\" whether the system satisfies the formula and \"false\" otherwise. The performed check is an exhaustive state space search that is guaranteed to terminate since the model is finite. In this paper, we use the Concurrency WorkBench of the New Century (CWB-NC) ([[https://www3.cs.stonybrook.edu/](https://www3.cs.stonybrook.edu/)]([https://www3.cs.stonybrook.edu/](https://www3.cs.stonybrook.edu/))\(\sim\)cwb/), a widespread formal verification environment. The (CWB-NC) is our model checker and checks the presence of the PUT and GET properties in the applications, which finally verifies if there is a collusion. Note that we can easily use CWB-NC for the extended CCS since, as shown in [20], the new operators can be easily translated using the standard CCS ones.