Hi folks, Last year, the replacement cycling attack for LN became publicly known, presenting a complex challenge for the analysis of mempool and Lightning Network. Upon reviewing proposed solutions, it initially appears that they work; however, upon careful consideration, they turn out to be non-fixes. (I am currently going through the thread "OP_Expire and Coinbase-Like Behavior: Making HTLCs Safer by Letting Transactions Expire Safely.")
I'm interested in whether there are any tools or frameworks available for the automated cryptanalysis of this issue. Ideally, I would like to have a proof assistant to formally verify that, under specific assumptions, the Lightning Network is secure against funds loss. Another option is a framework that models a system of several nodes, potentially attacking each other. It would streamline the search for attack vectors automatically by trying different approaches randomly and identifying profitable behaviors. Known attacks could be used as test cases within such a framework. I tried to find existing work in this direction but didn't find anything. If you know of any, please send it to me. There is Scaling Lightning project [1] which runs several real nodes. It can be used to verify the findings. [1] https://github.com/scaling-lightning/scaling-lightning Thanks, Boris _______________________________________________ Lightning-dev mailing list Lightning-dev@lists.linuxfoundation.org https://lists.linuxfoundation.org/mailman/listinfo/lightning-dev
