Reliability Block Diagrams (RBDs) allow us to model the failure relationships of complex systems and their sub-components and are extensively used for system reliability, availability, dependability and maintainability analyses. Traditionally, these RBD-based analyses are done using paper-and-pencil proofs or computer simulations, which cannot ascertain absolute correctness due to their inherent limitations. As a complementary approach, we propose to use the higher-order-logic theorem prover HOL to conduct RBD-based analysis. For this purpose, we present a higher-order-logic formalization of commonly used RBD configurations, i.e., series, parallel, parallel-series and series-parallel, and the formal verification of their equivalent mathematical expressions. A distinguishing feature of the proposed RBD formalization, is the ability to model nested RBD structures, i.e., a RBD block could itself be a RBD. This generality allows us to formally analyze the reliability of many real-world systems. For illustration purposes, we have formally analyzed the reliabilities of a oil/gas pipeline, exhibiting the series RBD, and a generic Virtual Data Center (VDC) in a cloud computing infrastructure exhibiting the nested series-parallel RBD.