| 主权项 |
一种智能电网分布式网络协议安全性检测方法，其特征在于该方法所包含的步骤为：步骤1)对分布式网络协议建立基于时间自动机的状态迁移系统及检测将分布式网络协议主体分为客户端、服务器端以及设备端三部分，为智能电网分布式网络协议的客户端、服务器端、设备端分别建立基于时间自动机的状态迁移系统；所述时间自动机是在有限状态自动机的基础上添加了时钟约束，可以看作实时系统进程的抽象模型，被广泛应用于实时系统的建模和分析；所述状态迁移系统是将系统抽象为一个有穷状态模型，用时间自动机表示系统的迁移结构；步骤11)对分布式网络协议客户端建立状态迁移系统步骤111)创建分布式网络协议客户端的基本状态，包括初始空闲状态、等待状态、发送状态、等待应答状态、终止状态、结束状态和有限个非初始空闲状态；在初始空闲状态设立一个状态标志位，记为A，设立一个时钟变量Ta，设立一个传输次数计数器Ca；步骤112)协议开始执行，客户端由初始空闲状态进入等待状态；步骤113)客户端在等待状态时收到开始传输数据的信号时，从等待状态进入发送状态，此时，当传输次数计数器Ca的数值大于用户指定的最大允许传输次数Cmax，则进入终止状态，转到第二步进行新一轮的执行；否则，继续执行下一步；步骤114)客户端在发送数据后进入等待应答状态，此时，当时钟变量Ta的数值超过用户指定的最大允许响应时间Tmax，则进入终止状态，转到第二步进行新一轮的执行；否则，当接收到“否”的响应消息，表明服务器端没有接收到传输的数据，则传输次数计数器Ca的数值加1，转到第三步继续执行，当接受到“是”的响应消息，服务器端确认接收到传输的数据，继续执行下一步；步骤115)协议执行完毕，客户端再次进入初始空闲状态；步骤12)对分布式网络协议服务器端建立状态迁移系统步骤121)创建分布式网络协议服务器端的基本状态，包括初始空闲状态、等待状态、接收状态、确认状态和有限个非初始空闲状态，在服务器端的初始空闲状态设立一个状态标志位，记为B；步骤122)协议开始执行，接收方由初始空闲状态进入等待状态，等待接收客户端的消息；步骤123)服务器端接收到客户端发出的消息，由等待状态进入接收状态，确认是否为所需传输的消息，如果是，发送确认消息Y，如果不是，发送确认消息N；步骤124)协议执行完毕，服务器端再次进入初始空闲状态；步骤13)对分布式网络协议设备端建立状态迁移系统，设备端在接收到相应的消息后，根据消息选择服务进行操作，将设备的接收消息及响应过程通过状态迁移系统表示出来；步骤14)对分布式网络协议性质进行检测步骤141)对建立的分布式网络协议模型的正确性进行检测，检测所建立的分布式网络协议模型是否正确，是否满足协议本身的相关性质，具体操作过程为：首先通过时序逻辑公式表示进行模型正确性检测时需要满足的性质，然后对建立模型的状态空间进行搜索，检测是否满足性质；步骤142)对建立的分布式网络协议模型安全性进行检测，具体操作过程为：首先通过时序逻辑公式表示进行安全性检测时需要满足的相关性质，然后对建立模型的状态空间进行搜索，检测分布式网络协议在没有任何攻击者时是否满足安全性相关的性质，如果满足相关的性质，则进入步骤2)；如果存在不符合的情况，则进入步骤3)；步骤2)建立攻击者模型并对分布式网络协议的安全性进行检测对分布式网络协议的安全性进行检测，具体操作过程为：首先通过时序逻辑公式表示进行协议安全性检测时需要满足的相关性质，然后建立攻击者模型,对攻击者模型的状态空间进行搜索，检测协议在有攻击者时是否满足安全性相关的性质；如果满足相关的性质，则表明分布式网络协议安全，将结果返回给用户；如果存在反例，则继续进行步骤3)；所述攻击者模型是模拟外界对系统进行攻击的模型；步骤3)建立检测者模型并对分布式网络协议安全性进行改进当在步骤1)或者步骤2)中发现不满足安全性的实例，通过模型检验工具的反跟踪特性设计出检测者模型，检测者模型指出发生不符合安全性质的情况，用户根据不符合安全性质的情况对分布式网络协议的漏洞及威胁进行改进，再一次重复前步骤1)和步骤2的检测过程，直到分布式网络协议安全性符合要求。所述检测者模型是通过模型检验工具对发现的不安全实例进行反向推导，利用工具分析问题产生的可能情况来建立模型。 |
