付 杰， 閆振林， 張玉民， 息明東， 李 升

(佳木斯大學(xué)現(xiàn)代教育技術(shù)中心，黑龍江 佳木斯 154007)

0 引言

安全協(xié)議是一種通信協(xié)議，它通過(guò)密碼技術(shù)實(shí)現(xiàn)通信過(guò)程中的密鑰分發(fā)及身份認(rèn)證，從而保證網(wǎng)絡(luò)通信的安全.

本文將基于模型檢測(cè)技術(shù)，采用轉(zhuǎn)換法將安全協(xié)議的UML模型轉(zhuǎn)換為形式化的PROMELA模型，討論UML模型向PROMELA語(yǔ)義轉(zhuǎn)換的方法，定義轉(zhuǎn)換規(guī)則.設(shè)計(jì)基于以上規(guī)則的從UML向PROMELA語(yǔ)義的轉(zhuǎn)換系統(tǒng)，來(lái)實(shí)現(xiàn)UML的自動(dòng)形式化驗(yàn)證，證明該方法的可行性.

1 模型檢測(cè)工具SPIN

SPIN對(duì)協(xié)議的形式化分析具體步驟如下:

(1)根據(jù)入侵分析對(duì)協(xié)議的運(yùn)行模式進(jìn)行分類(lèi)，寫(xiě)出PROMELA模型規(guī)范;

(2)寫(xiě)出需要驗(yàn)證的系統(tǒng)屬性要求，用LTL(Linear Temporal Logic)方程描述;

(3)利用SPIN對(duì)系統(tǒng)屬性進(jìn)行驗(yàn)證;

(4)若屬性為假，SPIN會(huì)生成一個(gè).tail文件，利用該文件進(jìn)行引導(dǎo)仿真，跟蹤協(xié)議運(yùn)行過(guò)程，找出攻擊序列;

(5)否則系統(tǒng)屬性為真，驗(yàn)證結(jié)束.

2 建模語(yǔ)言PROMELA

PROMELA(Protocol Meta Language)是用來(lái)對(duì)有限狀態(tài)系統(tǒng)進(jìn)行建模的形式化描述語(yǔ)言.類(lèi)似于C程序語(yǔ)言，允許動(dòng)態(tài)創(chuàng)建并行的進(jìn)程，并且可以在進(jìn)程之間通過(guò)消息通道進(jìn)行同步(使用rendezvous port)和異步(使用緩沖)通信.

3 安全協(xié)議可視化建模及對(duì)應(yīng)PROMELA語(yǔ)義轉(zhuǎn)換

3.1 Needham －Schroeder公鑰協(xié)議

為使描述更加清晰，我們采用消息序列的方式來(lái)表示協(xié)議:

(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 安全協(xié)議的UML模型

(1)安全協(xié)議的類(lèi)圖

類(lèi)圖是對(duì)類(lèi)及其之間關(guān)系的可視化表示，它是從一定抽象的視角來(lái)描述系統(tǒng)的靜態(tài)結(jié)構(gòu).安全協(xié)議中，一個(gè)主體可以看成一個(gè)類(lèi)的實(shí)例對(duì)象.主體有屬性和操作，在UML中定義其為Message類(lèi)，沒(méi)有方法，只有屬性，本文以Needham－Schroeder公鑰協(xié)議為例，如圖1所示.

從圖1中可知，需要建立的類(lèi)包括主體類(lèi)principal和消息類(lèi)Message.

圖1 Needham－Schroeder公鑰協(xié)議類(lèi)圖

(2)安全協(xié)議的序列圖

序列圖的建立方法是把發(fā)起者排放在圖的最左邊，而其它響應(yīng)者按交互的先后順序排放在發(fā)起者的右邊，主體對(duì)象按照安全協(xié)議中消息的先后次序進(jìn)行交互.當(dāng)執(zhí)行一個(gè)用例行為時(shí)，序列圖中每條消息對(duì)應(yīng)一個(gè)類(lèi)操作或狀態(tài)機(jī)中引起轉(zhuǎn)換的觸發(fā)事件.如圖2

圖2 Needham－Schroeder協(xié)議序列圖

(3)安全協(xié)議的狀態(tài)圖

狀態(tài)圖體現(xiàn)了一個(gè)狀態(tài)機(jī)，它由狀態(tài)、事件、轉(zhuǎn)換和活動(dòng)組成.因?yàn)闋顟B(tài)圖能夠完整地描述一個(gè)主體的動(dòng)態(tài)行為，所以對(duì)UML模型進(jìn)行檢測(cè)的主要對(duì)象是狀態(tài)圖.

1)發(fā)起者狀態(tài)圖.

2)響應(yīng)者狀態(tài)圖

3)入侵者狀態(tài)圖

4 UML模型的PROMELA語(yǔ)義轉(zhuǎn)換

安全協(xié)議UML模型在使用SPIN進(jìn)行分析驗(yàn)證之前，需要對(duì)UML子集中的圖在語(yǔ)義上進(jìn)行形式化處理，下面將定義安全協(xié)議UML子集中的圖在語(yǔ)義上向PROMELA語(yǔ)義轉(zhuǎn)換的規(guī)則.

4.1 類(lèi)圖的PROMELA語(yǔ)義

規(guī)則 A1:主體 Principal類(lèi)轉(zhuǎn)換為同名的PROMELA結(jié)構(gòu)體類(lèi)型，其中參數(shù)轉(zhuǎn)換成相應(yīng)結(jié)構(gòu)體參數(shù);

規(guī)則 A2:消息 Message類(lèi)轉(zhuǎn)換為同名的PROMELA結(jié)構(gòu)體類(lèi)型;

規(guī)則A3:proctype initiator(){}

規(guī)則A4:每個(gè)屬性轉(zhuǎn)換為對(duì)應(yīng)proctype的變量;

規(guī)則A5:忽略類(lèi)的關(guān)聯(lián)和關(guān)聯(lián)的角色名;

圖3 NS公鑰協(xié)議發(fā)起者狀態(tài)圖

4.2 序列圖的PROMELA語(yǔ)義

規(guī)則B1:類(lèi)圖名與它所對(duì)應(yīng)的順序圖中主體名相同;

規(guī)則B2:忽略序列圖中消息的編號(hào);

規(guī)則B4:忽略序列圖中的注釋連接NoteLink、注釋Note、元素的大小和位置等非形式化內(nèi)容.

4.3 狀態(tài)圖的PROMELA語(yǔ)義

(1)發(fā)起者和響應(yīng)者狀態(tài)圖的PROMELA語(yǔ)義

規(guī)則C1:類(lèi)圖名稱(chēng)應(yīng)與它所對(duì)應(yīng)的狀態(tài)圖名稱(chēng)相同;

規(guī)則C2:狀態(tài)圖中初始狀態(tài)所指的狀態(tài)作為相應(yīng)主體進(jìn)程Proctype的初始狀態(tài);

規(guī)則C3:忽略每一個(gè)狀態(tài)遷移的名稱(chēng);

規(guī)則C4:終止?fàn)顟B(tài)標(biāo)簽為End;

規(guī)則C5:忽略注釋Note，狀態(tài)圖個(gè)元素位置大小等非形式化內(nèi)容;

對(duì)照組病患吞咽不適例數(shù)與觀察組相比,P大于0.05,無(wú)明顯差異;對(duì)照組病患的切口黏連例數(shù)與觀察組相比,P大于0.05,無(wú)明顯差異;對(duì)照組病患的傷口疼痛例數(shù)與觀察組相比,P大于0.05,無(wú)明顯差異;但是對(duì)照組總并發(fā)癥發(fā)生率比觀察組高,P小于0.05,差異具有統(tǒng)計(jì)學(xué)意義。具體如下表所示。

(2)入侵者狀態(tài)圖的PROMELA語(yǔ)義

入侵者有三個(gè)狀態(tài):發(fā)送狀態(tài)(send)，接收狀態(tài) (receive)，和創(chuàng)建消息狀態(tài) (createMessage)，創(chuàng)建消息的具體動(dòng)作由Promela語(yǔ)言的inline函數(shù)編寫(xiě).

圖4 轉(zhuǎn)換工具的結(jié)構(gòu)

5 轉(zhuǎn)換工具的分析與設(shè)計(jì)

轉(zhuǎn)換工具的分析與設(shè)計(jì)考慮到以下三個(gè)問(wèn)題:

(1)UML模型作為輸入;

(2)根據(jù)本節(jié)的轉(zhuǎn)換規(guī)則進(jìn)行轉(zhuǎn)換;

(3)PROMELA模型作為輸出.

對(duì)于第一個(gè)問(wèn)題，如果直接采用UML模型作為輸入，將會(huì)產(chǎn)生難以讀取信息的困難.但在研究過(guò)程中，發(fā)現(xiàn)很多建模軟件都提供了將UML模型導(dǎo)出為XMI文件的功能.XMI是基于XML的元數(shù)據(jù)交換.它通過(guò)標(biāo)準(zhǔn)化的XML文檔格式為UML元模型定義了一種基于XML的數(shù)據(jù)交換格式，同時(shí)也定義了一個(gè)從UML到XML的映射，可用于把UML模型派生成XML.

對(duì)于第二個(gè)問(wèn)題，由于UML對(duì)應(yīng)的XMI文件是有著固定結(jié)構(gòu)的，因此，在XMI中，UML中的類(lèi)、類(lèi)的屬性、屬性節(jié)點(diǎn)、UML類(lèi)的方法由一系列節(jié)點(diǎn)列表構(gòu)成.

對(duì)于第三個(gè)問(wèn)題，轉(zhuǎn)換后的PROMELA模型代碼以文本文件保存，SPIN即可調(diào)用.

轉(zhuǎn)換工具的結(jié)構(gòu)如圖4所示:

6 UML可視化模型實(shí)例的形式化轉(zhuǎn)換

本文根據(jù)前面定義的轉(zhuǎn)換規(guī)則，以Gavin lowe小系統(tǒng)模型和Dolev－yao模型為基礎(chǔ)，以狀態(tài)圖為例，對(duì)協(xié)議進(jìn)行轉(zhuǎn)換，來(lái)驗(yàn)證轉(zhuǎn)換規(guī)則及轉(zhuǎn)換工具的正確性.

NS協(xié)議狀態(tài)圖的轉(zhuǎn)換

根據(jù)狀態(tài)圖中的每個(gè)狀態(tài)，在相應(yīng)主體中定義對(duì)應(yīng)的狀態(tài)標(biāo)簽;

本程序在SPIN中模擬運(yùn)行通過(guò).

7 總結(jié)

安全協(xié)議的分析與驗(yàn)證經(jīng)過(guò)多年的研究和實(shí)踐已越來(lái)越趨向于形式化方法，但形式化方法存在建模困難，難以使用等缺點(diǎn).統(tǒng)一建模語(yǔ)言UML能為設(shè)計(jì)者提供可視化的直觀模型，但是，其圖形化的符號(hào)缺乏精確的語(yǔ)義，不能提供嚴(yán)格的自動(dòng)分析和測(cè)試功能，給系統(tǒng)分析帶來(lái)了難度，難以保證系統(tǒng)建模的正確性.形式化的方法和UML可視化模型相結(jié)合可以互補(bǔ)，從而發(fā)揮各自的優(yōu)勢(shì)，降低了設(shè)計(jì)難度，提高了分析驗(yàn)證的效率和準(zhǔn)確度.

[1]馮登國(guó)，范紅.安全協(xié)議形式化分析理論與方法研究綜述[J].中國(guó)科學(xué)院研究生報(bào)學(xué)報(bào)，2003，20(4):389 －406.

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

[3]韋銀星，張申生，曹健.UML類(lèi)圖的形式化及分析[J].計(jì)算機(jī)工程與應(yīng)用，2002，10:5 －7.