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

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

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

1 引言

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

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

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

2 PCMS協(xié)議

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

圖1 PCMS支付子協(xié)議執(zhí)行順序圖

協(xié)議描述符號說明如表1所示。

協(xié)議描述如下：

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

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

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

表1 協(xié)議描述符號說明表

（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。

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

（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發(fā)送信息，完成轉賬操作；若無效，則通知客戶和商家取消交易。I在驗證了扣款請求和客戶賬戶的有效性后，將款項從客戶賬戶轉移到商家賬戶，并將包含交易狀態(tài)的扣款響應發(fā)送給支付網關。這部分交易均在銀行專有網絡內進行，安全性暫不做考慮。

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

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

3 協(xié)議的形式化分析

3.1 相關知識

3.1.1 串空間

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

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

3.1.2 認證測試

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

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

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

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

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

3.2 串空間建模

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

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

圖2 PCMS支付子協(xié)議串空間模型圖

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

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

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

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

圖3 PCMS協(xié)議部分串空間模型圖

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

3.3 安全目標分析

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

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

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

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

命題1假設C為PCMS協(xié)議串空間Σ中的一個叢，如果 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，節(jié)點＜S,3＞是符號為負的常規(guī)節(jié)點，構成項VCResponse的主動測試。由主動測試定理可得，叢C中必定存在一個常規(guī)節(jié)點n1，使得該項屬于uns_term(n1)，而該項是P傳遞的轉賬響應，故節(jié)點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協(xié)議串空間Σ中的一個叢，如果 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上的跡為：由于，節(jié)點＜S,3＞是符號為負的常規(guī)節(jié)點，構成項{VCRequest||IDM||z||h(KSC-Iz)}KSM-PGk||k||MAC[(VCRequest||IDM||z||h(KSC-Iz)||KSM-PGk+1]，的主動測試。由主動測試定理可得，叢C中必定存在一個常規(guī)節(jié)點n2，使得該項屬于term(n2)。而該項是M傳遞的轉賬請求，故節(jié)點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發(fā)送的轉賬請求，但若此時協(xié)議中斷，就不能保證VCResponse的產生，也無法確定M是否收到過P向其發(fā)送的轉賬響應。得出結論：當P收到轉賬請求時，M不一定能夠收到轉賬響應。這對于M來說是不公平的。此時，M已經得到付款，但由于未收到轉賬響應，不會向C發(fā)送貨物或提供服務，間接影響到了C的利益。

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

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

4 協(xié)議改進及驗證

4.1 協(xié)議改進

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

對原協(xié)議第（6）步修改如下：

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

增加退款子協(xié)議如下：

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

（3）PG→I：Price,NIDC；

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

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

4.2 SPIN模型檢測工具驗證

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

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

圖4 主體交易行為模擬圖

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

圖5 驗證輸出結果圖

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

5 結束語

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