SAT-based verification of NSPK protocol including delays in the network
Sabina Szymoniak, Olga Siedlecka-Lamch, Mirosław Kurkowski · 2017
Time analysis of security protocols plays an important role in computer networks security. However, it has been mainly used in the form of timestamps analysis, without taking into account the parameters related to time. In this paper previous studies with use of a synchronized network of automata and SAT techniques have been extended with the temporal aspect and time parameters. A model was developed to show the strengths and weaknesses of the tested protocol depending on the known parameters of time. It has been shown that even potentially weak protocols can be used with appropriate time constraints. We can also find a way to make it safer by strengthening the critical points. As part of the work we have implemented a tool that helps us in the mentioned work and it allows to present some experimental results.