2002 , Volume 7, № 4, p.18-43

In this paper we describe how to derive an abstract applicative specification of a complete Group Diffie-Hellman key agreement protocol, used in Dynamic Peer Groups (DPG), starting from informal requirements. In the process we detect inconsistencies in the informal requirements and translate the requirements to a formal abstract applicative specification.

By formally specifying the system, we ensure that all the informal requirements of the system are met and as such reduce the possibilities of errors that could have cropped up, had the system been implemented (using a programming language) without formally specifying it. Such errors could have serious financial, economic as well as human consequencies if not detected and corrected at this early stage in the development process.

Obvious candidates of software specification and verification, are sensitive software and hardware systems where an error could have catastrophic consequencies, an example include: distributed systems where the global behaviour depends on parallel interaction of different sub-systems.

We use the RAISE specification language (RSL) to specify our system and employ the RSL technique of seperate development to decompose the description of our system into components and compose the system from the (developed) components.

*68M10 Network design and communication

68M12 Network protocols

68U35 Information systems (hypertext navigation, interfaces, decision support, etc.)

*C.2.1 Network Architecture and Design

C.2.2 Network Protocols

H.4 Information Systems Applications

H.5 Information Interfaces and Presentation