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 language | English |
---|---|
Title of host publication | Proceedings of the 6th Workshop on Hot Issues in Security Principles and Trust (HotSpot 2020) |
Subtitle of host publication | Affiliated with Euro S&P 2020, 7 September 2020, Genova, Italy |
Publisher | IEEE Computer Science Press |
Number of pages | 13 |
Publication status | Accepted/In press - 21 Apr 2020 |