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

作者: Gerrit Rothmaier , Heiko Krumm

DOI:

关键词:

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

参考文章(12)
Catherine A. Meadows, Catherine A. Meadows, Formal Verification of Cryptographic Protocols: A Survey international cryptology conference. pp. 135- 150 ,(1994) , 10.1007/BFB0000430
C.R. Ramakrishnan, R. Sekar, Model-based analysis of configuration vulnerabilities Journal of Computer Security. ,vol. 10, pp. 189- 209 ,(2002) , 10.3233/JCS-2002-101-209
Gerard J. Holzmann, The SPIN Model Checker ,(2003)
Theodorus Cornelis Ruys, Towards effective model checking Universiteit Twente. ,(2001)
Michael Balser, Wolfgang Reif, Gerhard Schellhorn, Kurt Stenzel, Andreas Thums, Formal System Development with KIV fundamental approaches to software engineering. pp. 363- 366 ,(2000) , 10.1007/3-540-46428-X_25
Lester Randolph Ford, Flows in networks ,(1962)
Leslie Lamport, The temporal logic of actions ACM Transactions on Programming Languages and Systems. ,vol. 16, pp. 872- 923 ,(1994) , 10.1145/177492.177726
R.W. Ritchey, P. Ammann, Using model checking to analyze network vulnerabilities ieee symposium on security and privacy. pp. 156- 165 ,(2000) , 10.1109/SECPRI.2000.848453
Gerrit Rothmaier, Andre Pohl, Heiko Krumm, ANALYZING NETWORK MANAGEMENT EFFECTS WITH SPIN AND CTLA information security conference. pp. 65- 81 ,(2004) , 10.1007/1-4020-8143-X_5
Peter Herrmann, Heiko Krumm, A framework for modeling transfer protocols Computer Networks. ,vol. 34, pp. 317- 337 ,(2000) , 10.1016/S1389-1286(00)00089-X