基于Event-B的SSL握手协议建模分析与验证

发布时间：2018-11-05 19:59

【摘要】：随着互联网技术的发展和普及,网络环境正变得日益复杂。在开放的网络中,如何确保通信安全是当今—项重要的议题。以密码技术为基础,网络安全协议实现了开放网络环境中的通信安全,它是网络信息安全的基础。由于安全协议的重要性,它本身设计的合理性和正确性已经成为网络安全研究的重要内容。本文尝试使用形式化方法Event-B在Rodin平台上对安全套接层握手协议进行了建模分析与验证。文中首先介绍了形式化方法的概念并概述了安全网络协议及其性质的相关内容。然后对形式化方法Event-B及其工具Rodin进行了简要的介绍。其次,本文初步分析了安全套接层协议客栈的体系结构、工作原理和安全机制,并着重探究了握手协议。随后,试着提取了协议的需求说明,同时制定了模型精化策略,并在此基础上对握手协议进行了初步的建模分析。接着尝试对公钥真实性验证过程和有攻击者参与的情况分别进行了建模分析。最后借助Rodin平台的自动证明和交互式证明机制试着对模型正确性进行验证。本文的结果表明,采用Event-B方法对握手协议进行分析和验证是比较有效的,模型精化过程对深入理解协议较为有利。在一定前提下协议具有认证性和保密性,协议本身的机制能够有效检测出针对消息篡改类的攻击行为。本文对SSL握手协议部分进行了建模,未来可在本文基础上完成对整个协议栈的分析。
[Abstract]:With the development and popularization of Internet technology, the network environment is becoming more and more complex. In an open network, how to ensure communication security is an important issue today. Based on cryptography, network security protocol realizes communication security in open network environment, which is the basis of network information security. Due to the importance of security protocol, the rationality and correctness of its own design has become an important content of network security research. This paper attempts to use the formal method Event-B to model and verify the secure socket layer handshake protocol on the Rodin platform. In this paper, the concept of formal method is introduced, and the contents of secure network protocol and its properties are summarized. Then the formal method Event-B and its tool Rodin are briefly introduced. Secondly, this paper analyzes the architecture, working principle and security mechanism of secure socket layer protocol inn, and probes into handshake protocol. Then, the requirements of the protocol are extracted, and the model refinement strategy is formulated. Based on this, a preliminary modeling analysis of the handshake protocol is carried out. Then we try to model and analyze the public key authenticity verification process and the situation in which the attacker is involved. Finally, with the help of the automatic proof and interactive certification mechanism of Rodin platform, we try to verify the correctness of the model. The results of this paper show that the analysis and verification of handshake protocol using Event-B method is more effective, and the process of model refinement is more beneficial to the in-depth understanding of the protocol. Under certain conditions, the protocol has authentication and confidentiality, and the mechanism of the protocol itself can effectively detect the attacks against message tampering classes. In this paper, the SSL handshake protocol is modeled and the whole stack can be analyzed in the future.
【学位授予单位】：浙江大学
【学位级别】：硕士
【学位授予年份】：2017
【分类号】：TP393.08

【相似文献】