簡介
電子商務由消費者( customer )、商家( mer2chant)和銀行( bank)及所信任的第三方認證機構(CA)之間的信息流、資金流和物流的互動關係，各方通過遍及全球的、開放的但不安全的Internet相互聯繫。在電子商務模型中，各個主體(消費者、商家、銀行等) 進行互動必須遵循一定的規則，以保證各方的利益和安全，並且能控制交易風險，這就是協定的模式。安全的電子商務協定是保證電子商務活動正常開展的前提。我們可以用形式化的方法來描述與驗證網路協定，從而發現協定中潛在的錯誤。已經開發出多種基於時間自動機的網路協定驗證工具，UPPAAL就是很好的工具之一。
簡單網路支付協定(SNPP)是由MIT計算機科學實驗室的Semyon Dukach提出的。該協定使用UDP 數據報傳輸，DES 對稱加密技術，HOLD技術和相互獨立機制為不信任的雙方實現安全支付交易。對SNPP 協定進行過分析和檢驗，但是他們僅僅給出了簡化的SNPP 協定模型，並且在給出的銀行模型上還存在一些不足之處 。
簡單網路支付協定
消費者首先選擇信任的銀行開戶存入現金，得到相應的銀行賬號和採用對稱加密產生的密鑰。銀行記錄每個賬戶的現金類別和數量、現金預留表，密鑰，最近交易號碼和所有的歷史交易號碼列表的信息，通過賬號來索引。HOLD信息包含賬戶，賬號/銀行身份匹配認證以及逾時約束。當消費者傳送HOLD信息給商家時，協定開始運行，然後商家把信息轉送到自己的銀行，若商家和消費者不屬於同一個銀行，則把HOLD信息轉送到消費者銀行。
若消費者賬戶的資金足夠，銀行先將預留信息添加到消費者賬戶的現金預留列表，再返回一個確認信息給商家銀行，否則整個HOLD將被拒絕。商家在收到自己的銀行的通知後，將商品傳送給消費者。
同時，消費者收到商品後傳送PAY信息確認付款，商家把該信息轉送到商家銀行，商家銀行再把該信息轉送到消費者銀行，消費者銀行通過外部程式把資金送到商家銀行，商家銀行將要求的資金數量轉入商家賬號，交易完成 。
協定形式化建模及驗證
1.建立模型
對協定中的4個進程逾時約束別分設為單位時間15，20，20，20。若消費者在收到商家的發貨信息15個單位時間之後，仍未傳送付款訊息則傳送逾時訊息；若商家在傳送確認發貨訊息之後20個單位時間內未收到消費者的付款信息則傳送逾時信息；若商家銀行在傳送確認訊息給商家20個單位時間之後沒有收到付款訊息則傳送逾時信息；若消費者銀行在傳送已預留資金20個單位時間之後未收到付款訊息則認為是逾時，傳送逾時訊息。逾時計時器在接收到以上進程的逾時信息後，立即傳送訊息給外部仲裁程式。
建立模型時，假設消費者與商家的銀行是不同銀行。此外，在不影響協定關鍵性質檢測的前提下，假設銀行支付過程為理想過程，即不存在網路通信及其它設備故障的情況。
定義5個進程模組:消費者進程，商家進程，消費者銀行進程，商家銀行進程，逾時計時器進程。其中消費者進程只與商家進程進行通訊，商家進程只與商家銀行進程進行通訊，商家銀行只與消費者銀行進行通訊，逾時計時器只負責接收來自以上進程的逾時信息。
2.模型驗證
套用UPPAAL工具，先對協定原模型進行驗證，即驗證由消費者、商家、銀行進程構成的協定模型，再驗證本文建立的模型。結果表明，原模型滿足貨幣原子性，但是會存在消費者收到了商品而未付款的情況。而由協定的符號描述可知，若消費者收到了商品或服務，卻對此不滿意，則不會進行下一步驟。新模型驗證結果滿足該性質，表示消費者和商家等待信任第三方的仲裁，而銀行將預留資金凍結等待信任第三方的通知。這說明通過仲裁狀態可達性，使得協定的新模型滿足了商品原子性。
總結
從貨幣原子性和商品原子性這兩個角度對簡單網路支付協定進行了分析，通過UPPAAL 檢測發現該協定原模型滿足貨幣原子性，但在商品原子性上存在缺陷，可能產生消費者收到了商品而未付款的情況。所以在原模型的基礎上，我們增加了對不同銀行間交易行為和交易中逾時行為的分析，設計了逾時計時器模組，提出了用仲裁狀態可達性來通知外部仲裁程式解決交易糾紛，從而使新模型滿足了商品原子性 。
