Digital libraries (DL) are starting to play a central role in traditional libraries as well as becoming an important tool for publishers to present and sell their products. A lot of research has been carried out to study the usability and data representation in DL and has led to the development of a variety of software packages, both commercial and open source. However, very little research has focused on formal aspects of DL. This paper describes our attempt to formally specify DL using the RAISE Specification Language (RSL). The specification methodology, inspired by the 5S Framework defined by Gonccalves et al. [7], is kept at a fairly abstract level and aims to provide a basic model of the key DL issues (digital objects, collections, users and communities) as well as their relations within the DL framework and the implication of such relations in terms of security and human-computer interactions.