輕量級移動支付協議公平性分析

李 茜，王 崢，馬建芬，李 娜

1.太原理工大學 計算機科學與技術學院，太原 030024

2.國網山西省電力公司，太原 030024

1 引言

移動支付（Mobile Payment）作為移動電子商務的重要應用之一[1]，是依托其移動終端（一般為手機），通過無線網絡購買貨物或服務的一種新型支付方式[2]。移動互聯網絡的發展和無線設備的普及，使移動支付給人們的生活帶來極大便利。與此同時，其安全問題和支付效率問題也逐漸成為人們關注的熱點[3]。為保證移動支付安全、順利進行，在通信以及傳輸數據時，必須采用安全高效的移動支付協議。因此，對現有輕量級移動支付協議的形式化分析和研究已經成為信息安全領域中的一個重要課題[4]。

2004年，Kungpisdan等人提出一個適用于無線網絡的安全的基于帳戶的移動支付協議[5]，協議采用了對稱加密算法，無需對主體公鑰加解密計算，減輕移動終端的計算負荷，提高協議執行效率。Tan等人基于文獻[5]進一步提出安全的輕量級對稱密鑰移動支付協議[6]，他們認為公鑰體制計算量大，不適用于移動終端的支付活動。針對全連接場景未考慮到客戶和商家不能直接通信的情況，承接Kungpisdan等與Tan等人的設計思想，Isaac和Zeadally于2012年提出PCMS（secure Payment Centric Model using Symmetric cryptography protocol）[7]協議，該協議以支付網關為中心，采用輕量級對稱加密技術，適用于計算能力差，存儲資源有限的移動設備和無線信道帶寬低，不可靠的移動環境。同時，用臨時身份代替客戶的真實身份，保護客戶隱私，并在2014年繼續對PCMS協議進行了設計實現和性能分析[8]。結果表明，PCMS協議需要更少的計算量和存儲空間，可以部署在計算資源有限的移動設備上，使支付交易在無線網絡上有效地執行。2017年，吳格格等人用UPPAAL模型檢測工具對PCMS協議形式化分析，證明其滿足無死鎖、錢原子性、有效性和時效性[9]。

本文在前人研究基礎上，進一步分析該協議的隱私性、機密性、認證性和完整性等，并基于串空間理論和認證測試方法，研究分析PCMS協議的公平性，針對協議不滿足的安全屬性做出改進，用模型檢測工具SPIN（Simple Promela Interpreter）[10]對改進后的協議進行驗證分析。

2 PCMS協議

PCMS協議分為商家注冊子協議和支付子協議兩部分。商家注冊子協議在客戶和商家之間進行，主要用于交換主密鑰，并通過主密鑰生成一套新的會話密鑰。本文主要對支付子協議進行形式化分析研究，其執行順序如圖1所示。

圖1 PCMS支付子協議執行順序圖

協議描述符號說明如表1所示。

協議描述如下：

（1）C→PG→M：NIDC,i,TIDReq。

（2）M→PG→C：{TID,IDM}KSC-Mi。

客戶將自己的昵稱、指數i（用來生成客戶和商家之間的會話密鑰）和TID請求通過支付網關發送給商家，商家將自己的身份標識和交易特性用i生成的會話密鑰加密，通過支付網關發送給客戶，客戶和商家通過支付網關交換必要的信息。

表1 協議描述符號說明表

（3）C→PG→M：PRequest；PRequest={OI,Price,NIDC,IDI,TSTC,z,h(KSC-Iz),VSRequest}KSC-Mi,MAC[(OI,Price,NIDC,IDI,TSTC,z,h(KSC-Iz),KSC-Mi+1]；VSRequest=(MAC[(Price,h(OI),TSTC,TC,IDM),KSC-Iz],TC,TSTC。

客戶通過支付網關向商家發送支付請求，其中包含有扣款請求（可選擇使用借記卡或信用卡支付）和C生成的時間戳，用客戶和商家的共享密鑰加密。商家收到支付請求后，通過時間戳驗證支付請求的有效性。若有效，則將解密得到的扣款請求和M生成的時間戳發送給支付網關；若無效，則通知支付網關取消交易。

（5.1）PG→I：NIDC,IDM,VSRequest,TID,h(OI),z,Price,h(KSC-Iz)；

（5.2）PG→A：Price,IDM；

（5.3）I,A→PG：VSResponse,Stt,h(Stt,h(OI),,h(KSC-Iz))；VSResponse={Stt,h(OI),KSM-PGk+1}KSC-Iz。

支付網關解密得到轉賬請求后，通過M的時間戳驗證轉賬請求的有效性。若有效，則向I、A發送信息，完成轉賬操作；若無效，則通知客戶和商家取消交易。I在驗證了扣款請求和客戶賬戶的有效性后，將款項從客戶賬戶轉移到商家賬戶，并將包含交易狀態的扣款響應發送給支付網關。這部分交易均在銀行專有網絡內進行，安全性暫不做考慮。

（6）PG →M：VCResponse；VCResponse={Stt,h(Stt,

支付網關將轉賬響應和支付響應分別發送給商家和客戶。至此，商家賬戶已經收到款項，客戶確定商家將發送貨物或提供服務。

3 協議的形式化分析

3.1 相關知識

3.1.1 串空間

設兩個互不相交的原子項集合：A為原子消息集合，其中的元素用a表示；K為密鑰集合，其中的元素用k表示。設T為協議運行中，協議各主體之間相互交換傳遞的消息集合，其中的元素用t表示，及消息項。

定義1（串空間）帶符號的二元組＜σ,t＞表示一個事件。其中，σ∈{+,-}，“+”表示協議主體發送一條消息，“-”表示協議主體接收到一條消息；t∈T，表示協議中所有的消息項。±T表示串空間中所有事件的集合；是所有帶符號項的有限序列集合，其元素為 (＜σ1,a1＞,＜σ2,a2＞,…,＜σn,an＞)，n表示序列長度，term(n)=σt。一個串表示一個主體對消息的所有發送和接收行為。串到帶符號項的有限序列集合的一個映射tr稱為串的跡映射，通常把串的跡稱為串。二元組＜Σ,tr＞表示一個串空間。其中，Σ表示串的集合[11]。

3.1.2 認證測試

認證測試方法以串空間理論為基礎，是一種基于挑戰-應答機制，用于證明安全協議認證屬性的方法，串空間模型中的所有定義和性質都適用于認證測試[12]。

定義2（主動測試）如果t為a在n中的測試組件，且K?P，那么，接收節點（負節點）n是項t={h}k關于值a的主動測試。

定理1設C=＜NC,EC＞是T上的叢，n∈NC，n是項t={h}k關于值a的主動測試，可得：必然存在一個常規正節點包含t為組件[13]。

定理2設C=＜NC,EC＞是T上的叢，n∈NC，且n不是串空間的源節點，如果節點n的符號為正，且t?term(n)，那么必然存在一個包含t的發送邊[14]。

2000年，主動測試概念由Guttman等人首次提出，定理1是認證測試的一個推理，定理2是串空間理論的一個擴展，詳細證明見文獻[13]和[14]。

3.2 串空間建模

串空間是形式化分析方法中定理證明的一種[19]。綜合定理證明技術和協議跡分析技術的優勢，可以用消息串的代數表示法描述協議的執行，也可以用串空間圖的形式刻畫協議的執行過程。串空間中每一個叢就是協議的一個并發運行，協議的安全性通過叢保持的性質來證明，模型簡潔易懂。

PCMS協議執行過程中，客戶完全信任于發卡銀行，相信其不會把自己的隱私透露給商家或支付網關，客戶的昵稱由發卡銀行分配。給出PCMS協議的串空間模型[15]，如圖2所示。

圖2 PCMS支付子協議串空間模型圖

其中，客戶的目標在于，確定交易成功，款項以正確數額轉給正確的商家賬戶，商家承諾向其發送貨物或提供服務。客戶目標通過支付網關發送給客戶的支付響應來實現，支付響應中包含的Stt表明交易的成功與否。同時，客戶可以將自己的OI做哈希運算，與解密得到的h(OI)比對，驗證交易信息的正確性。商家的目標在于，收到準確數額的款項，確定交易成功。商家目標通過支付網關發送給商家的轉賬響應來實現。支付網關的目的是在客戶和商家之間傳遞消息，通知客戶和商家交易成功。因此，只要保證客戶和商家的目標可以實現，支付網關的目標即實現。

由此可見，保證協議公平性的關鍵在于，C收到支付響應，當且僅當P收到支付請求；M收到轉賬響應，當且僅當P收到轉賬請求。協議（1）、（2）步，只是客戶和商家通過支付網關交換必要的信息，不涉及各主體的切身利益。給出PCMS協議部分串空間模型圖[16]，如圖3所示。

定義3設Init[PRequest,PResponse]是客戶串的集合，其軌跡(trace)＜+PRequest,-PResponse＞。

定義4設Resp[PRequest,VCRequest,IDM,z,KSC-Iz,k,VCResponse]是商家串的集合，其軌跡為＜-PResponse,

圖3 PCMS協議部分串空間模型圖

定義5設Gateway[PRequest,VCRequest,k,VCResponse]是支付網關串的集合，其軌跡為-PResponse＞。

3.3 安全目標分析

客戶用昵稱NIDC代替其真實IDC，無論是商家還是支付網關都無法通過客戶的昵稱查找到其真實ID，可以有效保護客戶賬戶、密碼等隱私信息。同時，該協議采用對稱密鑰加密，根據完美密鑰假設，其不會被泄漏，是安全可靠的，用主密鑰生成新的會話密鑰，可有效防止密鑰猜測攻擊，同時對稱加密保證了主體之間的認證性。PCMS協議通過采用MAC技術，保證了所傳遞信息的源發性和完整性，使發送方的消息不可抵賴、不能偽造。

分析表明，PCMS協議滿足隱私性、機密性、認證性和完整性。

PCMS協議的公平性通過M與P之間的公平性和C與P之間的公平性分別證明。

執行過程中M與P之間是公平的，如果M收到轉賬響應，當且僅當P收到轉賬請求。首先，證明如果M收到轉賬響應，那么P一定能夠收到轉賬請求。用串空間理論形式化描述如下：

命題1假設C為PCMS協議串空間Σ中的一個叢，如果 S,SP?Σ,S?Resp[PRequest,VCRequest,IDM,z,KSC-IZ,k,VCResponse],C-height(S)=3，則C中必然存在正常串：Sp∈Gateway[PRequest,VCRequest,IDM,z,KSC-IZ,k,VCResponse]，且C-height(SP)≥3。

證明由假設可知S?Resp[PRequest,VCRequest,IDM,z,KSC-IZ,k,VCResponse]，且C-height(S)=3，則S在C上的跡為由于uns_term＜S,3＞=VCResponse，節點＜S,3＞是符號為負的常規節點，構成項VCResponse的主動測試。由主動測試定理可得，叢C中必定存在一個常規節點n1，使得該項屬于uns_term(n1)，而該項是P傳遞的轉賬響應，故節點n1只能在串SP上。

對串SP的跡分析可知，n1=＜SP,4＞，所以＜S,3＞唯一起源于＜SP,4＞，C-height(SP)=4，滿足命題中C-height(SP)≥3的條件。得出結論：當M收到轉賬響應時，P一定能夠收到轉賬請求。這對于M和P來說都是公平的。

接著，證明如果P能收到轉賬請求，那么M一定能夠收到轉賬響應。用串空間理論形式化描述如下：

命題2假設C為PCMS協議串空間Σ中的一個叢，如果 S,SM?Σ,S?Gateway[PRequest,VCRequest,IDM,z,KSC-IZ,k,VCResponse]，且C-height(S)=3，則C 中必然存在正常串：SM∈Resp[PRequest,VCRequest,IDM,z,KSC-Iz,k,VCResponse]，且C-height(SM)≥3。

證明由假設可知S?Gateway[PRequest,VCRequest,IDM,z,KSC-IZ,k,VCResponse]，且C-height(S)=3，則S在C上的跡為：由于，節點＜S,3＞是符號為負的常規節點，構成項{VCRequest||IDM||z||h(KSC-Iz)}KSM-PGk||k||MAC[(VCRequest||IDM||z||h(KSC-Iz)||KSM-PGk+1]，的主動測試。由主動測試定理可得，叢C中必定存在一個常規節點n2，使得該項屬于term(n2)。而該項是M傳遞的轉賬請求，故節點n2只能在串SM上。

對串SM的跡分析可知，n2=＜SM,2＞，所以＜S,3＞唯一起源于＜SM,2＞，即C-height(SM)=2，不滿足命題中 C-height(SM)≥3的條件。在串 S中，當C-height(S)=3時，S已經收到了M發送的轉賬請求，但若此時協議中斷，就不能保證VCResponse的產生，也無法確定M是否收到過P向其發送的轉賬響應。得出結論：當P收到轉賬請求時，M不一定能夠收到轉賬響應。這對于M來說是不公平的。此時，M已經得到付款，但由于未收到轉賬響應，不會向C發送貨物或提供服務，間接影響到了C的利益。

同理，定義PCMS協議執行過程中C與P之間是公平的，如果C收到支付響應，當且僅當P收到支付請求。用串空間理論建模和認證測試方法形式化證明，得到結論：如果C收到支付響應，那么P一定能夠收到支付請求；但如果P收到支付請求，C不一定能夠收到支付響應。這對于C來說是不公平的。但是，此時由于M已經收到貨款和轉賬響應，并且向C發送貨物或提供服務，只是C未收到支付響應，沒有一方的切身利益受到損害。

綜上所述，PCMS協議不滿足公平性。由于對C的不公平并不會使任何主體利益受損，因此，只針對M和P之間的不公平情況做出改進。

4 協議改進及驗證

4.1 協議改進

由上述可知，在協議執行到第（6）步，當P為不誠實主體或因網絡導致通信中斷時，P收到了M的轉賬請求，但M未收到相應的轉賬響應，M和P之間不滿足安全協議的公平性，使C的利益間接受損。針對以上情況，本文通過增加一個P的時間戳來保證M對轉賬響應的接收情況，在消息無效的情況下，通過退款子協議來完成后續步驟，保證C的利益。

對原協議第（6）步修改如下：

（6）PG→M：VCResponse;VCResponse={Stt,TSTP,

增加退款子協議如下：

（2）PG→A：NIDC,IDM,Price,TC,TID；

（3）PG→I：Price,NIDC；

（4）I,A→PG：Yes/No；

協議執行的第（6）步，若M 在P時間戳規定的時間內未收到轉賬響應，則執行退款子協議，向P發送消息終止交易。P與I和A溝通，再次將款項轉移，并通知M交易取消成功。

4.2 SPIN模型檢測工具驗證

SPIN模型檢測工具支持設計和驗證系統，可作為一個模擬器，快速對建立的系統模型進行隨意、引導性的或交互的仿真。使用Promela語言編程建模直觀、明白地描述系統設計，用線性時序邏輯LTL有力、簡明地描述系統需求，并通過有效算法驗證系統是否滿足需求[15]。

對改進后的協議，用Promela語言描述系統進行模擬分析，保證模型建立的正確性，通過simulate模擬協議中各主體的交易行為，如圖4所示。圖4中，從左至右分別代表客戶、商家、支付網關和銀行的交互過程，所示圖可成功模擬協議的執行順序，與設計一致。

圖4 主體交易行為模擬圖

協議屬性驗證輸出結果如圖5所示，此時SPIN產生一個分析器，其被編譯和執行，并將結果顯示在Verifiction Output窗口中。圖的第一部分表示：所用模型檢測工具的版本為Spin Version 6.4.6-2016.12.2，默認使用偏序簡約運算法則。第二部分表示：SPIN平臺按照實驗設計運行，默認在全部狀態空間搜索，整個檢測過程以正常狀態結束，無死鎖。由圖5第三部分第8行可知，描述該全局系統狀態使用68字節的內存空間，檢測運行過程中最長深度優先搜索路徑包含63個狀態轉移，查找過程中未檢測到錯誤，若有錯誤檢測會自動停止并報錯。有110個不同的全局系統狀態存儲在狀態空間中，每個狀態需要68個字節進行有效描述，遇到34曾遍歷過的狀態，總工作量為144個狀態搜索遍歷，用默認Hash算法函數存儲狀態時，無沖突產生。第四部分顯示數據使用的內存空間所占字節量。

圖5 驗證輸出結果圖

結果分析表明，通過對協議的改進可實現協議的公平性[16]。

5 結束語

本文形式化分析了輕量級移動支付協議PCMS的安全性，并基于串空間理論的認證測試方法，對其公平性進行形式化分析。原協議不滿足公平性存在漏洞，改進方案增加支付網關的時間戳來保證商家對轉賬響應信息的接收，增加退款子協議完成后續退款流程。改進方案使商家除了收到準確數額的款項，確定交易成功以外，還對客戶的利益負有責任。用模型檢測工具SPIN分析驗證，結果表明，改進后的協議設計合理，滿足公平性。下一步工作，將繼續對輕量級移動支付協議安全屬性進行深入研究分析，在保證安全屬性的前提下，簡化子協議。