The Web Infrastructure Model, or just WIM, is a comprehensive, expressive and precise model of the web infrastructure. The WIM is in fact the most comprehensive formal model of the Web infrastructure to date. It allows for accurate security and privacy analyses of current web standards and applications, and can serve as a reference for web security researchers, developers of new technologies and standards, and for teaching web security concepts.
The WIM has successfully been used to analyze several security critical web standards and applications. The formal analysis often uncovered attacks and let to fixes in the respective standards and applications, which we then proved secure based on the WIM. In the following, we give a short overview of the web standards and applications analyzed in the WIM so far.
The first version of the WIM was published at [S&P2014]. Throughout all further papers we improved and extended the WIM. For example, in the [CCS2015] paper, we made several improvements to enable privacy analysis. The most recent version of the WIM, including new features, such as WebRTC and WebSockets, can be found in Daniel Fett's PhD thesis.
We are currently working on mechanizing the WIM.
This work has been supported by Deutsche Forschungsgemeinschaft (DFG) as well as by the Studienstiftung des Deutschen Volkes (German National Academic Foundation).