Formale Modellierung und Analyse protokollbasierter Angriffe in TCP/IP Netzwerken am Beispiel von ARP und RIP.

Formale Modellierung und Analyse von netzwerkbasierten Angriffen ermoglichen zwar ein tieferes Verstandnis von Angriffsfolgen, sind aber meist so komplex, dass die Modellierung sehr aufwandig und eine Analyse mit automatischen Werkzeugen aufgrund der Grose des Zustandsraumes unmoglich ist. Wir stellen einen Ansatz vor, der Modelle fur praxisrelevante Angriffe und Szenarien mit vertretbarem Aufwand zu behandeln vermag. Dieser Ansatz kombiniert cTLA, ein Modellierungsframework und Optimierungsstrategien mit dem machtigen Modelchecker SPIN. Beispiele zu ARP und RIP zeigen die Anwendbarkeit auf.