News 2020. I am editor of the newly created corner Logic for Security and Privacy within the Journal of Logic and Computation. We welcome submisions presenting diverse logical approaches to security and privacy problems.
News 2019. We are involved in running a new Interdisciplinary Master Program in Space Resources.
I summarise key results and research directions.
Equivalence checking and privacy. In my previous post as senior research fellow at Nanyang Technological University, Singapore, we solved several problems in protocol verification which use logic to give us a better understanding of congruences for process calculi [CONCUR'17, LICS'18]. These breakthroughs enable us to define, what I argue is, an optimal technique for verifying privacy properties using cryptographic calculi. The methodology was used to discover a privacy vulnerability for e-passports [ESORICS'19]. A future challenge is to build the technique into tools used to verify cryptographic protocols.
Linked Data. My PhD thesis at University of Southampton was on high-level languages for consuming data published on the Web. Such language abstractions [Sci.Comp.Prog.'14, JLAMP'15, JLAMP'16] allow programs to engage in sessions, where information discovered in queries can be used to form new queries, thereby navigating an interlinked Web of Data. Providing high-level language abstractions makes such programming tasks easier. This led me to the notion of a descriptive type system, which assists the data consumer during such interactions by generating suggestions for how inconsistencies in data may be resolved. Currently, related to this topic, I represent Luxembourg in an EU COST Action on Distributed Knowledge Graphs.
On session types and proof theory. I have proposed a proof theoretic approach to multi-party session types [PSI'15, SACS'15, CONCUR'20, TCS'20]. This work perhaps challenges the culture of type theorists, who, at times, may equate proof theory for types with the Curry-Howard correspondence. While the Curry-Howard correspondence is a remarkable achievement; my message to the session type community is that structural proof theory has much more to offer. I explain this in a video presented at CONCUR'20.
Attack trees. Attack trees, employed for security assessment, are also amenable to proof theoretic techniques [Fund.Inf.'16, GramSec'18, GramSec'20]. This is natural, since there are explanations of the logical systems in terms of game semantics and argumentation, which account for tensions between an attacker and defender competing on an attack surface.
Logic on Graphs. This is just too cool! We prove you can generalise the foundations of logic, so that the arguments we reason about in logic are graphs rather than formulae [LICS'20].
September 2019: Our paper presented at ESORICS 2019 reports on a privacy vulnerability in the ICAO 9303 standard used by ePassports. The vulnerability allows an individual who has recently passed through a passport control point to be reidentified, even without opening their passport.
Ihor Filimonov, Ross Horne, Sjouke Mauw and Zach Smith. Breaking Unlinkability of the ICAO 9303 Standard for ePassports Using Bisimilarity. In Computer Security – ESORICS 2019. Springer International Publishing, pp. 577–594, 2019. DOI:10.1007/978-3-030-29959-0_28
Here are the slides presented at ESORICS 2019. Also we have a repository providing practical evidence for the vulnerability and the following video (featuring Ihor Filimonov, Zach Smith, Sevdenur Baloglu, and Husam Al-Jawaheri) suggesting how the vulnerability may be exploited.
Note, for this proof of concept, this demonstration uses phones but an attacker may use more discrete and powerful devices.
Responsible disclosure: The vulnerability has been reported to ICAO, along with our recommendation for how ePassport readers may mitigate the vulnerability. ICAO issued a public response both confirming the vulnerability and reassuring the public that the scope of the vulnerability is limited. Their response was reported in Delano magazine and Paperjam.
The press release on this privacy vulnerability was also reported in news outlets including the Luxembourg Times , the Luxemburger Wort , and the magazine of FNR: science.lu. The resulting public interest caused a motion to be submitted to the Luxembourg parliament, leading to a joint response from the prime minister Xavier Bettel and foreign affairs minister Jean Asselborn. The vulnerability was also reported on the 100komma7 radio station and RTL TV stations. The video from RTL (in Luxembourgish) is reproduced below.
September 2017: A paper on modal logics for processes was awarded best paper at CONCUR 2017. See the press release for the award. The paper concerns a process equivalence called open bisimilarity which is easily automated and has desirable algebraic properties. Open bisimilarity treats input values in a call-by-need fashion. For example, if you receive a notification that an e-mail has arrived, there is no need to immediately check the email; you can continue working and later read the email when you need a detail contained within. The surprising insight of our paper is that there is a fundamentally intuitionistic logical characterisation of open bisimilarity (due to the call-by-need treatment of inputs inducing ``intuitionistic hereditary'').
Ki Yung Ahn, Ross Horne and Alwen Tiu. A Characterisation of Open Bisimilarity using an Intuitionistic Modal Logic. 28th International Conference on Concurrency Theory (CONCUR 2017). Editors: Roland Meyer and Uwe Nestmann; Volume 85; Article No. 7; pp. 7:1-7:17. Leibniz International Proceedings in Informatics. DOI:10.4230/LIPIcs.CONCUR.2017.7
An extended journal version is under review.
March 2018: A follow up paper, presented at LICS 2018, explains why the else branch in a statement such as "if M = N then P else Q" should be treated intuitionistically when reasoning about processes compositionally. In particular, we introduce the coarsest bisimilarity congruence for processes with if-then-else branching. The logical characterisation of this congruence is intuitionistic, but private information is treated classically. We highlight that this congruence and logic have impact in the area of verifying privacy protocols, where "else" branches avoid inadvertent leaks by providing dummy data.
Ross Horne, Ki Yung Ahn, Shang-wei Lin and Alwen Tiu. Quasi-Open Bisimilarity with Mismatch is Intuitionistic. In Proceedings of LICS '18: 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, Oxford, United Kingdom, July 9-12, 2018 (LICS '18). 10 pages. DOI:10.1145/3209108.3209125
A technical report explains how the technique (quasi-open bisimilarity) lifts to the full applied π-calculus. Lifting to the applied π-calculus, makes it possible to verify privacy properties of real-world cryptographic protocols.
September 2020: I have a series of papers on multiparty session types employing analytic proof calculi developed using methods from structural proof theory:
Ross Horne. Session Subtyping and Multiparty Compatibility Using Circular Sequents. 31st International Conference on Concurrency Theory (CONCUR 2020), Editors: Igor Konnov and Laura Kovacs Volume: 171 (2020): 12:1-12:22. Leibniz International Proceedings in Informatics (LIPIcs). DOI:10.4230/LIPIcs.CONCUR.2020.12
Ross Horne. The consistency and complexity of multiplicative additive system virtual. Scientific Annals of Computer Science, 25.2(2015): 245-316. DOI:10.7561/SACS.2015.2.245
Gabriel Ciobanu and Ross Horne. Behavioural analysis of sessions using the calculus of structures. In Perspectives of System Informatics, 10th International Andrei Ershov Informatics Conference, PSI 2015, in Memory of Helmut Veith, Kazan and Innopolis, Russia, August 24-27, 2015. Editors: Mazzara, Manuel, Voronkov, Andrei. LNCS 9609, pages 91-106, Springer (2015). DOI:10.1007/978-3-319-41579-6_8
These papers present a purely logical approach to a rich multiparty subtype system that also captures multiparty compatibility. The videos lectures presented at CONCUR 2020 explain the connections with proof theory and provide a compelling real-world example.
There are also older slides from 2015 connecing this line of work with Scribble: Designing, Verifying and Monitoring Protocols inspired by Scribble.
September 2019. We have proposed a propositional approach to delegation in session types, called internal delebation. Delegation allows a participant in a protocol to delegate to another participant the ability to act on their behalf. I emphasise that we work at a propositional level, since previous approaches to deligation make use of more complex higher-order mechanisms leading to complications that we can avoid.
Ilaria Castellani, Mariangiola Dezani-Ciancaglini, Paola Giannini and Ross Horne. Global types with internal delegation. Theoretical Computer Science, 807:128 - 153, 2020. Elsevier (2020). DOI:10.1016/j.tcs.2019.09.027
Matteo Acclavio, Ross Horne, and Lutz Straßburger. Logic Beyond Formulas: A Proof System on Graphs. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS ’20), July 8–11, 2020, Saarbrücken, Germany. ACM, New York, NY, USA, 33 pages (2020). DOI:10.1145/3373718.3394763
Here are two videos presented at LICS 2020.
Video above: an informal chat on logic beyond formulas.
Video above: a long (uncool) presentation, explaining details to experts.
November 2020 We have a position paper on argumentation-based semantics for attack-defence trees. Argumentation, arrising from the systematisation of conflict in legal arguments, and attack-defence tree, inspired by fault trees, are both based on around 50 years of research. They have obvious parallels, since both deal symoblically with conflict, cooperation and competition, that we draw attention to here. The semantics we propose combines several models of argumentation in a new way, permitting more flexible generalisations of attack-defence trees. An argumentation-based semantics can be used to turn attack trees into decision making mecahnisms, which means that it plays quite a different role from the semantics of attack trees that preserve attribute domains.
Dov M. Gabbay, Ross Horne, Sjouke Mauw, Leon van der Torre. Attack-Defence Frameworks: Argumentation-Based Semantics for Attack-Defence Trees. In: Eades III H., Gadyatskaya O. (eds) Graphical Models for Security. GraMSec 2020. Lecture Notes in Computer Science, vol 12419. Springer. (2020) DOI:10.1007/978-3-030-62230-5_8
March 2017: A paper on causal attack trees has been published in Fundamenta Informaticae. Causal attack trees profile the sub-goals of the proponent of an attack, by refining goals disjunctively, conjunctively and sequentially. We provide the machinery for determining whether one attack specialises another attack. Specialisation preserves correlations between answers to quantitative questions concerning attacks such as the "minimum attack time".
Ross Horne, Sjouke Mauw and Alwen Tiu. Semantics for Specialising Attack Trees based on Linear Logic. Fundamenta Informaticae 153(1-2). pp. 57-86. IOS Press. (2017) DOI:10.3233/FI-2017-1531
A supporting technical report includes proofs omitted from the journal version.
The game semantics behind such attack trees is explored in a paper presented at GraMSec'18. We emphasise the difference between when an attacker making a choice and when the environment or defender makes a choice in an attack scenario.
Ross Horne, Sjouke Mauw and Alwen Tiu. The Attacker Does not Always Hold the Initiative: Attack Trees with External Refinement. In proceedings G. Cybenko et al. (Eds.): The Fifth International Workshop on Graphical Models for Security Oxford (GraMSec 2018), UK - July 8, 2018. Lecture Notes in Computer Science 11086, pp. 90–110, Springer. 2019 DOI:10.1007/978-3-030-15465-3_6
September 2019: A series of papers on logical systems for process calculi has been published in the proceedings of CONCUR 2016, FSCD 2019 and in the journals TOCL and MSCS. These papers introduce new logical systems, directly embedding various process calculi, not limited to Robin Milner's famous π-calculus. To model private names in the π-calculus, the trick is to decompose established self-dual nominal quantifiers into a De Morgan dual pair of nominal quantifiers. We use Cyrillic vowels И and Э, pronounced `new' and `wen' respectively, for our pair of nominal quantifiers.
Ross Horne, Alwen Tiu, Bogdan Aman and Gabriel Ciobanu. Private Names in Non-Commutative Logic. 27th International Conference on Concurrency Theory (CONCUR 2016). Editors: Josée Desharnais and Radha Jagadeesan; Article No. 31; pp. 31:1-31:16. Leibniz International Proceedings in Informatics. DOI:10.4230/LIPIcs.CONCUR.2016.31
Ross Horne, Alwen Tiu, Bogdan Aman and Gabriel Ciobanu. De Morgan Dual Nominal Quantifiers Modelling Private Names in Non-Commutative Logic.. ACM Transactions in Computational Logic (TOCL), 20(4):22:1–22:44, ACM, 2019 DOI:10.1145/3325821
Ross Horne and Alwen Tiu. Constructing Weak Simulations from Linear Implications for Processes with Private Names. Mathematical Structures in Computer Science. Volume 29, Special Issue 8 (A special issue on structural proof theory, automated reasoning and computation in celebration of Dale Miller’s 60th birthday) September 2019 , pp. 1275-1308. Cambridge University Press (2019). DOI:10.1017/S0960129518000452
Ross Horne. 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). LIPIcs, 2019 DOI:10.4230/LIPIcs.FSCD.2019.23
Slides CONCUR'16: Private Names in Non-Commutative Logic
The paper published in Mathematical Structures in Computer Science develops proof normalisation techniques allowing us to extract executions of processes from proofs. We prove that linear implication is strictly finer than established weak simulation preorders (and hence probabilistic may testing). The technique lifts to a range of process calculi, not only the π-calculus.
The paper published in FSCD'19 shows that the techniques extend to probabilistic choice and probabilistic simulation. To achieve this we introduce the (probabilistic) sub-additives --- logical operators which lie between conjunction and disjunction that forbid weakening.
February 2016: The second of two journal papers on RDF Schema from the perspective of type systems is published in Journal of Logical and Algebraic Methods in Programming. These two papers represent a mature line of work that is ready to be implemented by a graduate student interested in making data on the Web easier to consume.
Gabriel Ciobanu, Ross Horne, and Vladimiro Sassone. Minimal type inference for Linked Data consumers. Journal of Logical and Algebraic Methods in Programming 84.4 (2015): 485-504. DOI:10.1016/j.jlamp.2014.12.005
Gabriel Ciobanu, Ross Horne, and Vladimiro Sassone. A descriptive type foundation for RDF Schema. Journal of Logical and Algebraic Methods in Programming 85.5 (2016): 681-706. DOI:10.1016/j.jlamp.2016.02.006
The first of the two papers provides a gentle introduction to consuming data on the Web called Linked Data and introduces a simple scripting language, with a conventional "prescriptive" type system, that makes the consumer's life easier.
The second of the two papers addresses more challenging aspects of RDF Schema types. The paper introduces a novel "descriptive" type system that evolves to describe data discovered at run-time by the Linked Data consumer. The descriptive type system can adapt to several modes of inference ranging from W3C standard compliant RDF Schema inference to something more accommodating. When the descriptive type system is unsure about the appropriate mode of inference, a warning with a menu of options is generated for the consumer reflecting the subjective nature of knowledge published on the Web.
The slides are available.
Before joining the "Security and Trust of Software Systems" group at University of Luxembourg, I was a senior research fellow in the Cyber Security Lab at Nanyang Technological University Singapore. There I was driving a project, lead by Ass.Prof. Alwen Tiu, that advanced the state of the art for symbolic analysis of security protocols. I also had the pleasure to contribute to projects under Ass.Prof. Shang-Wei Lin and Assoc.Prof. Liu Yang.
The proceedings of the workshop Embracing Global Computing in Emerging Economies (EGC2015) represents my effort to galvanise grass roots computer science research in Almaty and across the region.
Almaty, the cosmopolitan hub of Central Asia, is a magical city for winter sports, the steppe in spring, the mountains in summer and fruits of autumn.
I defended my PhD in computer science, with a thesis titled Programming Languages and Principles for Read-Write Linked Data, in 2011 under the supervision of Prof Vladimiro Sassone at University of Southampton, UK. My BA in Mathematics and Computer Science, with first class honours and a thesis titled Computable Cyclic Functions, was awarded by Oxford University, UK, in 2005.
I have had the honour and pleasure to collaborate with Matteo Acclavio, Bogdan Aman, Ilaria Castellani, Gabriel Ciobanu, Mariangiola Dezani-Ciancaglini, Ihor Filimonov, Dov M. Gabbay, Paola Giannini, Nicholas Gibbins, Shang-wei Lin, Sjouke Mauw, Vladimiro Sassone, Zach Smith, Lutz Straßburger, Alwen Tiu, Cristian Văideanu, and Leon van der Torre. I look forward to future collaborations.