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.