Alturki, MA;
Ban Kirigin, T;
Kanovich, M;
Nigam, V;
Scedrov, A;
Talcott, C;
(2019)
A Multiset Rewriting Model for Specifying and Verifying Timing Aspects of Security Protocols.
In: Guttman, JD and Landwehr, CE and Meseguer, J and Pavlovic, D, (eds.)
Foundations of Security, Protocols, and Equational Reasoning: Essays Dedicated to Catherine A. Meadows.
(pp. pp. 192-213).
Springer: Berlin, Heidelberg.
Preview |
Text
Kanovich_AAM_CM_timed_intruders.pdf - Accepted Version Download (742kB) | Preview |
Abstract
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.
| Type: | Proceedings paper |
|---|---|
| Title: | A Multiset Rewriting Model for Specifying and Verifying Timing Aspects of Security Protocols |
| Event: | Catherine Meadows Festschrift Symposium, 22-23 May 2019, Fredericksburg, VA, USA |
| ISBN-13: | 9783030190514 |
| Open access status: | An open access version is available from UCL Discovery |
| DOI: | 10.1007/978-3-030-19052-1_13 |
| Publisher version: | https://doi.org/10.1007/978-3-030-19052-1_13 |
| Language: | English |
| Additional information: | This version is the author accepted manuscript. For information on re-use, please refer to the publisher’s terms and conditions. |
| Keywords: | authentication, computer architecture, computer networks, cryptographic protocols, cryptography, data privacy, formal security models, key management, logic and verification, network security, parallel processing systems, program compilers, public key cryptography, security protocols, semantics, software engineering, software evaluation, telecommunication traffic, type systems, verification |
| UCL classification: | UCL UCL > Provost and Vice Provost Offices > UCL BEAMS UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science |
| URI: | https://discovery.ucl.ac.uk/id/eprint/10081698 |
Archive Staff Only
 |
View Item |
