端到端安全协议验证方向博士研究员
PhD in End-to-End Verification of Security Protocols in Isabelle
原帖优先：申请材料、截止时间与资格以原帖和学校官方说明为准。
AI 中文速览
- 研究内容
- 本项目研究如何利用定理证明建立端到端保障，重点关注程序与安全协议所用表示形式之间经过验证的-translations，并以Isabelle/HOL作为主要的形式化环境，应用领域包括零知识证明系统（如STARK风格协议）。
- 申请条件
- 适合对形式化验证、编程语言、网络安全、密码学、编译器或定理证明感兴趣的候选人；具备Isabelle或零知识证明的相关经验会有所帮助，但并非必需。
- 待遇
- 奖学金提供2026/7学年每年的学费资助以及每年21,805英镑的生活津贴。
- 申请方式
- 截止日期为2026年12月8日，申请方式与具体提交地址请参考学校官方招生页面。
由 gemini-2.5-flash-lite 生成，博士岗判定置信度 100%。
岗位信息
- 截止
- （Europe/London） 剩 40 天
- 学科
- 计算机科学
- 合同类型
- 雇佣合同
- 原文薪资
- GBP 21,805 / 年（税前）
- 税后月薪（估）
- ¥13,700；房租后 ¥5,400
- 估算假设
- 单身、无子女、雇佣合同的粗略估算，以学校 offer 为准；扣除率 18%；汇率日期 2026-10-01
- 原帖发布
- 本站收录
- 内容更新
- 来源
- jobs.ac.uk（英国博士项目及学术招聘） · 最近核对 2026-10-28
- 详情核验
判定依据（原文摘录）
- 这是一个博士生培养项目
This PhD project will investigate how theorem proving can be used to establish such end-to-end guarantees.
- 主要使用Isabelle/HOL作为形式化环境
using Isabelle/HOL as the main formalisation environment.
- 奖学金提供学费和每年津贴
The studentship will provide funding of fees and a stipend per annum for 2026/7
原文
Modern security systems often rely on complex software that translates programs into forms that can be checked automatically. To trust such systems, it is not enough to verify the underlying security protocol: we must also know that the checked representation faithfully captures the intended program. This PhD project will investigate how theorem proving can be used to establish such end-to-end guarantees.
The work will focus on verified translations between programs and the representations used by security protocols, using Isabelle/HOL as the main formalisation environment. Zero-knowledge proof systems, including STARK-style protocols, will provide one important application area. The central research question is how to connect programs, compilation and cryptographic protocols so that correctness and security guarantees can be composed and reused.
The project spans formal methods, programming languages, cybersecurity and cryptography, with scope to shape its direction according to the student's interests. The student will develop and verify semantic models and compilation techniques in Isabelle/HOL, showing that generated representations faithfully capture source-program behaviour. The longer-term goal is to connect these results with mechanised security arguments for the underlying verification protocol.
The supervisory team brings expertise in Isabelle, formal methods, smart-contract verification and security-protocol verification. The project is suitable for candidates interested in formal verification, programming languages, cybersecurity, cryptography, compilers or theorem proving. Prior experience with Isabelle or zero-knowledge proofs is useful but not essential.
Location
University of Exeter, Streatham Campus £21,805. The studentship will provide funding of fees and a stipend per annum for 2026/7