Formal ontology-based quantum security requirements engineering by Petri nets

Abstract

Klassische Kryptographie als Schwachstelle. Konventionelle kryptographische Methoden basieren auf derzeit unbewiesenen Annahmen hinsichtlich der komplexitätstheoretischen Härte mathematische Probleme zu lösen. Aufgrund der technischen Evolution bei Leistungsindikatoren von Computersystemen sowie dem mathematischen Fortschritt ist es wahrscheinlich möglich diese unbewiesenen mathematischen Annahmen zu brechen. Quantencomputer sind imstande derartige Lösungen zu brechen, da die Implementierung von Quantenalgorithmen die Kompromittierung klassischer kryptographischer Methoden ermöglicht. Daher sind konventionelle Anwendungen gefährdet. Quantennetzwerke für große Distanzen. Quantenkryptographie ist auch als Quantenschlüsselverteilung (QKD) bekannt und ermöglicht Kommunikationspartnern derzeit über kurze Distanzen informationstheoretisch und daher beweisbar sichere Kryptographieschlüssel zu erzeugen. Um die QKD-Einschränkungen bezüglich der Übertragungsdistanz, der Schlüsselgenerierungsrate und der Übertragungskapazität zu überwinden stellen QKD-Netzwerke eine vielversprechende aber komplexe Lösung dar. Daher ist die Entwicklung herausfordernd und Requirements Engineering für QKD-Netzwerke anspruchsvoll und zudem nicht hinreichend untersucht. Formalisiertes Requirements Engineering für QKD-Netzwerke. Die experimentelle Entwicklung großer QKD-Netzwerke ist unausgereift. Zudem erfordern die vielseitigen Eigenschaften wie Asynchronität, Heterogenität, Non-Determinismus, Parallelismus und Verteilung der Systemkomponenten neue Lösungen im Security-Requirements-Engineering. Formale Methoden wie Ontologien und Petri Netze erscheinen intuitiv als die idealen Lösungen zur Ableitung formalisierter Anforderungen und Umsetzung automatisierter Simulationen für QKD-Netzwerke. Anhand der Entwicklung, Formalisierung und Simulation von Quantum-Security-Requirements zeigen wir, dass die erörterten formalisierten Methoden erfolgsversprechende Lösungen zur Evaluierung und aktiven Vermeidung von Sicherheitslücken in QKD-Netzwerken darstellen.

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.