The importance of formal methods in analyzing and designing security protocols is undeniable. Specifically, security properties have been established in terms of equivalences between processes, typically expressed in extensions of the pi-calculus. However, while this type of process algebra, based on synchronous communication between processes, is natural for analyzing protocols involving message exchange (such as the Needham-Schroeder mutual authentication protocol), it is less suitable for modeling electronic voting systems or Covid management systems, which are based on data access and sharing.

In this context, algebras based on a shared data space between processes, such as coordination models or constraint synchronization models, appear more natural. Since my engagement in early December 2022, I have focused on studying the mCRL2 process algebra. In particular, I analyzed the Needham-Schroeder protocol using this algebra. This research was presented during a conference-debate titled "Industry-Science Collaboration in Cybersecurity."

More recently, in collaboration with Jean-Marie Jacquet and Manel Barkallah, I developed an extension of the Bach coordination language (developed at UNamur) aiming to capture key concepts from the Ros language, such as "topics" and "nodes." This led to the integration of Bach into the Scala language. A presentation on the Bach language and its relevance for modeling communication protocols was given at the Cyber-Excellence project researcher's afternoon on November 24th at UCLouvain.