Ioana Boureanu, Stephan Wesemeyer (Surrey Centre for Cyber Security, University of Surrey)

Global Navigation Satellite Systems (GNSS) are critical for infrastructure like energy, telecommunications, and transportation, making their accuracy vital. To enhance security especially against location spoofing, in 2024, the Galileo GNSS system adopted the Timed Efficient Stream Loss-Tolerant Authentication (TESLA) protocol, for Navigation Message Authentication (NMA). However, past and present TESLA versions have lacked formal verification due to challenges in modelling their streaming and timing mechanisms. Given the importance of formal verification in uncovering protocol flaws, this work addresses that gap by formally modelling and verifying the latest TESLA protocol used in Galileo; we verify Galileo’s TESLA protocol in the well-known Tamarin prover. We discuss our findings and, since this is work-in-progress, we contextualise them in terms of next steps for us, as well as for future Navigation Message Authentication protocols inside GNSS systems.

View More Papers

“I’m 73, you can’t expect me to have multiple...

Ashley Sheil (Munster Technological University), Jacob Camilleri (Munster Technological University), Michelle O Keeffe (Munster Technological University), Melanie Gruben (Munster Technological University), Moya Cronin (Munster Technological University) and Hazel Murray (Munster Technological University)

Read More

The Skeleton Keys: A Large Scale Analysis of Credential...

Yizhe Shi (Fudan University), Zhemin Yang (Fudan University), Kangwei Zhong (Fudan University), Guangliang Yang (Fudan University), Yifan Yang (Fudan University), Xiaohan Zhang (Fudan University), Min Yang (Fudan University)

Read More

BrowserFM: A Feature Model-based Approach to Browser Fingerprint Analysis

Maxime Huyghe (Univ. Lille, Inria, CNRS, UMR 9189 CRIStAL), Clément Quinton (Univ. Lille, Inria, CNRS, UMR 9189 CRIStAL), Walter Rudametkin (Univ. Rennes, Inria, CNRS, UMR 6074 IRISA)

Read More

On Borrowed Time – Preventing Static Side-Channel Analysis

Robert Dumitru (Ruhr University Bochum and The University of Adelaide), Thorben Moos (UCLouvain), Andrew Wabnitz (Defence Science and Technology Group), Yuval Yarom (Ruhr University Bochum)

Read More