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

将代数和密码学的结果形式化，并开发 Web 应用程序端到端安全的统一理论

• 批准号: 2784426
• 金额: --
• 依托单位: University of Sheffield
• 依托单位国家: 英国
• 项目类别: Studentship
• 财政年份: 2022
• 资助国家: 英国
• 起止时间: 2022 至 无数据
• 项目状态: 未结题
• 来源: https://gtr.ukri.org/projects?ref=studentship-2784426
• 关键词: Formalise; results; algebra; cryptography; develop

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.

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