• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>International Journal of Information Security >OFMC: A symbolic model checker for security protocols
【24h】

OFMC: A symbolic model checker for security protocols

机译：OFMC：安全协议的符号模型检查器

获取原文
获取原文并翻译 | 示例
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

We present the on-the-fly model checker OFMC, a tool that combines two ideas for analyzing security protocols based on lazy, demand-driven search. The first is the use of lazy data types as a simple way of building efficient on-the-fly model checkers for protocols with very large, or even infinite, state spaces. The second is the integration of symbolic techniques and optimizations for modeling a lazy Dolev–Yao intruder whose actions are generated in a demand-driven way. We present both techniques, along with optimizations and proofs of correctness and completeness. Our tool is state of the art in terms of both coverage and performance. For example, it finds all known attacks and discovers a new one in a test suite of 38 protocols from the Clark/Jacob library in a few seconds of CPU time for the entire suite. We also give examples demonstrating how our tool scales to, and finds errors in, large industrial-strength protocols.
机译：我们介绍了动态模型检查器OFMC，该工具结合了两种思想，可以基于需求驱动的惰性搜索来分析安全协议。首先是使用惰性数据类型作为为具有非常大甚至无限状态空间的协议构建有效的动态模型检查器的简单方法。第二个是符号技术和优化的集成，用于对懒惰的Dolev–Yao入侵者进行建模，该入侵者的行为是以需求驱动的方式生成的。我们介绍了这两种技术，以及优化和正确性和完整性的证明。我们的工具在覆盖范围和性能方面都是最先进的。例如，它会在几秒钟的整个CPU时间内，从Clark / Jacob库中的38种协议的测试套件中找到所有已知的攻击并发现新的攻击。我们还提供了一些示例，展示了我们的工具如何扩展到大型工业强度协议并发现错误。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号