# Methodology of Testing the Security of Cryptographic Protocols Using the CMMTree Framework
## 4 Description of the Methodology
### Predicate Function: Searching for the Best Possible Solution  
The predicate function \(p\) (2) (PF) plays a key role in the CMMTree model (1). The rules for connecting successive tree nodes written there will directly impact the correctness of the obtained results and the data analysis time. It will depend on these rules whether analyzing a given problem at all with specific computing resources will be possible. For such special data as chains of protocol executions, the use of only rules \"**for yes**\"--according to the general principle (if the conditions are met, the node can be attached)--is clearly insufficient. This is due to the fact that the ETs will grow to gigantic sizes, and very often, they will grow indefinitely. Therefore, rules \"**for not**\" are also necessary for the PF, to allow effective pruning of \"non-perspective\" branches during the construction of the ET. One of the main goals of this work was to develop and test a tool that would allow the study of various cryptographic protocols. Therefore, it was necessary to find a compromise between a solution specialized for a specific protocol and a generalized solution allowing processing and analyzing a broader spectrum of protocols. We used an approach in which our solution (and related protocol analysis) was tested in four main stages. The text-encoded protocol (in the ProToc language [35]) was loaded into the program at stage one. There, its validation was carried out for the correctness of the writing. Then the protocol was converted into object (binary) form, according to the class hierarchy described in Section 4.2. From this point on, all subsequent protocol processing was carried out using objects of this class hierarchy. In the second step, the original form of the protocol was processed into a set of protocol executions. These executions were ordered lexicographically (at the stage of searching for the best possible form of the PF) or shuffled when a given form of the PF was evaluated. \begin{table}
\begin{tabular}{c c c c c} \hline \hline
**Send.** \(\rightarrow\)**Rec.;** & **Execution \& Step;** & **Needs;** & **Products;** & **Knowledge;** \\ \hline \(A\to S\); & (9, 1); & ; & \(N_{A}\); & \(N_{A}\); & \(N_{A}\); \\ \(S\to I\); & (9, 2); & \((\)9, 2); & \(N_{A}\); & \(K_{IA}\); & \(\langle i(A)|i(I)|N_{A}|K_{IA}\rangle_{K_{AS}},i(I),N_{A},K_{IA}\); \\ \(I\to A\); & (9, 3); & \(\langle i(A)|i(I)|N_{A}|K_{IA}\rangle_{K_{AS}}\), \(\langle N_{A}\rangle_{K_{IA}}\); & ; & \(i(I)\), \(N_{A}\), \(K_{IA}\), \(N_{I}\); \\ \(I\to A\); & (9, 3); & \(K_{AS}\), \(N_{A}\), \(K_{IA}\), \(\langle N_{A}\rangle_{K_{IA}}\); & ; & \(i(I)\), \(N_{A}\), \(K_{IA}\), \(N_{I}\); \\ \(I\to A\); & (9, 3); & \(\langle i(A)|i(I)|N_{A}|K_{IA}\rangle_{K_{AS}}\), \(K_{IA}\), \(N_{A}\); & ; & \(i(I)\), \(N_{A}\), \(K_{IA}\), \(N_{I}\); \\ \(I\to A\); & (9, 3); & \(K_{AS}\), \(N_{A}\), \(K_{IA}\), \(K_{IA}\), \(N_{A}\); & ; & \(i(I)\), \(N_{A}\), \(K_{IA}\), \(N_{I}\); \\ \(A\to I\); & (9, 4); & \(N_{I}\); & ; & \(N_{I}\); \\ \hline \hline \end{tabular}
\end{table} 
Table 3: The fragment of SoC for KaoChow protocol (execution no. 9). In the third step, the input data were transformed into a set of chains, according to the methodology described in [15; 16]. In the last--fourth--stage of our research, different variants of the protocol ETs were created and evaluated. It was at this stage that the general CMMTree model--along with its functionalities (see Section 4.1)--was concretized for the chain type containing primitives (see Section 4.2) defining individual protocols. We tested various conditions that decide the attachment of subsequent tree nodes. These conditions were evaluated for their impact on tree construction time and the time to find possible attacks, as well as their impact on the overall size of the ET. We tried to prune the branches of each tree as much as possible (during its construction), ensuring that no important data were unnecessarily omitted at any stage of data processing.