|
Published Articles >> Table of Contents >> Abstract
14th IEEE Computer Security Foundations Workshop (CSFW'01)
p. 0241
A Compositional Logic for Protocol Correctness
Nancy Durgin, Stanford University
John Mitchell, Stanford University
Dusko Pavlovic, Stanford University
Full Article Text:
  
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/CSFW.2001.930150
Send link to a friend
| Abstract |
|
We present a specialized protocol logic that is built around a process language for describing the actions of a protocol. In general terms, the relation between logic and protocol is like the relation between assertions in Floyd-Hoare logic and standard imperative programs. Like Floyd-Hoare logic, our logic contains axioms and inference rules for each of the main protocol actions and proofs are protocol-directed, meaning that the outline of a proof of correctness follows the sequence of actions in the protocol. We prove that the protocol logic is sound, in a specific sense: each provable assertion about an action or sequence of actions holds in any run of the protocol, under attack, in which the given actions occur. This approach lets us prove properties of protocols that hold in all runs, while explicitly reasoning only about the sequence of actions needed to achieve this property. In particular, no explicit reasoning about the potential actions of an attacker is required.
|
 Additional Information
|
Citation:
Nancy Durgin, John Mitchell, Dusko Pavlovic,
"A Compositional Logic for Protocol Correctness,"
csfw,
p. 0241,
14th IEEE Computer Security Foundations Workshop (CSFW'01),
2001
|
|
