Ross Horne

I am a Postdoctorate researcher within the Security and Trust of Software Systems (SaToSS) research group at the University of Luxembourg. The group is headed by Prof. Dr. Sjouke Mauw.


Research Collaborations and Contacts

News on Selected Publications

Why if-then-else in processes should be treated intuitionistically

31/3/2018: A paper on mismatch has been accepted at LICS 2018. The paper explains why mismatch (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 also intuitionistic, treating public information intuitionistically but private information 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.

Open Bisimilarity is Intuitionistic

Slides: A Characterisation of Open Bisimilarity using an Intuitionistic Modal Logic

See the press release for the award.

6/9/2017: A paper on modal logics for processes was awarded best paper at CONCUR 2017. 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'').

An extended journal verion is under review.

Causal Attack Trees

Slides: Specialisation of Attack Trees with Sequential Refinement

15/3/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".

A supporting technical report includes proofs omitted from the journal version.

Processes as Formulae

Slides: Private Names in Non-Commutative Logic

7/6/2016: The following paper on logical systems for process calculi is published in the proceedings of CONCUR 2016. The paper introduces a new logical system, directly embedding various process calculi, not limited to Robin Milner's famous π-calculus. The trick is, to capture private names, we decompose established self-dual nominal quantifiers into a De Morgan dual pair of nominal quantifiers. Following the tradition of Gabbay and Pitts, we use Cyrillic vowels И and Э, pronounced `new' and `wen' respectively, for our pair of nominal quantifiers. The logical system opens doors for reasoning about processes, particularly for soundly reasoning about processes deployed on scalable high-availability distributed systems.

A technical report submitted to a journal contains the details of the cut elimination proof. The state of the art of this research agenda is summarised in a companion submission accepted for publication in MSCS.

Session Types

Slides: Designing, Verifying and Monitoring Protocols inspired by Scribble.

16/12/2015: Two papers are published on session types employing techniques from proof theory:

Web of Linked Data

26/2/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 slides are available.

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.

Developing Research in Computer Science

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.

From 2012 to 2016, I was associate professor at Kazakh-British Technical University and a research associate at Romanian Academy.

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.

Background and Contacts

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 Sjouke Mauw, Alwen Tiu, Gabriel Ciobanu, Vladimiro Sassone, Mariangiola Dezani-Ciancaglini, Bogdan Aman, Shang-wei Lin, Barbara Kordy, Paola Giannini, Ilaria Castellani, Nicholas Gibbins, Cristian Văideanu, and Ki Yung Ahn. I look forward to future collaborations.

I am a European. I believe passionately that our doors should be open to everyone.