基于UPPAAL在線支付系統的安全性驗證

馬振立

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

關鍵詞：電子商務；支付系統；UPPAAL；模型檢測

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

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

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

1 時間自動機的基本概念

時間自動機可以表示成一個多元組 [Λi=（Li，l0i，Ti，Ci，Ii，Ei）] ，其中i表示不同的自動機，不同的自動機對應于不同的模版。其中[Li]是自動機的有限狀態集合；[l0i]是自動機的初始狀態；[Ti]是自動機所有動作（action）的集合；[Ci]是一個有限時鐘集合，[Ii]是一種映射關系，指明每個狀態上有加的時間約束，所以表示為[Ii=Ii（x）]；……