Cryptographic protocols are the cornerstone of security in distributedsystems. The formal analysis of their properties is accordingly one of thefocus points of the security community, and is usually split among two groups.In the first group, one focuses on trace-based security properties such asconfidentiality and authentication, and provides decision procedures for theexistence of attacks for an on-line attackers. In the second group, one focuseson equivalence properties such as privacy and guessing attacks, and providesdecision procedures for the existence of attacks for an offline attacker. Inall cases the attacker is modeled by a deduction system in which his possibleactions are expressed. We present in this paper a notion of finitary deductionsystems that aims at relating both approaches. We prove that for such deductionsystems, deciding equivalence properties for on-line attackers can be reducedto deciding reachability properties in the same setting.
展开▼
