A Game Of Drones: Extending the Dolev-Yao Attacker Model With Movement

Research output: Chapter in Book/Report/Conference proceedingConference paperpeer-review

417 Downloads (Pure)

Abstract

We introduce the idea of modelling security protocols and attacks on protocols in a mobile setting, where agents need to move in order to send and receive messages. More specifically, we consider an environment involving drones capable of long-distance flight and “base stations” with which they can communicate. To specify and reason about such an environment, we formalise a pi-calculus and an attacker model that extends the Dolev-Yao model with capabilities for movement and “environmental knowledge” of the position of the other agents. As a simple but illustrative case study, we show how, under certain geographical conditions, the man-in-the-middle attack on the NSPK protocol would require multiple movements to complete successfully. We also define a simple normalisation procedure that allows the attacker to avoid carrying out redundant movements. This procedure also sets the basis for future, more refined normalisations and for investigations into how movements of the attacker and of the honest agents could be optimised.
Original languageEnglish
Title of host publicationProceedings of the 6th Workshop on Hot Issues in Security Principles and Trust (HotSpot 2020)
Subtitle of host publicationAffiliated with Euro S&P 2020, 7 September 2020, Genova, Italy
PublisherIEEE Computer Science Press
Number of pages13
Publication statusAccepted/In press - 21 Apr 2020

Fingerprint

Dive into the research topics of 'A Game Of Drones: Extending the Dolev-Yao Attacker Model With Movement'. Together they form a unique fingerprint.

Cite this