The distributed nature and complexity of computer networks and various services provided via them, makes the networks vulnerable to numerous attacks. The TCP/IP presumptions which are based on using this protocol to provide a simple, open communication infrastructure in an academic and collaborative environment, causes this protocol lack of built-in mechanisms for authentication, integrity and privacy. Even though in the last few years a more systematic approach to TCP/IP network security problem has been followed, a formal approach to this problem is lacking. In this paper, we propose using Description Logics as a formal model which could be used to analyze TCP/IP networks against attacks. Moreover we have presented a case study which models one of famous attack categories, i.e. Man in the Middle (MITM). This model lets automatically verify and proof network safety or vulnerability against this attack.