Trust Management in Strand Spaces: A Rely-Guarantee Method

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. Cryptographic protocol analysis has aimed primarily to determine what messages another principal must have sent or received, when one princ...

• Type: Conference
• Year: 2004
• Where: ESOP
• Authors: Joshua D. Guttman, F. Javier Thayer, Jay A. Carlson, Jonathan C. Herzog, John D. Ramsdell, Brian T. Sniffen
• Keywords: ESOP 2004, Programming Languages, Protocol Analysis, Strand Space Framework, Trust Management