A New Effective Approach for Modelling and Verification of Security Protocols.
Olga Siedlecka-Lamch, Mirosław Kurkowski, Henryk Piech · 2012
This paper presents a new mathematical model, and based on it a new automatic approach for verification of security protocols. This model contains a representation of the actions executed during the realization of the protocol, and the representation of changes of knowledge states of honest users and an Intruder. These possibilities are given to us by the formal definition (also shown in the article) of the runs representing the execution of protocols in real, open computer networks. Our model uses a simple and intuitive idea of chains of states for which the concept of protocol's properties verification has been given. This idea has been implemented, and the results presented in this article are compared with the results obtained by the use of the best verification tools.