Abstract
The term virtual private network (VPN) encompasses a wide array of diverse technologies and network architectures. All VPNs should provide users with the isolation and security associated with private networks, but at lower costs made possible by implementing these networks over some type of shared infrastructure. Provider provisioned VPN allow enterprises to outsource their private backbone networks to service providers. For this reason, we will also refer to them as virtual private routed networks (VPRNs). This contrasts with other VPN technologies that require customers to manage their own point-to-point connections (leased lines or tunnels) and associated network administration. One type of VPRN currently being deployed is described in RFC 2547, which uses BGP to propagate routing information for all VPNs implemented within a provider's backbone, and a tunneling technology, such as MPLS, to isolate traffic. This technology requires fairly complex configurations within the backbone, and so poses challenges to providers supporting a large number of VPN customers. We present a formal analysis of several configuration and implementation concerns for VPRNs of the RFC 2547 variety. In particular, we focus on integrity constraints that must be maintained by providers in order to ensure that intraVPRN connectivity is achieved, and that disjoint VPRNs are isolated from each other.