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

将代数和密码学的结果形式化，并为web应用程序开发端到端安全的统一理论，结合可证明正确的密码学和基于语言的信息流安全。使用伊莎贝尔证明助理开发正式的数学库为先进的结果在场论。实例化其中一些结果来验证加密协议。尝试在Isabelle中发展信息流安全的一般理论，该理论可用于为基于web的系统提供正式的端到端保证。例如，他的理论将允许将(1)网络层互联网通信中使用的可证明的加密协议的安全性与(2)服务器上应用层建立的正式信息流安全保证相结合，以获得基于web的系统作为整体的端到端安全保证（从最终用户的角度来看）。这种程度的统一是一个雄心勃勃的目标，以前从未有人尝试过。如果没有这样一个统一的观点，互联网安全的前景目前是碎片化的，给最终用户留下了很多不确定性。

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.