Transcript ppt
Advantage and abuse-freeness in contract-signing protocols Rohit Chadha, John Mitchell, Andre Scedrov, Vitaly Shmatikov To appear in CONCUR 2003 Contract-signing protocols Two parties want to exchange signatures on preagreed texts over the internet Signers adversarial Both signers want to exchange signatures Neither wants to sign first Fairness • Each signer gets the other’s signature or neither does Timeliness: • No signer gets stuck Abuse-freeness: • No party can prove to an outside party that it can control the outcome Optimism Two categories of contract-signing protocols: • Gradual release protocols • Fixed-round protocols Fairness requires a third party, T • Even 81, FLP Trivial protocol • Send signatures to T which then completes the exchange Optimistic 3-party protocols • T contacted only for error recovery • Avoids communication bottlenecks Optimistic signer • Prefers not to go to T General protocol outline Willing to sell stock at this price OK, willing to buy stock at this price B Here is my signature C Here is my signature Trusted third party can force or abort the exchnage • Third party can declare exchange binding if presented with first two messages. Optimism and advantage Once customer commits to the purchase, he cannot use the committed funds for other purposes Customer likely to wait for some time for broker to respond: contacting T to force the exchange is costly and can cause delays Since broker can abort the exchange, this waiting period may give broker a way to profit: see if shares are available at a lower price The longer the customer is willing to wait, the greater chance the broker has to pair trades at a profit Broker has an advantage: she can control the outcome of the protocol Related work Need for trusted third party • Even 81 Mitchell and Shmatikov (Financial Crypto 2000) used Mur, a finite-state model checker, to analyze two signatureexchange protocols • Asokan-Shoup-Waidner (IEEE Symposium on Security and Privacy, 98) • Garay-Jakobsson-Mackenzie Protocol(GJM) (Crypto 1999) Chadha, Kanovich and Scedrov used MSR to analyze GJM protocol • Proved fairness • Defined and proved balance for honest participants Kremer and Raskin used model-checkers to study a version of abuse-freeness (CSFW 2002) Fairness, optimism, and timeliness Model and fairness We consider only single runs of the protocol Call the two participants P and Q Definitions lead to game-theoretic notions • If P follows strategy, then Q cannot achieve win over P • Or, P follows strategy from some class … A strategy of P is Q-silent if it succeeds whenever Q does nothing Need timeouts in the model “waiting” • The signers use timeouts to decide when to contact T Fairness for P • If Q has P’s contract, then P has a strategy to get Q’s contract Timeliness A protocol is timely for P if • For all reachable states, S, P has a (Q -silent) strategy to drive the protocol to a state S’ such that either P gets Q’s signature or Q cannot obtain P’s signature by talking to T • Protocol is timely if it is timely for both signers Optimism Protocol is optimistic for Q if, assuming P controls the timeouts of both Q and P, then and honest Q has a strategy to get honest P’s contract without any messages to/from T • The signers use timeouts to decide when to contact T • If P is willing to wait “long enough” for Q, then Q may exchange signatures with P without T getting involved Protocol is optimistic if it is optimistic for both signers Optimistic participant A participant P is honest if it follows the protocol Honest P is said to be optimistic if • Whenever P can choose between – waiting for a message from Q – contacting T for any purpose P waits and allows Q to move next • Modeled by giving the control of timeouts to Q Advantage Q is said to have the power to abort against an optimistic P in S • if Q has a strategy to prevent P from getting Q’s signature Q is said to have the power to resolve against an optimistic P in S • if Q has a strategy to get P’s signature Q has advantage against an optimistic P if Q has both the power to abort and the power to resolve Hierarchy Advantage against honest P H-adv Advantage against optimistic P O-adv Exchange subprotocol in GJM O R I am willing to sign may abort I am willing to sign Here is my signature may resolve may quit Here is my signature may resolve Advantage flow in GJM O R I am willing to sign O-adv O-adv I am willing to sign Here is my signature Here is my signature Impossibility theorems GJM is balanced for honest participants • No participant has an advantage In any optimistic and fair protocol • Some potentially dishonest participant has an advantage over its optimistic counterparty In any optimistic, fair, and timely protocol • Any potentially dishonest participant has an advantage at some non-initial point over its optimistic counterparty Abuse-freeness No evidence of advantage If • Q can provide evidence of P’s participation to an outside observer X, then • Q does not have advantage against an optimistic P • The protocol is said to be abuse-free Evidence: what does X know X knows fact in state • is true in any state consistent with X’s observations in Advantage flow in GJM O R I am willing to sign O-adv O-adv I am willing to sign Here is my signature Here is my signature Exchange subprotocol in Boyd-Foo O R I am willing to sign Here is my signature may resolve Here is my signature R may request T to enforce the exchange Advantage flow in BF O R I am willing to sign H-adv Here is my signature Here is my signature A non abuse-free protocol O T My signature R My signature Release sigs? Yes R’s signature O’s signature O can present message from T to C as proof of R’s participation Relationship between various properties Secure for optimistic signer Secure for honest signer Abuse-Free Fair Weak abuse-freeness The only proof of participation of P is P’s contract A protocol is weakly abuse-free for P if in any reachable state S where Q has received P’s contract, Q does not have advantage over P If a protocol is fair for P , then it is weakly abuse-free for P Conclusions A model to study contract signing protocols • • • • • • Use multiset rewriting framework Used timers to reflect natural bias Formal definitions of fairness and effectiveness given Natural bias: optimistic signers defined Give game-theoretic definitions of advantage and balance Advantage flows in GJM and BF Show that the addition of the third party does not guarantee balance Use epistemic logic to formalize abuse-freeness Further work Multiparty signature exchange protocols to be investigated Other properties like trusted-third party accountability to be investigated Use of automated theorem provers based on rewriting techniques • Maude developed by Denker, Lincoln, Meseguer, Eker, Clavel, etc. Explore solutions other than abuse-freeness to address lack of balance • Estimate cost of asymmetry Interested participant Honest P is said to be interested if • Whenever P can choose between – waiting for a message from Q – quitting or contacting T to abort P waits and allows Q to move next Modeled by giving the control of abort timeouts to Q Hierarchy Advantage against honest A H-adv Advantage against interested A I-adv Advantage against optimistic A O-adv