安全协议可视化建模和验证方法的分析与设计①

付 杰， 闫振林， 张玉民， 息明东， 李 升

(佳木斯大学现代教育技术中心，黑龙江 佳木斯 154007)

0 引言

安全协议是一种通信协议，它通过密码技术实现通信过程中的密钥分发及身份认证，从而保证网络通信的安全.

本文将基于模型检测技术，采用转换法将安全协议的UML模型转换为形式化的PROMELA模型，讨论UML模型向PROMELA语义转换的方法，定义转换规则.设计基于以上规则的从UML向PROMELA语义的转换系统，来实现UML的自动形式化验证，证明该方法的可行性.

1 模型检测工具SPIN

SPIN对协议的形式化分析具体步骤如下:

(1)根据入侵分析对协议的运行模式进行分类，写出PROMELA模型规范;

(2)写出需要验证的系统属性要求，用LTL(Linear Temporal Logic)方程描述;

(3)利用SPIN对系统属性进行验证;

(4)若属性为假，SPIN会生成一个.tail文件，利用该文件进行引导仿真，跟踪协议运行过程，找出攻击序列;

(5)否则系统属性为真，验证结束.

2 建模语言PROMELA

PROMELA(Protocol Meta Language)是用来对有限状态系统进行建模的形式化描述语言.类似于C程序语言，允许动态创建并行的进程，并且可以在进程之间通过消息通道进行同步(使用rendezvous port)和异步(使用缓冲)通信.

3 安全协议可视化建模及对应PROMELA语义转换

3.1 Needham －Schroeder公钥协议

为使描述更加清晰，我们采用消息序列的方式来表示协议:

(1)A→S:A，B

(2)S→A:{Pkb，B}pks－1

(3)A→B:{Na，A}pkb

(4)B→S:B，A

(5)S→B:{Pka，A}pks－1

(6)B→A:{Na，Nb}pka

(7)A→B:{Nb}pkb

3.2 安全协议的UML模型

(1)安全协议的类图

类图是对类及其之间关系的可视化表示，它是从一定抽象的视角来描述系统的静态结构.安全协议中，一个主体可以看成一个类的实例对象.主体有属性和操作，在UML中定义其为Message类，没有方法，只有属性，本文以Needham－Schroeder公钥协议为例，如图1所示.

从图1中可知，需要建立的类包括主体类principal和消息类Message.

图1 Needham－Schroeder公钥协议类图

(2)安全协议的序列图

序列图的建立方法是把发起者排放在图的最左边，而其它响应者按交互的先后顺序排放在发起者的右边，主体对象按照安全协议中消息的先后次序进行交互.当执行一个用例行为时，序列图中每条消息对应一个类操作或状态机中引起转换的触发事件.如图2

图2 Needham－Schroeder协议序列图

(3)安全协议的状态图

状态图体现了一个状态机，它由状态、事件、转换和活动组成.因为状态图能够完整地描述一个主体的动态行为，所以对UML模型进行检测的主要对象是状态图.

1)发起者状态图.

2)响应者状态图

3)入侵者状态图

4 UML模型的PROMELA语义转换

安全协议UML模型在使用SPIN进行分析验证之前，需要对UML子集中的图在语义上进行形式化处理，下面将定义安全协议UML子集中的图在语义上向PROMELA语义转换的规则.

4.1 类图的PROMELA语义

规则 A1:主体 Principal类转换为同名的PROMELA结构体类型，其中参数转换成相应结构体参数;

规则 A2:消息 Message类转换为同名的PROMELA结构体类型;

规则A3:proctype initiator(){}

规则A4:每个属性转换为对应proctype的变量;

规则A5:忽略类的关联和关联的角色名;

图3 NS公钥协议发起者状态图

4.2 序列图的PROMELA语义

规则B1:类图名与它所对应的顺序图中主体名相同;

规则B2:忽略序列图中消息的编号;

规则B4:忽略序列图中的注释连接NoteLink、注释Note、元素的大小和位置等非形式化内容.

4.3 状态图的PROMELA语义

(1)发起者和响应者状态图的PROMELA语义

规则C1:类图名称应与它所对应的状态图名称相同;

规则C2:状态图中初始状态所指的状态作为相应主体进程Proctype的初始状态;

规则C3:忽略每一个状态迁移的名称;

规则C4:终止状态标签为End;

规则C5:忽略注释Note，状态图个元素位置大小等非形式化内容;

对照组病患吞咽不适例数与观察组相比,P大于0.05,无明显差异;对照组病患的切口黏连例数与观察组相比,P大于0.05,无明显差异;对照组病患的伤口疼痛例数与观察组相比,P大于0.05,无明显差异;但是对照组总并发症发生率比观察组高,P小于0.05,差异具有统计学意义。具体如下表所示。

(2)入侵者状态图的PROMELA语义

入侵者有三个状态:发送状态(send)，接收状态 (receive)，和创建消息状态 (createMessage)，创建消息的具体动作由Promela语言的inline函数编写.

图4 转换工具的结构

5 转换工具的分析与设计

转换工具的分析与设计考虑到以下三个问题:

(1)UML模型作为输入;

(2)根据本节的转换规则进行转换;

(3)PROMELA模型作为输出.

对于第一个问题，如果直接采用UML模型作为输入，将会产生难以读取信息的困难.但在研究过程中，发现很多建模软件都提供了将UML模型导出为XMI文件的功能.XMI是基于XML的元数据交换.它通过标准化的XML文档格式为UML元模型定义了一种基于XML的数据交换格式，同时也定义了一个从UML到XML的映射，可用于把UML模型派生成XML.

对于第二个问题，由于UML对应的XMI文件是有着固定结构的，因此，在XMI中，UML中的类、类的属性、属性节点、UML类的方法由一系列节点列表构成.

对于第三个问题，转换后的PROMELA模型代码以文本文件保存，SPIN即可调用.

转换工具的结构如图4所示:

6 UML可视化模型实例的形式化转换

本文根据前面定义的转换规则，以Gavin lowe小系统模型和Dolev－yao模型为基础，以状态图为例，对协议进行转换，来验证转换规则及转换工具的正确性.

NS协议状态图的转换

根据状态图中的每个状态，在相应主体中定义对应的状态标签;

本程序在SPIN中模拟运行通过.

7 总结

安全协议的分析与验证经过多年的研究和实践已越来越趋向于形式化方法，但形式化方法存在建模困难，难以使用等缺点.统一建模语言UML能为设计者提供可视化的直观模型，但是，其图形化的符号缺乏精确的语义，不能提供严格的自动分析和测试功能，给系统分析带来了难度，难以保证系统建模的正确性.形式化的方法和UML可视化模型相结合可以互补，从而发挥各自的优势，降低了设计难度，提高了分析验证的效率和准确度.

[1]冯登国，范红.安全协议形式化分析理论与方法研究综述[J].中国科学院研究生报学报，2003，20(4):389 －406.

[2]Object Management Group，OMG Unified Modeling Language Specification[J].version1.5，2003.

[3]韦银星，张申生，曹健.UML类图的形式化及分析[J].计算机工程与应用，2002，10:5 －7.