本文研究部分可观测离散事件系统中的匿名性验证问题。匿名性是一种信息流安全属性，其核心思想是：在外部观察者通过系统输出（观测）推断系统内部状态时，系统不应让某一时刻的状态被唯一确定，从而保护用户隐私。在离散事件系统框架下，已有 K-步匿名性和无限步匿名性的定义：K-步匿名性要求当前时刻之前至多 K 个观测步内，状态估计不能是单例；无限步匿名性则不对 K 设限。作者针对由非确定有限状态自动机建模的部分可观测系统，提出了四种新的匿名性概念——两种强匿名性和两种弱匿名性，分别称为 K-步强/弱匿名性和无限步强/弱匿名性。这些概念与已有定义的本质区别在于引入了强匿名投影与弱匿名投影的考量，使匿名性刻画更加精细，能够适应不同的隐私需求。为了验证这四种性质，作者发展了一套基于并发组合（concurrent composition）的新方法：通过构造系统的并发组合结构，系统性地追踪观测一致的状态对/状态集，从而将匿名性验证转化为对组合图的结构性质检查。基于该结构，论文给出了四种匿名性可验证的充要条件，并分析了相应算法的时间复杂度。此外，还计算了 K-步强匿名性和弱匿名性中 K 的上界，为实际应用中选择合适的匿名窗口提供了理论依据。本文属于形式化方法与信息流安全的交叉方向，适合从事隐私验证、自动机理论、安全协议分析的研究人员阅读。由于仅有摘要，具体定理证明与实验评估细节需参见全文。

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