iSpin工具模型检测实验报告.docx
《iSpin工具模型检测实验报告.docx》由会员分享，可在线阅读，更多相关《iSpin工具模型检测实验报告.docx（12页珍藏版）》请在冰点文库上搜索。
iSpin工具模型检测实验报告
基于iSpin工具的Needham-Schroeder共享密钥
协议的模型检测分析
1研究背景与验证环境介绍
1.1研究背景与NS协议介绍
1.1.1研究背景
密码协议是以密码学为基础的消息交换协议，其目的是在网络环境下提供各种安全问题，在密码协议分析中，它的条件定义为：
小系统：
参与协议运行的各主体都是唯一的（如一个发送者，一个响应者），作用也是唯一的，这些主体也都是诚实的，诚实即是它们严格按照协议规定并遵循自己的身份参与协议运行。
为了便于理解，引入强安全性破坏的概念，即一个诚实的主体相信在协议运行中用到的一个值是仅他和另外诚实主体之间的共享密码，但入侵者知道这个值。
目前，对于模型检测技术分析密码协议，有以下已被证明的理论成果：
只要对被分析的密码协议在小系统上进行强安全性破坏分析，就可以保证协议在任意系统上的安全性。
这个理论结果极大地促进了模型检测技术在密码协议分析领域的应用，使密码协议形式化分析方法的主流从逻辑方法转向了模型检测。
1.1.2NS协议介绍
NS（Needham-Schroeder）协议是使用密钥分发中心KDC实现认证的经典协议，每一个主体A都有一个公钥，另一个主体也可以从公钥服务器上得到A的公钥，协议中的任何主体都可以用A的公钥加密产生加密信息，但只有A才能解开加密后的信息，下面给出它的一个简化协议表示如下：
消息1A->B:
{A,Na}kb
消息2B->A:
{Na,Nb}ka
消息3A->B:
{Nb}kb
这里A是初始发送者，B是接受者，Na,Nb分别表示A和B的临时值
消息1表示A选择了一个自己的临时值Na，通过从服务器上得到B的公钥kb后，发送给B。
消息2表示B收到A的请求后，用自己的密钥解开消息，并从服务器上得到A的公钥，将自己的临时值和收到的A的临时值用A的公钥加密后返回给A。
消息3表示A似乎可以确信它是在于B通信，因为只有B才能解开消息1获得Na，接下来即可互相传递信息了。
1.2基于SPIN/Promela的验证环境
SPIN是最强大的模型检测工具之一，也是迄今为止唯一获得ACM软件系统奖的模型检测工具，本文实验所用为SPIN的（GUI）界面化工具iSPAN,Promela是SPIN的一种建模语言，在此不在赘述SPIN的背景与Promela语言的语法，主要介绍一下在windows下搭建环境的步骤：
1在官网下载cygwin软件（用于虚拟Linux环境），点击下载所有下载包，以免出错。
2启动Xserver服务器（用于生成iSpin界面）
3启动Ispin
2、NS协议的Promela模型
本协议属于两方（不含入侵者）参与的通信密码协议的SPIN模型，模型图如下：
根据NS协议的消息描述，建立三个进程，分别为发送者Alice，接受者Bob，入侵者Intruder，消息的枚举类型mtype={ok，err，msg1，msg2，msg3，keyA，keyB，keyI，agentA，agentB，agentI，nonceA，nonceB，nonceI};
msg1，msg2，msg3为上述的消息1，消息2，消息3，keyA,keyB，keyI为三者的公钥，agentA,agentB，agentI分别代表三个通信主体，nonceA,nonceB，nonceI则为三者的临时值。
定义的通信通道为会面点通道Channetwork=[0]of{mtype,mtype,mtype,mtype,mtype},即同步通信的通道，通道中有5条内容，其中通道中第一条为消息号，第二条为响应者，后面为所发的信息。
（1）主体A作为协议发起的初始者,它的第一个通信动作是发送信息1,通信对象可以是B也可以是I,这是两个并发的通信动作,不确定地选择一个通信对象执行"当他接到消息2后,A要检验消息2是否以他的公钥加密,并且检查消息中是否含有他发出的临时值nonceA，否则,A进程将处于阻塞状态，如果消息2中是他期望的值,就把消息3发给他的通信对象,并认为通信成功。
（2）主体B的通信过程和A类似其通信动作含有二次接收和一次发送.
（3）入侵者I不是固定地按照协议的步骤运行,目的是让SPIN发现协议中可能存在的攻击，我们描述入侵者I的动作是非常不确定的,让SPIN选择它们执行，比如I存在发送和接收两个不确定的动作,如果选择接收动作,则接下来是拦截或接收一条信息,并将拦截的信息存储起来或者不存储;如果信息是以NonceI加密,则I可以解开并可以获得nonceA或nonceB,定义两个布尔变量knows_nonceA和如knows_nonceB表示是否知道这些临时值,如果选择发送动作,则入侵者I又有两个可选择的动作:
重放一个拦截的数据包或者从已知的信息中构造一个
新的数据包发出去,I作为冒充者,可冒充A的身份,以I（A）参与协议运行。
3模型检测过程
3.1忽略强安全破坏性的验证
首先，为了验证协议的正确性，给出发送者和接受者的进程描述，以下为发送者进程和接受者进程的promela代码：
activeproctypeAlice（）{
mtypepkey,pnonce;
mtypekey,data1,data2,partnerA;
mtypestatusA;
Release:
do
:
:
if
:
:
partnerA=agentI;pkey=keyI;
:
:
partnerA=agentB;pkey=keyB;
fi;
network!
msg1,partnerA,pkey,agentA,nonceA;
network?
msg2,agentA,key,data1,data2;
if
:
:
（key==keyA）&&（data1==nonceA）->
pnonce=data2;
network!
msg3,partnerA,pkey,pnonce,0;
statusA=ok;
:
:
else->gotoRelease;
fi;
od;
}
activeproctypeBob（）{
mtypepkey,pnonce;
mtypekey,data1,data2;
mtypekey2,data3,data4;
mtypepartnerB;
mtypestatusB;
progress:
do
:
:
network?
msg1,agentB,key,data1,data2->
if
:
:
（key==keyB）&&（data1==agentA）->
partnerB=agentA;
network!
msg2,partnerB,keyA,data2,nonceB;
:
:
（key==keyB）&&（data1==agentI）->
partnerB=agentI;
network!
msg2,agentI,keyI,data2,nonceB;
fi;
network?
msg3,agentB,key2,data3,data4;
if
:
:
（key2==keyB）&&（data3==nonceB）->
statusB=ok;
else->gotoprogress;
fi;
od;
}
运行得到：
一直都会在Alice与Bob之间通信，收发信息。
根据本例，首先构造出线性时序逻辑LTL（lineartemporallogic）公式，协议应该满足：
ltle1{[]（（statusA==ok）&&（statusB==ok））-><>（（partnerA==agentB）||（partnerA==agentA））}
注：
（e1为公式名，公式含义为总有发送者和接受者验证通过后，最终发送者的对象必为接受者或者接受者的对象必为发送者）。
点击verification进入验证，将useclaim选项选上之后，输入公式验证，验证通过.
3.2强安全破坏性的验证
增加入侵者的进程Intruder，并根据协议增加两个ltl公式：
ltle2{[]（<>（statusA==ok）&&（partnerA==agentB））->（!
knows_nonceA）}
注：
公式含义为总有发送者验证通过且确定对象为B时就不会收到入侵者攻击
ltle3{[]<>（statusB==ok）&&（partnerB==agentA））->（!
knows_nonceB）}
注：
公式含义为总有接受者验证通过且确定对象为A时就不会收到入侵者攻击
以下为入侵者进程promela代码：
activeproctypeIntruder（）{
mtypemsg,recpt;
mtypekey,data1,data2;
mtypekey1,data3,data4;
boolknows_nonceA,knows_nonceB;
do
:
:
network?
msg,_,key,data1,data2->
if
:
:
key1=key;data3=data1;data4=data2;
:
:
skip;
fi;
if
:
:
（key==keyI）->
if
:
:
（data1==nonceA）||（data2==nonceA）
->knows_nonceA=true;
:
:
（data1==nonceB）||（data2==nonceB）
->knows_nonceB=true;
:
:
else->skip;
fi;
:
:
else->skip;
fi;
if
:
:
msg=msg1;
:
:
msg=msg2;
:
:
msg=msg3;
fi;
if
:
:
recpt=agentA;
:
:
recpt=agentB;
fi;
if
:
:
skip
:
:
if
:
:
data3=agentA;
:
:
data3=agentB;
:
:
data3=agentI;
:
:
knows_nonceA->data3=nonceA;
:
:
knows_nonceB->data3=nonceB;
:
:
data3=nonceI;
fi;
if
:
:
data4=nonceI;
:
:
knows_nonceA->data4=nonceA;
:
:
knows_nonceB->data4=nonceB;
fi;
if
:
:
key1=keyA;
:
:
key1=keyB;
fi;
fi;
network!
msg,recpt,key1,data3,data4;
od;
}
ltle2{[]（<>（statusA==ok）&&（partnerA==agentB））->（!
knows_nonceA）}
ltle3{[]<>（statusB==ok）&&（partnerB==agentA））->（!
knows_nonceB）}
输入公式e1验证得到如下的错误：
通过分析流程图，得到以下的攻击：
（1）.A->I:
{A,Na,}ki,
（2）.I（A）->B:
{A,Na}kb,
（3）.B->I（A）:
{Na,Nb}ka
（4）.I->A:
{Na,Nb}ka,
（5）.A->I:
{Nb}ki,
（6）.I（A）->B:
{Nb}kb,
输入公式e2，e3得到同样的错误。
升级会员 