协议是通信实体之间进行通信的特定规则集合。协议实现是把设计完成的协议按照其规范通过软件或者硬件进行实现，进而可以部署到系统中。协议实现包含协议客户端实现和协议服务器端实现。协议实现安全主要研究协议实现与协议规范的一致性以及协议实现中的安全问题。协议实现往往要比其规范更为复杂，而且协议实现者的专业素质存在差异，进行协议实现时无法保证不引入逻辑错误或者代码错误甚至安全问题。很多实践表明，即使是已被证明安全的协议，在实现时可能由于协议实现者的失误而引入了新的安全问题，变得不再安全。

协议实现安全重点关注其软件实现的安全问题，分别基于以下3个假设：基于假设①，能够获取协议客户端实现及协议服务器端实现；基于假设②，仅能够获取协议客户端实现；基于假设③，不能获取协议客户端实现和协议服务器端实现。

基于假设①，主要研究方法有2种，一种以程序验证技术为主，另一种以模型抽取方法为主。应用程序验证技术对已有协议实现的安全性进行分析，分别基于逻辑、基于类型系统、类型系统与逻辑证明相结合，直接分析其安全性。这种方法大部分既没有证明分析过程的正确性，又依赖于在协议实现中添加大量的代码注释与断言。模型抽取方法即从协议实现中抽取协议抽象规范，并且证明抽取方法的正确性，然后用协议抽象规范安全性分析工具分析其安全性。此方法被认为非常有效和合理的，适合用来分析协议实现这种较小规模的代码。基于假设①分析协议实现安全性难度较小。但是在现实应用场景中，研究者不可能获取协议客户端实现和协议服务器端实现，故实用价值小。

基于假设②，主要研究方法结合了模型抽取方法和协议逆向工程。首先对获取的协议客户端实现进行分析，抽取协议客户端抽象规范。然后根据抽取的协议客户端抽象规范和协议逆向工程技术，得到协议服务器端抽象规范，进而得到协议完整抽象规范。最后应用形式化方法分析此规范的安全性，得到协议实现的安全性分析结果。基于假设②分析协议实现安全性难度适中。在大量现实应用场景中，研究者确实可以获取协议客户端实现，故实用价值大。

基于假设③，主要研究方法为协议逆向工程。通过分析协议会话过程，重构协议通信过程，从而得到协议的格式结构和功能，进而分析协议实现的安全性。协议逆向工程主要包含基于网络轨迹的分析和基于指令序列的分析。基于网络轨迹的分析方法首先通过捕获网络数据包，然后对其进行分析，进而还原协议的抽象规范，再使用形式化方法验证该规范的安全性，最后得到协议实现的安全性分析结果。基于指令序列的分析，通过监控、标记网络数据过程中的指令序列和对内存缓冲区的读写的操作，进而还原协议抽象规范，再使用形式化方法验证此规范的安全性，最后得到协议实现的安全性分析结果。基于假设③分析协议实现安全性难度最大。在某些实际应用场景中，研究者确实不能够获取协议客户端实现和协议服务器端实现，故实用价值较大。

综上可知，协议实现安全不仅可以分析协议实现的安全性，还可以丰富和发展协议、可信程序验证与密码学理论，同时也具有较大的应用价值。