This paper investigates the Lyapunov-based stability analysis and the construction of Lyapunov functions for Boolean networks (BNs) and establishes a new framework of Lyapunov theory for BNs via the semitensor product of matrices. First, we study how to define a Lyapunov function for BNs. A proper form of pseudo-Boolean functions is found, and the concept of (strict-) Lyapunov functions is thus given. It is shown that a pseudo-Boolean function in the proper form can play the role of Lyapunov functions for BNs, based on which several Lyapunov-based stability results are obtained. Second, we study how to construct a Lyapunov function for BNs and propose two methods for this problem: one is a definition-based method, and the other is a structure-based one. Third, the existence of strict-Lyapunov functions is studied, and a converse Lyapunov theorem as well as a necessary and sufficient condition are obtained for the asymptotical stability. Finally, as an application, the obtained results are applied to the stability analysis of switched Boolean networks. The study of illustrative examples shows that the new results/methods proposed in this paper work very well.