Formal correctness of complex multi-party network protocols can be
  difficult to verify. While models of specific fixed compositions of
  agents can be checked against design constraints, protocols which
  lend themselves to arbitrarily many compositions of agents--such as
  the chaining of proxies or the peering of routers--are more
  difficult to verify because they represent potentially infinite
  state spaces and may exhibit emergent behaviors that may not
  materialize under particular fixed compositions. We address this
  challenge by developing an algebraic approach that enables us to
  reduce arbitrary compositions of network agents into a
  behaviorally-equivalent (with respect to some correctness property)
  compact, canonical representation, which is amenable to mechanical
  verification. Our approach consists of an algebra and a set of
  property-preserving rewrite rules for the Canonical Homomorphic
  Abstraction of Infinite Network protocol compositions (CHAIN). Using
  CHAIN, an expression over our algebra (i.e., a set of configurations
  of network protocol agents) could be reduced to another
  behaviorally-equivalent expression (i.e., a smaller set of
  configurations). Repeated applications of such rewrite rules
  produces a canonical expression which can be checked mechanically.
  I will demonstrate the CHAIN approach as applied to standardized
  and experimental internet protocols, and discuss how it may be
  applied to a broad class of applications.