Fortunat RajaonaResearcher in formal methods & secure systems

Welcome

I am a researcher in formal methods and secure systems. I develop mathematical models and automated tools, and apply them to analyse real-world systems, with a focus on privacy, security, knowledge, and coordination in complex systems.

Research

My research sits at the intersection of formal verification, applied cryptography, and multi-agent systems. I use logic, semantics, model checking, and automated reasoning to make security and privacy claims precise, so that they can be stated rigorously, analysed systematically, and supported by formal evidence.

Projects

AUTOPASS Project (led by Prof Ioana Boureanu; EPSRC-funded, 2020–2022)

I developed a framework for reasoning about and analysing privacy in cryptographic protocols. It included:

  • Designing a protocol model and a non-classical logic language for specifying privacy properties.
  • Building Phoebe, a model-checking tool implementing the framework.
  • Analysing benchmark privacy-preserving protocols.

In 2024, the project received an Amazon Research Award to further enhance Phoebe. I co-authored several conference papers, including the Phoebe paper presented at CSF 2024; our work on epistemic logic and AI reasoning received the Best Paper Award at FM 2023.

ESKMARALD Project (led by Prof Ioana Boureanu; NCSC-funded, 2023–2024)

I investigated the security and privacy of the 3GPP AKMA protocol standard. Our work involved:

  • Formalising security and privacy requirements for AKMA.
  • Using formal verification tools such as Tamarin and Squirrel Prover to uncover privacy flaws.
  • Proposing a privacy-enhanced version of AKMA.

This research resulted in two publications: privacy analysis of AKMA at IEEE EuroS&P 2025 and post-compromise security of AKMA at ACM ASIACCS 2025.

Future of Digital Power of Attorney (dPOA) (led by Prof Helen Treharne; 2025–present)

Our current project explores the digitalisation of power-of-attorney schemes. We study:

  • Risks of fraud introduced by digitalisation.
  • Opportunities to mitigate existing fraud and abuse in traditional systems.
  • Usability challenges for vulnerable individuals, such as older people, who may require third-party digital assistance.

Output: Verifiable Digital Power of Attorney under Strategic Adversaries: Correctness, Delegation, and Fraud Detection under Collusion · ESORICS 2026.

Selected publications

  1. Verifiable Digital Power of Attorney under Strategic Adversaries: Correctness, Delegation, and Fraud Detection under CollusionIoana Boureanu, Fortunat Rajaona, Sasa Radomirovic, Daniel Gardham, Helen Treharne · ESORICS 2026
  2. A Systematic Study of Practical & Formal Privacy in the 5G AKMA ProcedureIoana Boureanu, Steve Wesemeyer, Fortunat Rajaona, Steve Schneider, Helen Treharne · IEEE EuroS&P 2025
  3. An SMT-based approach to the verification of knowledge-based programsFrancesco Belardinelli, Ioana Boureanu, Vadim Malvone, Fortunat Rajaona · Formal Aspects of Computing, 2024
  4. Epistemic Model Checking for PrivacyFortunat Rajaona, Ioana Boureanu, Ramaswamy Ramanujam, Steve Wesemeyer · IEEE CSF 2024
  5. Program Semantics and Verification Technique for AI-centred ProgramsFortunat Rajaona, Ioana Boureanu, Vadim Malvone, Francesco Belardinelli · FM 2023 · Best Paper Award
  6. Fine-Grained Trackability in Protocol ExecutionsKsenia Budykho, Ioana Boureanu, Steve Wesemeyer, Fortunat Rajaona et al. · NDSS 2023

Research experience

  1. Research Fellow in Secure Systems

    Surrey Centre for Cyber Security · University of Surrey, UK

  2. Research Fellow in Formal Verification of Privacy

    Surrey Centre for Cyber Security · University of Surrey, UK

  3. Visiting Researcher

    RWTH Aachen University, MOVES group · Germany

Current position

Research Fellow in Secure Systems
Surrey Centre for Cyber Security
University of Surrey, UK

Teaching experience

  1. Research Fellow and MSc Supervisor

    University of Surrey · Guildford, Surrey, UK

  2. Contractual Lecturer

    École Normale Supérieure, University of Antananarivo · Madagascar

  3. Teaching Assistant

    University of Cape Town · South Africa

Education

  1. PhD in Mathematics

    University of Stellenbosch · South Africa

  2. MSc in Computer Science

    University of Stellenbosch · South Africa

  3. Postgraduate Diploma in Mathematical Sciences

    African Institute for Mathematical Sciences · South Africa

  4. BSc in Mathematics

    University of Antananarivo · Madagascar

Recognition

Amazon Research Award

2024 · Phoebe+: automated reasoning for provable privacy in cryptographic systems.

Best Paper Award

2023 · FM 2023 for work on semantics and verification of AI-centred programs.

My academic adventure

I grew up in Madagascar and chose Mathematics because it was my favourite subject at school. I especially enjoyed geometry, probability, mechanics, mathematical puzzles, and jokes. I began my undergraduate studies at the University of Antananarivo in 2006.

After completing my first degree in 2009, I was selected for the AIMS programme in South Africa. Meeting students and lecturers from across Africa, Europe, and America opened up a new international academic world to me. I stayed in South Africa for my MSc and PhD, working with Jeff Sanders on formal methods, knowledge, and privacy. I received a full DAAD scholarship for my PhD.

In 2016, I moved to Germany and joined the MOVES group at RWTH Aachen University as a visiting researcher, where I worked on probabilistic programming and reasoning about knowledge and information flow. After returning to Madagascar, I taught Mathematics and Programming at the École Normale Supérieure in Antananarivo from 2018 to 2019.

In 2020, I joined the University of Surrey, where I continue the adventure as a researcher in formal methods and secure systems.

Beyond research, I remain interested in holistic education and education and development in Africa.

Contact

Fortunat Rajaona, Ph.D. · Surrey Centre for Cyber Security · University of Surrey, Guildford, UK

s.{my_surname}.surrey.ac.ukUniversity of Surrey ↗