Protocol
Security Analysis
A. Codes
B. Proofs
Theorem 6. Protocol 4.2 satisfies option correctness: If both the Alice and Bob are conforming, then if Alice does not exercise the right, Alice doesnโt lose the ๐ด๐ ๐ ๐๐ก๐ด and Bob doesnโt lose the ๐ด๐ ๐ ๐๐ก๐บ and ๐ด๐ ๐ ๐๐ก๐ต; or if Alice exercise the right, then Alice will receive ๐ด๐ ๐ ๐๐ก๐ต and Bob will receive ๐ด๐ ๐ ๐๐ก๐ด and ๐ด๐ ๐ ๐๐ก๐บ .
Proof. According to Protocol 4.2, it is evident that if Alice escrows her collateral in the ๐ถ๐๐๐ก๐๐๐๐ก๐ด contract and calls ๐๐ฅ๐๐๐๐๐ ๐ (), then a conforming Bob will reveal the pre-image ๐ต in ๐ถ๐๐๐ก๐๐๐๐ก๐ด to reclaim the guarantee ๐ด๐ ๐ ๐๐ก๐บ and Aliceโs collateral ๐ด๐ ๐ ๐๐ก๐ด. Subsequently, Alice can use ๐ต to obtain ๐ด๐ ๐ ๐๐ก๐ต. If Alice does not escrow the collateral, Bob will not reveal ๐ต. After the option expires at ๐๐ธ +2ฮ, Bob can call๐๐๐๐๐() and ๐๐ ๐ ๐ข๐๐ () on the respective chains to reclaim ๐ด๐ ๐ ๐๐ก๐บ and ๐ด๐ ๐ ๐๐ก๐ต.
Theorem 7. Protocol 4.2 satisfies exercisablity: During the transfer from Bob to Dave, the option remains active, allowing Alice to exercise the option without any delays.
Proof. According to Protocol 4.2.1, during the transfer from Bob to Dave, Alice can make a deposit and exercise her option at any time. If the transfer is in the Setup Phase, Bob will need to reveal ๐ต to fulfill his obligation and revoke the transfer. It is important to note that Dave can use ๐ต to reclaim ๐ ๐๐๐๐ ๐ . If the transfer is in the Attempt Phase and Bob acts maliciously by using ๐ต to take ๐ด๐ ๐ ๐๐ก๐บ , Alice can use ๐ต to obtain ๐ด๐ ๐ ๐๐ก๐ต. Dave will need to use ๐ต on ๐ถ๐๐๐ก๐๐๐๐ก๐ต to withdraw the transfer. Otherwise, when Dave uses ๐๐ to change the writer and the hash lock, he will reveal a new preimage secret ๐ท, which Alice can then use to obtain ๐ด๐ ๐ ๐๐ก๐ต.
Theorem 8. Protocol 4.2 satisfies failure compensation: Before expiration, Alice can exercise the option successfully, or if the exercise fails, she is compensated with the guarantee deposited by Bob.
Proof. By Theorem 6, if Alice successfully exercises her option, she will receive Bobโs collateral. Otherwise, after Alice makes a deposit and calls ๐๐ฅ๐๐๐๐๐ ๐ (), ๐ถ๐๐๐ก๐๐๐๐ก๐ด can invoke ๐๐ ๐ท๐๐๐๐ ๐๐ก๐๐ () to determine if the exercise has occurred. If Bob does not fulfill his obligation within a period of ฮ, Alice can call ๐๐๐๐๐() to obtain ๐ด๐ ๐ ๐๐ก๐บ as compensation, and Bob will lose his guarantee.
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.