Politecnico di Torino
The authors present a calculus for detecting guessing attacks, based on oracles that instantiate cryptographic functions. Adversaries can ob-serve oracles, or control them either on-line or off-line. These relations can be established by protocol analysis in the presence of a Dolev-Yao intruder, and the derived guessing rules can be used together with standard intruder deductions. Their rules also handle partial verifiers that t more than one secret. They show how to derive a known weakness in the Anderson-Lomas protocol, and new vulnerabilities for a known faulty ATM system.