This report is concerned with specifying communication protocols and proving their behavior correct. Many different approaches have been taken for modeling communication protocols; the approach taken here is algebraic. Communication protocols are seen as complex data types and are defined using the algebraic method. The modeling techniques devised are applied to the specification and verification of a complex data transfer protocol. Properties proven include system invariants and those of an operational nature. These experiments have been carried out using the Affirm system for designing abstract data types algebraically and proving their properties.