%0 Journal Article %A Cervesato, Iliano %D 1985 %T The Wolf Within %U https://kilthub.cmu.edu/articles/journal_contribution/The_Wolf_Within/6610817 %R 10.1184/R1/6610817.v1 %2 https://kilthub.cmu.edu/ndownloader/files/12102983 %K computer sciences %X 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. %I Carnegie Mellon University