fact: Definition GuardSpec : ADT GuardSig := IPGuard {{ iptables -P FORWARD DROP; iptables -A FORWARD --protocol "UDP" --source-port bootps --not --source 192*168*0*1 -j DROP; iptables -A FORWARD --protocol "UDP" --source-port bootpc --not --destination 255*255*255*255 -j DROP }}.
imports: Fiat.ADT Fiat.ADTNotation Fiat.ADTRefinement Fiat.ADTRefinement.BuildADTRefinements Fiat.Narcissus.Examples.Guard.Core Fiat.Narcissus.Examples.Guard.IPTablesGuard