| 摘要: |
| 电子商务协议的非否认性与公平性问题已成为电子商务和信息安全领域研究的热点。本文建立了网络支付协议ISI的有限状态机模型,并用SMV检验工具对其两个重要特性———非否认性与公平性进行了分析检验,发现了ISI协议不满足公平性。结果表明利用符号模型检验方法分析检验电子商务协议的新特性是行之有效的。 |
| 关键词: 电子商务协议 公平性 符号模型检测 信息安全 |
| DOI：10.3969/j.issn.1001-893X. |
| Received:January 21, 2005 |
| 基金项目:中国科学院资助项目;贵州省自然科学基金;贵州省教育厅自然科学基金 |
|
| Symbolic Model Checking Analysis for ISI Protocol |
|
| () |
| Abstract: |
| The non-repudiation and fairness between the sender and receiver is essential in E-commerce and information security field.In this paper,the network payment protocol ISI is modeled as finite state machine,and analysed in two vital aspects of accoutability property and fairness property using SMV.As a result,it is not fair in ISI protocol.This result shows that it is effective to analyse and check the new property of E-commerce protocols by symbol model checker. |
| Key words: E-commerce protocols,Fairness,Symbolic model checking,Information security |
