# Detecting Colluding Inter-App Communication in Mobile Environment
## 2 Model Checking Background  
Preliminary concepts about the model checking technique implemented in our proposed approach are provided below. To apply model checking, we first represent a system using a formal specification language. In the following, we use the calculus of communicating systems (CCS) in a slightly extended form [20]. Systems are described in terms of processes. Processes perform actions, evolving to become new (and usually different) processes after each action. The syntax to describe processes is shown in (1):  
\[p::=DONE\mid x\mid\alpha.p\mid p+p\mid p;p\mid p\|p\mid p\backslash L\mid p[f] \tag{1}\]  
where \(\alpha\) ranges over a finite set of actions \(\mathcal{A}=\{\tau,a,\overline{a},b,\overline{b},...\}\). The action \(\tau\in\mathcal{A}\) is called the _internal action_. The set of _visible actions_, \(\mathcal{V}\), ranged over by \(l\), is defined as \(\mathcal{A}-\{\tau\}\). The set \(L\), in processes of the form \(p\backslash L\), is a set of actions such that \(L\subseteq\mathcal{V}\); whereas the relabeling function \(f\), in processes of the form \(p[f]\), is a total function, \(f:\mathcal{A}\rightarrow\mathcal{A}\), such that the constraint \(f(\tau)=\tau\) is respected. Each action \(l\in\mathcal{V}\) (resp. \(\overline{l}\in\mathcal{V}\)) has a _complementary action_\(\overline{l}\) (resp. \(l\)). It holds that \(\overline{l}=l\). Given \(L\subseteq\mathcal{V}\), with \(L^{+}\) we denote the set \(\{\overline{l},l\mid l\in L\}\). Variable \(x\) ranges over a set of _constant_ names: each constant \(x\) is defined by a constant definition \(x\stackrel{{\text{def}}}{{=}}p\), where \(p\) is called the _body_ of \(x\). \(DONE\) is the constant defined as \(\delta.nil\) that corresponds to a process whose task is to terminate performing only the action \(\delta\). The process \(nil\) cannot perform any action; it is also said to be \"deadlocked\". We denote the set of all processes by \(\mathcal{P}\). Given a set \(\mathcal{D}\) of constant definitions, the standard _operational semantics_\(\mathcal{S}\) is given by a relation \(\longrightarrow_{\mathcal{D}}\subseteq\mathcal{P}\times\mathcal{A}\times \mathcal{P}\). \(\longrightarrow_{\mathcal{D}}\) (\(\longrightarrow\) for short) is the least relation defined by the rules in Table 1. Given a process \(p\) the semantic of \(p\) is the automaton is called _standard transition system_ for \(p\) and is denoted \(\mathcal{S}(p)\). We now informally explain the semantics of an extended CCS process. Note that there is no rule for the process \(nil\), which thus cannot perform any action. In the **Done** rule, shown in (2) in Table 1, the process can perform \(\delta\) and then reaches a deadlocked state. In **Act** rule, shown in (3) in Table 1, the process \(a.p\) can perform the action \(\alpha\) to become the process \(p\). **Seq\({}_{1}\)** and **Seq\({}_{2}\)** rules represent the sequentialization of two processes, as shown in (4) and (5) in Table 1. The \(q\) process can start its execution only when the \(p\) process has terminated its execution by performing the \(\delta\) action. The **Sum** rule, shown in (6) in Table 1, states that \(p\) and \(q\) are alternative choices for the behavior of \(p+q\). The operator \(\|\) expresses the parallel execution. The **Par** rule, shown in (7) in Table 1, shows how processes in a parallel composition can behave autonomously: if the process \(p\) performs \(\alpha\) and becomes \(p^{\prime}\), then \(p\|q\) performs \(\alpha\) and becomes \(p^{\prime}\|q\) (similarly for \(q\)). When **Com\({}_{1}\)** and **Com\({}_{2}\)** rules