计算机工程

• 安全技术 • 上一篇    下一篇

计算模型下的SSHV2协议认证性自动化分析

牛乐园,杨伊彤,王德军,孟博   

  1. (中南民族大学计算机科学学院,武汉 430074)
  • 收稿日期:2014-10-19 出版日期:2015-10-15 发布日期:2015-10-15
  • 作者简介:牛乐园(1990-),女,硕士研究生,主研方向:信息安全;杨伊彤,硕士研究生;王德军,讲师、博士;孟博(通讯作者),教授、博士后。
  • 基金项目:
    湖北省自然科学基金资助项目“安全协议代码的安全性自动化验证及软件工具开发”(2014CFB249);湖北省自然科学基金资助项目“有限射影几何方法研究高纬线性码的汉明重量”(2014CFB440);国家民族事务委员会自然科学基金资助项目“面向位置服务的隐私保护理论与方法研究”(12ZNZ009)。

Automatic Analysis on Authentication of SSHV2 Protocol in Computational Model

NIU Leyuan,YANG Yitong,WANG Dejun,MENG Bo   

  1. (College of Computer Science,South-Central University for Nationalities,Wuhan 430074,China)
  • Received:2014-10-19 Online:2015-10-15 Published:2015-10-15

摘要: 安全内壳(SSH)协议可以实现本地主机与远程节点的网络文件传输、远程登录、远程命令执行及其他应用程序的安全执行,其在保障网络安全方面发挥着重要作用。针对第二代安全内壳(SSHV2)协议的安全性进行研究,介绍SSHV2协议体系结构,解析出认证消息的消息结构,基于计算模型应用概率多项式进程演算,即Blanchet演算,对SSHV2安全协议进行形式化建模,并应用安全协议自动化分析工具CryptoVerif分析其认证性,结果表明,在计算模型下SSHV2安全协议具有认证性。

关键词: 第二代安全内壳协议, 安全协议, 计算模型, 认证性, CryptoVerif工具, 自动化分析

Abstract: Secure Shell(SSH) protocol can ensure the implementation of network file transfer between the local host and remote host,remote login,executing commands remotely and safe execution of other applications.It plays an important role in the protecting network security.This paper studies the security of the protocol.The main content of this article is the automated analysis of Secure Shell Version 2(SSHV2) protocol.This paper introduces the architecture of SSH protocol and gets the message terms by analyzing the authentication message flow of SSHV2 protocol.Based on computational model and application Blanchet calculus to give the formal model of SSHV2 security protocol,and analyzes the protocol’s certification by applying the security protocol automatic analysis tool CryptoVerif,shows that SSHV2 security protocol has authentication under the computational model.

Key words: Secure Shell Version 2(SSHV2) protocol, security protocol, computational model, authentication, CryptoVerif tool, automatic analysis

中图分类号: