Google scholar arxiv informatics ads IJAIS publications are indexed with Google Scholar, NASA ADS, Informatics et. al.

Call for Paper


January Edition 2023

International Journal of Applied Information Systems solicits high quality original research papers for the January 2023 Edition of the journal. The last date of research paper submission is December 15, 2022.

Modeling and Verification of Group Signatures Properties

Mboupda Moyo Achille, Atsa Etoundi Roger Published in Security

International Journal of Applied Information Systems
Year of Publication 2012
© 2010 by IJAIS Journal
Download full text
  1. Mboupda Moyo Achille and Atsa Etoundi Roger. Article: Modeling and Verification of Group Signatures Properties. International Journal of Applied Information Systems 3(9):25-32, August 2012. BibTeX

    	author = "Mboupda Moyo Achille and Atsa Etoundi Roger",
    	title = "Article: Modeling and Verification of Group Signatures Properties",
    	journal = "International Journal of Applied Information Systems",
    	year = 2012,
    	volume = 3,
    	number = 9,
    	pages = "25-32",
    	month = "August",
    	note = "Published by Foundation of Computer Science, New York, USA"


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.


  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.


Group Signature Scheme, Temporal Logic, Model Verification