摘要
BAN逻辑的推理过程中可能引入错误的推理条件,导致不安全的协议被验证为安全的。为解决该问题,对消息的形式化描述方式进行改进,在消息含义推理规则中加上一个隐含但不能被忽略的条件,以增强验证的可靠性,通过对发送和推理的消息单元进行限定,使消息新鲜性判定规则适用于更多类型的协议安全性验证。
Because an error condition may be added in BAN logic reasoning process, unsafe protocol can be verified safe. In order to solve the problem, this paper improves the formal description of message. An implicit but essential condition is added in the message-meaning inference rule, so that reliability of verification is enhanced. By defining message units of sending and reasoning, freshness rule is suitable to more kinds of protocols in safety verification.
出处
《计算机工程》
CAS
CSCD
2012年第17期110-115,共6页
Computer Engineering
基金
国家自然科学基金资助项目(60863005
61011130038)
贵州大学自然科学青年科研基金资助项目((2009)021)
贵州大学研究生创新基金资助项目(省研理工2010005
校研理工2011033)
关键词
BAN逻辑
安全协议
形式化
非形式化
消息新鲜性
推理
BAN logic
security protocol
formalization
informalization
message freshness
reasoning
