# Methodology of Testing the Security of Cryptographic Protocols Using the CMMTree Framework
## 5 Experimental Results
We can also see that attaching subsequent nodes can be carried out in two general cases:

* there are no nodes on the path \((length(\mathbf{P})=0\) ), **and** the current chain (as a candidate) is the chain of the first step of the protocol \((step(\beta)=1)\), **and** the set of needs necessary to perform the first step is the empty set \((needs(\beta)=\varnothing)\); there are appropriate nodes in the path \((length(\mathbf{P})>0\) ), **and** connecting the next node will not disturb the chronology (defined by the protocol) of the steps on the path \((chronology(\beta,\mathbf{P}))\), **and** on the path, there is a set of information that allows satisfying the set of needs necessary to connect the next node \((needs(\beta,\mathbf{P}))\), **and** the number of nonces generated by one user on the path matches the number of nonces per user declared in the protocol structure \((nonces(\beta,\mathbf{P}))\). The instructions in lines 6-9 do not affect the result returned by the operator(). They are auxiliary. They allow for potential attack paths (**AP**) to be remembered already during the construction of the tree. Below, but always before the instructions of lines 14-20, safety functions can be placed. Meeting the conditions they check should always cause the operator() to return false. We used such functions in the initial stages of studying different variants of the whole PF. For example, we were finishing a tree construction at level 10. Since CMMTree is a mapped structure (see Section 4.1), such controlled stopping of its construction allowed us to select single paths for detailed analysis to look for exploitable regularities. The need to use security functions in the PF considered the target indicates that the PF can still be improved. We are convinced that a properly defined PF does not require any additional protection against the uncontrolled expansion of the tree. We also tested a predicate function using only the pruning rules proposed by [PERSON] in [56], just as rules to prevent unlimited tree growth. Comparing the results obtained (see Figures 6 and 7), we found that our algorithm builds ETs much faster with fewer nodes. For example, we found attacks upon the Andrew\({}_{Lowe}\) protocol more than 160,000 times faster than using the pruning rules from [56], creating a tree with 278,848 times fewer nodes. We also see clearly that Andrew and Andrew\({}_{Lowe}\) protocols are in fact two different protocols, and how different the parametric descriptions are of the shape of their ETs. In Algorithm 2, we have specified the function chronology in pseudo-code. This function checks whether the candidate (\(\beta\)) for the current node's child matches the chronology of the information increment on the path. Figure 7: Parametric description of the execution tree shape for Andrew, Andrew\({}_{Lowe}\), and NSPK protocols obtained using the PF implementing only pruning rules proposed in [56]. ```
Data:\(\beta\)--candidate to be the current node child, P--data on path. Result:\(true\)or\(false\)
1 begin
2\(L\gets length(\textbf{P})\);
3 for\(i=0\)to\(L-1\)do
4 if\((\beta\_exec()==\textbf{P}[i]\_exec())\)then
5
6 for\(j=i\)to\(L-1\)do
7\(\{\)
8 if\((can\_be\_prune(\beta,\textbf{P}[j]))\)then
9\(\{\)
10 returnfalse;
11}
12
13
14}
15 if\((\beta\_step()==(\textbf{P}[i]\_step()+1))\)then
16
17 returntrue;
18
19}
20 else
21
22 for\(j=i\)to\(L-1\)do
23
24 if\((can\_be\_prune(\beta,\textbf{P}[j]))\)then
25
26 returnfalse;
27
28}
29 if\((\beta\_step()==1)\)then
30
31 returntrue;
32}
33}
34}
35 returnfalse;
36}
```
**Algorithm 2**_bool predicate<chain>::chronology(\(\beta\), P)

In this function, we have placed the rules \"for not\", as mentioned in Section 4.3, i.e., rules that result in pruning non-perspective branches. Here, we mainly rely on information regarding the protocol execution and step numbers. This information is returned, respectively, by the functions \(exec()\) and \(step()\). The general rule is very simple.