FM-SEC Network

Formal Methods for Security Network

FM-SEC Network

This a network of researchers and practitioners interested in formal methods for security, in theory, in tools and in the mix of both.

FM-SEC is born out of former “UK Network for Formal Methods in Security” (which was UK-based (see here).

FM-SEC is now a wider, international endavour. We run primarily as a seminar series, with monthly talks, by those active in and interested in formal methods for security.

We are co-hosting most of our events with the “Cyber Security & Privacy Seminar Series” (UK SPS); some events which are network-oriented or central to formal methods are hosted separately from UK SPS.

Forthcoming Talks

  • 13 April, 3PM UK time, Musard Balliu, joint with UK SPS, Title: Securing Cloud-based IoT Apps.
    Details (abstract, joining):
    **Abstract**: Innovative IoT apps break conventional paradigms to connect otherwise unconnected services and devices ranging from pacemakers, baby monitors, surveillance cameras to cars and smart cities. Unfortunately, the power of IoT apps can be abused by attackers, unnoticeably to users. In this talk, we will discuss how popular IoT app platforms are susceptible to attacks that violate user privacy resulting in massive exfiltration of sensitive information as well as suggest short- and long-term countermeasures based on language-based sandboxing and information flow control. **Zoom meeting link**: in email or via [UK SPS](; **Youtube live streaming**: [here](


  • 18 May, 3PM UK time, Bruno Blanchet, joint with UK SPS, Title: The security protocol verifier ProVerif and its recent improvements: lemmas, induction, fast subsumption, and much more.
    Details (abstract, joining):
    **Abstract**: ProVerif is a widely used automatic security protocol verifier that relies on symbolic model of cryptography. It can prove various security properties (secrecy, correspondences, some equivalences) for an unbounded number of sessions, as well as find attacks. In this talk, we will present an overview of ProVerif and its recent improvements. These improvements are twofold. First, we extended ProVerif with lemmas, axioms, proofs by induction, natural numbers, and temporal queries. These features not only extend the scope of ProVerif, but can also be used to improve its precision (that is, avoid false attacks) and make it terminate more often. Second, we reworked and optimized many of the algorithms used in ProVerif (generation of clauses, resolution, subsumption, ...), resulting in impressive speed-ups on large examples. These improvements are joint work with Vincent Cheval and Véronique Cortier, to appear at IEEE Security and Privacy 2022. **Zoom meeting link**: in email or via [UK SPS](; **Youtube live streaming**: [here](

Managed by

Ioana Boureanu and Erisa Karafili

What to Join or Give a Talk? Email us at