Das Design und die Analyse der sicheren Kommunikationsprotokolle haben sich als nichttriviale Aufgabe erwiesen. Der Beweis der Sicherheit einfacher kryptographischer Protokolle ist üblicherweise sehr komplex. Viele Protokolle wurden ohne theoretische Rechtfertigung, d.h. ohne formalen Sicherheitsbeweis, entwickelt. Dies umfasst etwa die Protokolle TLS/SSL, IPSec oder Kerberos. Aus diesem Grund gibt es in regelmäßigen Abständen Angriffe auf diese Protokolle. Daher ist die Analyse bestehender Protokolle, sowie der Entwurf theoretisch fundierter kryptographischer Protokolle von großer Wichtigkeit, wenn man solche Angriffe vermeiden möchte. Diese Arbeit beschäftigt sich mit Design und Analyse kryptographischer Protokolle in den aktuell gängigsten Sicherheitsmodellen. Wir zeigen, wie man Kommunikationsprotokolle systematisch konstruieren und analysieren kann, insbesondere für authentifizierte Schlüsselaustauschprotokolle in realitätsnahen Modellen.