The Wolf Within

A formal specification of a security protocol cannot be limited to listing the messages exchanged. In MSR, each construct is associated with typing and data access specification (DAS) rules, which describe under which circumstances a principal can access keys and other information. A protocol specification is completed with a description of the intruder in the style of Dolev and Yao, the wolf in the protocol world. In this paper, we show that the protocol determines the intruder: the wolf is deep within. More precisely we show that the Dolev-Yao intruder rules can be automatically reconstructed from the DAS rules, and that the DAS rules can themselves be inferred from annotated typing declarations for the various message constructors.