Research Interests

• Verification of systems and programs with formal methods (model checking, theorem proving, program refinement, ...)
• Analysis of security and privacy in cryptographic protocols
• Modelling AI agents knowledge and strategies with logics and formal methods
• Development of model checkers for systems verification (mainly Haskell and a little bit of Python)
• ...

Publications

• An SMT-based Approach to the Verification of Knowledge-Based Programs.
  Formal Aspects of Computing, in press.
  F. Belardinelli, I. Boureanu, V. Malvone, and S. F. Rajaona.
• Epistemic model checking for privacy.
  IEEE 37th Computer Security Foundations Symposium (CSF). IEEE Computer Society, 2024.
  F. Rajaona, I. Boureanu, R. Ramanujam, and S. Wesemeyer.
• Program semantics and verification technique for AI-centred programs
  The 25th International Symposium on Formal Methods, FM 2023 (best paper award).
  S. F. Rajaona, I. Boureanu, V. Malvone, and F. Belardinelli
• Automatically verifying expressive epistemic properties of programs
  The 37th AAAI Conference on Intelligent Systems, AAAI 2023.
  F. Belardinelli, I. Boureanu, V. Malvone, and S. F. Rajaona.
• Fine-Grained Trackability in Protocol Executions.
  The Network and Distributed System Security Symposium 2023, NDSS 2023.
  K. Budykho, I. Boureanu, S. Wesemeyer, F. Rajaona, D. Romero, M. Lewis, Y. Rahulan, and S. Schneider.
• An algebraic framework for reasoning about privacy.
  Doctoral dissertation, University of Stellenbosch, 2016.
  Fortunat Rajaona

Current Research Activities

In no particular order

• Expressing and verifying sessions unlinkability properties (in cryptographic protocols) as a trace property. Common approaches in symbolic protocol analysis (Dolev-Yao attacker model) for expressing and verifying sessions unlinkability (and other privacy properties) rely on some form of process/state equivalence. With process/state equivalence, protocol sessions are unlinkable if an attacker cannot distinguish a trace where two sessions are played by the same agent vs a trace where the two sessions are played by different agents. We propose to express sessions-unlinkability as a trace property rather than an equivalence property, by developing an appropriate model of agents knowledge still within the Dolev-Yao assumptions. We are exploring verification techniques to analyse sessions-unlinkability by looking at one trace at a time (privacy verification, cryptographic protocols, tool development, theoretical work).
• Verification of the 3GPP AKMA protocol/specs with the Phoebe Model Checker (CSF2024 paper) and with SQUIRELL Prover. We formalise desirable privacy properties of the 3GPP AKMA specifications and analyse them with protocol provers including Tamarin, Phoebe, SQUIRRELL. (privacy verification, cryptographic protocols, case study)
• Modelling Private Actions in Knowledge-Based Programs. We extend the programming language in the FM2023/FAC2024 paper with private actions. This will be able to express knowledge dynamics scenarios (card games, robots exchanging information, etc). (AI agents, epistemic logics, SMT solvers, model checking, program semantics, theoretical work)
• Adding Loops to the FM2023/FAC2024 paper. We will extend the programming language in the FM2023 paper with recursion/loops. (tool development)
• Programming techniques for Probabilistic Systems & Agents with Imperfect Knowledge with applications to Quantitative Information Flow and Differential Privacy. This is a long-term project. The idea is to use a programming language to reason about knowledge and probability. The programming language is inspired from with probabilistic programs (Morgan & MCIver Probabilistic Guarded Command Language). (AI agents, probability, knowledge, uncertainty, model checking, program semantics, theoretical work)