The Wolf Within Iliano Cervesato 10.1184/R1/6610817.v1 https://kilthub.cmu.edu/articles/journal_contribution/The_Wolf_Within/6610817 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. 1985-06-01 00:00:00 computer sciences