# Detecting Colluding Inter-App Communication in Mobile Environment
## 2 Model Checking Background
\begin{table}
\begin{tabular}{c c c c c} \hline \hline
**Done** & \(DONE\stackrel{{\delta}}{{\longrightarrow}}nil\) & (2) & **Act** & \(\alpha.p\stackrel{{\alpha}}{{\longrightarrow}}p\) & (3) \\
**Seq\({}_{1}\)** & \(\dfrac{p\stackrel{{\alpha}}{{\longrightarrow}}p^{\prime}}{p;q \stackrel{{\alpha}}{{\longrightarrow}}p^{\prime};q}\) & \(\alpha\
eq\delta\) & (4) & **Seq\({}_{2}\)** & \(\dfrac{p\stackrel{{\delta}}{{\longrightarrow}}nil}{p;q \stackrel{{\delta}}{{\longrightarrow}}q}\) & (5) \\
**Sum** & \(\dfrac{p\stackrel{{\alpha}}{{\longrightarrow}}p^{\prime}}{p+q \stackrel{{\alpha}}{{\longrightarrow}}p^{\prime}}\) & (and symmetric) & (6) & **Par** & \(\dfrac{p\stackrel{{\alpha}}{{\longrightarrow}}p^{\prime}}{p\|q \stackrel{{\alpha}}{{\longrightarrow}}p^{\prime}\|q}\) & \(\alpha\
eq\delta\) (and symmetric) & (7) \\
**Com\({}_{2}\)** & \(\dfrac{p\stackrel{{\delta}}{{\longrightarrow}}p^{\prime}}{p\|q \stackrel{{\delta}}{{\longrightarrow}}q^{\prime}}{p\|q \stackrel{{\delta}}{{\longrightarrow}}DONE}\) & (8) & **Com\({}_{1}\)** & \(\dfrac{p\stackrel{{\alpha}}{{\longrightarrow}}p^{\prime}}{p|q \stackrel{{\pi}}{{\longrightarrow}}p^{\prime}|q^{\prime}}\) & (9) \\
**Res** & \(\dfrac{p\stackrel{{\alpha}}{{\longrightarrow}}p^{\prime}}{p\backslash L \stackrel{{\alpha}}{{\longrightarrow}}p^{\prime}\backslash L}\) & \(\alpha\
ot\in L^{+}\) & (10) & **Rel** & \(\dfrac{p\stackrel{{\alpha}}{{\longrightarrow}}p^{\prime}}{p[f] \stackrel{{ f(\alpha)}}{{\longrightarrow}}p^{\prime}[f]}\) & (11) \\
**Con** & \(\dfrac{p\stackrel{{\alpha}}{{\longrightarrow}}p^{\prime}}{x \stackrel{{\alpha}}{{\longrightarrow}}p^{\prime}}\) & \(x\stackrel{{\text{def}}}{{=}}p\) & (12) & \\ \hline \hline \end{tabular}
\end{table} 
Table 1: Operational semantics for the extended calculus of communicating systems (CCS). (shown in (8) and (9) in Table 1) is used, we say that a _hundshake_ occurs. A handshake occurs only if two processes can simultaneously execute the complementary actions; the handshake results in an internal communication (the action \(\tau\)). When both possesses \(p\) and \(q\) have terminated their execution, the \(p\|q\) process becomes \(DONE\). The operator \(\backslash L\), in the **Res** rule (shown in (9) in Table 1), prevents actions in \(L^{+}\) to be done: if \(p\) can perform \(\alpha\) to become \(p^{\prime}\), then \(p\backslash L\) can perform \(\alpha\) to become \(p^{\prime}\backslash L\) only if \(\alpha\
ot\in L^{+}\). In the **Rel** rule, the operator \([f]\) renames actions by means of the relabeling function \(f\): if \(p\) can perform \(\alpha\) to become \(p^{\prime}\), then \(p[f]\) can perform \(f(\alpha)\) to become \(p^{\prime}[f]\). Finally, a constant \(x\) behaves as \(p\) if \(x\stackrel{{\text{def}}}{{=}}p\) as stated in the rule **Con**, (shown in (12) in Table 1). Roughly speaking, the **Con** rule states that a process behaves like its definition. Once we obtain the formal model of a system \(S\), we have to prove properties about \(S\). This is accomplished by using a temporal logic [21]. We use _mu-calculus_ logic [21]--the syntax is reported in (13). We suppose that \(Z\) ranges over a set of variables, \(K\) and \(R\) range over sets of actions \(\mathcal{A}\). \[ \begin{array}{rcl}\phi&::=&\tt\mid\ff\mid Z\mid\phi\vee\phi\mid\phi\wedge \phi\mid\\ &&[K]\phi\mid\langle K\rangle\phi\mid vZ.\phi\mid\mu Z.\phi\end{array}  \tag{13}\]  
The satisfaction of a formula \(\phi\) by a state \(s\) of a transition system, denoted by \(s\models\phi\), is so defined:  
* each state satisfies \(\tttt\) and no state satisfies \(\tt ff\) (as shown by (14) in Table 2);
* a state satisfies \(\phi_{1}\vee\phi_{2}\) (\(\phi_{1}\wedge\phi_{2}\)) if it satisfies \(\phi_{1}\) or (and) \(\phi_{2}\) (as shown by (15) in Table 2).