首页> 外文OA文献 >Model checking of knowledge in unconditionally secure cryptographic protocols
【2h】

Model checking of knowledge in unconditionally secure cryptographic protocols

机译:无条件安全密码协议中知识的模型检查

代理获取
本网站仅为用户提供外文OA文献查询和代理获取服务,本网站没有原文。下单后我们将采用程序或人工为您竭诚获取高质量的原文,但由于OA文献来源多样且变更频繁,仍可能出现获取不到、文献不完整或与标题不符等情况,如果获取不到我们将提供退款服务。请知悉。

摘要

Knowledge-based programs provide an abstract level of description of protocols in which agent actions are related to their states of knowledge. The thesis describes how epistemic model checking technology may be applied to discover and verify concrete implementations based on this abstract level of description. The details of the implementations depend on the specific context of use of the protocol. The knowledge-based approach enables the implementations to be optimized relative to these conditions of use. The approach is illustrated using extensions of the Dining Cryptographers protocol, a security protocol for anonymous broadcast.This thesis also provides a comprehensive introduction to epistemic logic model checking and its application to the verification of security protocols involving multiple agents. It gives the necessary background to model checking techniques. It then investigates the cause and effects of the state space explosion problem, known as the major drawback of the model checking approach. It develops ways to improve the performance of model checking for knowledge in Chaum's dining cryptographers protocol and its extensions.The thesis suggests 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 is used to optimize model checking of Dining Cryptographers-based protocols, and applied within a methodology for knowledge-based program implementation and verification.
机译:基于知识的程序提供了协议描述的抽象级别,其中代理的行为与其知识状态有关。本文描述了基于这种抽象描述水平的认知模型检查技术如何被发现和验证具体实现。实现的细节取决于协议使用的特定上下文。基于知识的方法使实现相对于这些使用条件得以优化。通过对匿名加密广播安全协议“加密餐厅”协议的扩展来说明这种方法。本文还全面介绍了认知逻辑模型检查及其在涉及多个代理的安全协议验证中的应用。它为模型检查技术提供了必要的背景。然后研究状态空间爆炸问题的因果关系,这是模型检查方法的主要缺点。提出了提高Chaum餐饮密码学家协议及其扩展知识模型检查性能的方法。本文提出了基于Chaum餐饮密码学家协议多轮协议的抽象协议。事实证明,抽象在知识逻辑中保留了丰富的规范类别,包括描述代理对其他代理知识的了解的规范。此结果用于优化基于餐饮密码学家的协议的模型检查,并应用于基于知识的程序实现和验证的方法学中。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号