Using TLA+/TLC for Modeling and Verification of Cryptographic Protocols

Interacting in open networks carries certain risks. To ensure the information security of network interaction participants, cryptographic protocols (CrPs) are used. High levels of security can be achieved through their formal verification. A common formal method for verifying the CrP is model checking. In this study, we propose using the TLA+/TLC toolset to check models of CrP. This toolset is widely applied in various practical fields. In the TLA+ specification language, the protocol model and the required security properties in the form of invariants are defined. The protocol model describes its behavior as a transition system containing all possible states of the protocol model and transitions between them. The TLC model checker is employed to automatically verify that the model meets the required properties. The task of verifying the CrP has its specifics. This study proposes three modeling techniques that take into account the specifics of both the task and the TLA+/TLC toolset being used. The first technique involves replacing a system consisting of an arbitrary number of agents with a three-agent system. This simplifies the model and reduces its state space. The second technique is related to representing transmitted messages as a hierarchical structure, allowing encrypted messages to be nested within others. The third technique consists of optimizing the model to improve the performance of the TLC model checker by defining a function that generates only those elements leading to transitions between states in the model. These techniques simplify the model and reduce the verification time. We demonstrate the application of these results on a simple protocol example—the Needham–Schroeder (NS) public-key authentication protocol. After detecting a known vulnerability in the original protocol by using TLC, we model and verify an improved version. The verification results show that the new version of the protocol does not have this vulnerability.