-
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.
-
Kleene Theorem for Higher-Dimensional Automata
Authors:
Uli Fahrenberg,
Christian Johansen,
Georg Struth,
Krzysztof Ziemiański
Abstract:
We prove a Kleene theorem for higher-dimensional automata. It states that the languages they recognise are precisely the rational subsumption-closed sets of finite interval pomsets. The rational operations on these languages include a gluing, for which we equip pomsets with interfaces. For our proof, we introduce higher-dimensional automata with interfaces, which are modelled as presheaves over la…
▽ More
We prove a Kleene theorem for higher-dimensional automata. It states that the languages they recognise are precisely the rational subsumption-closed sets of finite interval pomsets. The rational operations on these languages include a gluing, for which we equip pomsets with interfaces. For our proof, we introduce higher-dimensional automata with interfaces, which are modelled as presheaves over labelled precube, and develop tools and techniques inspired by algebraic topology, such as cylinders and (co)fibrations. Higher-dimensional automata form a general model of non-interleaving concurrency, which subsumes many other approaches. Interval orders are used as models for concurrent and distributed systems where events extend in time. Our tools and techniques may therefore yield templates for Kleene theorems in various models and applications.
△ Less
Submitted 8 April, 2024; v1 submitted 8 February, 2022;
originally announced February 2022.
-
Posets with Interfaces as a Model for Concurrency
Authors:
Uli Fahrenberg,
Christian Johansen,
Georg Struth,
Krzysztof Ziemiański
Abstract:
We introduce posets with interfaces (iposets) and generalise their standard serial composition to a new gluing composition. In the partial order semantics of concurrency, interfaces and gluing allow modelling events that extend in time and across components. Alternatively, taking a decompositional view, interfaces allow cutting through events, while serial composition may only cut through edges of…
▽ More
We introduce posets with interfaces (iposets) and generalise their standard serial composition to a new gluing composition. In the partial order semantics of concurrency, interfaces and gluing allow modelling events that extend in time and across components. Alternatively, taking a decompositional view, interfaces allow cutting through events, while serial composition may only cut through edges of a poset. We show that iposets under gluing composition form a category, which generalises the monoid of posets under serial composition up to isomorphism. They form a 2-category when a subsumption order and a lax tensor in the form of a non-commutative parallel composition are added, which generalises the interchange monoids used for modelling series-parallel posets. We also study the gluing-parallel hierarchy of iposets, which generalises the standard series-parallel one. The class of gluing-parallel iposets contains that of series-parallel posets and the class of interval orders, which are well studied in concurrency theory, too. We also show that it is strictly contained in the class of all iposets by identifying several forbidden substructures.
△ Less
Submitted 4 November, 2022; v1 submitted 21 June, 2021;
originally announced June 2021.
-
Languages of Higher-Dimensional Automata
Authors:
Uli Fahrenberg,
Christian Johansen,
Georg Struth,
Krzysztof Ziemiański
Abstract:
We introduce languages of higher-dimensional automata (HDAs) and develop some of their properties. To this end, we define a new category of precubical sets, uniquely naturally isomorphic to the standard one, and introduce a notion of event consistency. HDAs are then finite, labeled, event-consistent precubical sets with distinguished subsets of initial and accepting cells. Their languages are sets…
▽ More
We introduce languages of higher-dimensional automata (HDAs) and develop some of their properties. To this end, we define a new category of precubical sets, uniquely naturally isomorphic to the standard one, and introduce a notion of event consistency. HDAs are then finite, labeled, event-consistent precubical sets with distinguished subsets of initial and accepting cells. Their languages are sets of interval orders closed under subsumption; as a major technical step we expose a bijection between interval orders and a subclass of HDAs. We show that any finite subsumption-closed set of interval orders is the language of an HDA, that languages of HDAs are closed under binary unions and parallel composition, and that bisimilarity implies language equivalence.
△ Less
Submitted 3 September, 2021; v1 submitted 12 March, 2021;
originally announced March 2021.
-
A Multidisciplinary Definition of Privacy Labels: The Story of Princess Privacy and the Seven Helpers
Authors:
Johanna Johansen,
Tore Pedersen,
Simone Fischer-Hübner,
Christian Johansen,
Gerardo Schneider,
Arnold Roosendaal,
Harald Zwingelberg,
Anders Jakob Sivesind,
Josef Noll
Abstract:
Privacy is currently in distress and in need of rescue, much like princesses in the all-familiar fairytales. We employ storytelling and metaphors from fairytales to make reader-friendly and streamline our arguments about how a complex concept of Privacy Labeling (the 'knight in shining armor') can be a solution to the current state of Privacy (the 'princess in distress'). We give a precise definit…
▽ More
Privacy is currently in distress and in need of rescue, much like princesses in the all-familiar fairytales. We employ storytelling and metaphors from fairytales to make reader-friendly and streamline our arguments about how a complex concept of Privacy Labeling (the 'knight in shining armor') can be a solution to the current state of Privacy (the 'princess in distress'). We give a precise definition of Privacy Labeling (PL), painting a panoptic portrait from seven different perspectives (the 'seven helpers'): Business, Legal, Regulatory, Usability and Human Factors, Educative, Technological, and Multidisciplinary. We describe a common vision, proposing several important 'traits of character' of PL as well as identifying 'undeveloped potentialities', i.e., open problems on which the community can focus. More specifically, this position paper identifies the stakeholders of the PL and their needs with regard to privacy, describing how PL should be and look like in order to address these needs. Throughout the paper, we highlight goals, characteristics, open problems, and starting points for creating, what we consider to be, the ideal PL. In the end we present three approaches to establish and manage PL, through: self-evaluations, certifications, or community endeavors. Based on these, we sketch a roadmap for future developments.
△ Less
Submitted 9 May, 2021; v1 submitted 3 December, 2020;
originally announced December 2020.
-
Domain Semirings United
Authors:
Uli Fahrenberg,
Christian Johansen,
Georg Struth,
Krzysztof Ziemiánski
Abstract:
Domain operations on semirings have been axiomatised in two different ways: by a map from an additively idempotent semiring into a boolean subalgebra of the semiring bounded by the additive and multiplicative unit of the semiring, or by an endofunction on a semiring that induces a distributive lattice bounded by the two units as its image. This note presents classes of semirings where these approa…
▽ More
Domain operations on semirings have been axiomatised in two different ways: by a map from an additively idempotent semiring into a boolean subalgebra of the semiring bounded by the additive and multiplicative unit of the semiring, or by an endofunction on a semiring that induces a distributive lattice bounded by the two units as its image. This note presents classes of semirings where these approaches coincide.
△ Less
Submitted 22 March, 2021; v1 submitted 9 November, 2020;
originally announced November 2020.
-
Studying the Transfer of Biases from Programmers to Programs
Authors:
Johanna Johansen,
Tore Pedersen,
Christian Johansen
Abstract:
It is generally agreed that one origin of machine bias is resulting from characteristics within the dataset on which the algorithms are trained, i.e., the data does not warrant a generalized inference. We, however, hypothesize that a different `mechanism', hitherto not articulated in the literature, may also be responsible for machine's bias, namely that biases may originate from (i) the programme…
▽ More
It is generally agreed that one origin of machine bias is resulting from characteristics within the dataset on which the algorithms are trained, i.e., the data does not warrant a generalized inference. We, however, hypothesize that a different `mechanism', hitherto not articulated in the literature, may also be responsible for machine's bias, namely that biases may originate from (i) the programmers' cultural background, such as education or line of work, or (ii) the contextual programming environment, such as software requirements or developer tools. Combining an experimental and comparative design, we studied the effects of cultural metaphors and contextual metaphors, and tested whether each of these would `transfer' from the programmer to program, thus constituting a machine bias. The results show (i) that cultural metaphors influence the programmer's choices and (ii) that `induced' contextual metaphors can be used to moderate or exacerbate the effects of the cultural metaphors. This supports our hypothesis that biases in automated systems do not always originate from within the machine's training data. Instead, machines may also `replicate' and `reproduce' biases from the programmers' cultural background by the transfer of cultural metaphors into the programming process. Implications for academia and professional practice range from the micro programming-level to the macro national-regulations or educational level, and span across all societal domains where software-based systems are operating such as the popular AI-based automated decision support systems.
△ Less
Submitted 13 December, 2020; v1 submitted 17 May, 2020;
originally announced May 2020.
-
Generating Posets Beyond N
Authors:
Uli Fahrenberg,
Christian Johansen,
Georg Struth,
Ratan Bahadur Thapa
Abstract:
We introduce iposets---posets with interfaces---equipped with a novel gluing composition along interfaces and the standard parallel composition. We study their basic algebraic properties as well as the hierarchy of gluing-parallel posets generated from singletons by finitary applications of the two compositions. We show that not only series-parallel posets, but also interval orders, which seem mor…
▽ More
We introduce iposets---posets with interfaces---equipped with a novel gluing composition along interfaces and the standard parallel composition. We study their basic algebraic properties as well as the hierarchy of gluing-parallel posets generated from singletons by finitary applications of the two compositions. We show that not only series-parallel posets, but also interval orders, which seem more interesting for modelling concurrent and distributed systems, can be generated, but not all posets. Generating posets is also important for constructing free algebras for concurrent semirings and Kleene algebras that allow compositional reasoning about such systems.
△ Less
Submitted 14 October, 2019;
originally announced October 2019.
-
Sculptures in Concurrency
Authors:
Uli Fahrenberg,
Christian Johansen,
Christopher A. Trotter,
Krzysztof Ziemiański
Abstract:
We give a formalization of Pratt's intuitive sculpting process for higher-dimensional automata (HDA). Intuitively, an HDA is a sculpture if it can be embedded in (i.e., sculpted from) a single higher dimensional cell (hypercube). A first important result of this paper is that not all HDA can be sculpted, exemplified through several natural acyclic HDA, one being the famous "broken box" example of…
▽ More
We give a formalization of Pratt's intuitive sculpting process for higher-dimensional automata (HDA). Intuitively, an HDA is a sculpture if it can be embedded in (i.e., sculpted from) a single higher dimensional cell (hypercube). A first important result of this paper is that not all HDA can be sculpted, exemplified through several natural acyclic HDA, one being the famous "broken box" example of van Glabbeek. Moreover, we show that even the natural operation of unfolding is completely unrelated to sculpting, e.g., there are sculptures whose unfoldings cannot be sculpted. We investigate the expressiveness of sculptures, as a proper subclass of HDA, by showing them to be equivalent to regular ST-structures (an event-based counterpart of HDA) and to (regular) Chu spaces over 3 (in their concurrent interpretation given by Pratt). We believe that our results shed new light on the intuitions behind sculpting as a method of modeling concurrent behavior, showing the precise reaches of its expressiveness. Besides expressiveness, we also develop an algorithm to decide whether an HDA can be sculpted. More importantly, we show that sculptures are equivalent to Euclidean cubical complexes (being the geometrical counterpart of our combinatorial definition), which include the popular PV models used for deadlock detection. This exposes a close connection between geometric and combinatorial models for concurrency which may be of use for both areas.
△ Less
Submitted 13 April, 2021; v1 submitted 5 December, 2018;
originally announced December 2018.
-
InfoInternet for Education in the Global South: A Study of Applications Enabled by Free Information-only Internet Access in Technologically Disadvantaged Areas (authors' version)
Authors:
Johanna Johansen,
Christian Johansen,
Josef Noll
Abstract:
This paper summarises our work on studying educational applications enabled by the introduction of a new information layer called InfoInternet. This is an initiative to facilitate affordable access to internet based information in communities with network scarcity or economic problems from the Global South. InfoInternet develops both networking solutions as well as business and social models, toge…
▽ More
This paper summarises our work on studying educational applications enabled by the introduction of a new information layer called InfoInternet. This is an initiative to facilitate affordable access to internet based information in communities with network scarcity or economic problems from the Global South. InfoInternet develops both networking solutions as well as business and social models, together with actors like mobile operators and government organisations. In this paper we identify and describe characteristics of educational applications, their specific users, and learning environment. We are interested in applications that make the adoption of Internet faster, cheaper, and wider in such communities. When develo** new applications (or adopting existing ones) for such constrained environments, this work acts as initial guidelines prior to field studies.
△ Less
Submitted 28 August, 2018;
originally announced August 2018.
-
The Snowden Phone: A Comparative Survey of Secure Instant Messaging Mobile Applications
Authors:
Christian Johansen,
Aulon Mujaj,
Hamed Arshad,
Josef Noll
Abstract:
In recent years, it has come to attention that governments have been doing mass surveillance of personal communications without the consent of the citizens. As a consequence of these revelations, developers have begun releasing new protocols for end-to-end encrypted conversations, extending and making popular the old Off-the-Record protocol. Several new implementations of such end-to-end encrypted…
▽ More
In recent years, it has come to attention that governments have been doing mass surveillance of personal communications without the consent of the citizens. As a consequence of these revelations, developers have begun releasing new protocols for end-to-end encrypted conversations, extending and making popular the old Off-the-Record protocol. Several new implementations of such end-to-end encrypted messaging protocols have appeared, and commonly used chat applications have been updated with these implementations as well. In this survey, we compare the existing implementations, where most of them implement one of the recent and popular protocols called Signal.
We conduct a series of experiments on these implementations to identify which types of security and usability properties each application provides. The results of the experiments demonstrate that the applications have variations of usability and security properties, and none of them are infallible. Finally, the paper gives proposals for improving each application w.r.t. security, privacy, and usability.
△ Less
Submitted 30 July, 2019; v1 submitted 20 July, 2018;
originally announced July 2018.
-
Automated verification of dynamic root of trust protocols (long version)
Authors:
Sergiu Bursuc,
Christian Johansen,
Shiwei Xu
Abstract:
Automated verification of security protocols based on dynamic root of trust, typically relying on protected hardware such as TPM, involves several challenges that we address in this paper. We model the semantics of trusted computing platforms (including CPU, TPM, OS, and other essential components) and of associated protocols in a classical process calculus accepted by ProVerif. As part of the for…
▽ More
Automated verification of security protocols based on dynamic root of trust, typically relying on protected hardware such as TPM, involves several challenges that we address in this paper. We model the semantics of trusted computing platforms (including CPU, TPM, OS, and other essential components) and of associated protocols in a classical process calculus accepted by ProVerif. As part of the formalization effort, we introduce new equational theories for representing TPM specific platform states and dynamically loaded programs. Formal models for such an extensive set of features cannot be readily handled by ProVerif, due especially to the search space generated by unbounded extensions of TPM registers. In this context we introduce a transformation of the TPM process, that simplifies the structure of the search space for automated verification, while preserving the security properties of interest. This allows to run ProVerif on our proposed models, so we can derive automatically security guarantees for protocols running in a dynamic root of trust context.
△ Less
Submitted 7 March, 2017; v1 submitted 30 January, 2017;
originally announced January 2017.
-
Dynamic Structural Operational Semantics
Authors:
Christian Johansen,
Olaf Owe
Abstract:
We introduce Dynamic SOS as a framework for describing semantics of programming languages that include dynamic software upgrades, for upgrading software code during run-time. Dynamic SOS (DSOS) is built on top of the Modular SOS of P. Mosses, with an underlying category theory formalization. The idea of Dynamic SOS is to bring out the essential differences between dynamic upgrade constructs and pr…
▽ More
We introduce Dynamic SOS as a framework for describing semantics of programming languages that include dynamic software upgrades, for upgrading software code during run-time. Dynamic SOS (DSOS) is built on top of the Modular SOS of P. Mosses, with an underlying category theory formalization. The idea of Dynamic SOS is to bring out the essential differences between dynamic upgrade constructs and program execution constructs. The important feature of Modular SOS (MSOS) that we exploit in DSOS is the sharp separation of the program execution code from the additional (data) structures needed at run-time. In DSOS we aim to achieve the same modularity and decoupling for dynamic software upgrades. This is partly motivated by the long term goal of having machine-checkable proofs for general results like type safety.
We exemplify Dynamic SOS on two languages supporting dynamic software upgrades, namely the C-like Proteus, which supports updating of variables, functions, records, or types at specific program points, and Creol, which supports dynamic class upgrades in the setting of concurrent objects. Existing type analyses for software upgrades can be done on top of DSOS too, as we illustrate for Proteus.
As a side result we define of a general encapsulating construction on Modular SOS useful in situations where a form of encapsulation of the execution is needed. We use encapsulation in the Creol setting of concurrent object-oriented programming with active objects and asynchronous method calls.
△ Less
Submitted 20 July, 2018; v1 submitted 2 December, 2016;
originally announced December 2016.
-
A Comparison of Clustering and Missing Data Methods for Health Sciences
Authors:
Ran Zhao,
Deanna Needell,
Christopher Johansen,
Jerry L. Grenard
Abstract:
In this paper, we compare and analyze clustering methods with missing data in health behavior research. In particular, we propose and analyze the use of compressive sensing's matrix completion along with spectral clustering to cluster health related data. The empirical tests and real data results show that these methods can outperform standard methods like LPA and FIML, in terms of lower misclassi…
▽ More
In this paper, we compare and analyze clustering methods with missing data in health behavior research. In particular, we propose and analyze the use of compressive sensing's matrix completion along with spectral clustering to cluster health related data. The empirical tests and real data results show that these methods can outperform standard methods like LPA and FIML, in terms of lower misclassification rates in clustering and better matrix completion performance in missing data problems. According to our examination, a possible explanation of these improvements is that spectral clustering takes advantage of high data dimension and compressive sensing methods utilize the near-to-low-rank property of health data.
△ Less
Submitted 22 April, 2014;
originally announced April 2014.
