arXiv subjects

Christian Johansen

Publications and source records attributed to Christian Johansen.

17 recordsLinked to original sources

arXiv2026

Unlinkability and History Preserving Bisimilarity

An ever-increasing number of critical infrastructures rely heavily on the assumption that security protocols satisfy a wealth of requirements. Hence, the importance of certifying e.g., privacy properties using methods that are better at detecting attacks can hardly be overstated. This paper scrutinises the "unlinkability" privacy property using relations equating behaviours that cannot be distinguished by attackers. Starting from the observation that some reasonable design choice can lead to formalisms missing attacks, we draw attention to a classical concurrent semantics accounting for relationship between past events, and show that there are concurrency-aware semantics that can discover attacks on all protocols we consider.More precisely, we focus on protocols where trace equivalence is known to miss attacks that are observable using branching-time equivalences. We consider the impact of three dimensions: design decisions made by the programmer specifying an unlinkability problem (style), semantics respecting choices during execution (branching-time), and semantics sensitive to concurrency (non-interleaving), and discover that reasonable styles miss attacks unless we give attackers enough power to observe choices and concurrency. Our main contribution is to draw attention to how a popular concurrent semantics -- history-preserving bisimilarity -- when defined for the non-interleaving applied $\pi$-calculus, can discover attacks on all protocols we consider, regardless of the choice of style. Furthermore, we can describe all such attacks using a novel modal logic that is hence suitable to formally certify attacks on privacy properties.

cs.CR↗

arXiv2025

Many-body theory of false vacuum decay in quantum spin chains

In this work we theoretically investigate the false vacuum decay process in a ferromagnetic quantum spin-1/2 chain. We develop a many-body theory describing the nucleation and the coherent dynamics of true-vacuum bubbles that is analytically tractable and agrees with numerical matrix product state calculations in all parameter regimes up to intermediate times. This bosonic theory allows us to identify different regimes in the parameter space and unravel the underlying physical mechanisms. In particular, regimes that closely correspond to the cosmological false vacuum decay picture are highlighted and characterized in terms of observable quantities.

cond-mat.stat-mech↗

arXiv2024

LightSC: The Making of a Usable Security Classification Tool for DevSecOps

DevSecOps, as the extension of DevOps with security training and tools, has become a popular way of developing modern software, especially in the Internet of Things arena, due to its focus on rapid development, with short release cycles, involving the user/client very closely. Security classification methods, on the other hand, are heavy and slow processes that require high expertise in security, the same as in other similar areas such as risk analysis or certification. As such, security classification methods are hardly compatible with the DevSecOps culture, which to the contrary, has moved away from the traditional style of penetration testing done only when the software product is in the final stages or already deployed. In this work, we first propose five principles for a security classification to be \emph{DevOps-ready}, two of which will be the focus for the rest of the paper, namely to be tool-based and easy to use for non-security experts, such as ordinary developers or system architects. We then exemplify how one can make a security classification methodology DevOps-ready. We do this through an interaction design process, where we create and evaluate the usability of a tool implementing the chosen methodology. Since such work seems to be new within the usable security community, and even more so in the software development (DevOps) community, we extract from our process a general, three-steps `recipe' that others can follow when making their own security methodologies DevOps-ready. The tool that we build is in itself a contribution of this process, as it can be independently used, extended, and/or integrated by developer teams into their DevSecOps tool-chains. Our tool is perceived (by the test subjects) as most useful in the design phase, but also during the testing phase where the security class would be one of the metrics used to evaluate the quality of their software.

cs.CR↗

arXiv2022

Posets with Interfaces as a Model for Concurrency

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.

cs.FL↗

arXiv2022

Bisimulations Respecting Duration and Causality for the Non-interleaving Applied $π$-Calculus

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.

cs.LO↗

arXiv2022

Generating Posets with Interfaces

We generate and count isomorphism classes of gluing-parallel posets with interfaces (iposets) on up to eight points, and on up to ten points with interfaces removed. In order to do so, we introduce a new class of iposets with full interfaces and show that considering these is sufficient. We also describe the software (written in Julia) that we have used for our exploration and define a new incomplete isomorphism invariant which may be computed in polynomial time yet identifies only very few pairs of non-isomorphic iposets.

math.CO↗

arXiv2022

Kleene Theorem for Higher-Dimensional Automata

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 composition, 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 categories, 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.

cs.FL↗

arXiv2021

Languages of Higher-Dimensional Automata

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.

cs.FL↗

arXiv2021

A Multidisciplinary Definition of Privacy Labels: The Story of Princess Privacy and the Seven Helpers

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.

cs.CR↗

arXiv2021

Sculptures in Concurrency

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.

cs.LO↗

arXiv2021

Domain Semirings United

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.

cs.LO↗

arXiv2020

Studying the Transfer of Biases from Programmers to Programs

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.

cs.HC↗

arXiv2019

Generating Posets Beyond N

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.

cs.FL↗

arXiv2019

The Snowden Phone: A Comparative Survey of Secure Instant Messaging Mobile Applications

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.

cs.CR↗

arXiv2018

InfoInternet for Education in the Global South: A Study of Applications Enabled by Free Information-only Internet Access in Technologically Disadvantaged Areas (authors' version)

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 developing new applications (or adopting existing ones) for such constrained environments, this work acts as initial guidelines prior to field studies.

cs.CY↗

arXiv2018

Dynamic Structural Operational Semantics

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.

cs.PL↗

arXiv2017

Automated verification of dynamic root of trust protocols (long version)

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.

cs.CR↗