-
Brewer-Nash Scrutinised: Mechanised Checking of Policies featuring Write Revocation
Authors:
Alfredo Capozucca,
Maximiliano Cristiá,
Ross Horne,
Ricardo Katz
Abstract:
This paper revisits the Brewer-Nash security policy model inspired by ethical Chinese Wall policies. We draw attention to the fact that write access can be revoked in the Brewer-Nash model. The semantics of write access were underspecified originally, leading to multiple interpretations for which we provide a modern operational semantics. We go on to modernise the analysis of information flow in t…
▽ More
This paper revisits the Brewer-Nash security policy model inspired by ethical Chinese Wall policies. We draw attention to the fact that write access can be revoked in the Brewer-Nash model. The semantics of write access were underspecified originally, leading to multiple interpretations for which we provide a modern operational semantics. We go on to modernise the analysis of information flow in the Brewer-Nash model, by adopting a more precise definition adapted from Kessler. For our modernised reformulation, we provide full mechanised coverage for all theorems proposed by Brewer & Nash. Most theorems are established automatically using the tool {log} with the exception of a theorem regarding information flow, which combines a lemma in {log} with a theorem mechanised in Coq. Having covered all theorems originally posed by Brewer-Nash, achieving modern precision and mechanisation, we propose this work as a step towards a methodology for automated checking of more complex security policy models.
△ Less
Submitted 28 May, 2024; v1 submitted 20 May, 2024;
originally announced May 2024.
-
Thermal Earth Model for the Conterminous United States Using an Interpolative Physics-Informed Graph Neural Network (InterPIGNN)
Authors:
Mohammad J. Aljubran,
Roland N. Horne
Abstract:
This study presents a data-driven spatial interpolation algorithm based on physics-informed graph neural networks used to develop national temperature-at-depth maps for the conterminous United States. The model was trained to approximately satisfy the three-dimensional heat conduction law by simultaneously predicting subsurface temperature, surface heat flow, and rock thermal conductivity. In addi…
▽ More
This study presents a data-driven spatial interpolation algorithm based on physics-informed graph neural networks used to develop national temperature-at-depth maps for the conterminous United States. The model was trained to approximately satisfy the three-dimensional heat conduction law by simultaneously predicting subsurface temperature, surface heat flow, and rock thermal conductivity. In addition to bottomhole temperature measurements, we incorporated other physical quantities as model inputs, such as depth, geographic coordinates, elevation, sediment thickness, magnetic anomaly, gravity anomaly, gamma-ray flux of radioactive elements, seismicity, and electric conductivity. We constructed surface heat flow, and temperature and thermal conductivity predictions for depths of 0-7 km at an interval of 1 km with spatial resolution of 18 km$^2$ per grid cell. Our model showed superior temperature, surface heat flow and thermal conductivity mean absolute errors of 4.8° C, 5.817 mW/m$^2$ and 0.022 W/(C-m)$, respectively. The predictions were visualized in two-dimensional spatial maps across the modeled depths. This thorough modeling of the Earth's thermal processes is crucial to understanding subsurface phenomena and exploiting natural underground resources.
△ Less
Submitted 14 March, 2024;
originally announced March 2024.
-
Provably Unlinkable Smart Card-based Payments
Authors:
Sergiu Bursuc,
Ross Horne,
Sjouke Mauw,
Semen Yurkov
Abstract:
The most prevalent smart card-based payment method, EMV, currently offers no privacy to its users. Transaction details and the card number are sent in cleartext, enabling the profiling and tracking of cardholders. Since public awareness of privacy issues is growing and legislation, such as GDPR, is emerging, we believe it is necessary to investigate the possibility of making payments anonymous and…
▽ More
The most prevalent smart card-based payment method, EMV, currently offers no privacy to its users. Transaction details and the card number are sent in cleartext, enabling the profiling and tracking of cardholders. Since public awareness of privacy issues is growing and legislation, such as GDPR, is emerging, we believe it is necessary to investigate the possibility of making payments anonymous and unlinkable without compromising essential security guarantees and functional properties of EMV. This paper draws attention to trade-offs between functional and privacy requirements in the design of such a protocol. We present the UTX protocol - an enhanced payment protocol satisfying such requirements, and we formally certify key security and privacy properties using techniques based on the applied pi-calculus.
△ Less
Submitted 6 September, 2023;
originally announced September 2023.
-
A Logical Account of Subty** for Session Types
Authors:
Ross Horne,
Luca Padovani
Abstract:
We study the notion of subty** for session types in a logical setting, where session types are propositions of multiplicative/additive linear logic extended with least and greatest fixed points. The resulting subty** relation admits a simple characterization that can be roughly spelled out as the following lapalissade: every session type is larger than the smallest session type and smaller tha…
▽ More
We study the notion of subty** for session types in a logical setting, where session types are propositions of multiplicative/additive linear logic extended with least and greatest fixed points. The resulting subty** relation admits a simple characterization that can be roughly spelled out as the following lapalissade: every session type is larger than the smallest session type and smaller than the largest session type. At the same time, we observe that this subty**, unlike traditional ones, preserves termination in addition to the usual safety properties of sessions. We present a calculus of sessions that adopts this subty** relation and we show that subty**, while useful in practice, is superfluous in the theory: every use of subty** can be "compiled away" via a coercion semantics.
△ Less
Submitted 13 April, 2023;
originally announced April 2023.
-
Regulating trusted autonomous systems in Australia
Authors:
Rachel Horne,
Tom Putland,
Mark Brady
Abstract:
Australia is a leader in autonomous systems technology, particularly in the mining industry, borne from necessity in a geographically dispersed and complex natural environment. Increasingly advanced autonomous systems are becoming more prevalent in Australia, particularly as the safety, environmental and efficiency benefits become better understood, and the increasing sophistication of technology…
▽ More
Australia is a leader in autonomous systems technology, particularly in the mining industry, borne from necessity in a geographically dispersed and complex natural environment. Increasingly advanced autonomous systems are becoming more prevalent in Australia, particularly as the safety, environmental and efficiency benefits become better understood, and the increasing sophistication of technology improves capability and availability. Increasing use of these systems, including in the maritime domain and air domain, is placing pressure on the national safety regulators, who must either continue to apply their traditional regulatory approach requiring exemptions to enable operation of emerging technology, or seize the opportunity to put in place an agile and adaptive approach better suited to the rapid developments of the twenty first century. In Australia the key national safety regulators have demonstrated an appetite for working with industry to facilitate innovation, but their limited resources mean progress is slow. There is a critical role to be played by third parties from industry, government, and academia who can work together to develop, test and publish new assurance and accreditation frameworks for trusted autonomous systems, and assist in the transition to an adaptive and agile regulatory philosophy. This is necessary to ensure the benefits of autonomous systems can be realised, without compromising safety. This paper will identify the growing use cases for autonomous systems in Australia, in the maritime, air and land domains, assess the current regulatory framework, argue that Australia's regulatory approach needs to become more agile and anticipatory, and investigate how third party projects could positively impact the assurance and accreditation process for autonomous systems in the future.
△ Less
Submitted 7 February, 2023;
originally announced February 2023.
-
Assessing the Solid Protocol in Relation to Security & Privacy Obligations
Authors:
Christian Esposito,
Olaf Hartig,
Ross Horne,
Chang Sun
Abstract:
The Solid specification aims to empower data subjects by giving them direct access control over their data across multiple applications. As governments are manifesting their interest in this framework for citizen empowerment and e-government services, security and privacy represent pivotal issues to be addressed. By analyzing the relevant legislation, notably GDPR, and international standards, nam…
▽ More
The Solid specification aims to empower data subjects by giving them direct access control over their data across multiple applications. As governments are manifesting their interest in this framework for citizen empowerment and e-government services, security and privacy represent pivotal issues to be addressed. By analyzing the relevant legislation, notably GDPR, and international standards, namely ISO/IEC 27001:2011 and 15408, we formulate the primary security and privacy requirements for such a framework. Furthermore, we survey the current Solid protocol specifications regarding how they cover the highlighted requirements, and draw attention to potential gaps between the specifications and requirements. We also point out the contribution of recent academic work presenting novel approaches to increase the security and privacy degree provided by the Solid project. This paper has a twofold contribution to improve user awareness of how Solid can help protect their data and to present possible future research lines on Solid security and privacy enhancements.
△ Less
Submitted 15 October, 2022;
originally announced October 2022.
-
Space Plasma Physics: A Review
Authors:
Bruce T. Tsurutani,
Gary P. Zank,
Veerle J. Sterken,
Kazunari Shibata,
Tsugunobu Nagai,
Anthony J. Mannucci,
David M. Malaspina,
Gurbax S. Lakhina,
Shrikanth G. Kanekal,
Keisuke Hosokawa,
Richard B. Horne,
Rajkumar Hajra,
Karl-Heinz Glassmeier,
C. Trevor Gaunt,
Peng-Fei Chen,
Syun-Ichi Akasofu
Abstract:
Owing to the ever-present solar wind, our vast solar system is full of plasmas. The turbulent solar wind, together with sporadic solar eruptions, introduces various space plasma processes and phenomena in the solar atmosphere all the way to the Earth's ionosphere and atmosphere and outward to interact with the interstellar media to form the heliopause and termination shock. Remarkable progress has…
▽ More
Owing to the ever-present solar wind, our vast solar system is full of plasmas. The turbulent solar wind, together with sporadic solar eruptions, introduces various space plasma processes and phenomena in the solar atmosphere all the way to the Earth's ionosphere and atmosphere and outward to interact with the interstellar media to form the heliopause and termination shock. Remarkable progress has been made in space plasma physics in the last 65 years, mainly due to sophisticated in-situ measurements of plasmas, plasma waves, neutral particles, energetic particles, and dust via space-borne satellite instrumentation. Additionally high technology ground-based instrumentation has led to new and greater knowledge of solar and auroral features. As a result, a new branch of space physics, i.e., space weather, has emerged since many of the space physics processes have a direct or indirect influence on humankind. After briefly reviewing the major space physics discoveries before rockets and satellites, we aim to review all our updated understanding on coronal holes, solar flares and coronal mass ejections, which are central to space weather events at Earth, solar wind, storms and substorms, magnetotail and substorms, emphasizing the role of the magnetotail in substorm dynamics, radiation belts/energetic magnetospheric particles, structures and space weather dynamics in the ionosphere, plasma waves, instabilities, and wave-particle interactions, long-period geomagnetic pulsations, auroras, geomagnetically induced currents (GICs), planetary magnetospheres and solar/stellar wind interactions with comets, moons and asteroids, interplanetary discontinuities, shocks and waves, interplanetary dust, space dusty plasmas and solar energetic particles and shocks, including the heliospheric termination shock. This paper is aimed to provide a panoramic view of space physics and space weather.
△ Less
Submitted 29 September, 2022;
originally announced September 2022.
-
Bisimulations Respecting Duration and Causality for the Non-interleaving Applied $π$-Calculus
Authors:
Clément Aubert,
Ross Horne,
Christian Johansen
Abstract:
This paper shows how we can make use of an asynchronous transition system, whose transitions are labelled with events and which is equipped with a notion of independence of events, to define non-interleaving semantics for the applied $π$-calculus. The most important notions we define are: Start-Termination or ST-bisimilarity, preserving duration of events; and History-Preserving or HP- bisimilarit…
▽ More
This paper shows how we can make use of an asynchronous transition system, whose transitions are labelled with events and which is equipped with a notion of independence of events, to define non-interleaving semantics for the applied $π$-calculus. The most important notions we define are: Start-Termination or ST-bisimilarity, preserving duration of events; and History-Preserving or HP- bisimilarity, preserving causality. We point out that corresponding similarity preorders expose clearly distinctions between these semantics. We draw particular attention to the distinguishing power of HP failure similarity, and discuss how it affects the attacker threat model against which we verify security and privacy properties. We also compare existing notions of located bisimilarity to the definitions we introduce.
△ Less
Submitted 6 September, 2022;
originally announced September 2022.
-
Drift Orbit Bifurcations and Cross-field Transport in the Outer Radiation Belt: Global MHD and Integrated Test-Particle Simulations
Authors:
R. T. Desai,
J. P. Eastwood,
R. B. Horne,
H. J. Allison,
O. Allanson. E. J. Watt,
J. W. B. Eggington,
S. A. Glauert,
N. P. Meredith,
M. O. Archer,
F. A. Staples,
L. Mejnertsen,
J. K. Tong,
J. P. Chittenden
Abstract:
Energetic particle fluxes in the outer magnetosphere present a significant challenge to modelling efforts as they can vary by orders of magnitude in response to solar wind driving conditions. In this article, we demonstrate the ability to propagate test particles through global MHD simulations to a high level of precision and use this to map the cross-field radial transport associated with relativ…
▽ More
Energetic particle fluxes in the outer magnetosphere present a significant challenge to modelling efforts as they can vary by orders of magnitude in response to solar wind driving conditions. In this article, we demonstrate the ability to propagate test particles through global MHD simulations to a high level of precision and use this to map the cross-field radial transport associated with relativistic electrons undergoing drift orbit bifurcations (DOBs). The simulations predict DOBs primarily occur within an Earth radius of the magnetopause loss cone and appears significantly different for southward and northward interplanetary magnetic field orientations. The changes to the second invariant are shown to manifest as a dropout in particle fluxes with pitch angles close to 90$^\circ$ and indicate DOBs are a cause of butterfly pitch angle distributions within the night-time sector. The convective electric field, not included in previous DOB studies, is found to have a significant effect on the resultant long term transport, and losses to the magnetopause and atmosphere are identified as a potential method for incorporating DOBs within Fokker-Planck transport models.
△ Less
Submitted 4 September, 2021;
originally announced September 2021.
-
Interplanetary Shock-induced Magnetopause Motion: Comparison between Theory and Global Magnetohydrodynamic Simulations
Authors:
Ravindra T. Desai,
Mervyn P. Freeman,
Jonathan P. Eastwood,
Joseph. W. B. Eggington,
Martin. O. Archer,
Yuri Shprits,
Nigel P. Meredith,
Frances A. Staples,
I. Jonathan Rae,
Heli Hietala,
Lars Mejnertsen,
Jeremy P. Chittenden,
Richard B. Horne
Abstract:
The magnetopause marks the outer edge of the Earth's magnetosphere and a distinct boundary between solar wind and magnetospheric plasma populations. In this letter, we use global magnetohydrodynamic simulations to examine the response of the terrestrial magnetopause to fast-forward interplanetary shocks of various strengths and compare to theoretical predictions. The theory and simulations indicat…
▽ More
The magnetopause marks the outer edge of the Earth's magnetosphere and a distinct boundary between solar wind and magnetospheric plasma populations. In this letter, we use global magnetohydrodynamic simulations to examine the response of the terrestrial magnetopause to fast-forward interplanetary shocks of various strengths and compare to theoretical predictions. The theory and simulations indicate the magnetopause response can be characterised by three distinct phases; an initial acceleration as inertial forces are overcome, a rapid compressive phase comprising the majority of the distance travelled, and large-scale damped oscillations with amplitudes of the order of an Earth radius. The two approaches agree in predicting subsolar magnetopause oscillations with frequencies 2-13 mHz but the simulations notably predict larger amplitudes and weaker dam** rates. This phenomenon is of high relevance to space weather forecasting and provides a possible explanation for magnetopause oscillations observed following the large interplanetary shocks of August 1972 and March 1991.
△ Less
Submitted 9 July, 2021;
originally announced July 2021.
-
Unlinkability of an Improved Key Agreement Protocol for EMV 2nd Gen Payments
Authors:
Ross Horne,
Sjouke Mauw,
Semen Yurkov
Abstract:
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 dista…
▽ 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
Submitted 22 June, 2022; v1 submitted 5 May, 2021;
originally announced May 2021.
-
Assuming Just Enough Fairness to make Session Types Complete for Lock-freedom
Authors:
Rob van Glabbeek,
Peter Höfner,
Ross Horne
Abstract:
We investigate how different fairness assumptions affect results concerning lock-freedom, a typical liveness property targeted by session type systems. We fix a minimal session calculus and systematically take into account all known fairness assumptions, thereby identifying precisely three interesting and semantically distinct notions of lock-freedom, all of which having a sound session type syste…
▽ More
We investigate how different fairness assumptions affect results concerning lock-freedom, a typical liveness property targeted by session type systems. We fix a minimal session calculus and systematically take into account all known fairness assumptions, thereby identifying precisely three interesting and semantically distinct notions of lock-freedom, all of which having a sound session type system. We then show that, by using a general merge operator in an otherwise standard approach to global session types, we obtain a session type system complete for the strongest amongst those notions of lock-freedom, which assumes only justness of execution paths, a minimal fairness assumption for concurrent systems.
△ Less
Submitted 29 April, 2021;
originally announced April 2021.
-
Trust and Safety
Authors:
S. K. Devitt,
R. Horne,
Z. Assaad,
E. Broad,
H. Kurniawati,
B. Cardier,
A. Scott,
S. Lazar,
M. Gould,
C. Adamson,
C. Karl,
F. Schrever,
S. Keay,
K. Tranter,
E. Shellshear,
D. Hunter,
M. Brady,
T. Putland
Abstract:
Robotics in Australia have a long history of conforming with safety standards and risk managed practices. This chapter articulates the current state of trust and safety in robotics including society's expectations, safety management systems and system safety as well as emerging issues and methods for ensuring safety in increasingly autonomous robotics. The future of trust and safety will combine s…
▽ More
Robotics in Australia have a long history of conforming with safety standards and risk managed practices. This chapter articulates the current state of trust and safety in robotics including society's expectations, safety management systems and system safety as well as emerging issues and methods for ensuring safety in increasingly autonomous robotics. The future of trust and safety will combine standards with iterative, adaptive and responsive regulatory and assurance methods for diverse applications of robotics, autonomous systems and artificial intelligence (RAS-AI). Robotics will need novel technical and social approaches to achieve assurance, particularly for game-changing innovations. The ability for users to easily update algorithms and software, which alters the performance of a system, implies that traditional machine assurance performed prior to deployment or sale, will no longer be viable. Moreover, the high frequency of updates implies that traditional certification that requires substantial time will no longer be practical. To alleviate these difficulties, automation of assurance will likely be needed; something like 'ASsurance-as-a-Service' (ASaaS), where APIs constantly ** RAS-AI to ensure abidance with various rules, frameworks and behavioural expectations. There are exceptions to this, such as in contested or communications denied environments, or in underground or undersea mining; and these systems need their own risk assessments and limitations imposed. Indeed, self-monitors are already operating within some systems. To ensure safe operations of future robotics systems, Australia needs to invest in RAS-AI assurance research, stakeholder engagement and continued development and refinement of robust frameworks, methods, guidelines and policy in order to educate and prepare its technology developers, certifiers, and general population.
△ Less
Submitted 13 April, 2021;
originally announced April 2021.
-
An Analytic Propositional Proof System on Graphs
Authors:
Matteo Acclavio,
Ross Horne,
Lutz Straßburger
Abstract:
In this paper we present a proof system that operates on graphs instead of formulas. Starting from the well-known relationship between formulas and cographs, we drop the cograph-conditions and look at arbitrary undirected) graphs. This means that we lose the tree structure of the formulas corresponding to the cographs, and we can no longer use standard proof theoretical methods that depend on that…
▽ More
In this paper we present a proof system that operates on graphs instead of formulas. Starting from the well-known relationship between formulas and cographs, we drop the cograph-conditions and look at arbitrary undirected) graphs. This means that we lose the tree structure of the formulas corresponding to the cographs, and we can no longer use standard proof theoretical methods that depend on that tree structure. In order to overcome this difficulty, we use a modular decomposition of graphs and some techniques from deep inference where inference rules do not rely on the main connective of a formula. For our proof system we show the admissibility of cut and a generalisation of the splitting property. Finally, we show that our system is a conservative extension of multiplicative linear logic with mix, and we argue that our graphs form a notion of generalised connective.
△ Less
Submitted 20 October, 2022; v1 submitted 2 December, 2020;
originally announced December 2020.
-
Discovering ePassport Vulnerabilities using Bisimilarity
Authors:
Ross Horne,
Sjouke Mauw
Abstract:
We uncover privacy vulnerabilities in the ICAO 9303 standard implemented by ePassports worldwide. These vulnerabilities, confirmed by ICAO, enable an ePassport holder who recently passed through a checkpoint to be reidentified without opening their ePassport. This paper explains how bisimilarity was used to discover these vulnerabilities, which exploit the BAC protocol - the original ICAO 9303 sta…
▽ More
We uncover privacy vulnerabilities in the ICAO 9303 standard implemented by ePassports worldwide. These vulnerabilities, confirmed by ICAO, enable an ePassport holder who recently passed through a checkpoint to be reidentified without opening their ePassport. This paper explains how bisimilarity was used to discover these vulnerabilities, which exploit the BAC protocol - the original ICAO 9303 standard ePassport authentication protocol - and remains valid for the PACE protocol, which improves on the security of BAC in the latest ICAO 9303 standards. In order to tackle such bisimilarity problems, we develop here a chain of methods for the applied $π$-calculus including a symbolic under-approximation of bisimilarity, called open bisimilarity, and a modal logic, called classical FM, for describing and certifying attacks. Evidence is provided to argue for a new scheme for specifying such unlinkability problems that more accurately reflects the capabilities of an attacker.
△ Less
Submitted 1 June, 2021; v1 submitted 17 February, 2020;
originally announced February 2020.
-
Quantum rotation sensing with dual Sagnac interferometers in an atom-optical waveguide
Authors:
E. R. Moan,
R. A. Horne,
T. Arpornthip,
Z. Luo,
A. J. Fallon,
S. J. Berl,
C. A. Sackett
Abstract:
Sensitive and accurate rotation sensing is a critical requirement for applications such as inertial navigation [1], north-finding [2], geophysical analysis [3], and tests of general relativity [4]. One effective technique used for rotation sensing is Sagnac interferometry, in which a wave is split, traverses two paths that enclose an area, and then recombined. The resulting interference signal dep…
▽ More
Sensitive and accurate rotation sensing is a critical requirement for applications such as inertial navigation [1], north-finding [2], geophysical analysis [3], and tests of general relativity [4]. One effective technique used for rotation sensing is Sagnac interferometry, in which a wave is split, traverses two paths that enclose an area, and then recombined. The resulting interference signal depends on the rotation rate of the system and the area enclosed by the paths [5]. Optical Sagnac interferometers are an important component in present-day navigation systems [6], but suffer from limited sensitivity and stability. Interferometers using matter waves are intrinsically more sensitive and have demonstrated superior gyroscope performance [7-9], but the benefits have not been large enough to offset the substantial increase in apparatus size and complexity that atomic systems require. It has long been hoped that these problems might be overcome using atoms confined in a guiding potential or trap, as opposed to atoms falling in free space [10-12]. This allows the atoms to be supported against gravity, so a long measurement time can be achieved without requiring a large drop distance. The guiding potential can also be used to control the trajectory of the atoms, causing them to move in a circular loop that provides the optimum enclosed area for a given linear size [13]. Here we use such an approach to demonstrate a rotation measurement with Earth-rate sensitivity.
△ Less
Submitted 3 April, 2020; v1 submitted 11 July, 2019;
originally announced July 2019.
-
A Bisimilarity Congruence for the Applied pi-Calculus Sufficiently Coarse to Verify Privacy Properties
Authors:
Ross Horne
Abstract:
This paper is the first thorough investigation into the coarsest notion of bisimilarity for the applied pi-calculus that is a congruence relation: open barbed bisimilarity. An open variant of labelled bisimilarity (quasi-open bisimilarity), better suited to constructing bisimulations, is proven to coincide with open barbed bisimilarity. These bisimilary congruences are shown to be characterised by…
▽ More
This paper is the first thorough investigation into the coarsest notion of bisimilarity for the applied pi-calculus that is a congruence relation: open barbed bisimilarity. An open variant of labelled bisimilarity (quasi-open bisimilarity), better suited to constructing bisimulations, is proven to coincide with open barbed bisimilarity. These bisimilary congruences are shown to be characterised by an intuitionistic modal logic that can be used, for example, to describe an attack on privacy whenever a privacy property is violated. Open barbed bisimilarity provides a compositional approach to verifying cryptographic protocols, since properties proven can be reused in any context, including under input prefix. Furthermore, open barbed bisimilarity is sufficiently coarse for reasoning about security and privacy properties of cryptographic protocols; in constrast to the finer bisimilarity congruence, open bisimilarity, which cannot verify certain privacy properties.
△ Less
Submitted 6 November, 2018;
originally announced November 2018.
-
Generating Witness of Non-Bisimilarity for the pi-Calculus
Authors:
Ki Yung Ahn,
Ross Horne,
Alwen Tiu
Abstract:
In the logic programming paradigm, it is difficult to develop an elegant solution for generating distinguishing formulae that witness the failure of open-bisimilarity between two pi-calculus processes; this was unexpected because the semantics of the pi-calculus and open bisimulation have already been elegantly specified in higher-order logic programming systems. Our solution using Haskell defines…
▽ More
In the logic programming paradigm, it is difficult to develop an elegant solution for generating distinguishing formulae that witness the failure of open-bisimilarity between two pi-calculus processes; this was unexpected because the semantics of the pi-calculus and open bisimulation have already been elegantly specified in higher-order logic programming systems. Our solution using Haskell defines the formulae generation as a tree transformation from the forest of all nondeterministic bisimulation steps to a pair of distinguishing formulae. Thanks to laziness in Haskell, only the necessary paths demanded by the tree transformation function are generated. Our work demonstrates that Haskell and its libraries provide an attractive platform for symbolically analyzing equivalence properties of labeled transition systems in an environment sensitive setting.
△ Less
Submitted 30 May, 2017;
originally announced May 2017.
-
A Characterisation of Open Bisimilarity using an Intuitionistic Modal Logic
Authors:
Ki Yung Ahn,
Ross Horne,
Alwen Tiu
Abstract:
Open bisimilarity is defined for open process terms in which free variables may appear. The insight is, in order to characterise open bisimilarity, we move to the setting of intuitionistic modal logics. The intuitionistic modal logic introduced, called $\mathcal{OM}$, is such that modalities are closed under substitutions, which induces a property known as intuitionistic hereditary. Intuitionistic…
▽ More
Open bisimilarity is defined for open process terms in which free variables may appear. The insight is, in order to characterise open bisimilarity, we move to the setting of intuitionistic modal logics. The intuitionistic modal logic introduced, called $\mathcal{OM}$, is such that modalities are closed under substitutions, which induces a property known as intuitionistic hereditary. Intuitionistic hereditary reflects in logic the lazy instantiation of free variables performed when checking open bisimilarity. The soundness proof for open bisimilarity with respect to our intuitionistic modal logic is mechanised in Abella. The constructive content of the completeness proof provides an algorithm for generating distinguishing formulae, which we have implemented. We draw attention to the fact that there is a spectrum of bisimilarity congruences that can be characterised by intuitionistic modal logics.
△ Less
Submitted 9 August, 2021; v1 submitted 19 January, 2017;
originally announced January 2017.
-
De Morgan Dual Nominal Quantifiers Modelling Private Names in Non-Commutative Logic
Authors:
Ross Horne,
Alwen Tiu,
Bogdan Aman,
Gabriel Ciobanu
Abstract:
This paper explores the proof theory necessary for recommending an expressive but decidable first-order system, named MAV1, featuring a de Morgan dual pair of nominal quantifiers. These nominal quantifiers called `new' and `wen' are distinct from the self-dual Gabbay-Pitts and Miller-Tiu nominal quantifiers. The novelty of these nominal quantifiers is they are polarised in the sense that `new' dis…
▽ More
This paper explores the proof theory necessary for recommending an expressive but decidable first-order system, named MAV1, featuring a de Morgan dual pair of nominal quantifiers. These nominal quantifiers called `new' and `wen' are distinct from the self-dual Gabbay-Pitts and Miller-Tiu nominal quantifiers. The novelty of these nominal quantifiers is they are polarised in the sense that `new' distributes over positive operators while `wen' distributes over negative operators. This greater control of bookkee** enables private names to be modelled in processes embedded as formulae in MAV1. The technical challenge is to establish a cut elimination result, from which essential properties including the transitivity of implication follow. Since the system is defined using the calculus of structures, a generalisation of the sequent calculus, novel techniques are employed. The proof relies on an intricately designed multiset-based measure of the size of a proof, which is used to guide a normalisation technique called splitting. The presence of equivariance, which swaps successive quantifiers, induces complex inter-dependencies between nominal quantifiers, additive conjunction and multiplicative operators in the proof of splitting. Every rule is justified by an example demonstrating why the rule is necessary for soundly embedding processes and ensuring that cut elimination holds.
△ Less
Submitted 15 January, 2020; v1 submitted 18 February, 2016;
originally announced February 2016.
-
Bright Discrete Solitons in Spatially Modulated DNLS Systems
Authors:
P. G. Kevrekidis,
R. L. Horne,
N. Whitaker,
Q. E. Hoq,
D. Kip
Abstract:
In the present work, we revisit the highly active research area of inhomogeneously nonlinear defocusing media and consider the existence, spectral stability and nonlinear dynamics of bright solitary waves in them. We use the anti-continuum limit of vanishing coupling as the starting point of our analysis, enabling in this way a systematic characterization of the branches of solutions. Our stabilit…
▽ More
In the present work, we revisit the highly active research area of inhomogeneously nonlinear defocusing media and consider the existence, spectral stability and nonlinear dynamics of bright solitary waves in them. We use the anti-continuum limit of vanishing coupling as the starting point of our analysis, enabling in this way a systematic characterization of the branches of solutions. Our stability findings and bifurcation characteristics reveal the enhanced robustness and wider existence intervals of solutions with a broader support, culminating in the "extended" solution in which all sites are excited. Our eigenvalue predictions are corroborated by numerical linear stability analysis. Finally, the dynamics also reveal a tendency of the solution profiles to broaden, in line with the above findings. These results pave the way for further explorations of such states in discrete systems, including in higher dimensional settings.
△ Less
Submitted 7 July, 2015;
originally announced July 2015.
-
PT-symmetry Management in Oligomer Systems
Authors:
R. L. Horne,
J. Cuevas,
P. G. Kevrekidis,
N. Whitaker,
F. Kh. Abdullaev,
D. J. Frantzeskakis
Abstract:
We study the effects of management of the PT-symmetric part of the potential within the setting of Schrödinger dimer and trimer oligomer systems. This is done by rapidly modulating in time the gain/loss profile. This gives rise to a number of interesting properties of the system, which are explored at the level of an averaged equation approach. Remarkably, this rapid modulation provides for a cont…
▽ More
We study the effects of management of the PT-symmetric part of the potential within the setting of Schrödinger dimer and trimer oligomer systems. This is done by rapidly modulating in time the gain/loss profile. This gives rise to a number of interesting properties of the system, which are explored at the level of an averaged equation approach. Remarkably, this rapid modulation provides for a controllable expansion of the region of exact PT-symmetry, depending on the strength and frequency of the imposed modulation. The resulting averaged models are analyzed theoretically and their exact stationary solutions are translated into time-periodic solutions through the averaging reduction. These are, in turn, compared with the exact periodic solutions of the full non-autonomous PT-symmetry managed problem and very good agreement is found between the two.
△ Less
Submitted 16 August, 2013;
originally announced August 2013.
-
Local Type Checking for Linked Data Consumers
Authors:
Gabriel Ciobanu,
Ross Horne,
Vladimiro Sassone
Abstract:
The Web of Linked Data is the cumulation of over a decade of work by the Web standards community in their effort to make data more Web-like. We provide an introduction to the Web of Linked Data from the perspective of a Web developer that would like to build an application using Linked Data. We identify a weakness in the development stack as being a lack of domain specific scripting languages for…
▽ More
The Web of Linked Data is the cumulation of over a decade of work by the Web standards community in their effort to make data more Web-like. We provide an introduction to the Web of Linked Data from the perspective of a Web developer that would like to build an application using Linked Data. We identify a weakness in the development stack as being a lack of domain specific scripting languages for designing background processes that consume Linked Data. To address this weakness, we design a scripting language with a simple but appropriate type system. In our proposed architecture some data is consumed from sources outside of the control of the system and some data is held locally. Stronger type assumptions can be made about the local data than external data, hence our type system mixes static and dynamic ty**. Throughout, we relate our work to the W3C recommendations that drive Linked Data, so our syntax is accessible to Web developers.
△ Less
Submitted 1 August, 2013;
originally announced August 2013.
-
Linear and Nonlinear PT-symmetric Oligomers: A Dynamical Systems Analysis
Authors:
M. Duanmu,
K. Li,
R. L. Horne,
P. G. Kevrekidis,
N. Whitaker
Abstract:
In the present work we focus on the cases of two-site (dimer) and three-site (trimer) configurations, i.e. oligomers, respecting the parity-time (PT) symmetry, i.e., with a spatially odd gain-loss profile. We examine different types of solutions of such configurations with linear and nonlinear gain/loss profiles. Solutions beyond the linear PT-symmetry critical point as well as solutions with asym…
▽ More
In the present work we focus on the cases of two-site (dimer) and three-site (trimer) configurations, i.e. oligomers, respecting the parity-time (PT) symmetry, i.e., with a spatially odd gain-loss profile. We examine different types of solutions of such configurations with linear and nonlinear gain/loss profiles. Solutions beyond the linear PT-symmetry critical point as well as solutions with asymmetric linearization eigenvalues are found in both the nonlinear dimer and trimer. The latter feature is absent in linear PT-symmetric trimers, while both of them are absent in linear PT symmetric dimers. Furthermore, nonlinear gain/loss terms enable the existence of both symmetric and asymmetric solution profiles (and of bifurcations between them), while only symmetric solutions are present in the linear PT-symmetric dimers and trimers. The linear stability analysis around the obtained solutions is discussed and their dynamical evolution is explored by means of direct numerical simulations. Finally, a brief discussion is also given of recent progress in the context of PT-symmetric quadrimers.
△ Less
Submitted 14 October, 2012;
originally announced October 2012.
-
A Provenance Tracking Model for Data Updates
Authors:
Gabriel Ciobanu,
Ross Horne
Abstract:
For data-centric systems, provenance tracking is particularly important when the system is open and decentralised, such as the Web of Linked Data. In this paper, a concise but expressive calculus which models data updates is presented. The calculus is used to provide an operational semantics for a system where data and updates interact concurrently. The operational semantics of the calculus also t…
▽ More
For data-centric systems, provenance tracking is particularly important when the system is open and decentralised, such as the Web of Linked Data. In this paper, a concise but expressive calculus which models data updates is presented. The calculus is used to provide an operational semantics for a system where data and updates interact concurrently. The operational semantics of the calculus also tracks the provenance of data with respect to updates. This provides a new formal semantics extending provenance diagrams which takes into account the execution of processes in a concurrent setting. Moreover, a sound and complete model for the calculus based on ideals of series-parallel DAGs is provided. The notion of provenance introduced can be used as a subjective indicator of the quality of data in concurrent interacting systems.
△ Less
Submitted 22 August, 2012;
originally announced August 2012.
-
A Verified Algebra for Linked Data
Authors:
Ross Horne,
Vladimiro Sassone
Abstract:
A foundation is investigated for the application of loosely structured data on the Web. This area is often referred to as Linked Data, due to the use of URIs in data to establish links. This work focuses on emerging W3C standards which specify query languages for Linked Data. The approach is to provide an abstract syntax to capture Linked Data structures and queries, which are then internalised in…
▽ More
A foundation is investigated for the application of loosely structured data on the Web. This area is often referred to as Linked Data, due to the use of URIs in data to establish links. This work focuses on emerging W3C standards which specify query languages for Linked Data. The approach is to provide an abstract syntax to capture Linked Data structures and queries, which are then internalised in a process calculus. An operational semantics for the calculus specifies how queries, data and processes interact. A labelled transition system is shown to be sound with respect to the operational semantics. Bisimulation over the labelled transition system is used to verify an algebra over queries. The derived algebra is a contribution to the application domain. For instance, the algebra may be used to rewrite a query to optimise its distribution across a cluster of servers. The framework used to provide the operational semantics is powerful enough to model related calculi for the Web.
△ Less
Submitted 31 July, 2011;
originally announced August 2011.
-
Solitary Waves in Discrete Media with Four Wave Mixing
Authors:
R. L. Horne,
P. G. Kevrekidis,
N. Whitaker
Abstract:
In this paper, we examine in detail the principal branches of solutions that arise in vector discrete models with nonlinear inter-component coupling and four wave mixing. The relevant four branches of solutions consist of two single mode branches (transverse electric and transverse magnetic) and two mixed mode branches, involving both components (linearly polarized and elliptically polarized). T…
▽ More
In this paper, we examine in detail the principal branches of solutions that arise in vector discrete models with nonlinear inter-component coupling and four wave mixing. The relevant four branches of solutions consist of two single mode branches (transverse electric and transverse magnetic) and two mixed mode branches, involving both components (linearly polarized and elliptically polarized). These solutions are obtained explicitly and their stability is analyzed completely in the anti-continuum limit (where the nodes of the lattice are uncoupled), illustrating the supercritical pitchfork nature of the bifurcations that give rise to the latter two, respectively, from the former two. Then the branches are continued for finite coupling constructing a full two-parameter numerical bifurcation diagram of their existence. Relevant stability ranges and instability regimes are highlighted and, whenever unstable, the solutions are dynamically evolved through direct computations to monitor the development of the corresponding instabilities. Direct connections to the earlier experimental work of Meier et al. [Phys. Rev. Lett. {\bf 91}, 143907 (2003)] that motivated the present work are given.
△ Less
Submitted 26 September, 2005;
originally announced September 2005.
