摘要
通过对安全协议验证的形式化需求分析,论证了形式化描述和分析是描述电子商务协议并验证它们属性的有效方法.介绍了一个扩展的BAN逻辑,基于这个逻辑对一种电子交易协议NetBill协议进行形式化描述,并在有入侵的情况下对该协议所期望的属性(安全、原子、隐私)进行了正确的分析,证明了该协议在有入侵者的情况下能够满足安全、原子和隐私等要求.
With the requirement analysis of formalization verification for security protocols,it is confirmed that formalization description and analysis is an efficient way to describe electronic commerce protocol and verify their properties.An expanded BAN logic is introduced and,taking it as a basis,an electronic transaction protocol—NetBill protocol is formally described.The protocol is properly analyzed for its correctness of its desired attribution (security,atom,privacy) when there is an intruder.Thus,the protocol is proved to be meeting the requirement of security,atom,and,privacy under the condition of intrusion.
出处
《兰州理工大学学报》
CAS
北大核心
2004年第4期102-105,共4页
Journal of Lanzhou University of Technology
基金
国家科技攻关项目(2001BA201A32)
关键词
NetBill安全协议
电子商务
电子支付
属性
NetBill
security protocol
electronic commerce
electronic payment
attribution
