Modeling agreement problems in the universal composability framework

Agreement problems are one of the keys to distributed computing. In this paper, we propose a construction of the ideal-model functionality of one of the most important agreement problems, nonblocking atomic commitment (NBAC), in the universally-composability (UC) framework. NBAC is not only important in realizing dependable transactions in distributed computing environments but also useful in constructing security protocols that require the fairness property, such as fair exchange protocols. Our construction of NBAC functionality (namely FNBAC) is exactly equivalent to the NBAC definition; it is formally proved that a protocol UC-securely realizes FNBAC if and only if the protocol is an NBAC protocol. The proposed functionality and its proof of equivalence to NBAC enables the NBAC protocols to be used as a provably secure building block, and thus makes it much easier to feasibly and securely create higher-level protocols.