计算机工程与应用
計算機工程與應用
계산궤공정여응용
COMPUTER ENGINEERING AND APPLICATIONS
2014年
8期
6-10
,共5页
SVO逻辑%电子商务支付%Netbill协议%认证性
SVO邏輯%電子商務支付%Netbill協議%認證性
SVO라집%전자상무지부%Netbill협의%인증성
SVO logic%e-commerce payment%Netbill protocol%authentication properties
与证伪法（如模型检测）相比，采用证真法（如定理证明和逻辑推理）能验证协议在任意会话中的正确性，但分析难度较高，验证过程较为复杂。使用SVO逻辑方法，以Netbill微支付协议为例，对电子商务支付协议的认证性进行形式化分析。扩展了SVO逻辑的公理集；在不影响Netbill协议安全性的前提下，为其建立了简化模型；针对协议特点，修正和补充了其验证目标；给出了比之前更合理的协议假设，展示了具体的推理过程，分析了验证结果。结果表明，Netbill协议基本满足认证性。最后对相关研究工作进行了比较。
與證偽法（如模型檢測）相比，採用證真法（如定理證明和邏輯推理）能驗證協議在任意會話中的正確性，但分析難度較高，驗證過程較為複雜。使用SVO邏輯方法，以Netbill微支付協議為例，對電子商務支付協議的認證性進行形式化分析。擴展瞭SVO邏輯的公理集；在不影響Netbill協議安全性的前提下，為其建立瞭簡化模型；針對協議特點，脩正和補充瞭其驗證目標；給齣瞭比之前更閤理的協議假設，展示瞭具體的推理過程，分析瞭驗證結果。結果錶明，Netbill協議基本滿足認證性。最後對相關研究工作進行瞭比較。
여증위법（여모형검측）상비，채용증진법（여정리증명화라집추리）능험증협의재임의회화중적정학성，단분석난도교고，험증과정교위복잡。사용SVO라집방법，이Netbill미지부협의위례，대전자상무지부협의적인증성진행형식화분석。확전료SVO라집적공리집；재불영향Netbill협의안전성적전제하，위기건립료간화모형；침대협의특점，수정화보충료기험증목표；급출료비지전경합리적협의가설，전시료구체적추리과정，분석료험증결과。결과표명，Netbill협의기본만족인증성。최후대상관연구공작진행료비교。
Compared with the falsification-oriented approaches(such as model checking), the justification-oriented approaches (such as theorem proof and logic reasoning)can verify the correctness of protocols in unbounded number of sessions. However, those approaches are difficult and the verification process is complicated. Based on the SVO logic, this paper chooses the Netbill micropayment protocol to formally analyze the authentication properties of E-commerce payment pro-tocol. First, the axiom set of SVO is extended. Then, a simplified model of Netbill protocol is proposed without affecting the original security properties. According to the protocol’s characteristic, the verifying goals are improved. Moreover, the more reasonable protocol assumptions than before are given, the detailed reasoning process is showed, and the result is analyzed. The result shows that Netbill protocol satisfies the authentication properties. In the end, a comparison with other related research works is showed.
