IoT-Geräte verfügen oftmals nur über geringe Rechen- und Speicher-Ressourcen. Dies erschwert die Erkennung von Cyberangriffen direkt am Gerät deutlich. Prävention durch eine frühzeitige Erkennung von potentiellen Schwachstellen ist daher essentiell. Eine rein funktionale Sicherheitsevaluierung ist dabei nicht ausreichend. Beispielsweise können Protokolle auch unter Verwendung von starken kryptographischen Primitiven durch die Art der Komposition der Kommunikation Sicherheitslücken aufweisen. Eine Methode, um strukturiert potentielle Sicherheitsprobleme aufzudecken, sind formale Verifikationsmethoden. Diese Technik beinhaltet logische und mathematische Methoden, mit der design-bedingte Schwachstellen frühzeitig erkannt werden können. Zwei Anwendungsfelder werden detaillierter betrachtet: Einerseits formale Verifikation von Sicherheitseigenschaften von IoTProtokollen und anderseits formale Methoden für eine Risikoanalyse einer IoT-Architektur am Beispiel der smarten Steuerung einer Wasserversorgungsinfrastruktur.