A semantics for a logic of authentication (extended abstract) 论文

摘要

Abstract: Burrows, Abadi, and Needham have proposed a logic for the analysis of authentication protocols. It is a logic of belief, with special constructs for expressing some of the central concepts used in authentication. The logic has revealed many subtleties and serious errors in published protocols. Unfortunately, it has also created some confusion. In this paper, we provide a new semantics for the logic, our attempt to clarify its meaning. In the search for a sound semantics, we have identi ed many sources of the past confusion. Identifying these sources has helped us improve the logic's syntax and inference rules, and extend its applicability. One of the greatest di erences between our semantics and the original semantics is our treatment of belief as a form of resource-bounded, defeasible knowledge. 1