Trust Management in Strand Spaces: A Rely-Guarantee Method
| Title | Trust Management in Strand Spaces: A Rely-Guarantee Method |
| Publication Type | Conference Paper |
| Year of Publication | 2004 |
| Authors | Guttman, Joshua D., Javier F. Thayer, Jay A. Carlson, Jonathan Herzog, John D. Ramsdell, and Brian T. Sniffen |
| Editor | Schmidt, David |
| Conference Name | Programming Languages and Systems: 13th European Symposium on Programming |
| Publisher | Springer |
| Abstract | We show how to combine trust management theories with
nonce-based cryptographic protocols. The strand space framework for
protocol analysis is extended by associating formulas from a trust management logic with the transmit and receive actions of the protocol principals. The formula on a transmission is a guarantee; the sender must
ensure that this formula is true before sending the message. The formula
on a receive event is an assumption that the recipient may rely on in
deducing future guarantee formulas. The strand space framework allows
us to prove that a protocol is sound, in the sense that when a principal
relies on a formula, another principal has previously guaranteed it. We
explain the ideas in reference to a simple new electronic commerce protocol, in which a customer obtains a money order from a bank to pay a
merchant to ship some goods. |
| URL | http://files.jonathanherzog.com/guttman_trust.pdf |
