Verification of $K$- and Infinite-Step Strong/Weak Anonymity Using Concurrent Compositions
本文研究部分可观测离散事件系统中的匿名性验证问题。匿名性是一种信息流安全属性，其核心思想是：在外部观察者通过系统输出（观测）推断系统内部状态时，系统不应让某一时刻的状态被唯一确定，从而保护用户隐私。在离散事件系统框架下，已有 K-步匿名性和
#automata
共收录 2 条相关情报。
← 返回所有主题Automata-Based Automated Detection of State Machine Bugs in Protocol Implementations.
该论文提出了一种基于自动机的黑盒技术，用于自动检测有状态网络协议实现中的状态机漏洞。有状态安全协议的实现需要维护一个状态机来跟踪协议进展，管理消息的类型和顺序以及加密材料，而状态机错误（即状态机bug）可能导致严重安全漏洞。该方法以协议的状