安全協(xié)議可視化建模和驗證方法的分析與設計①

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

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

0 引言

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

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

1 模型檢測工具SPIN

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

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

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

(3)利用SPIN對系統(tǒng)屬性進行驗證;

(4)若屬性為假，SPIN會生成一個.tail文件，利用該文件進行引導仿真，跟蹤協(xié)議運行過程，找出攻擊序列;

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

2 建模語言PROMELA

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

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

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

為使描述更加清晰，我們采用消息序列的方式來表示協(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é)議的類圖

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

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

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

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

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

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

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

狀態(tài)圖體現(xiàn)了一個狀態(tài)機，它由狀態(tài)、事件、轉(zhuǎn)換和活動組成.因為狀態(tài)圖能夠完整地描述一個主體的動態(tài)行為，所以對UML模型進行檢測的主要對象是狀態(tài)圖.

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

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

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

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

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

4.1 類圖的PROMELA語義

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

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

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

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

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

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

4.2 序列圖的PROMELA語義

規(guī)則B1:類圖名與它所對應的順序圖中主體名相同;

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

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

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

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

規(guī)則C1:類圖名稱應與它所對應的狀態(tài)圖名稱相同;

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

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

規(guī)則C4:終止狀態(tài)標簽為End;

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

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

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

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

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

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

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

(1)UML模型作為輸入;

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

(3)PROMELA模型作為輸出.

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

對于第二個問題，由于UML對應的XMI文件是有著固定結(jié)構(gòu)的，因此，在XMI中，UML中的類、類的屬性、屬性節(jié)點、UML類的方法由一系列節(jié)點列表構(gòu)成.

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

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

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

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

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

根據(jù)狀態(tài)圖中的每個狀態(tài)，在相應主體中定義對應的狀態(tài)標簽;

本程序在SPIN中模擬運行通過.

7 總結(jié)

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

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

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

[3]韋銀星，張申生，曹健.UML類圖的形式化及分析[J].計算機工程與應用，2002，10:5 －7.