该论文提出了一种基于自动机的黑盒技术，用于自动检测有状态网络协议实现中的状态机漏洞。有状态安全协议的实现需要维护一个状态机来跟踪协议进展，管理消息的类型和顺序以及加密材料，而状态机错误（即状态机bug）可能导致严重安全漏洞。该方法以协议的状态机bug目录作为输入，每个bug被表示为一个有限自动机，接受能够暴露该bug的消息序列。同时，它利用模型学习获得的（可能不准确的）待测实现模型，构造出模型中可执行且自动机可暴露bug的消息序列集，然后将这些序列转化为实际实现上的测试用例，以发现bug证据或排除误报。研究人员将技术应用于三个广泛使用的SSH服务器实现和九个不同的DTLS服务器和客户端实现（包括最新版本）。实验表明，该方法轻松复现了此前安全研究人员发现的所有bug，并生成了证据。更重要的是，它发现了这些实现中多个之前未知的bug，包括两个新漏洞，以及在相同SSH和DTLS实现的新版本中的多种新bug和不符合规范问题。该方法完全黑盒、自动化，可扩展至其他有状态协议，为协议实现的安全性测试提供了有力工具。