An Encapsulated Authentication Logic for Reasoning About Key Distribution Protocols
journal contributionposted on 01.01.1965 by Iliano Cervesato, Catherine Meadows, Dusko Pavlovic
Any type of content formally published in an academic journal, usually following a peer-review process.
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.