International Journal of Applied Information Systems |
Foundation of Computer Science (FCS), NY, USA |
Volume 3 - Number 9 |
Year of Publication: 2012 |
Authors: Mboupda Moyo Achille, Atsa Etoundi Roger |
10.5120/ijais12-450576 |
Mboupda Moyo Achille, Atsa Etoundi Roger . Modeling and Verification of Group Signatures Properties. International Journal of Applied Information Systems. 3, 9 ( August 2012), 25-32. DOI=10.5120/ijais12-450576
A group signature allows any member of a group to sign anonymously and to act on behalf of the group in such a way that only the associated group manager, in case of any dispute, is able to reveal the identity of the author of a transaction. The functioning of the group signature is based on a set of rules that are required to be met at any time by the associated scheme. The state-of-the-art of the group signature research has shown that several schemes have been proposed but none of them satisfy all the fundamental group signature properties such as liveliness. When some of these properties are satisfied, only informal proofs are available. Hence, one cannot claim that these properties are really supported by the associated schemes. This paper contributes in the definition of a group signature scheme by integrating all the required constraints and making it possible to carry out their formal proof. The specification of the scheme is based on the finite state automata techniques and the temporal logic PLTL of CTL* to formally specify the required properties. Finally, the model-checker SPIN is used to verify the consistency of the resulting scheme.