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

郝穎,封雪，于穎

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

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

郝穎1,封雪1，于穎2

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

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

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

0 引言

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

1 背景知識介紹

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

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

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

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

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

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

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

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

定義2（點火規(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 的一個可觸發(fā)變遷序列，記做 M0[δ>Mn。

定義3（可達圖）

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

1.2 Maria的介紹

Maria[4]（Modular Reachability Analyzer）模塊可達性分析器是由赫爾辛基大學(xué)計算機理論實驗室進行的一個項目。其重點是應(yīng)用和對軟件業(yè)的形式化分析方法的使用。Maria能對分布式系統(tǒng)模型進行可達性分析、檢測安全性和活性。要檢測的模型可用手動建模或利用其他的形式化語言來自動建模。

1.3 TMN密碼協(xié)議

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

協(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ā)布的具有新鮮性的隨機數(shù)，Ex（Y）表示用X加密Y。

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

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

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

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

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é)議運行的主體狀態(tài)類型的庫所，Pm表示協(xié)議運行中所傳遞的信息類型的庫所；

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

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

定義5（點火規(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 的一個可觸發(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)識。

（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é)議運行的主體。

該描述經(jīng)過Maria工具分析后得到的模型的可達狀態(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é)議在沒有攻擊的情況下可以正常運行。

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

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

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冒充服務(wù)器S，截獲了A發(fā)送服務(wù)器S的消息，獲得了用S的公鑰加密的A產(chǎn)生的具有新鮮性的隨機數(shù)NA，之后入侵者I冒充A，發(fā)送截獲的消息與自己的標(biāo)識給服務(wù)器。然后I冒充B發(fā)送自己的隨機數(shù)x3給服務(wù)器S。最后I冒充S發(fā)消息給A，并且發(fā)送了用NA加密的自己的隨機數(shù)，使A認為它是與B共享了密鑰x3。

使用LPetri網(wǎng)對該攻擊模型建模的過程中共定義了 19 個庫所，其中 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ù)x1給A；

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

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

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

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

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

x2是I截獲的消息，即為A產(chǎn)生的隨機數(shù)NA，x1，x3均為入侵者產(chǎn)生的隨機數(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分析后得到的可達圖如圖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發(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)對協(xié)議建模并且使用Maria分析該模型這種方法是可行的。

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

4 結(jié)語

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

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

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

[1]梅翀，孟傳良，張成宇.安全協(xié)議擴展Petri網(wǎng)模型及檢測[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網(wǎng)的密碼協(xié)議分析[J].系統(tǒng)仿真學(xué)報，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)的雙重數(shù)字簽名的描述與驗證[J].系統(tǒng)仿真學(xué)報，2008，20（9）:2498-2501.

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

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

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

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

[12]張卉，李續(xù)武，趙媛莉，校云超.改進型有色Petri網(wǎng)的安全協(xié)議分析[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-），女，遼寧鞍山人，碩士，講師，研究方向為形式化驗證、云計算

封雪（1984-），女，遼寧營口人，碩士，講師，研究方向為計算幾何、機器人路徑規(guī)劃

于穎（1981-），女，山東日照人，中級，碩士，研究方向為計算機技術(shù)

2017-06-02

2017-09-05