CFP last date
15 April 2024
Reseach Article

Modeling and Verification of Group Signatures Properties

by Mboupda Moyo Achille, Atsa Etoundi Roger
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

@article{ 10.5120/ijais12-450576,
author = { Mboupda Moyo Achille, Atsa Etoundi Roger },
title = { Modeling and Verification of Group Signatures Properties },
journal = { International Journal of Applied Information Systems },
issue_date = { August 2012 },
volume = { 3 },
number = { 9 },
month = { August },
year = { 2012 },
issn = { 2249-0868 },
pages = { 25-32 },
numpages = {9},
url = { https://www.ijais.org/archives/volume3/number9/260-0576/ },
doi = { 10.5120/ijais12-450576 },
publisher = {Foundation of Computer Science (FCS), NY, USA},
address = {New York, USA}
}
%0 Journal Article
%1 2023-07-05T10:46:14.899007+05:30
%A Mboupda Moyo Achille
%A Atsa Etoundi Roger
%T Modeling and Verification of Group Signatures Properties
%J International Journal of Applied Information Systems
%@ 2249-0868
%V 3
%N 9
%P 25-32
%D 2012
%I Foundation of Computer Science (FCS), NY, USA
Abstract

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.

References
  1. D. Chaum: "Blind signature systems". In advances in cryptology-CRYPTO, 1983, pages 153. Plenum Press, 1984.
  2. G. Berry, P. Couronne and G. Gonthier: "Synchronous Programming of Reactive Systems: An introduction to ESTEREL". Proc. 1st Franco-Japanese Symp. on programming of Future Generation Computers, 1986, Tokyo. pp. 35-56.
  3. W. Thomas: "Automata on Infinite Objects". Handbook on Theoretical Computer Science, J. Van Leeuwen, ed, pp. 133-187, Elsevier Science, 1990.
  4. D. Chaum and E. Van Heyst: "Group signatures". In advances in cryptology-EUROCRYPT 1991, volume 547 of Lecture notes in computer Science, pages 257-265. Springer-Verlag, 1991.
  5. G. J. Holzmann: "Design and Validation of Computers Protocols". Englewood Cli s, N. J. Prentice Hall, 1991.
  6. Z. Manna, A. Pnueli: "The Temporal Logic of Reactive and Concurrent Systems Programs". Springer-Verlag, 1991.
  7. G. J. Holzmann: "Basic Spin Manual". AT&Bell Laboratories, Murray Hill, New Jersey. 1995.
  8. J. Magnier: "Représentation symbolique et Vérification formelle de machines séquentielles". State Thesis University of Montpellier II, France, 1996.
  9. J. Camenisch: "Efficient and generalized group signatures". In advances in cryptology-EUROCRYPT'97, volume 1233 of Lecture notes in computer Science, pages 465-479. Springer-Verlag, 1997.
  10. Jan Camenisch and Markus Stadler: "Efficient Group Signatures Schemes for large Groups". In advances in cryptology-CRYPTO, 1997, volume 1294 of Lecture notes in computer Science, pages 410-424. Springer-Verlag, 1997.
  11. B. Berard, M. Bidoit, F. Laroussinie, A. Petit, P. Schnoebelen: "Vérification de logiciels – Techniques et outils du model-checking". Vuibert, Paris, 1999.
  12. G. Ateniese and G. Tsudik: "Some Open Issues and New Directions in Group Signatures". In cryptography'99, 1999.
  13. Dan Boneh, Xavier BoyenetHovav Shacham: "Short Group Signatures" Advances in Cryptology – CRYPTO 2004, Volume 3152/2004, 227-242
  14. Jan Camenische and Jens Groth: "Group Signatures: Better Efficiency and New Theoretical Aspects" Security in Communication Networks, 2005, Volume 3352/2005, 120-133.
  15. Jens Groth: "Fully Anonymous Group Signatures without Random Oracles" Advances in Cryptology – ASIACRYPT, Volume 4833/2007, 164-180.
  16. Xiaojun Wen, Yuan Tian, Liping Ji1 and Xiamu Niu "A group signature scheme based on quantum teleportation" Physica Scripta; Volume 81; Number 5; May 2010.
  17. S. Dov Gordon and Jonathan Katz and Vinod Vaikuntanathan "A Group Signature Scheme from Lattice Assumptions" Cryptology ePrint Archive, Version: 20110208:170219, last revised 8 Feb 2011.
  18. G. J. Holzmann: "Basic Spin Manual". AT&Bell Laboratories, Murray Hill, New Jersey.
  19. M. Abdalla, D. Catalano, and D. Fiore. "Veritable random functions from identity-based key encapsulation. EUROCRYPT 2009, LNCS vol. 5479, Springer, pp. 554-571, 2009.
  20. M. Abe, G. Fuchsbauer, J. Groth, K. Haralambiev, and M. Ohkubo. "Structure-perserving signatures and commitments to group elements". CRYPTO 2010, LNCS vol. 6223, Springer, pp. 209-236, 2010.
  21. M. Abe, J. Groth, K. Haralambiev, and M. Ohkubo. "Optimal structure-preserving signatures in asymmetric bilinear groups". CRYPTO 2011, LNCS vol. 6841, Springer, pp. 649-666, 2011.
  22. Matthew Franklin, Haibin Zhang "Unique Group Signatures", ESORICS 2012.
Index Terms

Computer Science
Information Sciences

Keywords

Group Signature Scheme Temporal Logic Model Verification