基于Petri網(wǎng)和有窮自動(dòng)機(jī)形式化分析方法的電子商務(wù)協(xié)議研究與實(shí)現(xiàn).pdf

1、當(dāng)今時(shí)代已進(jìn)入互聯(lián)網(wǎng)絡(luò)的時(shí)代,網(wǎng)絡(luò)的飛速發(fā)展給社會(huì)帶來(lái)了巨大的變革,電子商務(wù)以及電子政務(wù)的蓬勃發(fā)展應(yīng)用就是一個(gè)典型的例子.但這種應(yīng)用及網(wǎng)絡(luò)的開放性也帶來(lái)了新的信息安全問(wèn)題.信息安全已成為影響國(guó)家安全、社會(huì)穩(wěn)定和經(jīng)濟(jì)發(fā)展的重要因素.基于信息安全的電子商務(wù)協(xié)議的設(shè)計(jì)和應(yīng)用,就是為了保證網(wǎng)絡(luò)和信息的安全.協(xié)議涉及到兩個(gè)方面的內(nèi)容,一是加密技術(shù)的選用,二是協(xié)議邏輯的設(shè)計(jì).通常加密技術(shù)倍受重視而忽略了協(xié)議邏輯設(shè)計(jì),這就為黑客的攻擊,留下了許多隱患

2、和漏洞.針對(duì)協(xié)議邏輯出現(xiàn)的問(wèn)題,為保證基于信息安全的電子商務(wù)協(xié)議設(shè)計(jì)的正確性,就需要用形式化的分析工具來(lái)精確描述和仿真協(xié)議的行為、協(xié)議所要達(dá)到的目標(biāo)以及能否達(dá)到其預(yù)期的目標(biāo).該論文重點(diǎn)研究了目前流行的電子商務(wù)協(xié)議的形式化分析方法、基于電子商務(wù)安全認(rèn)證的基本協(xié)議和交易協(xié)議、以及基于公鑰基礎(chǔ)設(shè)施PKI的安全認(rèn)證協(xié)議.在此基礎(chǔ)上,論文的作者完成了如下的工作:①提出了某工商管理部門電子商務(wù)的安全認(rèn)證協(xié)議.②創(chuàng)新性地提出了用Petri網(wǎng)理論描述了

3、①的認(rèn)證協(xié)議,建立了該協(xié)議的Petri網(wǎng)模型.在此基礎(chǔ)上對(duì)模型進(jìn)行了仿真分析,證明了協(xié)議存在的隱患和漏洞,并進(jìn)行了修改.最后得到了較為完善的適合某工商管理部門電子商務(wù)的安全認(rèn)證協(xié)議.③提出了某工商管理部門電子商務(wù)在完成認(rèn)證之后要進(jìn)行交易的支付協(xié)議.④根據(jù)支付協(xié)議的特點(diǎn),創(chuàng)新性地提出了用有窮自動(dòng)機(jī)理論建立③的支付協(xié)議的自動(dòng)機(jī)模型.通過(guò)對(duì)模型的仿真分析,證明了:·③的支付協(xié)議滿足可追究性·③的支付協(xié)議不滿足公平性根據(jù)結(jié)果,作者提出了同時(shí)滿足