A Multiset Rewriting Model for Specifying and Verifying Timing Aspects of Security Protocols

Published in Foundations of Security, Protocols, and Equational Reasoning, Springer, LNCS 11565, pp 192-213, 2019

Musab A. Alturki, Tajana Ban Kirigin, Max Kanovich, Vivek Nigam, Andre Scedrov and Carolyn Talcott

Catherine Meadows has played an important role in the advancement of formal methods for protocol security verification. Her insights on the use of, for example, narrowing and rewriting logic has made possible the automated discovery of new attacks and the shaping of new protocols. Meadows has also investigated other security aspects, such as, distance-bounding protocols and denial of service attacks. We have been greatly inspired by her work. This paper describes the use of Multiset Rewriting for the specification and verification of timing aspects of protocols, such as network delays, timeouts, timed intruder models and distance-bounding properties. We detail these timed features with a number of examples and describe decidable fragments of related verification problems.