Principles of Protocol Design

Wed, 07/16/2008 - 01:50 by Olivier Bonaventure • Categories:

This book written by Robin Sharp and published by Springer Verlag takes an unusual path to describe computer network protocols. While most standard networking texts mainly focus on a textual description of the different protocols and mechanisms, Robin Sharp starts from formal description techniques. More precisely, he chooses the Communicating Sequential Processes (CSP) notation proposed by Hoare. CSP is a process algebra that allows to model the interactions among communicating processes. The book starts with a detailed description of CSP and then uses the CSP formalism to describe several mechanisms such as flow and error control, fault tolerant broadcast or two phase commits. An advantage of using CSP is that the book contains proofs of several of the described mechanisms. However, as CSP does not contain reach datatypes, it is difficult to completely model in details complex protocols. Surprisingly, the author did not consider more powerful formal description techniques that evolved from CSP such as LOTOS.

The second part of the book is more heterogeneous. Several security protocols are discussed and the BAN logic is introduced. Then, the author briefly discusses real protocols. The discussion considers both OSI protocols and Internet protocols. This part is less interesting than the first part were the CSP models could be of interest for readers who are more interested in the application of formal description techniques to network protocols.