Reasoning about minimal anonymity in security protocols
Anonymity, as an instance of information hiding, is one of the security properties intensively studied nowadays due to its applications to various fields such as electronic voting, electronic commerce, electronic mail, and so on. This paper presents a comprehensive study on minimal anonymity properties in security protocols. In order to reach this objective, an epistemic language and logic to reason about anonymity properties in security protocols, are provided. Agent states are endowed with facts derived from actions performed by agents in protocol executions, and an inference system is proposed. To define minimal anonymity, an observational equivalence is used, which is shown to be decidable in deterministic polynomial time. We distinguish between various forms of sender and receiver anonymity with respect to two types of observers: honest agents and the intruder. A large spectrum of relationships between these anonymity concepts is then derived. It is also shown that an anonymous action in a security protocol under a passive intruder might not be anonymous in the same security protocol if the intruder is active, and vice-versa. The decidability and complexity status of the anonymity concepts introduced in the paper is finally investigated. Thus, it is shown that minimal anonymity is undecidable in unrestricted security protocols, is NEXPTIME-complete in bounded security protocols, and is NP-complete in 1-session bounded security protocols.
anonymity cryptographic protocols