Skip to Main content Skip to Navigation
Conference papers

Security Policy Enforcement Through Refinement Process

Abstract : In the area of networks, a common method to enforce a security policy expressed in a high-level language is based on an ad-hoc and manual rewriting process. We argue that it is possible to build a formal link between concrete and abstract terms, which can be dynamically computed from the environment data. In order to progressively introduce configuration data and then simplify the proof obligations, we use the B refinement process. We present a case study modeling a network monitor. This program, described by refinement following the layers of the TCP/IP suite protocol, has to warn for all observed events which do not respect the security policy. To design this model, we use the event-B method because it is suitable for modeling network concepts. This work has been done within the framework of the POTESTAT project, based on the research of network testing methods from a high-level security policy.
Document type :
Conference papers
Complete list of metadata

Cited literature [18 references]  Display  Hide  Download
Contributor : Nicolas Stouls <>
Submitted on : Thursday, April 8, 2010 - 9:32:02 AM
Last modification on : Wednesday, June 30, 2021 - 10:14:01 AM
Long-term archiving on: : Tuesday, September 14, 2010 - 5:05:06 PM


Files produced by the author(s)


  • HAL Id : inria-00384182, version 1
  • ARXIV : 1004.1460




Nicolas Stouls, Marie-Laure Potet. Security Policy Enforcement Through Refinement Process. B 2007, 2007, besançon, France. pp.216--231. ⟨inria-00384182⟩



Record views


Files downloads