安全协议论文：安全协议 形式化分析 串空间模型 认证测试.doc

安全协议论文：安全协议 形式化分析 串空间模型 认证测试【中文摘要】随着网络技术和信息技术的迅速发展,计算机网络在诸多领域内的应用日益普及,然而由于其运行环境具有开放性,使得计算机网络在给人们带来巨大便利的同时,也产生一系列的安全问题,因此如何确保网络中信息的安全性成为亟待解决的问题。安全协议又称密码协议,是以密码学技术为基础,在不安全的公共网络和分布式系统中提供各种安全服务的一种通信协议。由于安全协议的安全性是评价网络好坏的一个重要指标,所以在安全协议投入使用之前,对其安全性分析就显得尤为重要。至今,安全协议的形式化分析和自动化检测己成为分析和研究安全协议领域的两个重要方向,而研制可靠实用的安全协议自动化分析工具也逐渐成为主流趋势。本文以串空间理论为基础,通过对当前存在的一些安全协议形式化方法和自动化技术进行比较分析,深入地研究了安全协议的自动化分析方法。主要内容包括：1)深入研究了安全协议的安全性质,针对当前运用比较广泛的形式化分析方法串空间模型,通过研究构造方法,重点介绍了NSL协议的分析过程；同时,以SSM协议为例,探讨了如何使用认证测试验证协议的过程及设计原理。2)给出了一种基于串空间模型的安全协议自动化验证方法。在该方法中,针对参与方不检测某些消息的来源,只是将其作为消息的子项参与协议的运行的问题,通过构造和合法串结构相同的攻击者串的方式,给出了一种自动化验证方法；它不仅能够分析具有加密类型的攻击缺陷的协议,还将可信方引入到协议的参与方,使之能够分析具有重放类型攻击缺陷的协议,整个过程无需人工干预,直观和高效。在文章的最后借助两个实例,详细说明了该系统的验证过程,结果表明系统具有良好的性能。【英文摘要】With the fast development of network communication and information technology, network has exised in various fields. And network security problem is increasingly serious; whose reason is its circumstances is an open secret that can be easily modified, forged and replayed. So how to solve the network security problem has been the increasingly outstanding problem.Security protocol, called cryptographic protocol which seems especially important in safety and reliability, is a protocol for various types of security service over an insecure network. Before it is put into use, taking the openness of environmet and the imperfection of structrue into account, the attacker may execute effective attacks with the aid of shortcomings, therefore it is important for us to validate its correctness.So far, it has became a hotspot and important area in security protocols to give formal analysis and automatic detection, correspondingly, designing efficient and reliable tools for analyzing security protocols has been the dominant trend.Based on strand space model, this paper makes a research on some kinds of formal analysis and automatic analysis in security protocols nowadays, especially focus on the analysis of security protocols using automatic mehod. Following are the main results of this paper:1) This paper makes a deep study on security protocols, and focusing on the current formal analysis method boardly-strand space model, we mainly studies the analysis of NSL protocol process by whose construction method. At the same time, this paper also further studies the authentication process and puts forward the SSM protocol.2) This paper proposes a new automatic analysis method based on strand space model.Aming at the problem that not checking the source of information and only accepting it as a subset, the paper proposes an automatic method, which supports the string matching through structure the strings of identical construction, and it not only can analyze the two-party protocols but also makes it use three-side indentication protocols.lastly; it illuminates the structure of the tool, and implements technology with the aid of two agreements. All the whole process has majour or theoretic value and wideranging application.【关键词】安全协议 形式化分析 串空间模型 认证测试【英文关键词】Security protocols formal analysis strand space model authentication test method【目录】基于串空间模型的安全协议自动化验证方法研究摘要4-5Abstract5-6目录7-10图表目录10-111 绪论11-161.1 概述11-141.1.1 研究背景和意义11-121.1.2 国内外研究现状12-141.2 研究内容及章节安排14-161.2.1 论文研究内容141.2.2 论文解决的问题14-151.2.3 章节安排15-162 安全协议分析的基础和理论16-302.1 安全协议16-192.1.1 安全协议的基本理论16-172.1.2 安全协议的安全属性17-182.1.3 安全协议所面临的安全威胁18-192.2 密码学的基础19-232.2.1 密码学的分类20-212.2.2 密码学的应用21-232.3 串空间模型(Strand Space Model)23-272.3.1 串空间模型的基本理论232.3.2 串空间模型的基本概念23-272.4 串空间模型的应用27-292.4.1 串空间模型中正确性概念27-282.4.2 串空间模型的应用28-292.5 本章小结29-303 认证测试及其应用30-343.1 认证测试30-323.1.1 认证测试的概念31-323.2 SSM协议分析32-333.2.1 串空间模型323.2.2 认证性分析32-333.3 本章小结33-344 安全协议自动化分析技术34-434.1 协议自动化分析简介34-354.2 协议自动化分析技术35-424.2.1 模型框架35-384.2.2 算法描述38-424.3 本章小结42-435 系统设计与验证43-535.1 系统设计43-475.1.1 核心数据结构设计43-445.1.2 核心模块设计44-475.2 实例测试47-525.2.1 问题描述475.2.2 串空间模型47-485.2.3 实例验证48-515.2.4