Christian Johansen

Clément Aubert, Ross Horne, Christian Johansen et al.

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 \(π\)-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.

Johanna Johansen, Tore Pedersen, Simone Fischer-Hübner et al.

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.

Johanna Johansen, Tore Pedersen, Christian Johansen

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.

Johanna Johansen, Christian Johansen, Josef Noll

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.

Christian Johansen, Aulon Mujaj, Hamed Arshad et al.

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.

Sergiu Bursuc, Christian Johansen, Shiwei Xu

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.