摘要
该文提出一种论证安全协议之安全性质的非单调动态逻辑 .针对信息安全的特定需要 ,给出了一组与加密、解密、签名、认证和密钥分配等密码学操作有关的公理和推理规则 ,举例说明了这一逻辑框架在验证安全协议方面的应用 ,并讨论了需要进一步解决的问题 .
In this paper, a non monotonic dynamic logic that verifies properties of security protocols is introduced. In accordance with the specific requirement of information security, it provides axioms and inference rules about various cryptographic operations such as encryption, decryption, signature, authentication and key assignment. Several instances are given to illustrate its applications in security protocol verification. Open problems for further study are also discussed.
出处
《软件学报》
EI
CSCD
北大核心
2000年第2期213-221,共9页
Journal of Software
基金
国家 8 6 3高科技项目基金! (No.86 3- 30 6 - ZD- 10 - 0 2 )资助
关键词
信息安全
协议验证
INTERNET网
密码学
Information security, protocol verification, dynamic logic, non monotonic logic.