miTLS （镜像）miTLS是经过验证的TLS协议参考实现

miTLS 是经过验证的参考实现。我们的代码完全支持 RFC 中规定的有线格式、密码套件、会话和连接、重新握手和恢复、警报和错误以及数据碎片；它与主流网络浏览器和服务器互操作。我们的代码经过精心构建，实现了从主要 API 到加密算法的计算假设的模块化、自动化验证。实现是用编写，并在指定。我们介绍了其主要组件的安全规范，例如记录层的经过身份验证的流加密和握手的密钥建立。我们使用 F7 细化类型检查器描述了他们的验证。为此，我们为 TLS 的每个加密原语和构造配备了一个新的类型化接口，以捕获其安全属性，并逐渐用理想的功能替换具体的实现。我们最终对协议状态机进行类型检查，从而在实现和部署 TLS 时获得精确的安全定理。我们还重温了经典攻击并报告了一些新攻击。TLS 可能是最常用的安全通信协议，它有 18 年的缺陷和修复历史。