Meeting on Foundations of Security and Concurrency at The Norwegian Academy of Science and Letters

Bio: Sjouke Mauw is full professor and head of the SaToSS research group on Security and Trust of Software Systems at the University of Luxembourg. Until 2007 he worked at the Eindhoven University of Technology and at CWI (Center of Mathematics and Computer Science) in Amsterdam.
His research focuses on formalising and applying formal reasoning to real-world security problems and trust issues, including: Security protocols; Privacy; Attack trees; RFID security; E-voting; Trust and risk management; Contract signing protocols; Digital Rights Management.

Abstract:What do traditional keys, train tickets and coins have in common? They are increasingly being replaced by digital solutions, such as electronic car keys, smart tickets and contactless payment systems. Unfortunately, various physical properties that are easily verified in the traditional setting are significantly harder to achieve in the digital world. An example is the proximity of a lock and its key. In the physical world, in order to open a lock, the key needs to be physically inserted into it. However, proximity is much harder to ensure using digital means only, because digital communications can be easily relayed over large distances. A special class of security protocols, called distance-bounding protocols are the computer scientist's answer to such relay attacks.
This presentation offers some insights into the nature of such protocols, with a particular emphasis on their application in remote memory erasure. The goal of remote memory erasure is to force a nearby IoT device, like a smart lock, to erase its memory when it is suspected to be infected with a computer virus.

Bio: Krzysztof Ziemiański is an Associate Professor in the Department of Mathematics, Informatics and Mechanics of University of Warsaw. His research concentrates on problems lying at the intersection between algebraic topology, concurrency and language theory, in particular topological models for concurrency. In recent years he has worked mainly on theory of concurrent languages for higher dimensional automata.

Abstract: A classical theorem of Stephen Kleene states that any language that can be recognized by a finite state automaton can be written as a regular expression and vice versa: every regular expression can be realized as an automaton. Words of a language are regarded as possible sequences of events that may be observed during an execution of some system. In this talk I will discuss the concurrent analogue of this situation. For concurrent systems, events may be simultaneous; thus, a behaviour of the system is described by a labelled partially ordered set rather than a word. Also, finite state automata need to be replaced by higher dimensional automata. Still, there is a concurrent analogue of Kleene's theorem. I will formulate the Kleene theorem for higher dimensional automata and introduce novel methods required in the proof.

Bio: Ross Horne is a senior lecturer in the department of Computer and Information Sciences at University of Strathclyde, Glasgow, United Kingdom; a member of the Strathclyde Cyber Security Group (StrathCyber); and affiliated with the Mathematically Structured Programming (MSP) group. He is editor of the newly created corner Logic for Security and Privacy within the Journal of Logic and Computation, of Oxford University Press.
Current research interests include: Equivalence checking and privacy; Linked data and descriptive type systems; Session types and proof theory; Attack trees; and Logic on Graphs.

Abstract:When you make a payment using a credit card or phone, the device connects to the terminal of a merchant using a protocol. The protocol currently implemented -- the EMV protocol -- almost certainly broadcasts transaction details including personally identifying information during transactions. That information may be picked up on the air within a range of 20 meters. Furthermore, a device closer to your card can power it up and enter a session that also reveals personally identifying information, even if the card is not involved in a transaction with a merchant. We explain our design of a tighter protocol for contactless payments that counters both threats described above, as well as improving data minimisation (and hence data protection) within payment systems.

Bio: Ulrich (Uli) Fahrenberg is professor at EPITA Rennes and head of the automata research group at LRE, EPITA Paris. He holds a PhD in mathematics from Aalborg University and has worked at Aalborg University, IRISA Rennes, and at École polytechnique.
Fahrenberg works in algebraic topology, concurrency theory, real-time verification, categorical foundations, and general quantitative verification. He is a member of the steering committees of the RAMiCS and GETCO conferences.

Abstract:Automata are probably the simplest models of computation which have been devised. They consist of a number of states and transitions between them and have found their use in compiler construction, verification and many other areas of computer science. Various extensions of automata have been developed, and I will focus on three of them: timed and hybrid automata to model and analyse behavior of cyber-physical systems and concurrent automata for distributed systems. After a thorough introduction to these automata extensions, our central question will be how to combine them. This is a highly non-trivial task which involves reasoning about the nature of time itself: discrete time in computing components, continuous time in physical components, and asynchronous time in distributed systems. It is also highly rewarding, as most modern computing systems are both cyber-physical and distributed.

Bio: Rob van Glabbeek is a Royal Society Wolfson Fellow and Professor at the School of Informatics, University of Edinburgh, Scotland; Adjunct Professor at the School of Computer Science and Engineering, The University of New South Wales, Sydney, Australia; and Research Affiliate, in the Concurrency Group, Theory Division, Computer Science Department, Stanford University, USA. He is foreign member of the Royal Holland Society of Sciences and Humanities; member of Academia Europea; fellow of the Asia-Pacific Artificial Intelligence Association; and recipient of the CONCUR test-of-time award in 2020.
His main research interest include: Comparative Concurrency Semantics; Mathematical models and formal languages for the representation of distributed systems and the verification of statements about them; in particular foundational work investigating the possibilities of such models and languages.

Abstract: Concurrency theory applies mathematical techniques to the careful modelling of distributed systems, so that one can establish with the certainty of mathematical proof that a system behaves according to its specification. In this modelling effort, we need to abstract from unimportant implementation details, while keeping essential features in our model. This presentation offers a glimpse behind the design choices in some models of concurrency, such as transition systems and Petri nets. It illustrates features from which one may and may not abstract, depending on what properties one sets out to prove. In particular I show that some information on causal independence between actions of distributed systems needs to be retained when proving so-called liveness properties, stating that a desired goal state will be reached.

Bio: Clément Aubert is an Associate Professor in the School of Computer and Cyber Sciences and an associate faculty member of the Graduate School at Augusta University, USA. He obtained his B.S. in Philosophy from the University of Paris 1, his M.Sc. in Mathematics from the University of Paris 7, and his PhD in Computer Science from the University of Paris 13. His current research interests are in formal methods for concurrent systems, type systems for the study of complexity, and reversible concurrent systems.

Abstract:A typical computer user knows the difference between what can be undone on a computer, and what cannot. They may be familiar with the "undo" feature of text editors but understand the impossibility of recovering an unsaved document after an emergency shutdown. Creating programs guaranteeing that any action can be undone requires to design and implement reversible programming languages. While such languages come with interesting built-in security features (because any past action can be investigated), they also raise challenges when it comes to concurrency. Indeed, undoing an action that involved synchronization between multiple actors requires all actors to agree to undo said action. This talk offers to discuss current trends in solving the aforementioned problem, and to highlight some of the benefits that could result from well-designed concurrent and reversible programming languages.

Bio: Georg Struth is professor of theoretical computer science at the University of Sheffield, UK. His work includes algebras and logics for programs, program semantics and verification, and formalised mathematics with proof assistants. In recent years he has worked mainly on concurrency theory, hybrid systems verification and applications of higher categories in computing, in particular higher-dimensional rewriting and higher-dimensional automata.

Abstract: Formalised mathematics means the specification of mathematical theorems and the verification of their proofs using computer software – so-called proof assistants. While the idea of formal mathematics is centuries old and the first proof assistants appeared more than fifty years ago, broader attention among mathematicians is very recent. Currently, much of formalised mathematics seems to be reconstructive, devoted to engineering mathematical libraries for established subjects like algebra or probability theory, or to dispelling doubts about complex or tedious proofs. Yet there seems to be little discussion on how state-of-the-art proof assistants could support the creative process of mathematics, let alone how future proof assistants should be designed to do this even better. In this talk I will reflect on my own experiences with formalising mathematics and I will add some thoughts about the future.