# Methodology of Testing the Security of Cryptographic Protocols Using the CMMTree Framework
## 1 Introduction  
One of the significant aspects of modern civilization is Internet communication. People worldwide send vast amounts of information over the Internet at any given moment. Computer network users use banking, health, social, and shopping platforms and communicate via instant messaging. We can also observe the rapid development of communication between devices that make up the Internet of Things or Wireless Sensor Networks. Such networks connect various devices and sensors to exchange information between the devices and between them and other networks, nodes used to process and store data [1; 2; 3]. First, some honest users want to exchange data with other users or network nodes. However, on the web, we can meet rogue users called Intruders. The activity of an Intruder in the network depends on his imagination, needs and abilities. For example, an attacker might intercept messages sent by honest users, attempt to read, modify, and forward them, or intercept communications and retransmit messages to trick other network users. We should always be concerned that online activity can lead honest users to many losses, such as data loss and identity or material damage if an Intruder acquires credentials with a bank [4]. For this reason, securing communication between users plays an essential and pivotal role in exchanging messages. The communication course is supervised by complex communication protocols, constituting a message exchange sequence between users. Nevertheless, security protocols are used to secure essential parts of such communication. Such protocols may be one-way, mutual authentication, or establishing and exchanging a session key [5; 6]. In recent decades, numerous security protocols have been put out (see [7; 8; 9; 10; 11; 12; 13]). Each of them has been thoroughly tested regarding the level of security that a given protocol should provide. The provided studies suggested that the protocols could be broken in many cases (for example, Ref. [7]). The broken protocols have some vulnerabilities, thanks to which an Intruder can intercept and use data transferred between users, modify them, and transmit them again. The problem of potential attacks by dishonest users is related to verifying protocol security levels constantly. With this need in mind, we present a security protocol verification tool in this article. Primarily, this tool uses the Conditional Multiway Mapped Tree (CMMTree) methodology described in [14]. CMMTree is the primary framework that defines the structure and mechanism of operation of all the software we have created. The solution allows building trees reflecting various relationships between the processed data. Moreover, the implemented tool considers the approach proposed by [PERSON] et al. in [15; 16], enabling the modelling of information about the security protocol execution step. In the proposed approach, a single statement about the protocol execution step describes all actions performed by users during the protocol step (generating confidential information, knowledge acquisition) and the conditions for executing the protocol step (knowledge needs of the sender). This approach is advantageous and practical because, thanks to it, we can model each piece of information necessary to find an attack upon the protocol. Therefore, we decided to strengthen the mentioned approach with tree optimization methods (pruners) and a lexicographic sort rule and implement an automated security protocol verification tool according to the CMMTree methodology.