輕量級(jí)移動(dòng)支付協(xié)議公平性分析

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

1.太原理工大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，太原 030024

2.國(guó)網(wǎng)山西省電力公司，太原 030024

1 引言

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

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

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

2 PCMS協(xié)議

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

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

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

協(xié)議描述如下：

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

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

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

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

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

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

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

支付網(wǎng)關(guān)解密得到轉(zhuǎn)賬請(qǐng)求后，通過M的時(shí)間戳驗(yàn)證轉(zhuǎn)賬請(qǐng)求的有效性。若有效，則向I、A發(fā)送信息，完成轉(zhuǎn)賬操作；若無效，則通知客戶和商家取消交易。I在驗(yàn)證了扣款請(qǐng)求和客戶賬戶的有效性后，將款項(xiàng)從客戶賬戶轉(zhuǎn)移到商家賬戶，并將包含交易狀態(tài)的扣款響應(yīng)發(fā)送給支付網(wǎng)關(guān)。這部分交易均在銀行專有網(wǎng)絡(luò)內(nèi)進(jìn)行，安全性暫不做考慮。

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

支付網(wǎng)關(guān)將轉(zhuǎn)賬響應(yīng)和支付響應(yīng)分別發(fā)送給商家和客戶。至此，商家賬戶已經(jīng)收到款項(xiàng)，客戶確定商家將發(fā)送貨物或提供服務(wù)。

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

3.1 相關(guān)知識(shí)

3.1.1 串空間

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

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

3.1.2 認(rèn)證測(cè)試

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

定義2（主動(dòng)測(cè)試）如果t為a在n中的測(cè)試組件，且K?P，那么，接收節(jié)點(diǎn)（負(fù)節(jié)點(diǎn)）n是項(xiàng)t={h}k關(guān)于值a的主動(dòng)測(cè)試。

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

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

2000年，主動(dòng)測(cè)試概念由Guttman等人首次提出，定理1是認(rèn)證測(cè)試的一個(gè)推理，定理2是串空間理論的一個(gè)擴(kuò)展，詳細(xì)證明見文獻(xiàn)[13]和[14]。

3.2 串空間建模

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

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

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

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

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

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

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

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

定義5設(shè)Gateway[PRequest,VCRequest,k,VCResponse]是支付網(wǎng)關(guān)串的集合，其軌跡為-PResponse＞。

3.3 安全目標(biāo)分析

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

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

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

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

命題1假設(shè)C為PCMS協(xié)議串空間Σ中的一個(gè)叢，如果 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。

證明由假設(shè)可知S?Resp[PRequest,VCRequest,IDM,z,KSC-IZ,k,VCResponse]，且C-height(S)=3，則S在C上的跡為由于uns_term＜S,3＞=VCResponse，節(jié)點(diǎn)＜S,3＞是符號(hào)為負(fù)的常規(guī)節(jié)點(diǎn)，構(gòu)成項(xiàng)VCResponse的主動(dòng)測(cè)試。由主動(dòng)測(cè)試定理可得，叢C中必定存在一個(gè)常規(guī)節(jié)點(diǎn)n1，使得該項(xiàng)屬于uns_term(n1)，而該項(xiàng)是P傳遞的轉(zhuǎn)賬響應(yīng)，故節(jié)點(diǎn)n1只能在串SP上。

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

接著，證明如果P能收到轉(zhuǎn)賬請(qǐng)求，那么M一定能夠收到轉(zhuǎn)賬響應(yīng)。用串空間理論形式化描述如下：

命題2假設(shè)C為PCMS協(xié)議串空間Σ中的一個(gè)叢，如果 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。

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

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

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

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

4 協(xié)議改進(jìn)及驗(yàn)證

4.1 協(xié)議改進(jìn)

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

對(duì)原協(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時(shí)間戳規(guī)定的時(shí)間內(nèi)未收到轉(zhuǎn)賬響應(yīng)，則執(zhí)行退款子協(xié)議，向P發(fā)送消息終止交易。P與I和A溝通，再次將款項(xiàng)轉(zhuǎn)移，并通知M交易取消成功。

4.2 SPIN模型檢測(cè)工具驗(yàn)證

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

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

圖4 主體交易行為模擬圖

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

圖5 驗(yàn)證輸出結(jié)果圖

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

5 結(jié)束語(yǔ)

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