Local mirror of Formal Network Models and Their Application to Firewall Policies (UPF-Firewall) entry of the Archive of Formal Proofs (AFP).