A Formal Model for Network-wide Security Analysis
Result description
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 ofsecurity 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
networksecuritymodellingfiltering rulesreachability analysis
The result's identifiers
Result code in IS VaVaI
Result on the web
—
DOI - Digital Object Identifier
—
Alternative languages
Result language
angličtina
Original language name
A Formal Model for Network-wide Security Analysis
Original language description
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 ofsecurity 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.Czech name
Formální model a analýza bezpečnosti v počítačové síti
Czech description
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 ofsecurity 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.
Classification
Type
D - Article in proceedings
CEP classification
JC - Computer hardware and software
OECD FORD branch
—
Result continuities
Project
GA102/08/1429: Safety and security of networked embedded system applications
Continuities
Z - Vyzkumny zamer (s odkazem do CEZ)
Others
Publication year
2008
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Proceeding of the 15 IEEE International Symposium and Workshop on the Engineering of Computer-based Systems
ISBN
0-7695-3141-5
ISSN
—
e-ISSN
—
Number of pages
11
Pages from-to
—
Publisher name
University of Ulster
Place of publication
Belfast
Event location
Belfast
Event date
Mar 31, 2008
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—
Basic information
Result type
D - Article in proceedings
CEP
JC - Computer hardware and software
Year of implementation
2008