In recent years, formal security analysis of protocols has proven highly effective in finding security vulnerabilities and establishing strong security guarantees. Ideally, such formal analysis should be conducted during the development of protocols to ensure that emerging standards and their implementations are secure from the outset. In a nutshell, this approach consists of three steps: creating a mathematical model of the protocol, precisely formalizing the desired security goals, and creating a mathematical proof of these security goals.

In this session, we provide a general overview of formal methods for protocol security, and briefly present a selection of our previous and ongoing work conducted with the Web Infrastructure Model, including analyses of the OpenID FAPI, OpenID Federation, and OpenID VP/VCI protocols. We discuss how the formal approach was useful for identifying new kinds of attacks, clarifying the exact conditions under which these protocols are secure, and overall improvements of specifications. We also discuss the limitations of existing mechanized approaches that provide tool-based support for formal analysis. We conclude with an overview of our ongoing work to provide a mechanized framework that accounts for a rich model of the Web.