Paper 2025/1560 Original: eprint.iacr.org/2025/1560 ↗

On the Termination of the HotStuff Protocol Within the Universally Composable Framework

Abstract

HotStuff has gained widespread application in scenarios such as consortium chains in recent years due to its linear view change and pipelined decision making mechanisms. Although there have been studies on the performance of this algorithm, there remains a lack of analysis and formal termination proofs regarding its composability. This paper, for the first time, constructs a comprehensive formal system for the HotStuff protocol in a partially synchronous network environment under the Universally Composable (UC) framework and proves the termination of the HotStuff protocol within the UC framework. Specifically, we establish the ideal function and demonstrate that the HotStuff protocol UC realizes this ideal function, which guarantees the indistinguishability between the real protocol of HotStuff and the ideal function. Notably, in the context of network delay attacks, this paper uses a phased time analysis method with an exponential backoff timeout mechanism to show that the protocol can still achieve consensus within a bounded amount of time. The results of this work not only establish a formal proof paradigm for analyzing termination of BFT protocols in a composable framework, but also provide important theoretical foundations for ensuring reliable termination in industrial-grade blockchain systems (such as the Meta Diem project and Chang’an Chain that employ HotStuff).