n South African Computer Journal - Specification and justification of an Authenticated Contributory Group Key Agreement Protocol : research article

Volume 2002, Issue 29
  • ISSN : 1015-7999
  • E-ISSN: 2313-7835



The purpose of this paper is twofold. First, we present a formal specification, using the RAISE Specification Language (RSL), of a practical Authenticated Contributory Group Key Agreement protocol for Dynamic Peer Groups (DPGs). During the formalisation process, we use finite state automata notations to develop an improved development method for RAISE, which addresses some limitations of the RAISE method (lack of appropriate techniques for identifying and formulating properties of the system to be specified). Second, we formally specify two desired properties of a practical Authenticated Contributory Group Key Agreement Protocol for Dynamic Peer Groups (DPGs) as theorems and provide informal justifications of their correctness. Obvious candidates of software specification and verification are sensitive software and hardware systems where: an error could have catastrophic consequences and system security is a critical issue. Distributed systems, where the global behaviour depends on parallel interaction of different sub-systems, is an example of such systems. In this paper, we use the RAISE Specification Language (RSL) to specify our system and employ the RAISE method technique of seperate development to decompose the description of our system into components and compose the final system from the (developed) components

Loading full text...

Full text loading...


Article metrics loading...


This is a required field
Please enter a valid email address
Approval was a Success
Invalid data
An Error Occurred
Approval was partially successful, following selected items could not be processed due to error