移動(dòng)支付協(xié)議PCMS的形式化分析和驗(yàn)證
本文選題:移動(dòng)支付協(xié)議 切入點(diǎn):模型檢測(cè) 出處:《計(jì)算機(jī)工程與科學(xué)》2017年01期
【摘要】:移動(dòng)電子商務(wù)協(xié)議的形式化分析和驗(yàn)證是近年來(lái)移動(dòng)電子商務(wù)協(xié)議的一個(gè)重要研究熱點(diǎn)。以一個(gè)支付網(wǎng)關(guān)為中心的匿名的移動(dòng)電子商務(wù)支付協(xié)議PCMS為研究對(duì)象,建立了PCMS協(xié)議的時(shí)間自動(dòng)機(jī)模型,并用計(jì)算樹(shù)邏輯CTL公式描述PCMS協(xié)議的部分性質(zhì),最后利用模型檢測(cè)工具UPPAAL對(duì)PCMS協(xié)議的無(wú)死鎖、時(shí)效性、有效性和錢(qián)原子性進(jìn)行檢測(cè)驗(yàn)證。驗(yàn)證結(jié)果表明,以支付網(wǎng)關(guān)為中心的匿名的安全支付協(xié)議PCMS滿(mǎn)足無(wú)死鎖、時(shí)效性、有效性和錢(qián)原子性。
[Abstract]:Formal analysis and verification of mobile e-commerce protocols is an important research hotspot of mobile e-commerce protocols in recent years.Taking an anonymous mobile e-commerce payment protocol (PCMS) centered on a payment gateway as the research object, the time automata model of PCMS protocol is established, and some properties of the PCMS protocol are described by using the computational tree logic CTL formula.Finally, the model checking tool UPPAAL is used to verify the deadlock-free, timeliness, validity and money atomicity of PCMS protocol.The verification results show that the anonymous secure payment protocol (PCMS) centered on payment gateway satisfies deadlock-free, timeliness, validity and money atomicity.
【作者單位】: 鄭州大學(xué)信息工程學(xué)院;
【基金】:國(guó)家973計(jì)劃(2012CB315901) 國(guó)家自然科學(xué)基金(61379079) 河南省科技廳攻關(guān)項(xiàng)目(122102210042);河南省科技廳基礎(chǔ)研究項(xiàng)目(142300410231,142300410308)
【分類(lèi)號(hào)】:TN915.04
【相似文獻(xiàn)】
相關(guān)期刊論文 前10條
1 劉文琦;顧宏;;基于分層時(shí)間有色Petri網(wǎng)的支付協(xié)議公平性分析[J];電子與信息學(xué)報(bào);2009年06期
2 劉軍;;改進(jìn)的公平微支付協(xié)議[J];計(jì)算機(jī)工程與應(yīng)用;2010年27期
3 汪楊琴;;一個(gè)安全高效的移動(dòng)微支付協(xié)議[J];計(jì)算機(jī)工程;2008年01期
4 劉恩賢;呂磊;姜輝;;移動(dòng)商務(wù)中一種擴(kuò)展的微支付協(xié)議研究[J];青島大學(xué)學(xué)報(bào)(工程技術(shù)版);2009年01期
5 彭勛,董榮勝,郭云川,蔡國(guó)永;安全支付協(xié)議的設(shè)計(jì)與驗(yàn)證研究[J];計(jì)算機(jī)工程與應(yīng)用;2005年06期
6 彭冰;付才;韓蘭勝;;基于橢圓曲線(xiàn)的移動(dòng)電子支付協(xié)議[J];華中科技大學(xué)學(xué)報(bào)(自然科學(xué)版);2008年10期
7 ;科學(xué)研究、技術(shù)發(fā)展與經(jīng)濟(jì)活動(dòng)[J];電子科技文摘;2002年07期
8 張澤莉,馬華東;簡(jiǎn)單網(wǎng)絡(luò)支付協(xié)議的形式模型[J];北京郵電大學(xué)學(xué)報(bào);2002年04期
9 劉霞;古天龍;董榮勝;郭云川;;移動(dòng)環(huán)境公平支付協(xié)議的設(shè)計(jì)與分析研究[J];通信學(xué)報(bào);2007年04期
10 ;教材評(píng)介[J];中國(guó)電子教育;2000年03期
相關(guān)會(huì)議論文 前3條
1 萬(wàn)仁福;李方偉;陳宇;;一種基于UOBT的移動(dòng)微支付協(xié)議[A];第九屆全國(guó)青年通信學(xué)術(shù)會(huì)議論文集[C];2004年
2 余興超;馬爭(zhēng)先;王玉斌;董榮勝;;基于UPPAAL的簡(jiǎn)單網(wǎng)絡(luò)支付協(xié)議形式化驗(yàn)證[A];廣西計(jì)算機(jī)學(xué)會(huì)2010年學(xué)術(shù)年會(huì)論文集[C];2010年
3 董炳武;萬(wàn)健;徐向華;;一種基于票據(jù)的P2P微支付協(xié)議[A];浙江省電子學(xué)會(huì)第七次會(huì)員代表大會(huì)暨2007學(xué)術(shù)年會(huì)論文集[C];2007年
相關(guān)重要報(bào)紙文章 前1條
1 華建明;違約造成對(duì)方的律師費(fèi)用要賠償[N];人民法院報(bào);2001年
相關(guān)博士學(xué)位論文 前3條
1 郎為民;微支付協(xié)議研究[D];華中科技大學(xué);2005年
2 付雄;移動(dòng)學(xué)習(xí)資源有償服務(wù)的支付協(xié)議研究[D];華中科技大學(xué);2007年
3 張向軍;集成化電子貨幣支付協(xié)議的研究[D];上海交通大學(xué);2009年
相關(guān)碩士學(xué)位論文 前8條
1 邵th;專(zhuān)利反向支付協(xié)議的反壟斷認(rèn)定研究[D];華東政法大學(xué);2015年
2 張帆;醫(yī)藥行業(yè)反向支付協(xié)議的反壟斷規(guī)制[D];華東政法大學(xué);2016年
3 郭穎穎;藥品專(zhuān)利反向支付協(xié)議的反壟斷法規(guī)制[D];鄭州大學(xué);2016年
4 何文鑫;微支付協(xié)議研究分析與系統(tǒng)實(shí)現(xiàn)[D];北京郵電大學(xué);2009年
5 王希;視頻支付協(xié)議的設(shè)計(jì)與分析[D];北京郵電大學(xué);2010年
6 龔鳴;移動(dòng)支付在電子商務(wù)中認(rèn)證與支付協(xié)議分析[D];北京工業(yè)大學(xué);2011年
7 孫俊杰;基于P2P的微支付研究[D];安徽農(nóng)業(yè)大學(xué);2012年
8 黃莉;具有公平性、原子性的小額付款系統(tǒng)模型研究[D];西南師范大學(xué);2003年
,本文編號(hào):1695544
本文鏈接:http://www.sikaile.net/jingjilunwen/dianzishangwulunwen/1695544.html