Autonomous Trustworthy Monitoring and Diagnosis of CubeSat Health (AtMonSat)

Report (2022)

This document is the final report concluding the execution of the AtMonSat project co-funded by the European Space Agency (ESA) under the Open Space Innovation Platform (OSIP) and the University of ... [more ▼]

This document is the final report concluding the execution of the AtMonSat project co-funded by the European Space Agency (ESA) under the Open Space Innovation Platform (OSIP) and the University of Luxembourg. AtMonSat concerns on-board fault detection using artificial neural networks for CubeSat systems and related spacecraft where computing resources are limited. In particular, the concrete problem scenario of malfunctioning of CubeSat board elements is considered. The AtMonSat final report provides the problem statement, discusses the performed experiments designed to generate proper sets of data, and presents the details of the proposed solution. The report shows the devised framework to be both effective and suitable for implementation on a CubeSat. [less ▲]

Cloud removal from satellite imagery using multispectral edge-filtered conditional generative adversarial networks

in International Journal of Remote Sensing (2022), 43(5), 1881-1893

Is Eve nearby? Analysing protocols under the distant-attacker assumption

in IEEE Computer Security Foundations Symposium, August 7 - 10, 2022, Haifa, Israel (2022)

Compositional Analysis of Protocol Equivalence in the Applied pi-Calculus Using Quasi-open Bisimilarity

in Theoretical Aspects of Computing -- ICTAC 2021 (2021)

This paper shows that quasi-open bisimilarity is the coarsest bisimilarity congruence for the applied pi-calculus. Furthermore, we show that this equivalence is suited to security and privacy problems ... [more ▼]

This paper shows that quasi-open bisimilarity is the coarsest bisimilarity congruence for the applied pi-calculus. Furthermore, we show that this equivalence is suited to security and privacy problems expressed as an equivalence problem in the following senses: (1) being a bisimilarity is a safe choice since it does not miss attacks based on rich strategies; (2) being a congruence it enables a compositional approach to proving certain equivalence problems such as unlinkability; and (3) being the coarsest such bisimilarity congruence it can establish proofs of some privacy properties where finer equivalences fail to do so. [less ▲]

Assuming Just Enough Fairness to make Session Types Complete for Lock-freedom

in 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '21) (2021)

Attack-Defence Frameworks: Argumentation-Based Semantics for Attack-Defence Trees.

in Graphical Models for Security - 7th International Workshop (2020)

Breaking Unlinkability of the ICAO 9303 Standard for e-Passports using Bisimilarity

in Breaking Unlinkability of the ICAO 9303 Standard for e-Passports using Bisimilarity (2019, September 23)

We clear up confusion surrounding privacy claims about the ICAO 9303 standard for e-passports. The ICAO 9303 standard includes a Basic Access Control (BAC) protocol that should protect the user from being ... [more ▼]

We clear up confusion surrounding privacy claims about the ICAO 9303 standard for e-passports. The ICAO 9303 standard includes a Basic Access Control (BAC) protocol that should protect the user from being traced from one session to another. While it is well known that there are attacks on BAC, allowing an attacker to link multiple uses of the same passport, due to differences in implementation; there still remains confusion about whether there is an attack on unlinkability directly on the BAC protocol as specified in the ICAO 9303 standard. This paper clarifies the nature of the debate, and sources of potential confusion. We demonstrate that the original privacy claims made are flawed, by uncovering attacks on a strong formulation of unlinkability. We explain why the use of the bisimilarity equivalence technique is essential for uncovering our attacks. We also clarify what assumptions lead to proofs of formulations of unlinkability using weaker notions of equivalence. Furthermore, we propose a fix for BAC within the scope of the standard, and prove that it is correct, again using a state-of-the-art approach to bisimilarity. [less ▲]

The Sub-Additives: A Proof Theory for Probabilistic Choice extending Linear Logic

in 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). (2019)

Global Types with Internal Delegation

in Theoretical Computer Science (2019)

This paper investigates a new form of delegation for multiparty session calculi. Usually, delegation allows a session participant to appoint a participant in another session to act on her behalf. This ... [more ▼]

This paper investigates a new form of delegation for multiparty session calculi. Usually, delegation allows a session participant to appoint a participant in another session to act on her behalf. This means that delegation is inherently an inter-session mechanism, which requires session interleaving. Hence delegation falls outside the descriptive power of global types, which specify single sessions. As a consequence, properties such as deadlock-freedom or lock-freedom are difficult to ensure in the presence of delegation. Here we adopt a different view of delegation, by allowing participants to delegate tasks to each other within the same multiparty session. This way, delegation occurs within a single session (internal delegation) and may be captured by its global type. To increase flexibility in the use of delegation, our calculus uses connecting communications, which allow optional participants in the branches of choices. By these means, we are able to express conditional delegation. We present a session type system based on global types with internal delegation, and show that it ensures the usual safety properties of multiparty sessions, together with a progress property. [less ▲]

The Attacker Does not Always Hold the Initiative: Attack Trees with External Refinement

in Proc.\ 5th International Workshop on Graphical Models for Security (GraMSec'18) (2018)