10.1184/R1/6603269.v1 Iliano Cervesato Iliano Cervesato Catherine Meadows Catherine Meadows Dusko Pavlovic Dusko Pavlovic An Encapsulated Authentication Logic for Reasoning About Key Distribution Protocols Carnegie Mellon University 1965 computer sciences 1965-01-01 00:00:00 Journal contribution https://kilthub.cmu.edu/articles/journal_contribution/An_Encapsulated_Authentication_Logic_for_Reasoning_About_Key_Distribution_Protocols/6603269 Authentication and secrecy properties are proved by very different methods: the former by local reasoning, leading to matching knowledge of all principals about the order of their actions, the latter by global reasoning towards the impossibility of knowledge of some data. Hence, proofs conceptually decompose in two parts, each encapsulating the other as an assumption. From this observation, we develop a simple logic of authentication that encapsulates secrecy requirements as assumptions. We apply it within the derivational framework to derive a large class of key distribution protocols based on the authentication properties of their components.