基于形式化模型的电力信息审计系统安全协议验证方法

苏霞， 张晶晶， 孙静

(1.国网河北省电力有限公司， 河北,石家庄 050021；2.国网河北服务中心， 河北,石家庄 050000)

0 引言

网络技术的迅猛发展促使移动支付以及社交网络各种新型技术相继出现，有效地促进了信息安全领域的认证技术以及授权技术的发展[1],其中电力信息审计系统安全协议和安全协议验证得到社会学者的广泛关注。由于安全协议具有属性多样性和逻辑结构复杂等特点[2]，导致安全验证协议模型的建立以及协议精准描述变得更加困难,因此如何准确、快速地实现安全协议的认证是目前安全领域的一个重要课题。 最近几年，国内外相关专家针对该方面的内容进行了大量的研究，例如文献[3]基于Event-B方法，利用VCC等工具建模设计电力信息审计系统安全形式，完成安全协议验证;文献[4]通过形式化验证方法对半量子协议进行建模和验证。以上两种方法虽然在现阶段取得了较为满意的研究成果，但是由于未能使用形式化模型，导致安全协议验证效率降低，安全协议验证错误率和开销增加。因此，本文在电力信息审计系统中引入了一种形式化的安全协议验证方法。

1 方法

1.1 形式化建模

面向电力信息审计系统的安全认证协议不仅可以有效地确保用户信息的私密性[5]，同时也能够为用户提供私密的通信机制,其中通信机制主要通过包含属性的凭证方式实现。

现阶段针对认证协议的形式化工作只能利用粗粒度验证，对电力信息审计系统而言，现有的形式化验证工作无法满足其需求。针对以上问题，本文采用形式化的方法，对各实体间的通讯通道和各主体进行了研究,同时对各个实体的属性、功能以及交互进程进行了全面的分析。

电力信息审计系统的形式化建模是在标识信息的基础上，用户主要通过细粒度的方式对消息进行签名，在整个操作的过程中包含3个不同的主体[6]，各个主体主要具有以下几方面的功能。

(1) 属性证书发布机构

该机构负责发布具有权威效应的资格证书，其具体工作内容包括属性证书的编制与发行。

(2) 证明者

即认证系统的证明者，主要是由主机平台和可信平台模型两个部分组成。

(3) 验证者

在认证系统中，服务提供者其实是一个认证系统的验证者，它可以为证明者提供属性验证服务，使用一个经过权威认证的公钥，或由该证明者提供的属性证书来完成验证工作。

在面向可选择性披露的可信属性认证系统(SDABCS)中包含一组属性用户，其中属性用户的属性签名是通过属性密钥获取的，且属性签名可以采用不同的实体进行验证[7-8]。

SDABCS系统支持如下的安全特征：在已知用户属性签名密钥以及属性的情况下，认证机构需要验证后来使用者上传的属性签名，但不能决定待定密钥，因此无法判定该签名来源。

通常情况下，形式化模型可以表示成六元组的形式，即：

SDABCS-M=TE,UTF,C,PAR,ACT,ALG

(1)

式中，SDABCS-M代表模型的名称,TE代表模型中全部可信实体集合[9],UTF代表模型全部不可信实体集合,C代表模型中全部通道集合,PAR代表模型中全部参数集合,ACT代表模型中全部实体行为集合,ALG代表模型中全部函数集合。

利用图1给出属性对应的认证框架。

图1 基于属性的认证框架

C的具体表达形式为

C=ISDABCS-M，OSDABCS-M,IOSDABCS-M

(2)

式中，ISDABCS-M代表系统TSA中全部输入通道集合,OSDABCS-M代表系统TSA中全部输出通道集合,IOSDABCS-M代表系统TSA中全部输入输出通道集合。

PAR对应的表达形式为

PAR=V,CH,ATTR,OTHP

(3)

式中，V代表系统中全部变量,CH代表全部通道的集合,ATTR代表实体所包含的属性集合,OTHP代表其他参数集。

ACT的表达形式为

ACT=Input,Output,Inside-action

(4)

式中，Input代表系统中全部输入行为集合,Output代表系统中全部输出行为集合,Inside-action代表系统中所有内部行为集合[10-11]。

ALG集合主要通过以下算法组成：

ALG=Setup,AKeyGen,ASetup,AArep,AAproof

(5)

式中，Setup代表用于形成公共参数以及属性权威机构对应的密钥对,AKeyGen表示密钥属性,ASetup代表使用者的属性签名,AArep代表请求和发放证书的过程，具体的表达式为

AArep=ASign,VerSign,VerBSign

(6)

式中，ASign代表系统通过属性密钥进行划分,VerSign代表授权部门对证书的签名进行确认,VerBSign代表授权部门确认使用者的代理签名[12]。

式(5)中的AAproof代表用户为验证者提供属性证明，并且验证者对该属性进行验证的过程，即：

AAproof=Divatt,Divask,ZeroP,Asign,VerZeroP

(7)

式中，Divatt代表用户属性划分结果,Divask代表使用者通过属性密钥完成属性签名,ZeroP代表由鉴定人提供的属性签名,VerZeroP代表由鉴定人向用户提供的属性证明。

SDABCS系统中包含的主要安全特性如下。

(1) 准确性

当系统中参数准确时，采用签名算法完成签名验证。

(2) 属性隐私性

在属性证书初步显示阶段，即使系统中的验证者和各个权威机构存在关联也无法查看对应的属性信息。

(3) 不可伪造性

系统中任何人无法对签名数据进行伪造。

(4) 匿名性

当系统中的用户进行属性证书颁发时，主要使用盲化技术完成权威机构签名，有效保证不同机构之间不存在任何关联且无法查看自身签名，实现匿名保护。

不同的协议在不同的安全模型下均存在不同的隐患，为了全面系统的安全性和隐私性，不仅需要获取攻击者所具备的能力，同时还需要满足系统中的安全特征需求。

当用户和属性权威机构两者均处于诚实状态下时，需要提供符合系统需求的输出和输入，确保系统能够获取任何期望的正确执行结果。

系统中存在的诚实实体希望能够在与系统交互的过程中获取更多有价值的信息，并且结合权威模型的定义完成属性隐私性和签名匿名性的设定。

本文建立了一个形式化的电力信息审计系统。在此基础上，采用SPIN和AVISPA对电力信息审计系统安全协议进行改进。

1.2 电力信息审计系统安全协议验证

查找电力信息审计系统安全协议中存在的漏洞的操作流程如图2所示。

首先，为了检验电力信息审计系统的安全协议，必须对协议进行行为抽象以及形式化分析，基于时态逻辑属性，通过转换器结合安全协议形式化的语言描述各个主体的行为。

安全协议验证模型的建模过程除了诚实主体建模之外，更加主要的是攻击者建模，因此使用Doleo—Yao模型构建无法破解协议的密码算法，其中在知识以及能力方面，攻击者和合法主体两者相当，它能够截获网络中所传送的全部消息，通过Doleo—Yao模型能够查看全部的消息修改和发送。当确定攻击者模型后，设参与协议主体的合法者和攻击者为不同的安全属性，可以采用模式检测技术分析不同主体的网络协议的安全属性，具体操作步骤如下。

图2 电力信息审计系统安全协议验证流程图

(1) 结合攻击者模型以及协议运行模式，通过Promela进行建模。

(2) 通过LTL方程对需要验证的系统性质进行描述。

(3) 将每个实体转化为模型需要的源代码，加入指导器模拟的错误跟踪过程，也就是确定了状态和状态转移集合,在建立状态转移的过程中[13]下发pan命令，执行验证代码，经过权威机构双向校验和协议初始形式化分析后，能够确定安全协议的功能以及相关属性。过程如下：

① 通过SPIN对系统的性质进行验证,对应获取电力信息审计系统中攻击者相关信息以及系统存在的漏洞;

② 假设性质是假的，通过SPIN形成trail文件能够准确查找安全协议中存在的攻击行为，同时准确反映攻击者的进攻路径；

③ 假设性质是真的，则结束验证。

通过上述操作，有效实现电力信息审计系统安全协议验证。

2 仿真实验

为了验证所提基于形式化模型的电力信息审计系统安全协议验证方法的综合有效性，仿真测试环境详见表1。

(1) 安全协议验证效率

图3显示了3种不同安全协议有效性的比较结果。

分析图3中的实验数据可知，虽然3种方法的安全协议验证效率均在90%以上，但是由于所提方法在实际研究的过程中采用形式化模型对电力信息审计系统进行形式化研究，同时有效地改进了安全协议，促使整体的安全协议验证效率明显高于文献[3]方法和文献[4]方法。

表1 实验环境

图3 不同方法的安全协议验证效率对比结果

(2) 安全协议验证错误率

分别采用3种方法对相同的电力信息审计系统进行安全协议验证，本试验以安全协议验证错误率为指标，具体实验测试结果如表2所示。

表2 不同方法的安全协议验证错误率

分析表2可知，所提方法的安全协议验证错误率最低,文献[3]方法的安全协议验证错误率次之,文献[4]方法的安全协议验证错误率最低。由于所提方法采用形式模型对电力信息审计系统进行分析以及形式化研究，有效地简化了操作流程，同时促使所提方法的安全协议验证错误率得到有效降低。

(3) 安全协议验证开销

对电力信息审计系统进行安全协议验证的过程中会产生一定的费用，但是由于不同方法的验证过程不同导致开销也不同。表3为3种方法的安全协议验证开销结果。

表3 不同方法的安全协议验证开销对比

由表3可知，所提方法的安全协议验证开销明显低于文献[3]方法和文献[4]方法。这是因为所提方法中引用了形式化模型，通过形式化模型对电力信息审计系统进行形式化分析，同时进一步对安全协议进行完善，有效地避免了安全协议中存在的漏洞导致开销增加。

3 总结

本文针对传统方法存在的问题，结合形式化模型提出一种基于形式化模型的电力信息审计系统安全协议验证方法。仿真实验结果表明，所提方法能够有效地提升安全协议验证效率，降低安全协议验证错误率和安全协议验证开销。由于条件所限，本文尚存缺陷，未来将对以下几方面进行改进：

(1) 如何更加全面以及准确地对攻击者进行行为建模，确保攻击者的行为更加接近真实情况，大幅度增加验证结果的准确性;

(2) 引入无线传感器网络的研究，后续将花费大量的时间和精力对该方面的内容进行研究。