This story draft by @escholar has not been reviewed by an editor, YET.
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.