A Formal Treatment of Time and Range Integrity ChecK for Securing GNSS

<p dir="ltr">TRICK (Time and Range Integrity ChecK using Low Earth Orbiting Satellite for Securing GNSS) is a recently proposed protocol for more robust geometrically secure positioning system. Here, we cast TRICK's security requirements (explicit or implicit) into a cryptographic, cyber-physical framework. In so doing, we introduce ideal functionalities for authenticated broadcast and distance bounding (or two way ranging), and define new security notions of position- and time-soundness; these notions are of interest in their own right, aside of TRICK. We then outline a modular hybrid proof that reduces any successful position-spoofing strategy to either a cryptographic breach, a violation of the distance-bounding measurements, or a breach of physical constraints.</p>