# Methodology of Testing the Security of Cryptographic Protocols Using the CMMTree Framework
## 5 Experimental Results
If the compared chain objects come from the same execution \((\beta\_exec()==\textbf{P}[i]\_exec())\), and candidate (\(\beta\)) will not disturb the chronology of the data on the path (the \(can\_be\_prune(\beta,\textbf{P}[j])\) function returns false), then adding a new node is possible if the candidate's step is 1 larger than the last step executed \((\beta\_step()==(\textbf{P}[i]\_step()+1))\). However, if the candidate is an object from another execution, it must be an object representing the first step of the protocol \((\beta\_step()==1)\). As in the previous case, we call a function that checks whether this new path can be pruned before deciding to attach another node. Algorithm 3, shown below, is pseudo-code of the \(can\_be\_prune(\beta,\mathbf{P}[j])\) function. Here the role performed by the Intruder is checked. As mentioned earlier, the Intruder can impersonate an honest participant in the protocol. However, he cannot once again perform a step that was already performed by the other participant, regardless of whether it was a step performed by the sender or the receiver. Any such path, which after joining the candidate (\(\beta\)) could contain nodes of repeated steps, was classified as prunable, i.e., a path with a disturbed order of the steps performed. ``` Data:\(\beta\)--candidate to be the current node child, \(\mathbf{P}[j]\)--j-th chain on the path. Result:\(true\)or\(false\)
1 begin
2{3 pt}
3 if\((\beta\_step()==\mathbf{P}[j]\_step()\)
4 and
5\((\beta\_recipient()\_role()==\)
6\(\mathbf{P}[j]\_recipient()\_role()\)
7 or  
We are aware that there may or will be other protocols for which our solutions may not be effective or efficient enough. We are convinced, however, that in the approach we propose, it is possible to find a compromise between a solution specialized for one protocol and a general solution for a wider group of protocols. Conceptualization, J.P. and S.S.; methodology, J.P.; software, J.P.; validation, J.P. and S.S; formal analysis, S.S.; investigation, J.P. and S.S.; resources, S.S.; data curation, J.P. and S.S.; writing--original draft preparation, J.P. and S.S.; writing--review and editing, J.P. and S.S.; visualization, J.P.; supervision, J.P. and S.S.; project administration, J.P. All authors have read and agreed to the published version of the manuscript. This research received no external funding. Not applicable. Publicly available datasets were analyzed in this study. This data can be found here: [[https://cloud.icis.pcz.pl/s/zZmiiBA2](https://cloud.icis.pcz.pl/s/zZmiiBA2) YqxDprC]([https://cloud.icis.pcz.pl/s/zZmiiBA2](https://cloud.icis.pcz.pl/s/zZmiiBA2) YqxDprC) (accessed on 14 November 2023). The authors declare no conflict of interest. The following abbreviations are used in this manuscript: \begin{tabular}{l l} BAN logic & Burrows, Abadi, and Needham logic \\ CMMTree & Conditional Multiway Mapped Tree \\ ET & Execution Tree \\ NSPK protocol & Needham Schroeder Public Key protocol \\ PC & Pruning condition \\ PF & Predicate Function \\ ROM & Random Oracle Model \\ ROR & Real-Or-Random \\ RTTI & Run-Time Type Information \\ SoC & Set of Chains \\ SVO & Syverson-Van Oorschot logic \\ \end{tabular}