This is the topic of the project “Validation Using Modelling”, funded by Airbus through Tutech. The project has been conducted by the Institute for Secure Cyber-Physical Systems at Hamburg University of Technology under the leadership of Prof. Sibylle Fröschle. In three stages, from October 2022 to January 2026, a case study and corresponding methodology has been developed for “TAGA: a Touch and Go Assistant in the Aerospace Domain”. The route for certification is now laid out.
When an aircraft has landed and reached its parking slot at its destination airport many ground processes such as refuelling and preconditioning are performed. Currently standardized procedures are executed that sometimes are still paper-based. Machine-to-machine communication over wireless networks can improve these processes with respect to energy-efficiency, safety, and time. The aircraft will send sensor data such as fuel or temperature readings to the ground unit, and the ground unit will adapt the control of the process accordingly. To ensure that all data are securely exchanged the communication will be cryptographically authenticated and encrypted. However, the question remains: how do you securely establish the necessary cryptographic keys?
The approach behind TAGA is that a human ground operator can pair up the ground unit and the aircraft by means of a Near Field Communication (NFC) system. NFC is a short-range wireless communication technology that stands behind many everyday applications. For example, in contactless payment NFC enables us to carry out payment transactions by tapping a card or smartphone to a payment terminal. For TAGA, each ground unit and aircraft is equipped with an NFC reader, and the operator is provided with an NFC card.
During the physical setup of the ground process the operator usually walks from the ground unit to the aircraft, and back, e.g. to connect a supply hose. On this path, the operatortaps their card on the NFC readers and thereby enables an exchange of cryptographic messages between the machines for key establishment.
The corresponding verification methodology follows the modern approach of provable security: it does not merely rely on testing the system against a set of threat scenarios but establishes security and resilience properties against all combinations of a fine-grained attacker model. This involves that the underlying cryptographic protocols are modelled and
verified using formal methods and a semi-automated tool: the Tamarin Prover. Moreover, going beyond classical protocol verification, we have integrated requirements specific to the cyber-physical nature of the setting as well as resilience properties that take into account the international context of the airport setting. These give security and safety guarantees, even when the system is partially compromised, and, by design, mitigate risk in the event of a security breach.
Author:
Prof. Sibylle Fröschle
Hamburg University of Technology
Institute for Secure Cyber-Physical Systems
Phone: 040 30601- 4681
sibylle.froeschle(at)tuhh(dot)de
https://www.tuhh.de/scps/startseite
