Protocol Algebra

An overwhelming large number of new protocols are designed in the current software industry. Yet the design is a resource demanding and slow manual process, typically protocols are specified using pen and paper, and then implemented directly into software. We introduce a formal protocol-centric language for the specification, testing, simulation and analysis of both communication and security. Since the language is formal, it can be used as a basis for constructing tool support for automated construction, refinement and testing of protocols. In the paper we show how notions like roles, refinement, composition, equivalence, and execution of protocols can be handled, only by considering the protocol syntax. The language is specialized to handle security protocols, illustrated by the Otway-Rees authentication protocol.