Christian Johansen

Image of Christian Johansen
Norwegian version of this page
Phone +47-22850481
Room 9466
Available hours Tel: 28850481
Username
Visiting address Ole-johan Dahl hus Gaustadaleen 23B Oslo.
Postal address Postboks 70 2027 KJELLER

50% position at ITS.

My research focus

"Privacy and Access Control through Verifiable Security"

Short bio:

I am working as a researcher in the Precise Modelling and Analysis group of the University of Oslo (UiO) and I am member of the ConSeRNS interdisciplinary group "Concurrent Security and Resilience for Networked Systems”.
I finished my doctoral studies in 2010 at UiO and I have been working for UiO since. I have been involved in teaching and supervisory activities, in reviewing for international conferences and journals, in the organisation of conferences and workshops, and in writing of project proposals submitted to highly competitive calls, s.a.: EU-FP7-FET-Young-Explorers, Horison-2020, NFR-FRINATEK, UK’s EPSRC.

I have worked 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. My work, more than 15 international articles, has been published in highly ranked conferences s.a. CONCUR, ATVA, or LFCS, and top journals s.a. JLAP.

Application areas

Some areas where my work applies are:

  • security and privacy for Energy informatics and Smart grid (see the IoTSec project)
  • models and programming for Internet of Things (see Models4IoT)
  • concurrency models and parallel programming (together with ITU Copenhagen)
  • security through hardware, like TPM or the new Intel SGX (together with Bristol and Bergen Uni.)
  • security ceremonies and the role of the human and UI in security (together with Audun Jøsang)
  • verification of safety critical systems (see also the course on Model-checking)
  • automation for complex critical designs (see also the work on Railway designs in RailCons project)
  • automated parsing and validation of contracts (with application to Privacy through Terms of Services) in collaboration with Chalmers Uni.
  • formal specifications of distributed and communicating systems
Tags: security, privacy, concurrency models, formal methods, safety verification, automated tools, logic in computer science, process algebras, semantics of programming languages, security ceremonies, access control

Publications

  • Bursuc, Sergiu; Johansen, Christian & Xu, Shiwei (2017). Automated verification of dynamic root of trust protocols. Lecture Notes in Computer Science.  ISSN 0302-9743.  10204 LNCS, s 95- 116 . doi: 10.1007/978-3-662-54455-6_5
  • Hildebrandt, Thomas; Johansen, Christian & Normann, Håkon (2017). A stable non-interleaving early operational semantics for the Pi-calculus. Lecture Notes in Computer Science.  ISSN 0302-9743.  10168 LNCS, s 51- 63 . doi: 10.1007/978-3-319-53733-7_3
  • Luteberget, Bjørnar Steinnes & Johansen, Christian (2017). Efficient verification of railway infrastructure designs against standard regulations. Formal methods in system design.  ISSN 0925-9856.  s 1- 32 . doi: 10.1007/s10703-017-0281-z
  • Tokas, Shukun; Owe, Olaf & Johansen, Christian (2017). Code Diversification Mechanisms for Securing the Internet of Things, In Marina Walden (ed.),  Proceedings of the 29th Nordic Workshop on Programming Theory.  Turku Centre for Computer Science.  ISBN 978-952-12-3608-2.  kapittel.  s 10 - 12
  • Johansen, Christian (2016). ST-structures. The Journal of logical and algebraic methods in programming.  ISSN 2352-2216.  85(6), s 1201- 1233 . doi: 10.1016/j.jlamp.2015.10.009 Show summary
  • Johansen, Christian; Pedersen, Tore & Jøsang, Audun (2016). Towards Behavioural Computer Science. IFIP Advances in Information and Communication Technology.  ISSN 1868-4238.  473, s 154- 163 . doi: 10.1007/978-3-319-41354-9_12
  • Luteberget, Bjørnar Steinnes; Johansen, Christian; Feyling, C & Steffen, Martin (2016). Rule-based incremental verification tools applied to railway designs and regulations. Lecture Notes in Computer Science.  ISSN 0302-9743.  9995 LNCS, s 772- 778 . doi: 10.1007/978-3-319-48989-6_49
  • Luteberget, Bjørnar Steinnes; Johansen, Christian & Steffen, Martin (2016). Rule-based consistency checking of railway infrastructure designs. Lecture Notes in Computer Science.  ISSN 0302-9743.  9681, s 491- 507 . doi: 10.1007/978-3-319-33693-0_31
  • Normann, Håkon; Johansen, Christian & Hildebrandt, Thomas (2016). Declarative event based models of concurrency and refinement in psi-calculi. The Journal of logical and algebraic methods in programming.  ISSN 2352-2216.  85(3), s 368- 398 . doi: 10.1016/j.jlamp.2015.12.007
  • Johansen, Christian & Jøsang, Audun (2015). Probabilistic Modeling of Humans in Security Ceremonies, In Joaquín García-Alfaro; Jordi Herrera-Joancomartí; Emil Lupu; Joachim Posegga; Alessandro Aldini; Fabio Martinelli & Neeraj Suri (ed.),  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.  Springer Publishing Company.  ISBN 978-3-319-17016-9.  Konferanseartikkel.
  • Johansen, Christian & Jøsang, Audun (2015). Probabilistic modelling of humans in security ceremonies. Lecture Notes in Computer Science.  ISSN 0302-9743.  8872, s 277- 292 . doi: 10.1007/978-3-319-17016-9_18
  • Taherkordi, Amirhosein; Johansen, Christian; Eliassen, Frank & Römer, Kay (2015). Tokenit: Designing State-Driven Embedded Systems through Tokenized Transitions, In Lisa OConner (ed.),  Distributed Computing in Sensor Systems (DCOSS).  IEEE.  ISBN 978-1-4799-8856-3.  6.  s 52 - 61
  • Johansen, Christian (2014). Actor network procedures as Psi-calculi for security ceremonies. Electronic Proceedings in Theoretical Computer Science.  ISSN 2075-2180.  148, s 63- 77 . doi: 10.4204/EPTCS.148.5
  • Normann, Håkon; Johansen, Christian & Hildebrandt, Thomas (2014). Concurrency models with causality and events as psi-calculi. Electronic Proceedings in Theoretical Computer Science.  ISSN 2075-2180.  166, s 4- 20 . doi: 10.4204/EPTCS.166.3
  • Aceto, Luca; Ingolfsdottir, Anna; Prisacariu, Cristian & Sack, Joshua (2013). Compositional Reasoning for Multi-modal Logics, In Sergei Artemov (ed.),  Symposium on Logical Foundations of Computer Science (LFCS13).  Springer.  ISBN 978-3-642-35721-3.  Chapter.  s 1 - 15 Show summary
  • Prisacariu, Cristian (2012). The Glory of the Past and Geometrical Concurrency. EasyChair Proceedings in Computing.  ISSN 2040-557X.  10, s 252- 267 Show summary
  • Prisacariu, Cristian & Schneider, Gerardo (2012). A dynamic deontic logic for complex contracts. Journal of Logic and Algebraic Programming.  ISSN 1567-8326.  81(4), s 458- 490 . doi: 10.1016/j.jlap.2012.03.003
  • Prisacariu, Cristian (2010). Modal Logic over Higher Dimensional Automata, In Paul Gastin & Francois Laroussinie (ed.),  21st International Conference on Concurrency Theory (CONCUR10).  Springer.  ISBN 978-3-642-02260-9.  34.  s 494 - 508
  • Prisacariu, Cristian (2010). Modal Logic over Higher Dimensional Automata. Lecture Notes in Computer Science.  ISSN 0302-9743.  6269, s 494- 508
  • Prisacariu, Cristian (2010). Synchronous Kleene algebra. Journal of Logic and Algebraic Programming.  ISSN 1567-8326.  79(7), s 608- 635 . doi: 10.1016/j.jlap.2010.07.009
  • Okika, Joseph; Owe, Olaf & Prisacariu, Cristian (2009). Operational Semantics for BPEL Complex Features in Rewriting Logic, In Michael R. Hansen & Aske Brekling (ed.),  21st Nordic Workshop on Programming Theory.  Danmarks Tekniske Universitet, DTU.  ISBN 978-87-643-0565-4.  34.  s 95 - 97 Show summary
  • Prisacariu, Cristian (2009). A Decidable Logic for Complex Contracts, In Michael R. Hansen & Aske Brekling (ed.),  21st Nordic Workshop on Programming Theory.  Danmarks Tekniske Universitet, DTU.  ISBN 978-87-643-0565-4.  24.  s 65 - 67 Show summary
  • Prisacariu, Cristian & Schneider, Gerardo (2009). Abstract specification of legal contracts, In Pompeu Casanovas (ed.),  The 12th International Conference on Artificial Intelligence and Law (ICAIL'09).  ACM Press.  ISBN 978-1-60558-597-0.  Chapter 26.  s 218 - 219
  • Prisacariu, Cristian & Schneider, Gerardo (2009). An Action-Based Logic for Reasoning about Contracts, In Hiroakira Ono (ed.),  16th International Workshop on Logic, Language, Information and Computation (WoLLIC 2009).  Springer.  ISBN 978-3-642-02260-9.  Chapter 27.  s 335 - 349
  • Kyas, Marcel; Prisacariu, Cristian & Schneider, Gerardo (2008). Run-time monitoring of electronic contracts. Lecture Notes in Computer Science.  ISSN 0302-9743.
  • Prisacariu, Cristian (2008). Extending Kleene Algebra with Synchrony: Completeness and Decidability, In Tarmu Uurstalu; Juri Vain & Juhan Ernits (ed.),  Proceedings of the Nordic Workshop of Programming Theory 2008 (NWPT'08).  Alfapress.  ISBN 978-9949-430-24-6.  Chapter 19.  s 69 - 72
  • Pace, Gordon; Prisacariu, Cristian & Schneider, Gerardo (2007). Model Checking Contracts -a case study. Lecture Notes in Computer Science.  ISSN 0302-9743.  4762, s 82- 97 . doi: 10.1007/978-3-540-75596-8_8
  • Prisacariu, Cristian & Schneider, Gerardo (2007). A Formal Language for Electronic Contracts. Lecture Notes in Computer Science.  ISSN 0302-9743.  4468, s 174- 189
  • Prisacariu, Cristian & Schneider, Gerardo (2007). Towards model checking contracts, In Einar Broch Johnsen; Olaf Owe & Gerardo Schneider (ed.),  NWPT07/Flacos'07 Workshop Proceedings.  Unipub forlag.  ISBN 82-7368-324-9.  artikkel.

View all works in Cristin

  • Kruegel, Christopher; Myers, Andrew; Halevi, Shai & Johansen, Christian (2016). Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security. Association for Computing Machinery (ACM).  ISBN 978-1-4503-4139-4.  1892 s.

View all works in Cristin

  • Luteberget, Bjørnar Steinnes; Camilleri, John J.; Johansen, Christian & Schneider, Gerardo (2017). Participatory Verification of Railway Infrastructure Regulations using RailCNL (long version). Full text in Research Archive.
  • Pedersen, Tore; Johansen, Christian & Jøsang, Audun (2017). Intelligence Analysis: Reflections on the Future Human - Machine Analytic Enterprise from a Behavioral Computer Science Perspective.
  • Tokas, Shukun; Owe, Olaf & Johansen, Christian (2017). Code Diversification Mechanisms for Securing the Internet of Things.
  • Johansen, Christian; Jøsang, Audun & Migdal, Denis (2016). Offpad: Offline personal authenticating device: implementations and applications.
  • Johansen, Christian; Jøsang, Audun & Migdal, Denis (2016). Usable Authentication with an Offline Trusted Device Proxy Architecture (long version). Full text in Research Archive.
  • Johansen, Christian; Norman, Håkon & Hildebrandt, Thomas (2016). Non-interleaving Operational Semantics for the Pi-calculus -- technicalities. Full text in Research Archive.
  • Johansen, Christian; Pedersen, Tore & Jøsang, Audun (2016). Reflections on Behavioural Computer Science. Full text in Research Archive.
  • Luteberget, Bjørnar Steinnes; Johansen, Christian & Steffen, Martin (2016). Rule-Based Consistency Checking of Railway Infrastructure Designs. Conference proceedings (Universitetet i Oslo. Institutt for informatikk). 450. Full text in Research Archive.
  • Migdal, Denis; Johansen, Christian & Jøsang, Audun (2016). DEMO: OffPAD - Offline Personal Authenticating Device with Applications in Hospitals and e-Banking, In Christopher Kruegel; Andrew Myers; Shai Halevi (ed.),  Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security.  Association for Computing Machinery (ACM).  ISBN 978-1-4503-4139-4.  chapter.  s 1847 - 1849
  • Prisacariu, Cristian (2012). The Glory of the Past and Geometrical Concurrency.
  • Prisacariu, Cristian (2010). A Dynamic Deontic Logic over Synchronous Actions.
  • Prisacariu, Cristian (2010). Modal Logic over Higher Dimensional Automata - technicalities.
  • Okika, Joseph; Owe, Olaf & Prisacariu, Cristian (2009). Operational Semantics for BPEL Complex Features in Rewriting Logic.
  • Prisacariu, Cristian (2009). Synchronous Kleene Algebra vs. Concurrent Kleene Algebra.
  • Prisacariu, Cristian (2008). Deontic modalities over synchronous actions - technicalities. Conference proceedings (Universitetet i Oslo. Institutt for informatikk). 381.
  • Prisacariu, Cristian (2008). Extending Kleene Algebra with Synchrony - technicalities. Conference proceedings (Universitetet i Oslo. Institutt for informatikk). 376.
  • Prisacariu, Cristian & Schneider, Gerardo (2008). A Logic for Reasoning about Legal Contracts -Semantics. Conference proceedings (Universitetet i Oslo. Institutt for informatikk). 371.
  • Prisacariu, Cristian; Schneider, Gerardo & Kyas, Marcel (2008). Run-time Monitoring of Electronic Contracts - theoretical results. Conference proceedings (Universitetet i Oslo. Institutt for informatikk). 378.
  • Pace, Gordon; Prisacariu, Cristian & Schneider, Gerardo (2007). Model checking contracts -a case study (long version). Conference proceedings (Universitetet i Oslo. Institutt for informatikk). 362.
  • Prisacariu, Cristian & Schneider, Gerardo (2007). An Algebraic Structure for the Action-Based Contract Language CL - theoretical results. Conference proceedings (Universitetet i Oslo. Institutt for informatikk). 361.
  • Prisacariu, Cristian & Schneider, Gerardo (2007). Towards a Formal Definition of Electronic Contracts. Conference proceedings (Universitetet i Oslo. Institutt for informatikk). 348.

View all works in Cristin

Published Mar. 24, 2011 10:06 AM - Last modified Sep. 19, 2017 1:42 PM