### Abstract

We present a formal model of network protocols and their application to modeling firewall policies. The formalization is based on the Unified Policy Framework (UPF). The formalization was originally developed with for generating test cases for testing the security configuration actual firewall and router (middle-boxes) using HOL-TestGen. Our work focuses on modeling application level protocols on top of tcp/ip.

### License

BSD License

### Topics

- Computer science/Security
- Computer science/Networks

### Session UPF_Firewall

- NetworkCore
- DatatypeAddress
- DatatypePort
- IntegerAddress
- IntegerPort
- IntegerPort_TCPUDP
- IPv4
- IPv4_TCPUDP
- NetworkModels
- PolicyCore
- PolicyCombinators
- PortCombinators
- ProtocolPortCombinators
- Ports
- PacketFilter
- NAT
- FWNormalisationCore
- NormalisationGenericProofs
- NormalisationIntegerPortProof
- NormalisationIPPProofs
- ElementaryRules
- FWNormalisation
- LTL_alike
- StatefulCore
- FTP
- FTP_WithPolicy
- VOIP
- FTPVOIP
- StatefulFW
- UPF-Firewall
- DMZDatatype
- DMZInteger
- DMZ
- Voice_over_IP
- Transformation01
- Transformation02
- Transformation
- NAT-FW
- PersonalFirewallInt
- PersonalFirewallIpv4
- PersonalFirewallDatatype
- PersonalFirewall
- Examples

### Depends on

- The Unified Policy Framework (UPF)

## Cite

×

UPF_Firewall-AFP

    @article{UPF_Firewall-AFP,
      author  = {Achim D. Brucker and Lukas Brügger and Burkhart Wolff},
      title   = {Formal Network Models and Their Application to Firewall Policies},
      journal = {Archive of Formal Proofs},
      month   = {January},
      year    = {2017},
      note    = {\url{https://isa-afp.org/entries/UPF_Firewall.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Jan 11, 2017 : Isabelle2016-1