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 (CrP) are used. High levels of security can be achieved through their formal verification. A common formal method for verifying CrP is model checking. In this work, we propose using the TLA+/TLC toolset to check models of CrP. This toolset is widely applied in various practical fields. The protocol model is defined in the TLA+ specification language, as well as the required security properties in the form of invariants. The model of a protocol 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 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 verification time. We demonstrate the application of these results on a simple protocol example — the Needham-Schroeder public key authentication protocol. After detecting a known vulnerability in the original protocol by using TLC, we model and verify an improved version. Verification results show that the new version of the protocol does not have this vulnerability.