file.pdf (103.54 kB)

The Wolf Within

Download (103.54 kB)
journal contribution
posted on 01.06.1985, 00:00 by Iliano Cervesato
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.




Usage metrics