1.基于非单调性动态认知逻辑的密码协议分析方法，其特征在于，包括如下步骤：S1、对给定的一个具有知识非单调性的密码协议，建立用于描述所述密码协议的具有非单调性用Forget扩展的动态认知逻辑语言 包括该语言的语法和相应的语义；

S2、基于所述动态认知逻辑语言 结合克里普克模型和寄存器模型来描述及分析所述密码协议中各主体拥有的知识和协议执行过程中其知识的变化，描述过程为协议分析过程，描述结束得出该密码协议是否具有安全性；

在客户端和服务器都有会话密钥的前提下，描述及分析所述密码协议详细为：S21、客户端生成文件以及主密钥；

S22、客户端对文件与主密钥联结加密并加入新鲜纳时后发送至服务器，新鲜纳时用于表示文件消息的新鲜性，所述新鲜纳时仅使用一次，当如果服务器再收到含有这个新鲜纳时的消息，服务器忽略这条消息；

S23、客户端用主密钥加密会话密钥并保留后删除文件、主密钥和会话密匙，服务器解密后得到文件和主密钥；

S31、服务器生成票据；

S32、服务器发送主密钥、用会话密钥加密的票据与文件至客户端，客户端收到后解密最终得到文件和票据；

服务器忽略攻击者发送的带有新鲜纳时的文件消息，带有新鲜纳时的消息在主体的信息集内更新，主体包括服务器和客户端；

S23中，攻击者获得客户端中主密钥加密会话密钥后的数据，即攻击者获取加密后的数据为寄存器的值，攻击者无法得到主密钥和会话密钥，攻击者无法计算得到文件消息和票据，此时协议为安全的，密钥受到保护；

S32中，攻击者窃听在服务器至客户端的发送数据路径，如果攻击者控制客户端，窃听到客户端知道的主密钥，攻击者解密获得会话密钥，从而获得票据和文件消息，票据和文件消息暴露，协议不安全；

基于非单调性动态认知逻辑语言分析密码协议时，所述逻辑语言 包括其语法和相应的语义；

其中逻辑语言 的语法具体如下：P为基本命题集或寄存器的集合，A为主体集，具有知识非单调性的密码协议的语言的语法归纳定义如下：

α::＝Sam|Forgetam|α∨α|α；α这里，p∈P，a∈A， p是命题也是寄存器，N是自然数，α是认知行为，Sam表示a发送消息m，Forgetam表示a忘记消息m，(α∨α)表示认知行为的选择，(α；α)表示认知行为的顺序执行；

所述消息m包括但不限于主体拥有的消息，还包括所述消息m是主体从信息集中的信息构造的消息，构造规则如下：所述构造规则中，分子表示构造条件，分母表示依据所述构造条件得到的结果；

基于非单调性动态认知逻辑语言分析密码协议时，所述逻辑语言 包括描述密码协议的语义；

语义包括认知行为的前提条件(Precondition)和后置条件(Postcondition)认知行为动作的前提条件如下：Pre(Sam)＝Ka(m＝N)Pre(Forgetam)＝Ka(m＝N)Pre(α；α′)＝Pre(α)∧[α]Pre(α′)Pre(α∨α′)＝Pre(α)∨Pre(α′)动作Sam，Forgetam要执行的前提是该主体先得有m，就是主体得知道m的值，Ka(m＝N)表示a知道m的值；

给定原子命题集或寄存器集P和主体集A，令模型 状态 h是 上的一个指派；

语言 的语义定义如下：

当且仅当

当且仅当p∈Pw；

当且仅当h(p)＝N；

当且仅当

当且仅当 或者

当且仅当对任一 如果 那么，对任一当且仅当对任一 如果 那么，对任一当且仅当如果 和对所有的 和那么

当且仅当对所有的 和 如果 和那么(m＝N)∈Pw′并且当且仅当对所有的 和 如果和 那么 并且

|α∨α′|＝|α|∨|α′|。

2.根据权利要求1所述的基于非单调性动态认知逻辑的密码协议分析方法，其特征在于，所述描述的过程中，用表示动态认知逻辑语言的模型——克里普克模型来描述所述密码协议中各参与方的知识。

3.根据权利要求2所述的基于非单调性动态认知逻辑的密码协议分析方法，其特征在于，所述Forget扩展动态认知逻辑语言，所述主体包括协议中各参与方，所述Forget行为是用于表示主体忘记已经拥有的部分知识。

4.根据权利要求1所述的基于非单调性动态认知逻辑的密码协议分析方法，其特征在于，所述寄存器模型如下：

一个寄存器模型 中，(W,R)是一个多主体的 框架，V是一个值函数，它指派给每一个世界的值是一个元组(Pw,fw)；

在世界w为真的基本命题集；

fw是在Q上的一个函数，指派每一个q∈Q( 变量的全局集)是一个元组(I,J,X)，其

0 1 2

中：I，J∈Z，I≤J， (这里Z表示整数集合)表示以下意思：fw(q)通过fw (q)，fw (q)，fw(q)来表示q在w的取值范围；所述范围有一个下界I，上界J，一个排除值的集合X，即：fw(q)＝(I,J,X)表示在世界w，q的可能值是I和J之间的数除了X，即：