Classical cryptosystems as vulnerabilities. Conventional cryptographic techniques are based on unproven assumptions concerning the computational hardness of certain mathematical principles. The growth of performance regarding the equipment of malicious attackers as well as mathematical efforts demand new requirements regarding the security of subsequent communications. The implementation of quantum algorithms enable quantum computers to breaking conventional cryptosystems in polynomial time. Thus, classical applications may be compromised in the future. QKD networks to bridge large distances. QKD relies on the particular fundamentals of quantum mechanics. It enables two adjacent communication partners to negotiate on an information theoretically secure quantum key that is provable secure over short distances, currently. However, QKD is limited to physical constraints. Therefore, we need QKD networks to overcome the limitations concerning the transmission capacity, the key generation rate, and the distance between two QKD nodes. QKD Networks are a promising solution but its implementation seems to be complex and requirements engineering in this field has not been sufficiently investigated, yet. Formalized QSRE. The development of large-scale QKD networks is challenging due to its complex characteristics. QKD networks are asynchronous, heterogeneous, non-deterministic, and provide parallel executions on a distributed architecture of QKD systems components. Formal methods are promising approaches to model QKD networks. We propose formalized quantum security ontologies, Petri nets and maintain a repository of formalized quantum security requirements. Moreover, we execute automated simulations on our QKD models. Thus, we show that formal methods are adequate solutions regarding the evaluation, and the prevention of vulnerabilities in large-scale QKD networks.