![]() Horne, Ross James ![]() ![]() ![]() 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 ▲] Detailed reference viewed: 39 (0 UL)![]() Horne, Ross James ![]() ![]() ![]() Scientific Conference (2022, August 10) To address known privacy problems with the EMV standard, EMVCo have proposed a Blinded Diffie-Hellman key establishment protocol, which is intended to be part of a future 2nd Gen EMV protocol. We point ... [more ▼] To address known privacy problems with the EMV standard, EMVCo have proposed a Blinded Diffie-Hellman key establishment protocol, which is intended to be part of a future 2nd Gen EMV protocol. We point out that active attackers were not previously accounted for in the privacy requirements of this proposal protocol, and demonstrate that an active attacker can compromise unlinkability within a distance of 100cm. Here, we adopt a strong definition of unlinkability that does account for active attackers and propose an enhancement of the protocol proposed by EMVCo. We prove that our protocol does satisfy strong unlinkability, while preserving authentication. [less ▲] Detailed reference viewed: 54 (6 UL)![]() ; Horne, Ross James ![]() ![]() in International Journal of Remote Sensing (2022), 43(5), 1881-1893 Detailed reference viewed: 44 (1 UL)![]() Acclavio, Matteo ![]() ![]() ![]() in Felty, Amy P. (Ed.) Proc. 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022) (2022) Logical time is a partial order over events in distributed systems, constraining which events precede others. Special interest has been given to series-parallel orders since they correspond to formulas ... [more ▼] Logical time is a partial order over events in distributed systems, constraining which events precede others. Special interest has been given to series-parallel orders since they correspond to formulas constructed via the two operations for "series" and "parallel" composition. For this reason, series-parallel orders have received attention from proof theory, leading to pomset logic, the logic BV, and their extensions. However, logical time does not always form a series-parallel order; indeed, ubiquitous structures in distributed systems are beyond current proof theoretic methods. In this paper, we explore how this restriction can be lifted. We design new logics that work directly on graphs instead of formulas, we develop their proof theory, and we show that our logics are conservative extensions of the logic BV. [less ▲] Detailed reference viewed: 29 (0 UL)![]() Gil Pons, Reynaldo ![]() ![]() ![]() in IEEE Computer Security Foundations Symposium, August 7 - 10, 2022, Haifa, Israel (2022) Detailed reference viewed: 70 (13 UL)![]() Horne, Ross James ![]() ![]() in Logical Methods in Computer Science (2021), 17(2), 241--2452 Detailed reference viewed: 23 (1 UL)![]() Horne, Ross James ![]() ![]() ![]() 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 ▲] Detailed reference viewed: 34 (5 UL)![]() ; Horne, Ross James ![]() in Logical Methods in Computer Science (2021), 17(3), 21240 Detailed reference viewed: 40 (0 UL)![]() ; ; Horne, Ross James ![]() in 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '21) (2021) Detailed reference viewed: 30 (0 UL)![]() Horne, Ross James ![]() ![]() in LICS '20: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (2020) Detailed reference viewed: 164 (5 UL)![]() Gabbay, Dov M. ![]() ![]() ![]() in Graphical Models for Security - 7th International Workshop (2020) Detailed reference viewed: 59 (11 UL)![]() Horne, Ross James ![]() in In 31st International Conference on Concurrency Theory (CONCUR 2020). (2020) Detailed reference viewed: 53 (3 UL)![]() Horne, Ross James ![]() ![]() ![]() 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 ▲] Detailed reference viewed: 87 (4 UL)![]() Horne, Ross James ![]() in ACM Transactions on Computational Logic (2019), 20(4), 221--2244 Detailed reference viewed: 61 (2 UL)![]() Horne, Ross James ![]() in 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). (2019) Detailed reference viewed: 34 (0 UL)![]() ; Horne, Ross James ![]() Scientific Conference (2019) Detailed reference viewed: 52 (0 UL)![]() ; ; et al 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 ▲] Detailed reference viewed: 33 (1 UL)![]() Horne, Ross James ![]() in Mathematical Structures in Computer Science (2019) Detailed reference viewed: 104 (0 UL)![]() Horne, Ross James ![]() ![]() in Proc.\ 5th International Workshop on Graphical Models for Security (GraMSec'18) (2018) Detailed reference viewed: 118 (10 UL)![]() Horne, Ross James ![]() in Proceedings of LICS '18: 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, Oxford, United Kingdom, July 9-12, 2018 (LICS '18) (2018) Quasi-open bisimilarity is the coarsest notion of bisimilarity for the π-calculus that is also a congruence. This work extends quasi-open bisimilarity to handle mismatch (guards with inequalities). This ... [more ▼] Quasi-open bisimilarity is the coarsest notion of bisimilarity for the π-calculus that is also a congruence. This work extends quasi-open bisimilarity to handle mismatch (guards with inequalities). This minimal extension of quasi-open bisimilarity allows fresh names to be manufactured to provide constructive evidence that an inequality holds. The extension of quasi-open bisimilarity is canonical and robust --- coinciding with open barbed bisimilarity (an objective notion of bisimilarity congruence) and characterised by an intuitionistic variant of an established modal logic. The more famous open bisimilarity is also considered, for which the coarsest extension for handling mismatch is identified. Applications to checking privacy properties are highlighted. Examples and soundness results are mechanised using the proof assistant Abella. [less ▲] Detailed reference viewed: 117 (8 UL) |
||