CHAPTER 24 Formal Analysis of Policy-Based Security Configurations in Enterprise Networks access list := access rule[. . . , access rule] access rule := order, filter, action filter := protocol , src ip, src port , dst ip, dst port action := protect | bypass | discard map list := map rule[. . . , map rule] map rule := priority, filter, transform list transform list := transform[. . . , transform] transform := sec protocol , encaps mode, parameters sec protocol := AH | ESP encaps mode := Transport | Tunnel tunnel dst 617 FIGURE 24-3 The syntax of IPSec policy statements. IPSec implementations [14]. This policy model is composed of two lists of packet-filtering rules: Crypto-Access-List. It consists of ordered filtering rules that specify actions to be per- the map-list (lower section). We consider that inbound traffic arriving at a device interface is matched against a mirror image of the outbound IPSec policy of this interface, i.e., the inbound