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