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

MTZK: Testing and Exploring Bugs in Zero-Knowledge (ZK) Compilers

Dongwei Xiao (The Hong Kong University of Science and Technology), Zhibo Liu (The Hong Kong University of Science and Technology), Yiteng Peng (The Hong Kong University of Science and Technology), Shuai Wang (The Hong Kong University of Science and Technology)

Read More

Mysticeti: Reaching the Latency Limits with Uncertified DAGs

Kushal Babel (Cornell Tech & IC3), Andrey Chursin (Mysten Labs), George Danezis (Mysten Labs & University College London (UCL)), Anastasios Kichidis (Mysten Labs), Lefteris Kokoris-Kogias (Mysten Labs & IST Austria), Arun Koshy (Mysten Labs), Alberto Sonnino (Mysten Labs & University College London (UCL)), Mingwei Tian (Mysten Labs)

Read More

Securing the Satellite Software Stack

Samuel Jero (MIT Lincoln Laboratory), Juliana Furgala (MIT Lincoln Laboratory), Max A Heller (MIT Lincoln Laboratory), Benjamin Nahill (MIT Lincoln Laboratory), Samuel Mergendahl (MIT Lincoln Laboratory), Richard Skowyra (MIT Lincoln Laboratory)

Read More

CounterSEVeillance: Performance-Counter Attacks on AMD SEV-SNP

Stefan Gast (Graz University of Technology), Hannes Weissteiner (Graz University of Technology), Robin Leander Schröder (Fraunhofer SIT, Darmstadt, Germany and Fraunhofer Austria, Vienna, Austria), Daniel Gruss (Graz University of Technology)

Read More