馬振立

摘要：隨著電子商務(wù)的不斷發(fā)展，消費者對于在線支付系統(tǒng)的服務(wù)質(zhì)量要求越來越高，支付系統(tǒng)不僅要高速完成每筆交易，更要保證支付過程的安全性。在線支付是電子商務(wù)的核心功能模塊，而這個核心模塊又由各個地理位置上分離的各個子模塊組成，在該文中會對四個主要子模塊進行建模，分析各模塊之間的依賴關(guān)系及超時的擴散效應(yīng)，通過UPPAAL對建模后的系統(tǒng)進行模型檢測。經(jīng)實驗驗證，所設(shè)計的支付系統(tǒng)模型可以在產(chǎn)生某個模塊的超時后依然能滿足安全性。

關(guān)鍵詞：電子商務(wù)；支付系統(tǒng)；UPPAAL；模型檢測

中圖分類號：TP393 文獻標識碼：A 文章編號：1009-3044（2014）34-8341-02

在線支付是電子商務(wù)[1]的一個核心模塊，是比傳統(tǒng)的先下支付更快捷，更方便的一種交易方式。在線支付的出現(xiàn)極大的降低了交易的額外成本，加快了交易速度，使得市場經(jīng)濟下的自由貿(mào)易更為興盛。在線支付改變了人們傳統(tǒng)的支付方式，使得消費者可以在有網(wǎng)絡(luò)的任意地方進行購物消費或者辦理轉(zhuǎn)賬業(yè)務(wù)。

目前，安全的在線支付方式是通過通信方式和密碼技術(shù)實現(xiàn)的，主要有以下3種：1） 帳號直接傳輸方式；2） SET方式；3） 專用協(xié)議方式。

1 時間自動機的基本概念

時間自動機可以表示成一個多元組 [Λi=（Li，l0i，Ti，Ci，Ii，Ei）] ，其中i表示不同的自動機，不同的自動機對應(yīng)于不同的模版。其中[Li]是自動機的有限狀態(tài)集合；[l0i]是自動機的初始狀態(tài)；[Ti]是自動機所有動作（action）的集合；[Ci]是一個有限時鐘集合，[Ii]是一種映射關(guān)系，指明每個狀態(tài)上有加的時間約束，所以表示為[Ii=Ii（x）]；[Ei?Li × Ti × B（Ci） × 2Ci × Li]是所有遷移的集合，如遷移[（l，g，a，x，l'）]

表示從狀態(tài)[l]出發(fā)的遷移在有約束條件g的作用下，執(zhí)行一個動作a， 最后轉(zhuǎn)換成狀態(tài)[l'] ，其中x為所在自動機的始終變量。

2 在線支付系統(tǒng)在UPPAAL[3]中的建模

在線支付系統(tǒng)的模型含有三個4個模版類（Template）：消費者模型（Consumer），商家模型（Merchant），

支付網(wǎng)關(guān)模型（Payment Gateway），銀行模型（Bank）。

1） Consumer 模版類（如圖1所示），主要有7個狀態(tài)：Start，Wait1，ToPay，Wait2，Reset，Success

其中初始狀態(tài)是Start 狀態(tài)，因此在這個狀態(tài)時，沒有任何變量。Consumer模版類發(fā)送一個BUY信號給商家的模版類Merchant，之后Consumer會進入等待狀態(tài)Wait。

當Consumer收到enough信號后，會進入ToPay狀態(tài)，當消費者付款之后，將進入另一個等待狀態(tài)Wait2，等待商家回復(fù)一個確認信號complete，之后進入Success狀態(tài)；

2） Merchant 模版類（如圖2所示），主要有7個狀態(tài)：Start，Check，Wait1，Wait2，Wait3，Reset，Success

Merchant 模版類初始狀態(tài)為Start，收到Consumer發(fā)送的BUY信號，Merchant會進入短暫的Check狀態(tài)后，發(fā)送request信號給支付網(wǎng)關(guān)（Payment Gateway），Merchant 發(fā)送charge信號給Payment Gateway請求對消費者賬戶進行扣款，當Payment Gateway返回received信號后表示已經(jīng)扣款成功，最后Merchant復(fù)位到Start狀態(tài)。

3） PaymentGateway模版（如圖3所示）主要有8個狀態(tài)： Start，ToCheck，Wait1，Checking，Wait2，Wait3，Reset，Success

PaymentGateway模版類的結(jié)構(gòu)和Merchant 模版類類似，PaymentGateway相當與整個支付系統(tǒng)的Controller，其負責接收來自商家的消費者賬戶驗證請求，以及接收扣款請求。但是真正負責驗證消費者賬戶和執(zhí)行扣款的操作是由Bank模版類處理，PaymentGateway起到的是轉(zhuǎn)發(fā)請求和第三方認證的作用。

4） Bank模版類（如圖4所示），主要有7個狀態(tài)：Start，Checking，YES，NO，Wait，Reset，Success

Bank是真正負責執(zhí)行賬戶驗證和支付操作的模版類，Checking狀態(tài)是銀行進行驗證賬戶時的狀態(tài)，Bank會把驗證的結(jié)果（no信號或yes信號）返回給支付網(wǎng)關(guān)PaymentGateway，之后Bank會進入NO 或YES狀態(tài)，如能收到transaction則會進入等待狀態(tài)Wait，當Bank完成扣款后，則回復(fù)deal消息給PaymentGateway，且自身進入Success狀態(tài)，并最后回到初始狀態(tài)。

3 各模版的時間自動機定義

1） 消費者自動機模型定義

2） 商家自動機模型定義

3） 支付網(wǎng)關(guān)模型定義

4） 銀行模型定義

4 對于在線支付系統(tǒng)中的超時問題的分析與解決

為了保證在線支付系統(tǒng)操作的原子性，當?shù)讓幽KBank 產(chǎn)生了超時，就必須把其上層的所有模塊重置到初始狀態(tài)。在圖4中，Bank模塊的超時發(fā)生在兩處狀態(tài)：YES 和Wait，超時時間分別設(shè)定為5T 和6T。超時時Bank都會進入Reset狀態(tài)，且之后會發(fā)送reset_PG信號給上層模塊PaymentGateway。

如果在PaymentGateway模塊中的Wait2，ToTrans，Wait3 時接到Bank模塊的回復(fù)信息是reset_PG，表明Bank模塊已超時或者說已失效，PaymentGateway就會進入Reset狀態(tài)，并且在恢復(fù)到初始狀態(tài)之前會發(fā)送reset_M信號給上層模塊Merchant。endprint

與PaymentGateway模塊相似，Merchant模塊可能會收到reset_M信號的等待狀態(tài)是Wait2， ToCharge， Wait3三個狀態(tài)。同樣在收到reset_M后都會進入Reset狀態(tài)，恢復(fù)到初始化狀態(tài)前發(fā)送reset_C給Consumer。

同樣，Consumer如果在ToPay和Wait2狀態(tài)時收到reset_C信號，Consumer就會恢復(fù)到初始狀態(tài)Start。

5 使用UPPAAL對模型進行驗證

先使用UPPAAL軟件對上述四個模版類建立模型，模型建立之后要對系統(tǒng)的性質(zhì)進行驗證。為避免系統(tǒng)發(fā)生死鎖，需要驗證 A[] not deadlock 這一屬性。為了驗證最終支付操作能順利完成，需要驗證下列三個屬性：

6 結(jié)束語

本課題通過形式化方法模型檢測語言并采用UPPAAL建模工具進行在線支付系統(tǒng)支付過程的建模及結(jié)果驗證，最終的驗證結(jié)果是各個模版類最終都能達到理想狀態(tài)，即時是在Bank模型出現(xiàn)超時的情況下。實驗中如果底層模型出現(xiàn)超時，上層模型必須重置其狀態(tài)，重置的過程是自底向上依次重置。設(shè)計中并為考慮多個模型出現(xiàn)超時的情況，但處理方法也可類似設(shè)計。 本文的側(cè)重點是要滿足系統(tǒng)的安全性，關(guān)于快速性，即超時問題將在后續(xù)的研究中得到改進。

參考文獻：

[1] 肖修林，吳朝暉.可信用電子商務(wù)系統(tǒng)體系架構(gòu)研究[J].計算機集成制造系統(tǒng)，CIMS.2003.

[2] Lu，Shiyong，Model checking the secure electronic transaction （SET） protocol[D].Univ of New York at Stony Brook， Stony Brook， United States，1999.

[3] Gerd Behrmann， Alexandre David， Kim G Larsen.A Tutorial on Uppaal[D].Aalborg University， Denmark，Updated 17th November 2004.

[4] 劉如娟，戴桂蘭，胡長軍，等.Web服務(wù)的模型檢測技術(shù)探討[J].小型微型計算機系統(tǒng)，2007（11）.

（下轉(zhuǎn)第8346頁）

（上接第8342頁）

[5] 官尚元，伍衛(wèi)國，董小社，等.自動信任協(xié)商的形式化描述與驗證研究[J].通信學報，2011（2）.

[6] 郭華， 莊雷，張習勇.UPPAAL——一種適合自動驗證實時系統(tǒng)的工具[D].西安：西安理工大學，2006.

[7] 梁少華.網(wǎng)上銀行電子商務(wù)支付的實現(xiàn)[D].長春：吉林大學，2013.

[8] 付雄，程文青，郎為民，等.安全電子支付系統(tǒng)研究[J].計算機科學，2005（1）.

[9] 張傳武，彭啟琮，沈野樵，等.安全支付網(wǎng)關(guān)技術(shù)研究與系統(tǒng)實現(xiàn)[J].系統(tǒng)工程與電子技術(shù)，2002（3）.

[10] 袁姍姍.基于SET的支付網(wǎng)關(guān)的研究與設(shè)計[D].武漢：華中科技大學，2006.endprint

與PaymentGateway模塊相似，Merchant模塊可能會收到reset_M信號的等待狀態(tài)是Wait2， ToCharge， Wait3三個狀態(tài)。同樣在收到reset_M后都會進入Reset狀態(tài)，恢復(fù)到初始化狀態(tài)前發(fā)送reset_C給Consumer。

同樣，Consumer如果在ToPay和Wait2狀態(tài)時收到reset_C信號，Consumer就會恢復(fù)到初始狀態(tài)Start。

5 使用UPPAAL對模型進行驗證

先使用UPPAAL軟件對上述四個模版類建立模型，模型建立之后要對系統(tǒng)的性質(zhì)進行驗證。為避免系統(tǒng)發(fā)生死鎖，需要驗證 A[] not deadlock 這一屬性。為了驗證最終支付操作能順利完成，需要驗證下列三個屬性：

6 結(jié)束語

本課題通過形式化方法模型檢測語言并采用UPPAAL建模工具進行在線支付系統(tǒng)支付過程的建模及結(jié)果驗證，最終的驗證結(jié)果是各個模版類最終都能達到理想狀態(tài)，即時是在Bank模型出現(xiàn)超時的情況下。實驗中如果底層模型出現(xiàn)超時，上層模型必須重置其狀態(tài)，重置的過程是自底向上依次重置。設(shè)計中并為考慮多個模型出現(xiàn)超時的情況，但處理方法也可類似設(shè)計。 本文的側(cè)重點是要滿足系統(tǒng)的安全性，關(guān)于快速性，即超時問題將在后續(xù)的研究中得到改進。

參考文獻：

[1] 肖修林，吳朝暉.可信用電子商務(wù)系統(tǒng)體系架構(gòu)研究[J].計算機集成制造系統(tǒng)，CIMS.2003.

[2] Lu，Shiyong，Model checking the secure electronic transaction （SET） protocol[D].Univ of New York at Stony Brook， Stony Brook， United States，1999.

[3] Gerd Behrmann， Alexandre David， Kim G Larsen.A Tutorial on Uppaal[D].Aalborg University， Denmark，Updated 17th November 2004.

[4] 劉如娟，戴桂蘭，胡長軍，等.Web服務(wù)的模型檢測技術(shù)探討[J].小型微型計算機系統(tǒng)，2007（11）.

（下轉(zhuǎn)第8346頁）

（上接第8342頁）

[5] 官尚元，伍衛(wèi)國，董小社，等.自動信任協(xié)商的形式化描述與驗證研究[J].通信學報，2011（2）.

[6] 郭華， 莊雷，張習勇.UPPAAL——一種適合自動驗證實時系統(tǒng)的工具[D].西安：西安理工大學，2006.

[7] 梁少華.網(wǎng)上銀行電子商務(wù)支付的實現(xiàn)[D].長春：吉林大學，2013.

[8] 付雄，程文青，郎為民，等.安全電子支付系統(tǒng)研究[J].計算機科學，2005（1）.

[9] 張傳武，彭啟琮，沈野樵，等.安全支付網(wǎng)關(guān)技術(shù)研究與系統(tǒng)實現(xiàn)[J].系統(tǒng)工程與電子技術(shù)，2002（3）.

[10] 袁姍姍.基于SET的支付網(wǎng)關(guān)的研究與設(shè)計[D].武漢：華中科技大學，2006.endprint

與PaymentGateway模塊相似，Merchant模塊可能會收到reset_M信號的等待狀態(tài)是Wait2， ToCharge， Wait3三個狀態(tài)。同樣在收到reset_M后都會進入Reset狀態(tài)，恢復(fù)到初始化狀態(tài)前發(fā)送reset_C給Consumer。

同樣，Consumer如果在ToPay和Wait2狀態(tài)時收到reset_C信號，Consumer就會恢復(fù)到初始狀態(tài)Start。

5 使用UPPAAL對模型進行驗證

先使用UPPAAL軟件對上述四個模版類建立模型，模型建立之后要對系統(tǒng)的性質(zhì)進行驗證。為避免系統(tǒng)發(fā)生死鎖，需要驗證 A[] not deadlock 這一屬性。為了驗證最終支付操作能順利完成，需要驗證下列三個屬性：

6 結(jié)束語

本課題通過形式化方法模型檢測語言并采用UPPAAL建模工具進行在線支付系統(tǒng)支付過程的建模及結(jié)果驗證，最終的驗證結(jié)果是各個模版類最終都能達到理想狀態(tài)，即時是在Bank模型出現(xiàn)超時的情況下。實驗中如果底層模型出現(xiàn)超時，上層模型必須重置其狀態(tài)，重置的過程是自底向上依次重置。設(shè)計中并為考慮多個模型出現(xiàn)超時的情況，但處理方法也可類似設(shè)計。 本文的側(cè)重點是要滿足系統(tǒng)的安全性，關(guān)于快速性，即超時問題將在后續(xù)的研究中得到改進。

參考文獻：

[1] 肖修林，吳朝暉.可信用電子商務(wù)系統(tǒng)體系架構(gòu)研究[J].計算機集成制造系統(tǒng)，CIMS.2003.

[2] Lu，Shiyong，Model checking the secure electronic transaction （SET） protocol[D].Univ of New York at Stony Brook， Stony Brook， United States，1999.

[3] Gerd Behrmann， Alexandre David， Kim G Larsen.A Tutorial on Uppaal[D].Aalborg University， Denmark，Updated 17th November 2004.

[4] 劉如娟，戴桂蘭，胡長軍，等.Web服務(wù)的模型檢測技術(shù)探討[J].小型微型計算機系統(tǒng)，2007（11）.

（下轉(zhuǎn)第8346頁）

（上接第8342頁）

[5] 官尚元，伍衛(wèi)國，董小社，等.自動信任協(xié)商的形式化描述與驗證研究[J].通信學報，2011（2）.

[6] 郭華， 莊雷，張習勇.UPPAAL——一種適合自動驗證實時系統(tǒng)的工具[D].西安：西安理工大學，2006.

[7] 梁少華.網(wǎng)上銀行電子商務(wù)支付的實現(xiàn)[D].長春：吉林大學，2013.

[8] 付雄，程文青，郎為民，等.安全電子支付系統(tǒng)研究[J].計算機科學，2005（1）.

[9] 張傳武，彭啟琮，沈野樵，等.安全支付網(wǎng)關(guān)技術(shù)研究與系統(tǒng)實現(xiàn)[J].系統(tǒng)工程與電子技術(shù)，2002（3）.

[10] 袁姍姍.基于SET的支付網(wǎng)關(guān)的研究與設(shè)計[D].武漢：華中科技大學，2006.endprint