Formal Methods for Security 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

  • 21 September, 3PM UK time, Steve Kremer, joint with UK SPS, Title: Symbolic protocol verification with dice: process equivalences in the presence of probabilities
    Details (abstract):
    Symbolic protocol verification generally abstracts probabilities away, considering computations that succeed only with negligible probability, such as guessing random numbers or breaking an encryption scheme, as impossible. This abstraction, sometimes referred to as the perfect cryptography assumption, has shown very useful as it simplifies automation of the analysis. However, probabilities may also appear in the control flow where they are generally not negligible. In this paper we consider a framework for symbolic protocol analysis with a probabilistic choice operator: the probabilistic applied pi calculus. We define and explore the relationships between several behavioral equivalences. In particular we show the need for randomized schedulers and exhibit a counter-example to a result in a previous work that relied on non-randomized ones. As in other frameworks that mix both non-deterministic and probabilistic choices, schedulers may sometimes be unrealistically powerful. We therefore consider two subclasses of processes that avoid this problem. In particular, when considering purely non-deterministic protocols, as is done in classical symbolic verification, we show that a probabilistic adversary has-maybe surprisingly-a strictly superior distinguishing power for may testing, which, when the number of sessions is bounded, we show to coincide with purely possibilistic similarity. This is joint work with Vincent Cheval and Raphaëlle Crubillé.

Join us on Zoom here: here (passcode on via email or on the UK SPS website)

See this, live, on Youtube here: here

Past Talks

  • 20 July, 3PM UK time, Charlie Jacomme, joint with UK SPS, Title: Not so AdHoc testing: formal methods in the standardization of the EDHOC protocol.
    Details (abstract):
    Abstract : We believe that formal methods in security should be leveraged in all the standardisation's of security protocols in order to strengthen their guarantees. To be effective, such analyses should be: * maintainable: the security analysis should be performed on every step of the way, i.e. each iteration of the draft; * pessimistic: all possible threat models, notably all sort of compromise should be considered; * precise: the analysis should notably include as many real life weaknesses of the concrete cryptographic primitives specified. In this talk, we illustrate how such a goal may be approached by detailing our analysis of the current IETF draft standard of the EDHOC protocol, as well as our subsequent interactions with its LAKE working group. We will proceed in three steps, first introducing the Sapic+ platform that allows from a single modeling of a protocol to benefit from all the capabilities of multiple automated verification tools (ProVerif,Tamarin,DeepSec). We will then introduce multiple recent advances on how to better model the cryptographic primitives and their real life weaknesses. We will finally show how we leveraged Sapic+ along with the advanced primitive models to analyze the EDHOC protocol and provide feedback to the LAKE working group that has been integrated in latter drafts.

See this on Youtube here: here

  • 29 June, 3PM UK time, Vincent Cheval, joint with UK SPS, Title: A little more conversation, a little less action, a lot more satisfaction: Global states in ProVerif.
    Details (abstract):
    Abstract : ProVerif is a popular tool for the fully automatic analysis of security protocols, offering very good support to detect flaws or prove security. One exception is the case of protocols with global states such as counters, tables, or more generally, memory cells. ProVerif fails to analyse such protocols, due to its internal abstraction. In the original paper of GSVerif, our key idea was to devise a generic transformation of the security properties queried to ProVerif. We proved the soundness of our transformation and implemented it into a front-end GSVerif. Our experiments showed that our front-end (combined with ProVerif) outperforms the few existing tools, both in terms of efficiency and protocol coverage. We successfully applied our tool to a dozen of protocols of the literature, yielding the first fully automatic proof of a security API and a payment protocol of the literature. In the newest version of ProVerif, the generic transformations of GSVerif can be fully described in term of axioms, thus taking advantage of this new ProVerif feature.

    See this on Youtube: 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):
    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.

    See this on Youtube: here

  • 13 April, 3PM UK time, Musard Balliu, joint with UK SPS, Title: Securing Cloud-based IoT Apps.
    Details (abstract):
    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.

    See this on Youtube: here

Managed by

Ioana Boureanu and Erisa Karafili

What to Join or Give a Talk? Email us at