基于Dining密码协议的认知模型检验抽象
Abstraction for Epistemic Model Checking of Dining Cryptographers-based Protocols
摘要：
本文描述了一个抽象的协议，是基于多轮的Chaum的用餐密码协议。证明了这种抽象在知识逻辑中保留了丰富的规范，包括描述一个主体对其他主体知识的了解的规范。该结果可用于优化基于Dining Cryptographers协议的模型检验，并应用于基于知识的程序实现和验证方法中。这样的应用程序的一些案例研究给出了一个协议，使用的用餐密码协议作为一个原始的匿名广播系统。给出了该协议的具体模型和抽象模型的模型检验性能结果，并得出了一些新的结论。
英文摘要：
The paper describes an abstraction for protocols that are based on multiple rounds of Chaum's Dining Cryptographers protocol. It is proved that the abstraction preserves a rich class of specifications in the logic of knowledge, including specifications describing what an agent knows about other agents' knowledge. This result can be used to optimize model checking of Dining Cryptographers-based protocols, and applied within a methodology for knowledge-based program implementation and verification. Some case studies of such an application are given, for a protocol that uses the Dining Cryptographers protocol as a primitive in an anonymous broadcast system. Performance results are given for model checking knowledge-based specifications in the concrete and abstract models of this protocol, and some new conclusions about the protocol are derived.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
