# 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
As already mentioned, the executions of each tested protocol were first sorted lexicographically. Thanks to this, we were able to ensure the repeatability of testing conditions for both the protocol and the PF. Then, the tested version of the PF was run several times on randomized data. We used the std::mersenne_twister_engine algorithm [55] to shuffle the set of chains of all possible protocol executions. We considered a tested rule to be valuable (in the context of the entire predicate) if the use of a given version of the PF allowed us to:  
* find attacks for those protocols for which attacks are known;
* significantly reduce the size of the ET of each of the tested protocols;
* obtain ETs with the same CMMTree shape description (5), both for sorted and shuffled data. We have also implemented mechanisms to prevent the tree from growing indefinitely, i.e., time safeguard and protection that controls the total number of nodes in the tree. The program stopped its work after saving all current results when 3 h of operation elapsed (for one protocol) or the tree reached one billion nodes. The values of these protections were determined experimentally for the computer we used. It was a desktop computer with an AMD Ryzen 9 3900X processor (12 cores, 24 threads) and 64 GB RAM, with the Linux Mint 20.3 operating system. The CMMTree construction algorithm has been implemented as a single separate thread of the program. Separate threads responsible for implementing the protections mentioned above did not block the processed data. Figure 4 illustrates the main idea behind the pruning process of the protocol ET. An example is the ET (a small fragment of it, to be precise) of the NSPK protocol. Here we can see that the CMMTree is actually a forest, that is, a collection of the root node subtrees. This is a case where the CMMTree root node does not represent any element from the input dataset. The nodes corresponding to the possible executions of the first step of the protocol are the roots of these subtrees. CMMTree takes the form of a forest with other protocols as well. We also see two exemplary protocol paths, resulting in the execution of its last step, and one path that can be considered \"non-perspective\" and suitable for pruning. The path of steps (18,1), (18,2), and (18,3) is the proper realization of the protocol. The path of (10,1), (8,1), (8,2), (10,2), (10,3), and (8,3) is the realization of the protocol with the participation of the Intruder, which ends with a successful attack. The path of (10,1), (1,1), (3,1), and so on is not prospective because it does not guarantee the expected progress in the execution of the protocol. Furthermore, each of these nodes could be treated as the root of another subtree, and thus, the forest would grow to infinity. Direct analysis of trees containing millions or tens of millions of nodes is beyond human perceptual capabilities--certainly beyond our abilities. Therefore, to evaluate the effects of our experiments, we used quantitative and qualitative measures describing the shape of created trees, as discussed in [14]. These measures are based on the parametric form of the CMMTree description expressed by Formula (5). Among other things, they allow us to immediately identify places where--in general--something happened, or something started to happen. Since CMMTree is a mapped structure, such a place can be reached in \(O(1)\) time without traversing the entire tree, which would always have to start at the root. In further explanations, we will also use:  
\[\Delta\Phi\ =\ \Phi_{l}\ -\ \Phi_{l-1}\ \text{and}\ \Delta\Lambda\ =\ \Lambda_{l}\ -\ \Lambda_{l-1}.\]  
Figure 5 and Table 4 portray three examples of CMMTree shape descriptions of the execution tree (ET) of the NSPK protocol obtained during the development of the predicate function (PF). Figure 5a is an image of the ET constructed using the PF without conditions that cause the pruning of branches--without \"for not\" conditions. Tree construction was terminated (on tree level \(l=10\)) after exceeding the 1 billion node limit.