A Formal Model for Network-Wide Security Analysis

Author

Matousek, Petr ; Rab, Jaroslav ; Rysavy, Ondrej ; Sveda, Miroslav

Author_Institution

Brno Univ. of Technol., Brno

fYear

2008

fDate

March 31 2008-April 4 2008

Firstpage

171

Lastpage

181

Abstract

Network designers perform challenging tasks with so many configuration options that it is often hard or even impossible for a human to predict all potentially dangerous situations. In this paper, we introduce a formal method approach for verification of security constraints on networks with dynamic routing protocols in use. A unifying model based on packet-filters is employed for modelling of network behaviour. Over this graph model augmented with filtering rules over edges verification of reachability properties can be made. In our approach we also consider topology changes caused by dynamic routing protocols.

Keywords

computer networks; filtering theory; graph theory; routing protocols; telecommunication network topology; telecommunication security; dynamic routing protocol; filtering rules; formal method; graph model; network behaviour modelling; network topology; network-wide security analysis; packet-filter; security constraint verification; Computer networks; Computer security; Condition monitoring; Conferences; Information filtering; Information filters; Network topology; Reachability analysis; Routing protocols; Testing; dynamic routing protocols; formal verification; netowrk design; network security; packet filters;

fLanguage

English

Publisher

ieee

Conference_Titel

Engineering of Computer Based Systems, 2008. ECBS 2008. 15th Annual IEEE International Conference and Workshop on the

Conference_Location

Belfast

Print_ISBN

0-7695-3141-5

Type

conf

DOI

10.1109/ECBS.2008.13

Filename

4492398