# Methodology of Testing the Security of Cryptographic Protocols Using the CMMTree Framework
## 2 Related Works  
Verifying the communication and security protocols is essential in securing network communication. Each network and used protocol are exposed to many attacks, for example, an impersonation attack during which the dishonest network user uses the identities of other network users. The choice of a security protocol depends on the implementation of the network and its purpose. Networks, like the Internet of Things or Wireless Sensor Networks, require secure authentication to protect the network against network node capture attacks. They use one protocol type. The vast area networks, where each stage of communication requires an appropriate level of security, will use different kinds of protocols (for example, communication, authentication, or key distribution) [1; 3; 17].  
So far, many methods of verifying cryptographic protocols have been proposed. Among them, some approaches use timed automata. Thanks to these methods, it is possible to demonstrate time's influence on communication security. In [18], [PERSON] proposed a method translation attack tree into timed automata. The author can verify security protocol vulnerabilities using a set network of timed automata. Also, [PERSON] et al. in [19] proposed attack tree models. Moreover, in [20], [PERSON] employed probabilistic timed automata for security protocol verification. The author tried to find the probability of breaking the encryption key.  
To verify the security of the protocol, we can also use formal proofs, e.g., BAN logic [21], Real-Or-Random (ROR) [22], Random Oracle Model (ROM) [23], or Syverson-Van Oorschot (SVO) [24]. However, these proofs are very complex, so for verifying protocols, we mostly used the tools that automatically implement the described methods for verifying protocols (Scyther [25,26], Tamarin [27,28], ProVerif [29, 30, 31], AVISPA [32], or the tool mentioned in [5]).  
It is worth pointing out that [PERSON] et al. proposed an interesting security protocol modelling and verification method in [15,16]. Authors consider the protocol step a tuple that includes information about each cryptographic primitive and users' activities. The tuple consists of information about:  
* execution and step;
* sender and receiver;
* sender's needs, i.e., those cryptographic primitives that the sender should know before step execution;
* cryptographic primitives that should be generated before step execution;
* receiver knowledge, i.e., those cryptographic primitives the receiver learns during step execution.  
The included information is enough for step definition because it describes each activity users perform during step execution. Also, they offer conditions and restrictions for step execution. Thanks to them, it is possible to create a protocol execution tree (ET) and find if there is any attack upon the security protocol. We observed that building a tree of each possible security protocol execution using CMMTree lets us thoroughly check all possible combinations of steps of these executions. For this reason, we decided to use [PERSON] et al.'s approach as a predicate for CMMTree and find if the CMMTree model is suitable for security protocol verification.