Abstract
Standard approaches to the formal and automated analysis of security protocols typically do not consider explicitly the fact that certain protocols require the agents to move to specific locations in order to send or receive particular messages. In this paper, we formalise a formal and automated approach in which security protocols with explicit agent movement are analysed in the presence of a Dolev-Yao attacker. We define movements as timed processes in an applied pi-calculus that allows us to build traces that show how the location and the movements of the agents and of the attacker significantly affect the execution of a protocol as well as the execution of possible attacks. We have automated our approach by using the UPPAAL tool. As proof-of-concept, we show our approach in action by analysing several security properties of a concrete case study, the SegCom protocol for vehicular ad-hoc networks.
| Original language | English |
|---|---|
| Title of host publication | ITASEC 2023: The Italian Conference on CyberSecurity |
| Publisher | CEUR Workshop Proceedings |
| Number of pages | 16 |
| Publication status | Accepted/In press - 28 Mar 2023 |