Distributed contract signing over a network involves many challenges in mimicking the features of paper contract signing. For instance, a paper contract is usually signed by both parties at the same time and at the same place, but distributed electronic transactions over a network is inherently asymmetric in that someone has to send the first message. Several digital contract-signing protocols have been devised in order to overcome this basic asymmetry and to achieve symmetric properties such as fairness, namely: 1) if nothing goes wrong, both participants receive a valid contract, 2) every participant may complete the protocol, and 3) either both participants receive a valid contract or neither one does. Such protocols often involve a trusted third party that can enforce the contract after it witnesses a partial completion of the protocol. In optimistic contract-signing protocols the trusted third party is contacted only in case of a dispute, otherwise the protocol can be completed without involving the third party. Such protocols involve several subprotocols that allow a contract to be signed normally or aborted or resolved by the trusted third party. Another kind of symmetry desirable in distributed contract signing was identified by Garay, Jakobsson, and MacKenzie: a fair protocol is said to be abuse-free if, at any stage of the protocol, it is impossible for any participant, say A, to be able to prove to an outside challenger that A has the power to choose between completing the contract and aborting it. A formal analysis of the Garay-Jakobsson-MacKenzie two-party contract-signing protocol was carried out by Mitchell and Shmatikov using a finite state verification tool. They showed that negligence of the trusted third party may lead to loss of abuse-freeness or fairness. Based on their analysis, Mitchell and Shmatikov also suggested a revision of the protocol. This revised version is our reference point. We study an approximation of the abuse-freeness property, namely, at any stage of a fair protocol, any protocol participant does not have an advantage over its counterparty in the sense that it has both the power to complete the contract as well as the power to abort it. As noted by Mitchell and Shmatikov, this property is not trace-based. We use a multiset-rewriting formalism for protocol analysis to formally state an approximation of this property in terms of a certain recursive property of the protocol execution tree, which we then prove by inductive methods. Our proof relies on a strong notion of fairness adopted from which itself we formally state in the multiset-rewriting formalism and prove by inductive methods. We also show that our approximation of abuse-freeness, even though it is not a trace-based property, it may nevertheless be represented in by means of provability in a logical system, in the multiplicative additive fragment of linear logic, in which formal derivations correspond to full protocol execution trees and vice versa. This work was carried out in collaboration with Max Kanovich and Andre Scedrov. We also discuss current work in progress with John Mitchell, Andre Scedrov, and Vitaly Shmatikov. We strengthen the definition of abuse-freeness in two ways. We consider strategies against honest participants interested in completing the contract and whose actions display a bias toward a positive outcome. We suggest a formulation of "evidence to an outside participant" by means of epistemic logic.