This dissertation presents a physical layer-inspired approach to the design, implementation, and formal verification of security protocols tailored for ‘Internet-of-Things(IoT)’ devices, introducing the ComPass protocol as a key contribution. ComPass leverages the inherent randomness of wireless channels to generate shared passphrases between devices, reducing the need for user-generated passwords and mitigating vulnerabilities associated with weak passwords, while also offering a new direction for network-level onboarding for resource-constrained devices. Additionally, ASOP, an application-level device onboarding protocol is proposed that operates independently of manufacturers or third-party certificate authorities. ASOP enhances security and future-proofs IoT systems through the integration of post-quantum cryptography primitives. Beyond protocol design, this dissertation also evaluates the effectiveness of passphrases. This analysis begins by defining key concepts in information measurement, such as entropy, the standard metric for quantifying information content. We review several entropy estimation algorithms, including those from the widely recognized NIST entropy estimation tool. To address gaps in current metrics, we introduce a metric, termed Expectation entropy, as well as the concept of Remaining entropy. This discussion on Remaining entropy aims to establish a relationship between Shannon entropy, min-entropy, and Jensen’s inequality, providing a more understanding of information security in passphrase generation. The dissertation further explores the application of new protocols in smart city contexts, particularly within the healthcare sector. Here, Ultra-Wideband (UWB) technology, combined with the Permission Voucher protocol, is proposed as a solution for creating privacy-preserving and resilient communication systems. To verify the security of the above mentioned protocols, formal analysis is conducted within symbolic model using the Tamarin Prover, demonstrating their resistance to common attack vectors and identifying potential areas for improvement, such as mitigating insider threats and enhancing key management.
Diese Dissertation stellt einen von dem „Physical Layer“ inspirierten Ansatz für den Aufbau, die Implementierung und die formale Verifizierung vonSicherheitsprotokollen dieauf ’Internet-of-Things’-Geräte ausgerichtet sind vor, und stellt das ComPass-Protokoll als einen wichtigen Beitrag vor. ComPass nutzt die inhärente Zufälligkeit drahtloser Kanäle, um gemeinsame Passphrasen zwischen Geräten zu generieren, wodurch der Bedarf an benutzergenerierten Passwörtern reduziert und die mit schwachen Passwörtern verbundenen Schwachstellen gemildert werden, während gleichzeitig eine neue Richtung für das Onboarding auf Netzwerkebene für ressourcenbeschränkte Geräte vorgeschlagen wird. Darüber hinaus wird in dieser Arbeit das ASOP-Protokoll untersucht, ein Onboarding-Protokoll für Geräte auf Anwendungsebene, das unabhängig von Herstellern oder Zertifizierungsstellen Dritter funktioniert. ASOP erhöht die Sicherheit und Zukunftssicherheit von IoT-Systemen durch die Integration von Post-Quantum-Kryptographie -Primitiven. Über das Protokolldesign hinaus wird auch die Bewertung der Wirksamkeit von Passphrasen urchgeführt. Die Analyse der Passphrasen beginnt mit der Definition der Schlüsselkonzepten, der Informationsmessung, wie der Entropie. Es werden verschiedene Algorithmen zur Entropieschätzung untersucht, darunter auch die des anerkannten NIST-Tools zur Entropieschätzung. Um Lücken in den aktuellen Metriken zu schließen, wird eine neue Metrik vorgestellt, die als Expectation entropy bezeichnet wird, sowie das Konzept der Remaining entropy. Ziel der Remaining entropy ist es, das Potenzial für die Herstellung einer Verbindung zwischen Shannon-Entropie, Min-Entropie und Jensen’s Ungleichung zu untersuchen. In dieser Dissertation wird auch die Anwendung neuer Sicherheitsprotokolle im Smart-City-Kontext, insbesondere im Gesundheitswesen, untersucht. Hierfür wird die UWB in Kombination mit dem Permission Voucher Protokoll als Lösung für die Realisierung von Privatsphäre-erhaltenden und robusten Kommunikationssystemen vorgeschlagen. Um die Sicherheit dieser Protokolle zu überprüfen, wird eine formale Analyse mittels des Tamarin Provers durchgeführt, die ihre Widerstandsfähigkeit gegen gängige Angriffsvektoren demonstriert und potenzielle Verbesserungsmöglichkeiten aufzeigt. Ein Beispiel hierfür ist die Abschwächung von Insider-Bedrohungen und die Verbesserung der Schlüsselverwaltung.
