基于spin工具模型检测

《基于spin工具模型检测》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、基于Spin工具的KDC密钥交换协议的模型检测分析专业:计算机软件与理论学号：2013021453姓名:马海峰指导老师：许道云基于Spin工具的KDC密钥交换协议的模型检测分析2013级计算机软件与理论马海峰20130214531研宄背景与验证环境介绍1.1研究背景与KDC密钥交换协议介绍1.1.1研究背景密码协议是以密码学为基础的消息交挽协议，其经常运用与计算机通信网络和分布式系统屮，运用密码算法来实现密钥分配和身份认证等功能。现在，密码协议已经在计算机领域得到广泛应用，但是，对密码协议的安全性认证和没计依然很困难。它的条件定义为：小

2、系统：参与协议运行的各主体都是唯一的(如一个发送者，一个响应者)，作用也是唯一的，这些主体也都是诚实的，诚实即是它们严格按照协议规定并遵循自己的身份参与协议运行。为了便于理解，引入强安全性破坏和一般安全性破坏的概念。强安全性破坏：即一个诚实的主体相信在协议运行中用到的一个值是仅他和另外诚实主体之间的共享密码，但入佼者知道这个值。-•般安全性破坏：一个诚实主体相信在一个完整协议运行中用到一个值是仅他和另外诚实主题之间共享秘密，但入侵者知道这个值。目前，对于模型检测技术分析密码协议，有以下己被证明的理论成果：如果在小系统上没有对协议的攻击导

3、致强安全性破坏，那么在任意系统上一定没有攻击导致强安全性破坏，淡然也就没有攻击导致一般安全性破坏。即：只要对被分析的密码协议在小系统上进行强安全性破坏分析，就可以保证协议在任意系统上的安全性。这个理论结果极大地促进了模型检测技术在密码协议分析领域的应用，使密码协议形式化分析方法的主流从逻辑方法转向了模型检测。1.1.2KDC密钥交换协议介绍网络通信双方进行安全通信需要两个条件：1保密通信的双方密钥需要共亨。2进行共享的密钥需要经常更换。假设有N个通信实体，保证他们之间任意两者都能进行通信，就需要N(N-1)/2个共享密钥。如果N很大，那

4、么根据上述公式可知需要分配的密钥数量是庞大的，也不利于实际利用；解决这个问题，可以采取密钥分配屮心KDC(KeyDistributionCenter)方案：如果有N个通信实体，迷药分配中心KDC只需要分发N个密钥(MasterKey,验证密钥)，实体间通信用会话密钢(SessionKey)來进行加密传输。这个方案的前提是，通信的各个实体必须信任KDC。下面介绍通过密钥分配中心KDC的网络通信协议的步骤：SteplA->KDC:A,BStep2KDC->A:KA(K),KB(K)Step3A->B:KB(K),K(M)经由密钥分配巾心KD

5、C(KeyDistributionCenter)的A和B之间的网络保密通信协议(所有通信实体A，B,C......的密钥都有KDC保管)：消息1表示A向KDC送去信息(A，B)，提出要同B保密通信；消息2KDC接到(A,B)后，随机产生“通信密钥”K,并用A,B的密钥分别加密:KA(K),KB(K)送给Ao消息3表示A接到KA(K),KB(K)后用自己的密钥KA解山通信密钥K,加密明文M,K(M)连同KB(K)送给B。消息4B得到K(M)与Kb(K),用自己的密钥Kb解出通信密钥K,在解出K(M)得到明文M。对于一个KDC系统，由于网络

6、是开放的，或者有恶意者通过其他方式非法入佼网络。则一个KDC系统也会受到攻击。对计算机网络系统安全构成威胁的主要是经过精心策划和设计的认为攻击，可以从攻击对原始信息产生的损害将其分为主动攻击和被动攻击两类。被动攻击不会导致对系统屮所含信息的任何改动，而且系统的操作和状态也不被改变,它主要威胁信息的保密性，主要手段有窃听和分析；主动攻击则是要篡改系统中所含信息，或者改变系统的状态和操作，它主要威胁信息的完整性、可川性和真实性，主要手段又3种：冒充，篡改，抵赖。1.2基于SPIN/Promela的验证环境SPIN是最强大的模型检测工具之一，

7、也是迄今为止唯一获得ACM软件系统奖的模型检测工具，本文实验所用为SPIN的(GUI)界面化工具iSPAN，Promela是SPIN的一种建模语言，在此不在赞述SPIN的背景与Promela语言的语法，主要介绍一下在windows下搭建环境的步骤：1在官网下载cygwin软件(用于虚拟Linux环境)，点击下载所有下载包，以免出错SelectPackagesSelectpackagestoinstalltSearchClearOKeepCurr(')ExpViewCategoryCategoryNewB..S..SizePackage>

8、日All4>Instal：田AccessibiliInstall田AdminInstall田Archive分Install田Audio分Install田Base4^Install田Database4^Ins