Protocol
Security Analysis
A. Codes
B. Proofs
Lemma 9. The holder transfer procedure of Protocol 4.2.1 does not require Bobâs participation.
Proof. It is evident that, Alice does not own the exercise secret, holderâs transfer is required to replace the holder address and transfer public key, and the inconsistency of two chains will not harm the interest of Bob. According to the Protocol 4.1, Bob cannot use the transfer private key of Alice, i.e. ð ððŽ to claim assets. Therefore, during the reveal phase and consistency phase, Bob is not required to participate and not allowed to make any change on ð¶ððð¡ðððð¡ðŽ and ð¶ððð¡ðððð¡ðµ.
Lemma 10. If Bob and Dave are conforming, then the writer transfer procedure of Protocol 4.2.1 does not require Aliceâs participation.
Proof. Obviously, honest Bob will not leak two signatures or ð ððµ and honest Dave will submit signature ðð on both ð¶ððð¡ðððð¡ðŽ and ð¶ððð¡ðððð¡ðµ, Alice only needs to make operations when there is any dishonest party.
Theorem 2. Protocol 4.2.1 satisfies liveness: If Alice, Bob, and Carol/Dave are conforming, then Alice/Bob will obtain Carol/Daveâs collateral, Carol/Dave will obtain Alice/Bobâs position, and Bob/Alice will retain their original position.
Proof. By Lemma 9, Bobâs participation is not required during the holder transfer. If Alice and Carol are conforming, Carol will create ð¶ððð¡ðððð¡ð¶ contract and lock her collateral using signature of Alice before ðð» â 3Î. Alice will then reveal signature by ð ððŽ and callððð£ððð() onð¶ððð¡ðððð¡ð¶ atðð» â2Î. An honest Carol will forward the signature, setting the holder to Carol. Alice can then wait for 3Î withdrawl delayed period to obtain the collateral, while the writers ofð¶ððð¡ðððð¡ðŽ andð¶ððð¡ðððð¡ðµ are still Bob, Bob maintains the writerâs position. During the process where Bob transfers his position to Dave, if both parties are conforming, Bob will not expose two different signatures. After ðð + Î, Bob will not be obstructed and will surely obtain Daveâs collateral. Meanwhile, Dave can submit ðð betweenðð âÎ andðð to ð¶ððð¡ðððð¡ðŽ and ð¶ððð¡ðððð¡ðµ to change the writer, Alice retaining the holder position.
Theorem 3. Protocol 4.2.1 satisfies unobstructibility: Alice/Bob can transfer the position to another party even if Bob/Alice is adversarial.
Proof. By Lemma 9, Bobâs participation is not required, it is evident that Bob cannot block the process of transferring a holderâs position. During Bobâs transfer to Dave, Alice can only obtain Bobâs collateral by two different messages signed with ð ððµ or the exercise secret. If Bob is honest, he will neither leak ð ðµ, sign multiple messages nor leak exercise secret. Consequently, Alice cannot interrupt the transfer process.
Proof. After ðŽððððð transfers to ðŽððððð+1, the holder in the current optionâs ð¶ððð¡ðððð¡ðŽ and ð¶ððð¡ðððð¡ðµ is updated to Aliceð+1, and the transfer key is known only to ðŽððððð+1. Therefore, after a holder transfer, ðŽððððð+1 can transfer the position to ðŽððððð+2 by re-performing Protocol 4.2.1 with the transfer key of ðŽððððð+2. Similarly, after ðµððð transfers to ðµððð+1 (holder Alice does not contest within Î), the writer in the current optionâs ð¶ððð¡ðððð¡ðŽ and ð¶ððð¡ðððð¡ðµ is updated to Bobð+1. At this point, only ð ð ð+1 ðµ or its signatures can be used for the next transfer. ðµððð+1 can also transfer the position by re-performing Protocol 4.2.1 with the new transfer key.
Lemma 11. Protocols 4.2.1 satisfy atomicity: If conforming Alice/Bob loses their position, she/he will be able to obtain Carol/Daveâs collateral.
Proof. Following Theorem 2, in transferring the holder position, after Carol correctly escrows the collateral, Alice temporarily locks the holder position in both contracts using ð»(ð¶). If Carol uses ð¶ to obtain the position before ðð» , then Alice will obtain Carolâs collateral at ðð» + Î. If Carol does not reveal ð¶ before ðð» , Alice will not receive Carolâs collateral. Similarly, in transferring the writer position, if Bob does not reveal his signature honestly, then Bob will lose the position and Dave can retrieve and will not lose the collateral. If honest Bob signs for a buyer Dave, the honest Dave will use the signature to obtain Bobâs position at ðð . Bob will then obtain Daveâs collateral at ðð + Î.
B.1.1 Safety.
Proof. In the ð¶ððð¡ðððð¡ðŽ, the following elements are defined:
⢠ððž: The expiration time of this option.
⢠exercise_hashlock: The hash lock of this option, which is the hash of a secret value known only to the writer.
⢠old_exercise_hashlock: The hash lock of this option, which is the hash of a secret value known only to the writer.
⢠holder: The holder can call ðð¥ððððð ð () to exercise the option before ððž.
⢠guarantee: The writerâs asset, i.e. ðŽð ð ðð¡ðº , which can be any asset mutually agreed upon by the holder and writer as guarantee. This can include tokens, NFTs, or any other type of asset.
⢠writer: The writer can use the secret value to call ðð ð ð¢ðð () to retrieve the guarantee or retrieve it directly after ððž + 2Î.
⢠collateral: The collateral that Alice must deposit if she decides to exercise the option to purchase Bobâs asset.
⢠holder_transfer_public_key: the transfer key of Alice, ðððŽ, used for verify the transfer signature of Alice to Carol.
⢠writer_transfer_public_key: New transfer key of Dave, ððð· , used for verify the transfer signature of Dave to others.
⢠old_writer_transfer_public_key: Old transfer key of Bob, ðððµ, used for verify the transfer signature of Bob to Dave, Within the period of one Î, during which the transfer signature must be submitted to this contract, we still need to record the old transfer public key in case of Bobâs misbehavior.
⢠writer_transfer_time: The writer transfer time, used for Alice to claim assets if there exits misbehavior of Bob.
In the ð¶ððð¡ðððð¡ðµ, there are other additional items:
⢠collateral: The writerâs collateral, i.e.ðŽð ð ðð¡ðµ, it can be claimed by holder with preimage of hashlock.
⢠holder: The holder can call ðð¥ððððð ð () to exercise the option before ððž.
⢠writer: The writer can callðð ð ð¢ðð () to retrieve the guarantee or retrieve it directly after ððž + 2Î.
In the ð¶ððð¡ðððð¡ð· , the following elements are defined:
⢠T_W: The deadline for seller to reveal signature.
⢠buyer: writer position buyer, i.e. Dave.
⢠seller: writer position seller, i.e. Bob.
⢠old_exercise_hashlock: The hashlock of exercise, if Bob reveals during the transfer, Dave is able to reclaim with preimage.
⢠exercise_hashlock: The new hashlock of exercise, generated by Dave.
⢠old_writer_transfer_public_key: Bobâs transfer public key, used for verify the signature of Bob.
⢠writer_transfer_public_key: New transfer public key generated by Dave, used for replacing Bobâs key.
⢠transfer_time: Used for record the time of transfer (the time reveal signature) and calculate the withdrawal delayed period.
Take Bob transferring his position to Dave as an example, since Bob deposit ðŽð ð ðð¡ðº and ðŽð ð ðð¡ðµ into the contracts, which is more complex. Transferring Aliceâs position to Carol is more simple.
By Lemma 11, if compliant Bob loses his position, he will at least obtain Daveâs collateral during the writer transfer process.
If Dave is conforming, then if Bob acts maliciously on his own, Bob provides two different signatures to different buyers, Dave can reclaim the transfer fee with extracted ð ððµ since ð· records old_writer_transfer_public_key i.e. ðððµ. If Bob reveals ðµ at the same time during transfer process, then Dave can use ðµ to reclaim ð ððð¡ððð¹ðð since ð¶ððð¡ðððð¡ð¶ records old_exercise_hashlock i.e. ð»(ðµ). If Alice and Bob collude, they can use ð ððµ or ðµ to withdraw ðŽð ð ðð¡ðº and ðŽð ð ðð¡ðµ. Then, Dave can observe ð ððµ or ðµ and withdraw ð ððð¡ððð¹ðð during withdrawal delay period since ð¶ððð¡ðððð¡ð· records transfer_time.
If Alice is conforming, then If Bob provides two different signatures to different buyers, Alice can extract ð ððµ and submit it to obtain ðŽð ð ðð¡ðº and ðŽð ð ðð¡ðµ. If Bob or Dave publishes one signature exclusively on either ð¶ððð¡ðððð¡ðŽ or ð¶ððð¡ðððð¡ðµ, Alice can forward this signature to another chain to make sure the exercise secret hashlocks are consistent on two chains. If Bob and Dave collude, they use two signatures to change the hashlock. During the withdrawal delay period, Alice can obtain ðŽð ð ðð¡ðº and ðŽð ð ðð¡ðµ using the extracted ð ððµ.
Transferring Aliceâs position to Carol is simpler, as Alice does not deposit assets into the option contracts and cannot modify the exercise secret hashlock. Carol only needs to ensure consistency between the holders on the two chains. Otherwise, she can extract ð ððŽ and refund the ð»ðððððð¹ðð during the withdrawal delay period.
Theorem 5. Protocol 4.2.2 satisfies isolation: Alice and Bob can simultaneously and separately transfer their positions to Carol and Dave, respectively. This means that transferring holder and the transferring writer can proceed concurrently.
Proof. Suppose both Carol and Dave are interested in Aliceâs and Bobâs positions, respectively. According to Lemma 9, Alice transferring to Carol does not require Bobâs involvement, hence Alice and Carol will not be interfered with. Similarly, it is known that during Bobâs transfer to Dave, by Lemma 10, if Bob and Dave are both compliant, Alice does not need to participate. Considering the case when Bob reveals two different signatures: (i) If Carol has already revealed the secret value ð¶ of the transfer hash lock, then Carol becomes the new holder and can use two different signatures by ð ðµ to obtain ðŽð ð ðð¡ðµ and ðŽð ð ðð¡ðº . (ii) If Carol has not revealed ð¶ and will reveal it after Î, Carol can simultaneously revealð¶ and call ððððððð() on both chains after Î to obtain ðŽð ð ðð¡ðµ and ðŽð ð ðð¡ðº . If Dave or Bob publishes ðð on one single chain, Carol must forward ðð to the other chain while revealing ð¶.
Authors:
(1) Zifan Peng, The Hong Kong University of Science and Technology (Guangzhou) Guangzhou, Guangdong, China ([email protected]);
(2) Yingjie Xue, The Hong Kong University of Science and Technology (Guangzhou) Guangzhou, Guangdong, China ([email protected]);
(3) Jingyu Liu, The Hong Kong University of Science and Technology (Guangzhou) Guangzhou, Guangdong, China ([email protected]).
This paper is available on arxiv under CC BY 4.0 license.