计算机科学
对手
匿名
计算机安全
对手模型
协议(科学)
对抗制
作者
Yoshishige Kawabe,Hideki Sakurada
出处
期刊:IEICE Transactions on Fundamentals of Electronics, Communications and Computer Sciences
[Institute of Electronics, Information and Communications Engineers]
日期:2008-04-01
卷期号:E91-A (4): 1112-1120
被引量:1
标识
DOI:10.1093/ietfec/e91-a.4.1112
摘要
The use of a formal method is a promising approach to developing reliable computer programs. This paper presents a formal method for anonymity, which is an important security property of communication protocols with regard to a user's identity. When verifying the anonymity of security protocols, we need to consider the presence of adversaries. To formalize stronger adversaries, we introduce an adversary model for simulation-based anonymity proof. This paper also demonstrates the formal verification of a communication protocol. We employ Crowds, which is an implementation of an anonymous router, and verify its anonymity. After describing Crowds in a formal specification language, we prove its anonymity with a theorem prover.
科研通智能强力驱动
Strongly Powered by AbleSci AI