Conclusion


Network operators and protocol designers need a logic to reason about routing protocols like BGP

The routing logic provides
A set of properties to describe protocol behavior
Rules to reason about them

Set of properties is not complete, but it is an important and interesting set

Promising for reasoning, verification, and design