|
IP
Addresses
Title: |
IP Addresses |
Authors:
|
Cornelius Diekmann,
Julius Michaelis and
Lars Hupel
|
Submission date: |
2016-06-28 |
Abstract: |
This entry contains a definition of IP addresses and a library to work
with them. Generic IP addresses are modeled as machine words of
arbitrary length. Derived from this generic definition, IPv4 addresses
are 32bit machine words, IPv6 addresses are 128bit words.
Additionally, IPv4 addresses can be represented in dot-decimal
notation and IPv6 addresses in (compressed) colon-separated notation.
We support toString functions and parsers for both notations. Sets of
IP addresses can be represented with a netmask (e.g.
192.168.0.0/255.255.0.0) or in CIDR notation (e.g. 192.168.0.0/16). To
provide executable code for set operations on IP address ranges, the
library includes a datatype to work on arbitrary intervals of machine
words. |
BibTeX: |
@article{IP_Addresses-AFP,
author = {Cornelius Diekmann and Julius Michaelis and Lars Hupel},
title = {IP Addresses},
journal = {Archive of Formal Proofs},
month = jun,
year = 2016,
note = {\url{http://isa-afp.org/entries/IP_Addresses.shtml},
Formal proof development},
ISSN = {2150-914x},
}
|
License: |
BSD License |
Depends on: |
Automatic_Refinement, Word_Lib |
Used by: |
Iptables_Semantics, LOFT, Routing, Simple_Firewall |
Status: [ok] |
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.
|
|