Formalise results in algebra and cryptography, and develop a unified theory of end-to-end security for web applications

Formalise results in algebra and cryptography, and develop a unified theory of end-to-end security for web applications, combining provably correct cryptography and language-based information flow security. Use the Isabelle proof assistant to develop formal mathematical libraries for advanced results in field theory. Instantiate some of these results to certify cryptographic protocols. Attempt to develop in Isabelle a general theory of information flow security that can be used to provide formal end-to-end guarantees to web-based systems. For example, his theory will allow to combine (1) the provable security of cryptographic protocols used in internet communication at the network layer with (2) formal information flow security guarantees established at the application layer on the server, to obtain an end-to-end security guarantee for the web-based system as whole (from the end user's perspective). This degree of unification is an ambitious aim that has not been attempted before. Without such a unified view, the landscape of internet security is currently fragmented, leaving a lot of uncertainty for the end users.