Background and activities
See my homepage https://christian.johansenresearch.info/
I work in Theoretical Computer Science focusing on developing and using formal methods and tools for ensuring reliability of complex systems, including properties regarding security, safety, and concurrency. Applications of such methods are numerous, e.g., verification of safety properties of software systems (like absence of certain bugs) or of hybrid systems like the Smart Grids, ensuring security of Internet of Things, or modelling the concurrency of modern multi-core or high-performance computing. Among methods or models that I have created I can list: the Timed Distributed pi-calculus, the ST-structures, the Dynamic Structural Operational Semantics, the Synchronous Kleene Algebra, or the Higher Dimensional Modal Logic. Together with my students I have worked on developing tools, e.g., together with Manish Shrestha we made the LightSC Security Classification Method for Smart Grids and IoT and the associated usable security tool with the same name; whereas together with Bjørnar Luteberget we made the SAT modulo Discrete Event Simulation method and tool applied to railway capacity verification. A nice and long collaboration with Tore Pedersen has taken me also into the realm of modelling of human behaviour, where some of my contributions are: proposing the Behavioural Computer Science agenda, where models of human behaviour are combined with CS models of system behaviour (execution); or the probabilistic modelling of humans in security ceremonies.
I have done research in different areas of computer science, including modelling of security protocols; (object-oriented) programming languages and their formal semantics; modelling languages and verification of networked systems; models and tools for parallel programming and concurrent systems; algebras and logics as used in computer science; timed process calculi for distributed and mobile communicating systems; (legal) electronic contracts and privacy agreements (ToS -- Terms of Services). My work, more than 45 international articles, has been published in highly ranked conferences s.a. CONCUR, ATVA, LFCS, FM, POST, or CCS, and top journals s.a. JLAMP, IJCIP, FMSD, or LMCS. More recent works usually target concurrency, security, and privacy. I finished my doctoral studies in 2010 at University of Oslo and have been involved ever since in teaching and supervision, in reviewing for international conferences and journals, in the organisation of conferences and workshops, and in the coordination and writing of projects submitted to highly competitive calls, s.a.: EU-FP7-FET-Young-Explorers, Horison-2020, NFR-FRINATEK, UK’s EPSRC, ECSEL-JU.
Scientific, academic and artistic work
Displaying a selection of activities. See all publications in the database
- (2021) lr-Multisemigroups, Modal Quantales and the Origin of Locality. Lecture Notes in Computer Science (LNCS). vol. 13027.
- (2021) Languages of higher-dimensional automata. Mathematical Structures in Computer Science. vol. 31 (5).
- (2021) Sculptures in concurrency. Logical Methods in Computer Science. vol. 17 (2).
- (2021) The Snowden Phone: A Comparative Survey of Secure Instant Messaging Mobile Applications. Security and Communication Networks.
- (2021) InfoInternet for education in the Global South: A study of applications enabled by free information-only internet access in technologically disadvantaged areas. African Journal of Science, Technology, Innovation and Development (AJSTID).
- (2021) Studying human-to-computer bias transference. AI & Society: The Journal of Human-Centred Systems and Machine Intelligence.
- (2021) SAT modulo discrete event simulation applied to railway design capacity analysis. Formal methods in system design. vol. 57.
- (2021) Drawing with SAT: four methods and A tool for producing railway infrastructure schematics. Formal Aspects of Computing. vol. 33.
- (2020) A Methodology for Security Classification applied to Smart Grid Infrastructures. International Journal of Critical Infrastructure Protection. vol. 28.
- (2020) Generating Posets Beyond N. Lecture Notes in Computer Science (LNCS). vol. 12062.
- (2020) Tool Support for Security Classification for Internet of Things (long version). Universitetet i Oslo. 2020. ISBN 978-82-7368-460-8.
- (2020) Building Confidence using Beliefs and Arguments in Security Class Evaluations for IoT (long version). Universitetet i Oslo. 2020. ISBN 978-82-7368-458-5.
- (2020) Code Diversification Mechanisms for Internet of Things (Revised Version 2). 2020. ISBN 978-82-7368-438-7.
- (2019) A stable non-interleaving early operational semantics for the pi-calculus. Journal of Logical and Algebraic Methods in Programming. vol. 104.
- (2019) Dynamic Structural Operational Semantics. Journal of Logical and Algebraic Methods in Programming. vol. 107.
- (2019) Summary of: Dynamic Structural Operational Semantics. Lecture Notes in Computer Science (LNCS). vol. 11918.
- (2019) Automated Drawing of Railway Schematics Using Numerical Optimization in SAT. Lecture Notes in Computer Science (LNCS). vol. 11918 LNCS.
- (2019) Synthesis of railway signaling layout from local capacity specifications. Lecture Notes in Computer Science (LNCS). vol. 11800 LNCS.
- (2019) Behavioural artificial intelligence: an agenda for systematic empirical studies of artificial inference. AI & Society: The Journal of Human-Centred Systems and Machine Intelligence.
- (2019) Criteria for Security Classification of Smart Home Energy Management Systems (long version). Universitetet i Oslo. 2019. ISBN 978-82-7368-457-8.
- (2018) The Future Mechanism and Information Flow Security. The 30th Nordic Workshop on Programming Theory, Oslo ; 2018-10-24 - 2018-10-26.
- (2018) Perspectives in Secure SMART Environments. Measurable and Composable Security, Privacy, and Dependability for Cyberphysical Systems : The SHIELD Methodology.
- (2018) Behavioural Computer Science: an agenda for combining modelling of human and system behaviours. Human-centric Computing and Information Sciences. vol. 8:7.
- (2017) Automated verification of dynamic root of trust protocols. Lecture Notes in Computer Science (LNCS). vol. 10204 LNCS.
- (2017) A stable non-interleaving early operational semantics for the Pi-calculus. Lecture Notes in Computer Science (LNCS). vol. 10168 LNCS.
- (2017) Comparing Implementations of Secure Messaging Protocols (long version). Universitetet i Oslo. 2017. ISBN 978-82-7368-440-0.
- (2017) Participatory Verification of Railway Infrastructure Regulations using RailCNL (long version). 2017. ISBN 978-82-7368-430-1.
- (2017) Participatory verification of railway infrastructure by representing regulations in RailCNL. Lecture Notes in Computer Science (LNCS). vol. 10469 LNCS.
- (2017) Efficient verification of railway infrastructure designs against standard regulations. Formal methods in system design. vol. 52 (1).
- (2017) Intelligence Analysis: Reflections on the Future Human - Machine Analytic Enterprise from a Behavioral Computer Science Perspective. AF Security Seminar Series . University of Oslo, Department of Informatics; Oslo. 2017-06-16 - 2017-06-16.
- (2017) Security Classification for Smart Grid Infra structures (long version). Universitetet i Oslo. 2017. ISBN 978-82-7368-441-7.
- (2017) Code Diversification Mechanisms for Securing the Internet of Things. Proceedings of the 29th Nordic Workshop on Programming Theory.
- (2017) Code Diversification Mechanisms for Securing the Internet of Things. 29th Nordic Workshop on Programming Theory (NWPT'17) . Åbo University; Turku. 2017-11-01 - 2017-11-03.
- (2016) ST-structures. Journal of Logical and Algebraic Methods in Programming. vol. 85 (6).
- (2016) Offpad: Offline personal authenticating device: implementations and applications. 2016. ISBN 978-82-7368-419-6.
- (2016) Usable Authentication with an Offline Trusted Device Proxy Architecture (long version). 2016. ISBN 978-82-7368-418-9.
- (2016) Non-interleaving Operational Semantics for the Pi-calculus -- technicalities. Universitetet i Oslo. 2016. ISBN 978-82-7368-416-5.
- (2016) Reflections on Behavioural Computer Science. 2016. ISBN 978-82-7368-417-2.
- (2016) Towards Behavioural Computer Science. IFIP Advances in Information and Communication Technology. vol. 473.
- (2016) Rule-based incremental verification tools applied to railway designs and regulations. Lecture Notes in Computer Science (LNCS). vol. 9995 LNCS.
- (2016) Rule-Based Consistency Checking of Railway Infrastructure Designs. Universitetet i Oslo. 2016. Conference proceedings (Universitetet i Oslo. Institutt for informatikk) (450).
- (2016) Rule-based consistency checking of railway infrastructure designs. Lecture Notes in Computer Science (LNCS). vol. 9681.
- (2016) DEMO: OffPAD - Offline Personal Authenticating Device with Applications in Hospitals and e-Banking. Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security.
- (2016) Declarative event based models of concurrency and refinement in psi-calculi. Journal of Logical and Algebraic Methods in Programming. vol. 85 (3).
- (2015) Probabilistic Modeling of Humans in Security Ceremonies. Data Privacy Management, Autonomous Spontaneous Security, and Security Assurance: 9th International Workshop, DPM 2014, 7th International Workshop, SETOP 2014, and 3rd International Workshop, QASA 2014, Wroclaw, Poland, September 10-11, 2014. Revised Selected Papers.
- (2015) Probabilistic modelling of humans in security ceremonies. Lecture Notes in Computer Science (LNCS). vol. 8872.
- (2015) Tokenit: Designing State-Driven Embedded Systems through Tokenized Transitions. Distributed Computing in Sensor Systems (DCOSS).