基于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