Abstract
Analysis methods for cryptographic protocols have often focused on information leakage rather than on seeing whether a protocol meets its goals. Many protocols, however, fall far short of meeting their goals, sometimes for quite subtle reasons