基于Maria的TMN协议的LPetri网模型检测

郝颖,封雪，于颖

（1．营口理工学院电气工程系，营口115000；2.鞍山供电公司，鞍山 114000）

基于Maria的TMN协议的LPetri网模型检测

郝颖1,封雪1，于颖2

（1．营口理工学院电气工程系，营口115000；2.鞍山供电公司，鞍山 114000）

运用形式化方法分析密码协议的安全性已成为网络信息安全领域的研究热点之一。提出一种新的扩展Petri网——LPetri网。并且利用LPetri网对TMN密码协议进行建模，采用模型检测工具Maria分析LPetri网模型的可达性，说明利用LPetri网对安全协议建模的有效性。

TMN协议；Maria；LPetri网；模型检测

0 引言

随着Internet技术的迅速发展，网络上的信息安全问题日益突出。以密码学为基础的密码协议的安全性分析是网络安全领域的一个难题。采用形式化方法对密码协议进行分析和检测是该领域的研究热点之一[1]。目前，密码协议的形式化分析方法包括：逻辑方法[2]、模型检测方法、定理证明方法和基于Petri网的方法等[3]。

1 背景知识介绍

1.1 Petri网及相关概念

Petri网自1962年提出以来，经过四十余年的发展己在许多领域得到广泛应用。Petri网有严格的模型语义和直观的图形化语言，是一种描述和验证密码协议的有效手段[5]。在协议工程领域，应用最广泛的方法是利用颜色Petri网对网络协议进行建模并且分析[6，7]。

LPetri网的不同之处在于它是针对密码协议所提出的，将协议运行中传递的所有信息归为一个集合，库所也统一分为主体类型与信息类型，能够直观地表示参与协议运行的各个主体处于何种状态、协议运行中传递了哪些信息，并且需要定义的数据类型较少，结构比较简单。

首先给出 Petri网的基本概念[8，9]。

定义 1（Petri网）PN=（P，T，F，M0）是一个 Petri网，其中：

P={p1，p2，…，pn}是有限库所集，T={t1，t2，…，tn}是有限变迁集；

F⊆（P×T）∪（T×P）是有向弧集，代表结点之间流关系；

M0:P → {0，1，2，…}是初始标识，并且：P∩T＝Φ，P∪T≠Φ。

定义2（点火规则）

（1）变迁t∈T称作在状态M下是使能的，当且仅当Vp∈·t，M（P）≥l记作 M[t>；

（2）若M0[t1>M1[t2>···Mn-1[tn>Mn（其中Mi∈R（M0），ti∈T，i=1，2，···，n），则称δ=t1t2···tn，为 PN 的一个可触发变迁序列，记做 M0[δ>Mn。

定义3（可达图）

一个Petri网的可达图是一个有向图G=（M，F，R），其中:m∈M表示一类可达的标识；f∈F表示从一类可达标识到另一类可达标识的有向弧；R是一个转换关系，R:F→M×M。

1.2 Maria的介绍

Maria[4]（Modular Reachability Analyzer）模块可达性分析器是由赫尔辛基大学计算机理论实验室进行的一个项目。其重点是应用和对软件业的形式化分析方法的使用。Maria能对分布式系统模型进行可达性分析、检测安全性和活性。要检测的模型可用手动建模或利用其他的形式化语言来自动建模。

1.3 TMN密码协议

TMN[10，11，12]密码协议是一种用于数字移动通信系统的密钥分配协议。协议的主要目的是使网络上的两个节点在服务器的帮助下获得一个用于今后互相传输秘密信息的共享密钥。

协议的原始版本如下：

Ml:A->S：B，Es（Na）

M2:S->B：A

M3:B->S：A，Es（Nb）

M4:S->A：B，ENa（Nb）

其中A代表初始者，B代表响应者，S代表服务器，s是服务器S的公开密钥。Na，Nb分别是A、B发布的具有新鲜性的随机数，Ex（Y）表示用X加密Y。

TMN协议的内容描述如下：

M1：A向S发送标识B和用s加密的随机数Na；M2：S向B发送A的标识通知B，A要与它进行通信；M3：B向S发送标识A及用s加密的随机数Nb；M4：S将B及用Na加密的信息Nb发送给A，A解密后得到Nb，从而达到共享密钥的目的。

2 LPetri网及其Maria语言描述

LPetri网（Label Petri Net，LPN）针对密码协议的特点将库所与标识分为两种类型：一种是协议运行主体的集合；另一种是协议运行中传递信息的集合。

2.1 LPetri网的基本概念

定义 4（LPetri网）LPN=（P，T，F，M0，L）称作 LPetri网，其中：

（1）P∩T＝Φ，P∪T≠Φ；

（2）P=Ps∪Pm，其中Ps是表示参与协议运行的主体状态类型的库所，Pm表示协议运行中所传递的信息类型的库所；

（3）EXP：F → L，其中 L=LsULm，其中 Ls表示主体状态标识，Lm表示传递信息内容的标识；

（4）M0:P → {L∪Φ}。

定义5（点火规则）

（1）变迁t∈T称作在状态M下是使能的，当且仅当 Vp∈·t，M（P）>≥L 记作 M[t>；

（2）若M0[t1>M1[t2>···Mn-1[tn>Mn（其中Mi∈R（M0），ti∈T，i=1，2，···，n），则称δ=t1t2···tn，为 PN 的一个可触发变迁序列，记做 M[δ>Mn；

（3）L（Fin）=L（Fout），Fin⊆ T×P，Fout⊆（P×T）。

2.2 Maria描述Petri网模型的基本语法

Maria语言描述LPetri网的基本语法[4]。

（1）库所定义

place name typedefinition[':'marking list]

name表示库所的名称，typedefinition是库所的类型，marking list表示库所中的初始标识。

（2）变迁定义

trans[’:’]name IN trans_places

OUT trans_places

name表示变迁的名字，In trans_plac

es与Out trans_places分别表示变迁的所有输入和输出库所集。

3 TMN协议LPetri网模型分析

3.1 TMN密码协议的LPetri网模型

TMN密码协议的原始协议的LPetri网模型如图1所示。

根据LPetri网的定义将库所分为两种类型：主体状态类型Ps和消息类型Pm。库所集合Ps={p1，p2，p3，p5，p6，p8}，其余库所为 Pm 类型。变迁 t1，t2，t3，t4分别表示TMN原始协议的四条消息的传递，t5表示主体A从等待状态转换为结束状态。

TMN协议的原始协议的LPetri网模型用Maria语言描述如下：

TMNT协议原始协议的Maria语言描述

typedef enum{As，Aw，Ae}A;

typedef enum{Ss，Sw，Se}S;

typedef enum{Bs，Bw，Be}B;

typedef enum{A，B，S，I}subject;

typedef enum{msg1，msg2，msg3，msg4}msg;

place p1 A:As; place p2 A;

place p3 A; place p4 msg;

place p5 S; place p6 S;

place p7 msg; place p8 B;

place p9 msg; place p10 msg;

trans t1 in{place p1:As;}

out{place p2:Aw;place p4:msg1;};

trans t2 in{place p4:msg1;}

out{place p5:Sw;place p7:msg2;};

trans t3 in{place p7:msg2;}

图1 TMN协议的原始协议的LPetri网模型

out{place p8:Be;place p9:msg3;};

trans t4 in{place p5:Sw;place 9:msg3;}

out{place p6:Se;place p10:msg4;};

trans t5

in{place p2:Aw;place p10:msg4;}

out{place p3:Ae;};

deadlock true;

前三条条语句分别表示A，S，B的开始、等待和结束状态。第四条语句表示参与协议运行的主体。

该描述经过Maria工具分析后得到的模型的可达状态为M0（As，Φ，Φ，Φ，Φ，Φ，Φ，Φ，Φ，Φ）àM1（Φ，Aw，Φ，msg1，Φ，Φ，Φ，Φ，Φ，Φ）àM2（Φ，Aw，Φ，Φ，Sw，Φ，msg2，Φ，Φ，Φ）àM3（Φ，Aw，Φ，Φ，Sw，Φ，Φ，Be，msg3，Φ）àM4（Φ，Aw，Φ，Φ，Φ，Se，Φ，Be，Φ，msg4）àM5（Φ，Φ，Ae，Φ，Φ，Se，Φ，Be，Φ，Φ），标记中的 As，Aw，Ae，分别表示代表A的开始，等待，和结束状态。其它关于B和S的状态与A类似。结束状态中只有p3，p6，p8中包含标记，分别表示A，B，S的结束状态。该模型的变迁发生序列为 t1，t2，t3，t4，t5，由此可见 TMN 协议在没有攻击的情况下可以正常运行。

3.2 TMN协议的攻击检测

张玉清等人将TMN密码协议的攻击分为10类19种攻击[11]，本文选择其中一种攻击模型[13]来证明使用LPetri网建模，并应用Maria检测TMN协议中存在的攻击的可行性。结合LPetri网描述密码协议的特点，将这种攻击表示如下:

1.1 A→I（S）：B，EsNA

2.1 I→S：I，EsNA

2.2 S→I:I

2.3 I→S：I，Esx3

1.4 I（S）→A：B，ENAx3

2.4 S→I：I，ENAx3

该攻击所表达的含义是在第一次运行中，入侵者I冒充服务器S，截获了A发送服务器S的消息，获得了用S的公钥加密的A产生的具有新鲜性的随机数NA，之后入侵者I冒充A，发送截获的消息与自己的标识给服务器。然后I冒充B发送自己的随机数x3给服务器S。最后I冒充S发消息给A，并且发送了用NA加密的自己的随机数，使A认为它是与B共享了密钥x3。

使用LPetri网对该攻击模型建模的过程中共定义了 19 个库所，其中 p1，p2，p3，p7，p8，p9，p11，p12，p14，p19为主体状态类型，其余为信息类型。变迁所代表的含义分别为：

t1：I截获了A发送给S的信息；

t2：I冒充服务器发送B的标识和自己的随机数x1给A；

t3：状态转换；

t4：I发送标识I与x2给S；

t5：S发送主体标识 I；

t6：I发送消息给S，包括I的标识和用S的公钥加密的x3；

t7：S发送消息给I，包括I的标识与用x2加密的x3；

x2是I截获的消息，即为A产生的随机数NA，x1，x3均为入侵者产生的随机数。

TMN协议的一种攻击模型的LPetri网模型如图2。

该模型中包含的数据类型如下：

TMN协议攻击模型的LPetri网的数据类型typedef enum{As，Aw，Ae}A;typedef enum{Ss，Sw，Se}S;

typedef enum{Is，Iw，Ie}I;//入侵者状态

typedef enum{A，B，S，I}subject;

typedef enum

{EsNA，ENAx1，Esx2，Esx3，Ex2x3，ENAx3}encrypt;

//加密信息

typedef enum{msg1，msg2，msg3，msg4}

msg;//消息

以msg1为例说明消息的类型

typedef struct

{subject B;encrypt

EsNA;}msg1;

该描述用Maria分析后得到的可达图如图3。由可达图可知包含以下几种攻击路径：t1，t4，t5，t6，t7，t2，t3，t8；t1，t4，t5，t6，t7，t2，t8，t3；t1，t4，t5，t6，t7，t8，t2，t3，它们所表达的含义均为I截获A发送给S的信息，I冒充A发信息给S，I截获S发送给B的消息，I冒充B发送自己的密钥给S，拦截S发送给A的消息，I冒充S发送消息给A，接下来A与I分别由等待状态转换为结束状态。由此可见使用LPetri网对协议建模并且使用Maria分析该模型这种方法是可行的。

图3 TMN协议攻击模型的可达图

4 结语

图2 TMN协议一种攻击模型的LPetri网

本文首先提出了一种描述密码协议的扩展Petri网，LPetri网。LPetri网将密码协议运行中传递的内容分为主体状态与信息类型。与着色Petri网相比，LPe⁃tri网需要定义的数据类型较少，并且能够直观地表示参与协议运行的各个主体处于何种状态、协议运行中传递的信息。接着用LPetri网对TMN密码协议的原始协议和一种攻击模型建模。最后用模型检测工具Maria对这两种模型进行了分析，证明了LPetri网建模并分析密码协议的有效性。

下一步的工作就是要继续扩展LPetri网模型，将协议运行中的加解密信息以函数的形式加到弧的标记中去，并且实现LPetri网模型到Maria语言的自动转化。

[1]梅翀，孟传良，张成宇.安全协议扩展Petri网模型及检测[J].信息安全，2007，23:59-61.

[2]Burrows M，Abadi M，Needham R.A logic of authentication[A].Proceedings of the Royal Socity of London，1989，A（426）:233-271.

[3]张广胜，吴哲辉，逢玉叶.基于时间Petri网的密码协议分析[J].系统仿真学报，2003，15，增刊：11-16.

[4]Marko Mäkelä.Maria:Modular Reach-ability Analyser for Algebraic System Nets.http://www.tcs.hut.fi/Personnel/marko.html

[5]林松，李舟军.基于Petri网的双重数字签名的描述与验证[J].系统仿真学报，2008，20（9）:2498-2501.

[6]彭磊，吴磊，毕亚雷，曾家智.基于着色解释Petri网的网络协议建模及协同仿真方法[J].计算机集成制造系统，2009，15（1）:82-88.

[7]刘文琦，顾宏.基于分层时间有色Petri网的支付协议公平性分析[J].电子与信息学报，2009，3（6）:1445-1449.

[8]周建涛，叶新铭.Petri网的可达图与可达树的比较[J].内蒙古大学学报：自然科学版，2000，33（1）：117-120.

[9]袁志祥，蒋昌俊.基于Petri网的安全电子交易协议描述与分析[J].计算机工程，2003，29（10）：56-59.

[10]Tatebayashi M，Matsuzaki N.Newman D B.Key Distribution Protocol for DigiTal Mobile Communication System.In Advance in Crytology-CRYPTO'89，Volume 435 of LNCS，Springer-Verlag，1989

[11]刘秀英，张玉清，杨波，邢戈.TMN协议的攻击及其分类研究[J].计算机工程，2004，30（16）：47-50.

[12]张卉，李续武，赵媛莉，校云超.改进型有色Petri网的安全协议分析[J].计算机工程与科学，2013，35（70）:60-63.

[13]董卫.基于Petri网的密码协议分析方法[D].山东科技大学，2005.

Abstract：Using formal method to analyze the cipher protocol has been one of the hot spots in the domain of network information security.Proposes a new extended Petri Net named LPetri Net.Establishes the TMN cipher protocol model with LPetri Net and then uses the model checking tool Maria to analyze the reachability of the LPetri Net.The efficiency of using LPetri Net to model security protocol has been proved.

Keywords：TMN Protocol；Maria；LPetri Nets；Model Checking

Checking LPetri Net Model of the TMN Protocol Based on Maria

HAO Ying1,FENG Xue1，YU Ying2

(1.Yingkou Institute of Technology,Yingkou 115000;2.Anshan Power Supply Company,Anshan 114001)

1007-1423（2017）26-0013-05

10.3969/j.issn.1007-1423.2017.26.003

郝颖（1984-），女，辽宁鞍山人，硕士，讲师，研究方向为形式化验证、云计算

封雪（1984-），女，辽宁营口人，硕士，讲师，研究方向为计算几何、机器人路径规划

于颖（1981-），女，山东日照人，中级，硕士，研究方向为计算机技术

2017-06-02

2017-09-05