• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>IFIP 177; IFIP(International Federation for Information Processing) TC-11 International Workshop on Certification and Security in Inter-Organizational E-Services(CSES), World Computer Congress; 20040822-27; Toulouse(FR) >GENERATING NETWORK SECURITY PROTOCOL IMPLEMENTATIONS FROM FORMAL SPECIFICATIONS
【24h】

GENERATING NETWORK SECURITY PROTOCOL IMPLEMENTATIONS FROM FORMAL SPECIFICATIONS

机译：通过正式规范生成网络安全协议的实现

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

摘要

We describe the Spi2Java code generation tool, which we have developed in an attempt to bridge the gap between formal security protocol specification and executable implementation. Implemented in Prolog, Spi2Java can input a formal security protocol specification in a variation of the Spi Calculus, and generate a Java code implementation of that protocol. We give a brief overview of the role of code generation in the wider context of security protocol development. We cover the design and implementation of Spi2Java which we relate to the high integrity code generation requirements identified by Whalen and Heim-dahl. By defining a Security Protocol Implementation API that abstracts cryptographic and network communication functionality we show that protocol logic code can be separated from underlying cryptographic algorithm and network stack implementation concerns. The design of this API is discussed, particularly its support for pluggable implementation providers. Spi2Java's functionality is demonstrated by way of example: we specify the Needham-Schroeder Public Key Authentication Protocol, and Lowe's attack on it, in the Spi Calculus and examine a successful attack run using Spi2Java generated implementation of the protocol roles.
机译：我们描述了Spi2Java代码生成工具，我们开发该工具的目的是弥合形式安全协议规范和可执行程序实现之间的差距。 Spi2Java在Prolog中实现，可以在Spi Calculus的变体中输入正式的安全协议规范，并生成该协议的Java代码实现。我们简要概述了代码生成在安全协议开发的更广泛上下文中的作用。我们介绍了Spi2Java的设计和实现，它与Whalen和Heim-dahl所确定的高完整性代码生成要求有关。通过定义一个抽象加密和网络通信功能的安全协议实现API，我们证明了协议逻辑代码可以与基础加密算法和网络堆栈实现问题分开。讨论了此API的设计，尤其是其对可插拔实现提供程序的支持。通过示例演示Spi2Java的功能：我们在Spi Calculus中指定Needham-Schroeder公钥身份验证协议以及Lowe对它的攻击，并使用Spi2Java生成的协议角色实现检查成功的攻击。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号