Modellierung und Verifikation kryptographischer Protokolle mit Zustandsautomaten
Im Rahmen des Aufbaustudiums nahm ich an einem Kryptographie-Seminar teil. Das von mir auszuarbeitende Thema beschäftigt sich mit der Modellierung und Verifikation kryptographischer Protokolle mit Zustandsautomaten.
Abstract: Kryptographische Protokolle spielen im täglichen Leben eine immer wichtigere Rolle. Doch für einen sicheren Einsatz der Protokolle ist es von entscheidender Bedeutung, dass die kryptographischen Verfahren korrekt sind. Da die menschliche Kontrolle nicht ausreichend ist, bedarf es einer automatisierten Überprüfung durch einen Computer. Diese Arbeit zeigt, wie kryptographische Protokolle weitestgehend automatisch veriziert werden können, indem die Protokolle auf endliche Zustandsautomaten übertragen werden. Nach den theoretischen Grundlagen wird abschließend gezeigt, wie das Needham-Schröder Protokoll mithilfe des Werkzeugs Murφ modelliert und verifiziert werden kann.
Die Seminararbeit ist hier vollständig nachlesbar: Modellierung und Verifikation kryptographischer Protokolle mit Zustandsautomaten
Stefan Schreinert ist seit über 10 Jahren in Bereich der Software-Entwicklung, strategischen IT-Beratung und eCommerce-Management tätig. Informationen über einige Projekte gibt es in der Kategorie "