郝穎,封雪，于穎

（1．營(yíng)口理工學(xué)院電氣工程系，營(yíng)口115000；2.鞍山供電公司，鞍山 114000）

基于Maria的TMN協(xié)議的LPetri網(wǎng)模型檢測(cè)

郝穎1,封雪1，于穎2

（1．營(yíng)口理工學(xué)院電氣工程系，營(yíng)口115000；2.鞍山供電公司，鞍山 114000）

運(yùn)用形式化方法分析密碼協(xié)議的安全性已成為網(wǎng)絡(luò)信息安全領(lǐng)域的研究熱點(diǎn)之一。提出一種新的擴(kuò)展Petri網(wǎng)——LPetri網(wǎng)。并且利用LPetri網(wǎng)對(duì)TMN密碼協(xié)議進(jìn)行建模，采用模型檢測(cè)工具M(jìn)aria分析LPetri網(wǎng)模型的可達(dá)性，說明利用LPetri網(wǎng)對(duì)安全協(xié)議建模的有效性。

TMN協(xié)議；Maria；LPetri網(wǎng)；模型檢測(cè)

0 引言

隨著Internet技術(shù)的迅速發(fā)展，網(wǎng)絡(luò)上的信息安全問題日益突出。以密碼學(xué)為基礎(chǔ)的密碼協(xié)議的安全性分析是網(wǎng)絡(luò)安全領(lǐng)域的一個(gè)難題。采用形式化方法對(duì)密碼協(xié)議進(jìn)行分析和檢測(cè)是該領(lǐng)域的研究熱點(diǎn)之一[1]。目前，密碼協(xié)議的形式化分析方法包括：邏輯方法[2]、模型檢測(cè)方法、定理證明方法和基于Petri網(wǎng)的方法等[3]。

1 背景知識(shí)介紹

1.1 Petri網(wǎng)及相關(guān)概念

Petri網(wǎng)自1962年提出以來，經(jīng)過四十余年的發(fā)展己在許多領(lǐng)域得到廣泛應(yīng)用。Petri網(wǎng)有嚴(yán)格的模型語義和直觀的圖形化語言，是一種描述和驗(yàn)證密碼協(xié)議的有效手段[5]。在協(xié)議工程領(lǐng)域，應(yīng)用最廣泛的方法是利用顏色Petri網(wǎng)對(duì)網(wǎng)絡(luò)協(xié)議進(jìn)行建模并且分析[6，7]。

LPetri網(wǎng)的不同之處在于它是針對(duì)密碼協(xié)議所提出的，將協(xié)議運(yùn)行中傳遞的所有信息歸為一個(gè)集合，庫所也統(tǒng)一分為主體類型與信息類型，能夠直觀地表示參與協(xié)議運(yùn)行的各個(gè)主體處于何種狀態(tài)、協(xié)議運(yùn)行中傳遞了哪些信息，并且需要定義的數(shù)據(jù)類型較少，結(jié)構(gòu)比較簡(jiǎn)單。

首先給出 Petri網(wǎng)的基本概念[8，9]。

定義 1（Petri網(wǎng)）PN=（P，T，F(xiàn)，M0）是一個(gè) Petri網(wǎng)，其中：

P={p1，p2，…，pn}是有限庫所集，T={t1，t2，…，tn}是有限變遷集；

F?（P×T）∪（T×P）是有向弧集，代表結(jié)點(diǎn)之間流關(guān)系；

M0:P → {0，1，2，…}是初始標(biāo)識(shí)，并且：P∩T＝Φ，P∪T≠Φ。

定義2（點(diǎn)火規(guī)則）

（1）變遷t∈T稱作在狀態(tài)M下是使能的，當(dāng)且僅當(dāng)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 的一個(gè)可觸發(fā)變遷序列，記做 M0[δ>Mn。

定義3（可達(dá)圖）

一個(gè)Petri網(wǎng)的可達(dá)圖是一個(gè)有向圖G=（M，F(xiàn)，R），其中:m∈M表示一類可達(dá)的標(biāo)識(shí)；f∈F表示從一類可達(dá)標(biāo)識(shí)到另一類可達(dá)標(biāo)識(shí)的有向?。籖是一個(gè)轉(zhuǎn)換關(guān)系，R:F→M×M。

1.2 Maria的介紹

Maria[4]（Modular Reachability Analyzer）模塊可達(dá)性分析器是由赫爾辛基大學(xué)計(jì)算機(jī)理論實(shí)驗(yàn)室進(jìn)行的一個(gè)項(xiàng)目。其重點(diǎn)是應(yīng)用和對(duì)軟件業(yè)的形式化分析方法的使用。Maria能對(duì)分布式系統(tǒng)模型進(jìn)行可達(dá)性分析、檢測(cè)安全性和活性。要檢測(cè)的模型可用手動(dòng)建?；蚶闷渌男问交Z言來自動(dòng)建模。

1.3 TMN密碼協(xié)議

TMN[10，11，12]密碼協(xié)議是一種用于數(shù)字移動(dòng)通信系統(tǒng)的密鑰分配協(xié)議。協(xié)議的主要目的是使網(wǎng)絡(luò)上的兩個(gè)節(jié)點(diǎn)在服務(wù)器的幫助下獲得一個(gè)用于今后互相傳輸秘密信息的共享密鑰。

協(xié)議的原始版本如下：

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

M2:S->B：A

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

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

其中A代表初始者，B代表響應(yīng)者，S代表服務(wù)器，s是服務(wù)器S的公開密鑰。Na，Nb分別是A、B發(fā)布的具有新鮮性的隨機(jī)數(shù)，Ex（Y）表示用X加密Y。

TMN協(xié)議的內(nèi)容描述如下：

M1：A向S發(fā)送標(biāo)識(shí)B和用s加密的隨機(jī)數(shù)Na；M2：S向B發(fā)送A的標(biāo)識(shí)通知B，A要與它進(jìn)行通信；M3：B向S發(fā)送標(biāo)識(shí)A及用s加密的隨機(jī)數(shù)Nb；M4：S將B及用Na加密的信息Nb發(fā)送給A，A解密后得到Nb，從而達(dá)到共享密鑰的目的。

2 LPetri網(wǎng)及其Maria語言描述

LPetri網(wǎng)（Label Petri Net，LPN）針對(duì)密碼協(xié)議的特點(diǎn)將庫所與標(biāo)識(shí)分為兩種類型：一種是協(xié)議運(yùn)行主體的集合；另一種是協(xié)議運(yùn)行中傳遞信息的集合。

2.1 LPetri網(wǎng)的基本概念

定義 4（LPetri網(wǎng)）LPN=（P，T，F(xiàn)，M0，L）稱作 LPetri網(wǎng)，其中：

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

（2）P=Ps∪Pm，其中Ps是表示參與協(xié)議運(yùn)行的主體狀態(tài)類型的庫所，Pm表示協(xié)議運(yùn)行中所傳遞的信息類型的庫所；

（3）EXP：F → L，其中 L=LsULm，其中 Ls表示主體狀態(tài)標(biāo)識(shí)，Lm表示傳遞信息內(nèi)容的標(biāo)識(shí)；

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

定義5（點(diǎn)火規(guī)則）

（1）變遷t∈T稱作在狀態(tài)M下是使能的，當(dāng)且僅當(dāng) 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 的一個(gè)可觸發(fā)變遷序列，記做 M[δ>Mn；

（3）L（Fin）=L（Fout），F(xiàn)in? T×P，F(xiàn)out?（P×T）。

2.2 Maria描述Petri網(wǎng)模型的基本語法

Maria語言描述LPetri網(wǎng)的基本語法[4]。

（1）庫所定義

place name typedefinition[':'marking list]

name表示庫所的名稱，typedefinition是庫所的類型，marking list表示庫所中的初始標(biāo)識(shí)。

（2）變遷定義

trans[’:’]name IN trans_places

OUT trans_places

name表示變遷的名字，In trans_plac

es與Out trans_places分別表示變遷的所有輸入和輸出庫所集。

3 TMN協(xié)議LPetri網(wǎng)模型分析

3.1 TMN密碼協(xié)議的LPetri網(wǎng)模型

TMN密碼協(xié)議的原始協(xié)議的LPetri網(wǎng)模型如圖1所示。

根據(jù)LPetri網(wǎng)的定義將庫所分為兩種類型：主體狀態(tài)類型Ps和消息類型Pm。庫所集合Ps={p1，p2，p3，p5，p6，p8}，其余庫所為 Pm 類型。變遷 t1，t2，t3，t4分別表示TMN原始協(xié)議的四條消息的傳遞，t5表示主體A從等待狀態(tài)轉(zhuǎn)換為結(jié)束狀態(tài)。

TMN協(xié)議的原始協(xié)議的LPetri網(wǎng)模型用Maria語言描述如下：

TMNT協(xié)議原始協(xié)議的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協(xié)議的原始協(xié)議的LPetri網(wǎng)模型

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的開始、等待和結(jié)束狀態(tài)。第四條語句表示參與協(xié)議運(yùn)行的主體。

該描述經(jīng)過Maria工具分析后得到的模型的可達(dá)狀態(tài)為M0（As，Φ，Φ，Φ，Φ，Φ，Φ，Φ，Φ，Φ）àM1（Φ，Aw，Φ，msg1，Φ，Φ，Φ，Φ，Φ，Φ）àM2（Φ，Aw，Φ，Φ，Sw，Φ，msg2，Φ，Φ，Φ）àM3（Φ，Aw，Φ，Φ，Sw，Φ，Φ，Be，msg3，Φ）àM4（Φ，Aw，Φ，Φ，Φ，Se，Φ，Be，Φ，msg4）àM5（Φ，Φ，Ae，Φ，Φ，Se，Φ，Be，Φ，Φ），標(biāo)記中的 As，Aw，Ae，分別表示代表A的開始，等待，和結(jié)束狀態(tài)。其它關(guān)于B和S的狀態(tài)與A類似。結(jié)束狀態(tài)中只有p3，p6，p8中包含標(biāo)記，分別表示A，B，S的結(jié)束狀態(tài)。該模型的變遷發(fā)生序列為 t1，t2，t3，t4，t5，由此可見 TMN 協(xié)議在沒有攻擊的情況下可以正常運(yùn)行。

3.2 TMN協(xié)議的攻擊檢測(cè)

張玉清等人將TMN密碼協(xié)議的攻擊分為10類19種攻擊[11]，本文選擇其中一種攻擊模型[13]來證明使用LPetri網(wǎng)建模，并應(yīng)用Maria檢測(cè)TMN協(xié)議中存在的攻擊的可行性。結(jié)合LPetri網(wǎng)描述密碼協(xié)議的特點(diǎn)，將這種攻擊表示如下:

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

該攻擊所表達(dá)的含義是在第一次運(yùn)行中，入侵者I冒充服務(wù)器S，截獲了A發(fā)送服務(wù)器S的消息，獲得了用S的公鑰加密的A產(chǎn)生的具有新鮮性的隨機(jī)數(shù)NA，之后入侵者I冒充A，發(fā)送截獲的消息與自己的標(biāo)識(shí)給服務(wù)器。然后I冒充B發(fā)送自己的隨機(jī)數(shù)x3給服務(wù)器S。最后I冒充S發(fā)消息給A，并且發(fā)送了用NA加密的自己的隨機(jī)數(shù)，使A認(rèn)為它是與B共享了密鑰x3。

使用LPetri網(wǎng)對(duì)該攻擊模型建模的過程中共定義了 19 個(gè)庫所，其中 p1，p2，p3，p7，p8，p9，p11，p12，p14，p19為主體狀態(tài)類型，其余為信息類型。變遷所代表的含義分別為：

t1：I截獲了A發(fā)送給S的信息；

t2：I冒充服務(wù)器發(fā)送B的標(biāo)識(shí)和自己的隨機(jī)數(shù)x1給A；

t3：狀態(tài)轉(zhuǎn)換；

t4：I發(fā)送標(biāo)識(shí)I與x2給S；

t5：S發(fā)送主體標(biāo)識(shí) I；

t6：I發(fā)送消息給S，包括I的標(biāo)識(shí)和用S的公鑰加密的x3；

t7：S發(fā)送消息給I，包括I的標(biāo)識(shí)與用x2加密的x3；

x2是I截獲的消息，即為A產(chǎn)生的隨機(jī)數(shù)NA，x1，x3均為入侵者產(chǎn)生的隨機(jī)數(shù)。

TMN協(xié)議的一種攻擊模型的LPetri網(wǎng)模型如圖2。

該模型中包含的數(shù)據(jù)類型如下：

TMN協(xié)議攻擊模型的LPetri網(wǎng)的數(shù)據(jù)類型typedef enum{As，Aw，Ae}A;typedef enum{Ss，Sw，Se}S;

typedef enum{Is，Iw，Ie}I;//入侵者狀態(tà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分析后得到的可達(dá)圖如圖3。由可達(dá)圖可知包含以下幾種攻擊路徑：t1，t4，t5，t6，t7，t2，t3，t8；t1，t4，t5，t6，t7，t2，t8，t3；t1，t4，t5，t6，t7，t8，t2，t3，它們所表達(dá)的含義均為I截獲A發(fā)送給S的信息，I冒充A發(fā)信息給S，I截獲S發(fā)送給B的消息，I冒充B發(fā)送自己的密鑰給S，攔截S發(fā)送給A的消息，I冒充S發(fā)送消息給A，接下來A與I分別由等待狀態(tài)轉(zhuǎn)換為結(jié)束狀態(tài)。由此可見使用LPetri網(wǎng)對(duì)協(xié)議建模并且使用Maria分析該模型這種方法是可行的。

圖3 TMN協(xié)議攻擊模型的可達(dá)圖

4 結(jié)語

圖2 TMN協(xié)議一種攻擊模型的LPetri網(wǎng)

本文首先提出了一種描述密碼協(xié)議的擴(kuò)展Petri網(wǎng)，LPetri網(wǎng)。LPetri網(wǎng)將密碼協(xié)議運(yùn)行中傳遞的內(nèi)容分為主體狀態(tài)與信息類型。與著色Petri網(wǎng)相比，LPe?tri網(wǎng)需要定義的數(shù)據(jù)類型較少，并且能夠直觀地表示參與協(xié)議運(yùn)行的各個(gè)主體處于何種狀態(tài)、協(xié)議運(yùn)行中傳遞的信息。接著用LPetri網(wǎng)對(duì)TMN密碼協(xié)議的原始協(xié)議和一種攻擊模型建模。最后用模型檢測(cè)工具M(jìn)aria對(duì)這兩種模型進(jìn)行了分析，證明了LPetri網(wǎng)建模并分析密碼協(xié)議的有效性。

下一步的工作就是要繼續(xù)擴(kuò)展LPetri網(wǎng)模型，將協(xié)議運(yùn)行中的加解密信息以函數(shù)的形式加到弧的標(biāo)記中去，并且實(shí)現(xiàn)LPetri網(wǎng)模型到Maria語言的自動(dòng)轉(zhuǎn)化。

[1]梅翀，孟傳良，張成宇.安全協(xié)議擴(kuò)展Petri網(wǎng)模型及檢測(cè)[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]張廣勝，吳哲輝，逢玉葉.基于時(shí)間Petri網(wǎng)的密碼協(xié)議分析[J].系統(tǒng)仿真學(xué)報(bào)，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網(wǎng)的雙重?cái)?shù)字簽名的描述與驗(yàn)證[J].系統(tǒng)仿真學(xué)報(bào)，2008，20（9）:2498-2501.

[6]彭磊，吳磊，畢亞雷，曾家智.基于著色解釋Petri網(wǎng)的網(wǎng)絡(luò)協(xié)議建模及協(xié)同仿真方法[J].計(jì)算機(jī)集成制造系統(tǒng)，2009，15（1）:82-88.

[7]劉文琦，顧宏.基于分層時(shí)間有色Petri網(wǎng)的支付協(xié)議公平性分析[J].電子與信息學(xué)報(bào)，2009，3（6）:1445-1449.

[8]周建濤，葉新銘.Petri網(wǎng)的可達(dá)圖與可達(dá)樹的比較[J].內(nèi)蒙古大學(xué)學(xué)報(bào)：自然科學(xué)版，2000，33（1）：117-120.

[9]袁志祥，蔣昌俊.基于Petri網(wǎng)的安全電子交易協(xié)議描述與分析[J].計(jì)算機(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協(xié)議的攻擊及其分類研究[J].計(jì)算機(jī)工程，2004，30（16）：47-50.

[12]張卉，李續(xù)武，趙媛莉，校云超.改進(jìn)型有色Petri網(wǎng)的安全協(xié)議分析[J].計(jì)算機(jī)工程與科學(xué)，2013，35（70）:60-63.

[13]董衛(wèi).基于Petri網(wǎng)的密碼協(xié)議分析方法[D].山東科技大學(xué)，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-），女，遼寧鞍山人，碩士，講師，研究方向?yàn)樾问交?yàn)證、云計(jì)算

封雪（1984-），女，遼寧營(yíng)口人，碩士，講師，研究方向?yàn)橛?jì)算幾何、機(jī)器人路徑規(guī)劃

于穎（1981-），女，山東日照人，中級(jí)，碩士，研究方向?yàn)橛?jì)算機(jī)技術(shù)

2017-06-02

2017-09-05