## 4 Security Analysis
### Single-Step Attacks
Immediate transitions are controlled with transferring probabilities and guard functions. Timed transitions are measured with firing rate, whereas their firing time is an exponentially distributed random variable. Places \(P_{0}\) and \(P_{VW}\) initially have a token, respectively, representing that the ACD node receives the task. The executing process contains two steps: (1) task execution, and (2) arbitration. Task execution. If the place \(P_{0}\) holds a token, the task is allocated to each SCV. This is described by transition \(t_{d}\). After the place \(P_{i}\) receives the token, the corresponding \(SCV_{i}\) executes the task in _working_, \(attacked\), or \(error\) status and outputs a corresponding result. As shown in Table 3, tokens go in such three statuses with different firing probabilities. Such firing probabilities would be assigned based on the parameters measured in reality and current scores of vulnerabilities in each SCV [50]. These details are shown in Section 5. The place \(P_{WW}\), \(P_{AW}\), and \(P_{EW}\) receive tokens when SCVs return results. When all SCVs finish their task, they wait for RMS arbitration. Figure 5: SRN model. Arbitration. The arbitration process is mainly controlled by guard functions, which are listed in Table 4. Guard functions are Boolean expressions evaluated based on the net current marking. They disable the associated transition when the boolean expression returns false [26]. When all SCVs finish their task, tokens represented _correct_, _compromised_, _error_ results are intercepted at places \(P_{WW}\), \(P_{AW}\), and \(P_{EW}\) respectively due to the function _done_. According to the voting rule and the number of tokens in such \(P_{xW}\) places, RMS will pick one vector as the \"correct\" output. The picked vector reflects the state of this node. Hence one of the three functions _work_, _attack_, and _error_ will return 1, and the other two will return 0. The detailed definition of guard functions is listed in Table 4. Then the token in arbitrating sub-model goes to the corresponding place \(P_{X}\). After a while, the token moves \begin{table}
\begin{tabular}{l l} \hline \hline
\begin{tabular}{l} if(\#\(P_{V}==1\)) return (1); else return (0); \\ \end{tabular} \\ \hline \hline \end{tabular}
\end{table} 
Table 4: Guard functions of the SRN. \begin{table}
\begin{tabular}{c l} \hline \hline
**Notation** & **Description** \\ \hline \(P_{0}\) & The ACD node receives a task \\ \hline \(t_{d}/P_{i}\) & \(SCV_{i}\) starts proceeding the task \\ \hline \(t_{iw}/P_{WW}\) & \(SCV_{i}\) executes the task in _working_ status \\ \hline \(t_{ia}/P_{iA}\) & \(SCV_{i}\) is attacked \\ \hline \(t_{ie}/P_{iE}\) & There are some errors in \(SCV_{i}\) \\ \hline \(t_{ixw}/P_{WW}\) & \(SCV_{i}\) returns a _correct_ result to the RMS and waits for arbitrating \\ \hline \(t_{iaw}/P_{AW}\) & \(SCV_{i}\) returns a _compromised_ result to the RMS and waits for arbitrating \\ \hline \(t_{ixw}/P_{EW}\) & \(SCV_{i}\) returns another _error_ result to the RMS and waits for voting \\ \hline \(t_{x}/P_{V}\) & RMS finishes the vote \\ \hline \(P_{VW}\) & RMS is waiting for voting \\ \hline \(t_{xv}/P_{X}\) & The \(x\) vector is arbitrated as the right one. The ACD node is in an \(x\) state \\ \hline \(t_{xd}/P_{D}\) & The arbitration is done \\ \hline \(t_{f-a}/t_{f-e}\) & Flash and the next round \\ \hline \hline \end{tabular}
\end{table} 
Table 2: Notation in the SRN. \begin{table}
\begin{tabular}{c c} \hline \hline
**Transition** & **Firing Probability** \\ \hline \(t_{ia}\) & \(\lambda(t_{ia})=r_{i}\) \\ \hline \(t_{ie}\) & \(\lambda(t_{ix})\) \\ \hline \(t_{ixv}\) & \(\lambda(t_{ixv})=1-\lambda(t_{ia})-\lambda(t_{ie})\) \\ \hline \hline \end{tabular}
\end{table} 
Table 3: Firing probabilities of transitions in the SRN. to the place \(P_{D}\), indicating the end of arbitration. By this time, the function _done_ of the task sub-model returns 1, and all tokens move to place \(P_{V}\). Places \(P_{V}\) and \(P_{D}\) collect tokens in the proposed sub-models.