Network’s delays in timed analysis of security protocols

Abstract

For several years, the analysis of security protocols time properties has been very important in the area of computer networks security. Up to now, however, it has been primarily used for timestamps analysis, without the other time related parameters being taken into account. As we can see in literature using formal, mathematical structures many problems can be considered and solved. In order to present the assets and liabilities of the tested protocol, depending on the known time parameters, we have proposed a mathematical model. For our research on security protocols time properties we use synchronized networks of timed automata – a specifically designed discrete mathematical model. This model allows to express and investigate the mentioned properties. In our work we also use encoding of structures and properties into Boolean propositional formulas that can be solved using SAT techniques. The investigation based on our model proved that even protocols which are potentially weak can be used with proper time constraints. In this paper we consider one of the popular security protocols: the WooLamPi protocol and its variations. By strengthening the crucial points, a way to improve protocol safety may also be found. Part of the work was to implement a tool which not only helps in the above mentioned activity, but also allows to display experimental results.