# Methodology of Testing the Security of Cryptographic Protocols Using the CMMTree Framework
## 4 Description of the Methodology
### Primary Structures and Generalization of the Problem
For example, if an Intruder should send the following message \(<N_{A}\cdot N_{B}>_{K_{AB}}\) according to the execution structure, he has two possible ways to execute this step. Firstly, he can send the message if he knows the entire ciphertext. In a second method, he can send the message if he has in his knowledge each element forming a ciphertext (\(N_{A}\), \(N_{B}\), and \(K_{AB}\)). Analogous to the chain class, vectors of pointers represent the primitives whose actual type can be known only during input processing to the content class. At the predicate optimization stage, we used lexicographic sorting of protocol executions. The consistent use of a specific order of marking executions and steps definitely facilitates the analysis of both the tested protocol and the PF code under test. We compared the obtained ETs with trees built for randomized data to check the performance of the created PF. \begin{table}
\begin{tabular}{l l} \hline \hline
**Class** & **Description** \\ \hline player & information about honest and dishonest protocol participants \\ antichain & information about the ways of step execution by Intruder \\ id & information about the identifiers of protocol participants \\ aKey & information about users’ asymmetric keys \\ nonce & information about the random number that is used only once during the protocol execution \\ sKey & information about users’ symmetric keys \\ tStamp & information about the user timestamp that indicates the moment of the message creation \\ stepMeas & information about messages sent during the step \\ text & information about the message part that will be sent as plain text \\ aCryptogram & information about cryptogram encrypted by asymmetric key \\ sCryptogram & information about cryptogram encrypted by symmetric key \\ \hline \hline \end{tabular}
\end{table} 
Table 1: Class hierarchy prepared for protocol predicate. Each analyzed chain is uniquely identified by a pair of \((execution\_number,step\_number)\). The key to sorting the execution of the protocol is information identifying players and information provided by sets of cryptographic objects that the Intruder can use during the execution of the protocol. Also, it is worth mentioning that our methodology considers four Intruder models. The set of executions contains honest and dishonest (with Intruder) executions. Executions with Intruder are generated for the following Intruder models:  
* Dolev-Yao model--in which the Intruder controls the network, accesses transmitted messages, can intercept, block, and process messages against the protocol, but requires a decryption key for ciphertext information [52]. * Lazy Intruder--which can be considered a type of virus that can deliver complete messages, yet cannot alter or modify them [53; 54]. * Restricted Dolev-Yao--enabling a feature that the Dolev-Yao Intruder may only access messages specifically directed to them [5]. * Restricted Lazy Intruder--enabling a feature that the Lazy Intruder may only access messages specifically directed to them [5]. For example, in the NSPK protocol, we have two players (\(A\) and \(B\)). We add an Intruder (\(I\)) to the players' set. The sorted player set has an Intruder on zero indexes. Next, based on the players' set, we generate a set of all possible executions using variations without repetition. In this way, we obtained the following sorted set of executions (using sender \(\rightarrow\) recipient designation):  
\[I\to A,\ I\to B,\ A\to I,\ A\to B,\ B\to I,\ B\to A.\]  
Also, for each mentioned execution with the Intruder, we generate three parallel executions different from each other by cryptographic primitives used by the Intruder. For such an ordered set of possible protocol executions, one of the four paths containing an attack on the NSPK protocol will be represented by steps (10,1), (8,1), (8,2), (10,2), (10,3), and (8,3), i.e., step one of execution no. 10, step one of execution no. 8, and so on. We prepare the set of chains (SoC) for all possible protocol executions. Each chain has this same structure as described earlier.