AI 中文总结
本章围绕证明助手，介绍其在系统安全、基于语言的安全、安全编译、密码学领域用于验证安全属性及支持认证的应用。
AI 中文摘要
证明助手常被用于验证设计与实现是否符合预期安全属性，使用证明助手的另一动机是支持认证。本章聚焦其在系统安全、基于语言的安全、安全编译及密码学中的应用。
英文摘要
Proof assistants are often used to validate that designs and implementations meet their expected security properties. A further motivation for using proof assistants is to support certification. This chapter focuses on their applications to system security, language-based security, secure compilation, and cryptography.
CommentsTo appear as chapter19 of the book "Proof Assistants and Their Applications in Mathematics and Computer Science"
