. Recherche-d-'attaques-sur-les-protocoles-de-groupe...... and .. Asokan-ginzboorg, 94 4.6.1 Exemple de protocole de groupe, p.96

. Notre-modèle-est-une-extension-des-modèles-classiques..., 174 6.5.1 Poids des termes, contraintesélémentairescontraintesélémentaires, blocs et systèmes de contraintes175 6.5.2 Terminaison pour les protocoles sans indices et sans mpair, p.176

. Pour-la-r-`-egle, 16], la contrainte Sub est transformée en une contrainte de type Sub avec le même terme t et le sous-terme t i de t 1

. Pour-la-r-`-egle, autonomie de mpair, on a V ar I (u) = {k}. La R` egle [5.20] ´ elimine tout le bloc. Ainsi, l'invariant est valide pour ces deux r` egles, eliminent soit une contrainte (?) soit un bloc (?). L'invariant reste donc satisfait

R. La, 23] transforme une contrainte d'´ egalité de deux termes t et t ? en des contraintes d'´ egalité des sous-termes de t et t ?

. Pour-la-r-`-egle, 24], selon la propriété d'autonomie de mpair, on a V ar I (u) = {k} et V ar I (v) = {l}. Ainsi

R. La, ] remplace une variable d'indice par une autre dans un bloc

. Pour-les-r-`-egles, système de contraintes résultant de l'application de ces r` egles a les mêmes termes

L. R. De-même, transforment un système de contraintes en un autre construit sur les mêmes termes que le système initial modulo un remplacement d'indices. Enfin, la R` egle [5.32] ´ elimine un bloc. L'invariant est alors satisfait par ces différents r` egles. Ladeuxì eme propriété exprime la conservation d'au moins une contrainte pour chaque variable , une fois que cette variable a déjà admis une contrainte. Cette propriété est représentée par l

. Preuve, Nous montrons que l'application des r

R. La, [5.2] transforme une contrainte pour Y en une autre contrainte pour Y sanséliminersanséliminer les autres contraintes. Ainsi, nous avons toujours des contraintes pour X et Y
URL : https://hal.archives-ouvertes.fr/jpa-00218986

´. Elimine-tout-le-bloc.-l-'invariant-reste-donc-valide, Les R` egles [5.4], [5.5], et [5.8] ne changent pas de contraintes. La R` egle [5.6] transforme une contrainte pour X en une autre contrainte pour X sanséliminersanséliminer d'autres contraintes. Ainsi, nous avons toujours des contraintes pour X et Y j . La R` egle [5.7] transforme une contrainte pour X en une autre contrainte pour X

L. 'invariant-reste-donc-valide and . La-r-`-egle, 15] peut ajouter de contraintes pour une variable mais ne peut paséliminerpaséliminer d'autres. Quant aux autres r` egles du groupe G 3 , elles ne manipulent pas de contraintes pour des variables. L'invariant reste donc valide. La R` egle [5.23] peut ajouter de contraintes pour une variable mais ne peut paséliminerpaséliminer d'autres. Quant aux autres r` egles du groupe G 4 , elles ne manipulent pas de contraintes pour des variables. L'invariant reste donc Chapitre 6, Décidabilité pour les protocoles paramétrés bien taguéstaguésà clefs autonomes de type (2) pour X. Nous concluons que les r` egles dutroisì eme groupe satisfont l'invariant

. Néanmoins, ) pour la variable X i qui est (X i = u) Le même raisonnement est valide pour la R` egle [5.29]. Pour la r` egle [5.30], il existe une contrainte de type (1 ? ) pour A

R. Les and . Egles, la même contrainte donnée par pre(r) Le R` egle [5.35] utilise les mêmes termes pour les contraintes d'´ egalité Elle transforme une contrainte de type (3) pour les variables de v ou X m en d'autres contraintes de même type. Nous concluons que les r` egles dusixì eme groupe satisfont l'invariant. Nous présentons maintenant la propriété qui caractérise lapremì ere phase de la normalisation

. Preuve, Nous introduisons tout d'abord la prétention suivante

. Preuve, Nous montrons par contradiction que si ctr = (Y = u) et X ?

=. Soit-ctr, v ? ) ? post(L l ) o` u Y ? v ? et u ? u ? et pre(L l ) = (u " = v " ) o` u u ? < u " et v ? < v " . La contrainte (u ? = v ? ) est obtenue soit en transformant une contrainte de type Sub en une contrainte d'´ egalité par la R` egle [5.15], soit par entrelacement (R` egle [5.35])

X. <. Vu-que, ?. , L. Et-qu, E. , and K. , on calcule CBS i , selon l'Invariant 6.4.1.4, L(Y ) ? L(X), ce qui contredit l'hypothèse : L(Y ) = L(X) Le même raisonnement est valide si pre

L. Cas-o-`-u and =. , 35], alors pre(L l ) = (X m = u ? ) et comme contrainte ma??trema??tre, nous avons (X i = v ? ) Vu que nous sommes dans lapremì ere phase, i.e. avantétiquetageavantétiquetage des labels ma??tresma??tres et sous-ma??tresma??tres pour les variables de niveau E i?1 , alors L(v ? ) ? E i?1, Vu que L(X) = E i?1 et Y < v ? alors L(Y ) ? L(X), ce qui contredit l'hypothèse de L(Y ) = L(X)

C. Notons-que-de, nous avons uniquement des contraintes résolues (Hypothèse H 1 ) Nous montrons par contradiction qu'il existe une contrainte ctr pour X dans chaque bloc du système de contraintes S. Soit B un bloc de S tel que ?ctr ? B sous-ma??tresma??tres. Ainsi, S diminue, nous avons pre

B. Ainsi, Nous montrons d'unemanì ere similairè a la R` egle [5.10] que pour la R` egle [5.11], S diminue

B. Ainsi, S. , +. , +. , +. |e| et al., Dans ledeuxì eme cas, post(R [5.15]) = [k, t + u, k, t + u + |E|] En outre, vu que cette r` egle ne modifie pas le nombre de contraintes sous-ma??tresma??tres, S diminue. Nous montrons d'unemanì ere similairè a la R

. Ainsi, pre(R [5.23]) > post(R [5.23]) et vu que le nombre de contraintes sous-ma??tresma??tres reste inchangé

´. Elimine-tout-le-bloc, Nous concluons que les r` egles du groupe G 3 satisfont l'invariant

R. La, La R` egle [5.22] ´ elimine tout le bloc. La R` egle [5.23] transforme une contrainte d'´ egalité (u = v) en une autre contrainte (u ? = v ? ) o` u u ? m u et v ? m v. Ainsi, si ?X i , Y j tels que X i m u ? et Y j m v ? , alors X i m u et Y j m v. Or, par hypothèse d'induction, i, j ? Q, ce qui satisfait l'invariant. La R` egle [5.21] transforme une contrainte d'´ egalité en une autre (u = w? l,k ) o` u V ar I (u) = V ar I (v)

R. La, 26] génère une nouvelle contrainte (u = v) Supposons que ?Z k , Y j tel que Z k m u et Y j m v. Par hypothèse d'induction, en considérant la contrainte (X i = u)

R. La, . `-egle-le-même-terme-t.-l-'invariant-reste-donc-valide, and . La-r-`-egle, Supposons que ?Y j tel que Y j m u o ? o . Or, selon l'Invariant 6.6.1.1 appliquéappliquéà la contrainte ma??trema??tre (X o = u o ) en tenant compte de ? o , nous avons j = m. En outre, par hypothèse d'induction appliquéè a la contrainte (X m ? F orge c (E ? , K)), nous avons m ? Q, ce qui valide l'invariant. La R` egle [5.35] génère deux nouvelles contraintes Supposons d'un remplacement par application de la R` egle [5.25] ` a la contrainte (c i = c j ). Or, selon l'Invariant 6.6.1.4, i est fra??chefra??che ou i ? V ar R I (E) Le premier cas (i est fra??chefra??che) est contradictoire avec l'existence de (c i = c j ), ledeuxì eme cas (i ? V ar R I (E)), la seulemanì ere pour remplacer i par j est d'avoir ant(i, j) = {j}. Vu que i ? V ar R I (E), ce cas n'est possible que si j ? V ar R I (E)

L. Ainsi and . Nombre, Sub dans ce cas est borné par id Nous nous intéressons maintenant, en Proposition 6.6.2.9, ` a borner l'ensemble d'indices dans V , défini en Définition 6.6.2.3 en montrant que cet ensemble est stable par notre système de r` egles. Cette proposition sera utilisée pour la preuve des Propositions 6

. Preuve, La preuve de la Proposition 6.6.2.9 est une conséquence directe de l'Invariant 6

R. La, egle [5.35] pour une contrainte (X m = v) quand ?Z m m v est borné

. Preuve, E. La-r-`-egle, E. , and K. Qui-peut-contenir-un-nouvel-indice-quantifié-existentiellement-dans-u?, Or, ?Z j m t et grâcè a la Proposition 6.6.2.8 et la Proposition 6.6.2.7, l'ensemble d'indices quantifiés existentiellement que peut générer la R` egle [5.19] est borné. D'unemanì ere similaire, la R` egle [5.33] peut générer de nouveaux indices quantifiés existentiellementàexistentiellementà l'intérieur d'une contrainte de type Sub

R. La, Or, l'ensemble de ces indices est borné En effet, le nombre d'indices quantifiés existentiellement dans u o ? o est borné par le nombre de contraintes de la forme u o ? o ? F orge(E ? , K) qui est borné par : (le nombre de différents K * le nombre de différents E ? * le nombre d'indices quantifiés existentiellement dans u o ? o en fixant E ? et K) Or, le nombre de différents E est borné par 2 st vu que les termes dans E n'ont pas d'indices en dehors des mpairs selon la restriction de protocoles bien tagués (voir Définition 5.6.2.3) En outre

L. Ensuite and . Nombre, ? et K est le nombre de remplacements possibles qui est borné par (le nombre de variables indicées dans les contraintes F orge * le nombre de contraintes ma??tresma??tres) vu que nous avons exactement un indice frais par variable indicée et par contrainte ma??trema??tre. Le nombre de contraintes ma??tresma??tres est borné par le nombre de contraintes dans E qui est fixe

. Pour-la-r-`-egle, Invariant 6.6.1.2. Pour cette r` egle, les indices quantifiés existentiellement peuvent donc appara??treappara??tre seulement dans u o ? o . Ainsi, le nombre d'indices frais générés par cette r` egle est borné par le nombre de contraintes de la forme (u o ? o = v) qui est borné par ((st * l'ensemble d'indices quantifiés universellement) * l'ensemble d'indices quantifiés existentiellement dans u o ? o en fixant v). Or, l'ensemble d'indices quantifiés universellement est borné selon la Proposition 6.6.2.6. En outre, l'ensemble d'indices quantifiés existentiellement dans u o ? o en fixant v est borné par (le nombre de variables indicées dans les contraintes d'´ egalité * le nombre de contraintes ma??tresma??tres) vu que nous avons exactement un indice frais par variable indicée dans une contrainte d'´ egalité par contrainte ma??trema??tre, De plus, le nombre de contraintes ma??tresma??tres est borné par le nombre de contraintes dans E qui est fixe. D'ailleurs, le nombre de variables indicées dans des contraintes d'´ egalité de la forme (X m = v) est borné par

R. La, 35] pour une contrainte (X m = v) quand ?Z m m v

E. La-r-`-egle, E. , and K. , soit en une autre contrainte de type Sub d avec le même t et donc V 1 reste stable, soit en une contrainte d'´ egalité (t = u) Supposons que ?X i t.q. X i m t ou X i m u. Nous distinguons deux cas

. Supposons-que-?c-j-t, Or, j appartient toujoursàtoujoursà V 2 . Ainsi, V 2 ? V 3 reste Preuve. Nous proposons la Proposition 6.6.2.12 en prouvant l'invariant suivant, (v = u) ? (u = v) ? B}) est stable ou cro??tcro??t par un ensemble d'indices qui est déjà borné

R. La, 21] ´ elimine une contrainte. La R` egle [5.22] ´ elimine tout le bloc Si la R` egle [5.24] génère un nouvel indice, alors il est quantifié universellement. Ainsi, pour ces r` egles, l'invariant est valide

R. La, Or, selon l'Invariant 6.6.2.13, ant(i, j) ? V . Ainsi, même si la R` egle [5.25] génère de nouveaux indices dans d'autres contraintes d'´ egalité, alors, ces indices appartiennentàappartiennentà un ensemble déjà borné vu que ces indices sont dans V et que V est borné selon la Proposition 6.6.2.9. Ainsi, l'invariant est valide

. Seules-les-r-`-egles, eme groupe peuvent générer de nouvelles contraintes d'´ egalité, Or, les indices possibles dans ces contraintes appartiennent déjà aux contraintes d'´ egalitéegalitéà gauche de ces r` egles. L'ensemble des indices est alors stable et donc l'invariant est valide

R. Seule-la, egle [5.35] dusixì eme groupe peut générer de nouvelles contraintes d'´ egalité : (u o ? o = v)

J. Si-?c, il appartientàappartientà la contrainte (X m = v) et que, selon la Proposition 6.6.2.11, l'ensemble des ces indices est borné Si ?c j t.q. j ? R et c j m u o ? o , alors nous avons un indice frais par variable indicée par contrainte ma??trema??tre. Ainsi, le nombre d'indices quantifiés existentiellement générés de cettemanì ere est borné par (le nombre de variables indicées * le nombre de contraintes ma??tresma??tres). Or, le nombre de contraintes ma??tresma??tres est borné par le nombre de contraintes dans E qui est fixe De plus, En outre, le nombre de variables indicées est borné par

. En-outre and . Le-nombre, ´ egalité est la somme des indices quantifiés universellement et ceux quantifiés existentiellement. L'ensemble des indices quantifiés universellement est borné selon la Proposition 6.6.2.6. L'ensemble de ceux quantifiés existentiellement est borné selon la Proposition 6

. Tab, 1 ? Synthèse des preuves de correction et de complétude [1] Security protocols open repository

A. Armando, D. Basin, Y. Boichut, Y. Chevalier, L. Compagna et al., The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications, 17th International Conference on Computer Aided Verification, CAV, 2005.
DOI : 10.1007/11513988_27

URL : https://hal.archives-ouvertes.fr/inria-00000408

A. Armando and L. Compagna, Automatic SAT-Compilation of Protocol Insecurity Problems via Reduction to Planning, FORTE '02 : Proceedings of the 22nd IFIP WG
DOI : 10.1007/3-540-36135-9_14

N. Asokan and P. Ginzboorg, Key agreement in ad hoc networks, Computer Communications, vol.23, issue.17, pp.1627-1637, 2000.
DOI : 10.1016/S0140-3664(00)00249-8

G. Ateniese, M. Steiner, and G. Tsudik, Authenticated group key agreement and friends, Proceedings of the 5th ACM conference on Computer and communications security , CCS '98, pp.17-26, 1998.
DOI : 10.1145/288090.288097

G. Ateniese, M. Steiner, and G. Tsudik, New multiparty authentication services and key agreement protocols, IEEE Journal on Selected Areas in Communications, vol.18, issue.4, pp.628-639, 2000.
DOI : 10.1109/49.839937

URL : http://www.zurich.ibm.com/security/publications/./2000/AtStTs2000.ps.gz

F. Bao, R. Deng, K. Nguyen, and V. Varadharajan, Multi-Party Fair Exchange with an Off-Line Trusted Neutral Party, DEXA '99 : Proceedings of the 10th International Workshop on Database & Expert Systems Applications, p.858, 1999.

D. Basin, S. Mödersheim, and L. Viganò, OFMC: A symbolic model checker for security protocols, International Journal of Information Security, vol.7, issue.3, pp.181-208, 2005.
DOI : 10.1109/CSFW.2001.930145

K. Becker and U. Wille, Communication complexity of group key distribution, Proceedings of the 5th ACM conference on Computer and communications security , CCS '98, pp.1-6, 1998.
DOI : 10.1145/288090.288094

B. Blanchet, An efficient cryptographic protocol verifier based on prolog rules, Proceedings. 14th IEEE Computer Security Foundations Workshop, 2001., pp.82-96, 2001.
DOI : 10.1109/CSFW.2001.930138

B. Blanchet, Automatic proof of strong secrecy for security protocols, IEEE Symposium on Security and Privacy, 2004. Proceedings. 2004, p.86, 2004.
DOI : 10.1109/SECPRI.2004.1301317

B. Blanchet and A. Podelski, Verification of Cryptographic Protocols: Tagging Enforces Termination, Foundations of Software Science and Computation Structures (FoSSaCS'03), pp.136-152, 2003.
DOI : 10.1007/3-540-36576-1_9

J. M. Bohli, M. Vasco, and R. Steinwandt, Secure group key establishment revisited, International Journal of Information Security, vol.34, issue.10, 2005.
DOI : 10.1007/BFb0053744

URL : http://eprint.iacr.org/2005/395.ps.gz

M. Bouallagui, Y. Chevalier, M. Rusinowitch, M. Turuani, and L. Vigneron, Analyse Automatique de Protocoles de Sécurité avec CASRUL, Actes de SAR'2002, Sécurité et Architecture Réseaux, 2002.

M. S. Bouassida, N. Chridi, I. Chrisment, O. Festor, and L. Vigneron, Automatic Verification of a Key Management Architecture for Hierarchical Group Protocols, Proceedings of 5th Conference on Security and Network Architectures (SAR), pp.381-397, 2006.

M. S. Bouassida, N. Chridi, I. Chrisment, O. Festor, and L. Vigneron, Automated Verification of a Key Management Architecture for Hierarchical Group Protocols, Annals of Telecommunications, vol.62, pp.11-121365, 2007.
URL : https://hal.archives-ouvertes.fr/inria-00594389

C. Boyd, On key agreement and conference key agreement, ACISP'97 : Proceedings of the Second Australasian Conference on Information Security and Privacy, pp.294-302, 1997.
DOI : 10.1007/BFb0027936

L. Bozga, Y. Lakhnech, and M. Périn, HERMES: An Automatic Tool for Verification of Secrecy in Security Protocols, Computer Aided Verification, 15th International Conference, pp.219-222, 2003.
DOI : 10.1007/978-3-540-45069-6_23

E. Bresson, O. Chevassut, A. Essiari, and D. Pointcheval, Mutual authentication and group key agreement for low-power mobile devices, Special Issue on Security and Performance in Wireless and Mobile Networks, pp.1730-1737, 2004.
DOI : 10.1016/j.comcom.2004.05.023

J. Bull, D. Otway, and D. /. Sc, The authentication protocol, Defence Research Agency, vol.3, issue.1, 1997.

Y. Chevalier, Résolution deprobì emes d'accessibilité pour la compilation et la validation de protocoles cryptographiques, Thèse de doctorat, 2003.

Y. Chevalier, L. Compagna, J. Cuellar, P. Hankes-drielsma, J. Mantovani et al., A High Level Protocol Specification Language for Industrial Security-Sensitive Protocols, Proceedings of Workshop on Specification and Automated Processing of Security Requirements (SAPS)SAPS04.pdf. [26] N. Chridi, B. Fontan, and S. Mota. L2.5 SAFECAST : Spécification du système global -Intégration des services de sécurité au protocole de gestion de clés -. Contrat RNRT SAFECAST, LAAS-LORIA, 2004.
URL : https://hal.archives-ouvertes.fr/inria-00099882

N. Chridi, M. Turuani, and M. Rusinowitch, Constraints-based Verification of Parameterized Cryptographic Protocols, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00336539

N. Chridi, M. Turuani, and M. Rusinowitch, Towards a Constrained-based Verification of Parameterized Cryptographic Protocols Logic-based Program Synthesis and Transformation, 2008.

N. Chridi, M. Turuani, and M. Rusinowitch, Decidable Analysis for a Class of Cryptographic Group Porotocols with Unbounded Lists, CSF 2009 : 22nd IEEE Computer Security Foundations Symposium, pp.277-289, 2009.

N. Chridi and L. Vigneron, Modélisation des propriétés de sécurité de protocoles de groupe, Actes du 1er Colloque sur les Risques et la Sécurité d'Internet et des Systèmes, pp.119-132, 2005.

N. Chridi and L. Vigneron, Sécurité des communications de groupe Revue de l'´ electricité et de l'´ electronique, pp.51-60, 2006.

N. Chridi and L. Vigneron, Strategy for Flaw Detection Based on a Service-Driven Model for Group Protocols, Proceedings of the 1st Workshop on Constraints in Software Testing, Verification and Analysis, CSTVA, pp.88-99, 2006.
DOI : 10.1002/9780470612309.ch24

N. Chridi and L. Vigneron, Strategy for Flaws Detection based on a Services-driven Model for Group Protocols, chapter 24, Future and Trends in Constraint Programming. ISTE, pp.361-370, 2007.

J. Clark and J. Jacob, A survey of authentication protocol literature, 1997.

E. M. Clarke, S. Jha, and W. Marrero, Verifying security protocols with Brutus, ACM Transactions on Software Engineering and Methodology, vol.9, issue.4, pp.443-487, 2000.
DOI : 10.1145/363516.363528

URL : http://www.aladdin.cs.cmu.edu/papers/pdfs/y2000/brutus.pdf

H. Comon and R. Nieuwenhuis, Induction=I-Axiomatization+First-Order Consistency. Information and Computation, pp.151-186, 2000.
DOI : 10.1006/inco.2000.2875

URL : https://doi.org/10.1006/inco.2000.2875

H. Comon-lundh and V. Cortier, New Decidability Results for Fragments of First-Order Logic and Application to Cryptographic Protocols, 14th International Conference on Rewriting Techniques and Applications (RTA'03), pp.148-164, 2003.
DOI : 10.1007/3-540-44881-0_12

H. Comon-lundh and V. Cortier, Tree automata with one memory set constraints and cryptographic protocols, Theoretical Computer Science, vol.331, issue.1, pp.143-214, 2005.
DOI : 10.1016/j.tcs.2004.09.036

URL : https://hal.archives-ouvertes.fr/inria-00000553

V. Cortier, V??rifier les protocoles cryptographiques, Techniques et sciences informatiques, vol.24, issue.1, pp.115-140, 2005.
DOI : 10.3166/tsi.24.115-140

R. J. Cramer, M. Franklin, L. A. Schoenmakers, and M. Yung, Multi-Authority Secret-Ballot Elections with Linear Work, 1995.
DOI : 10.1007/3-540-68339-9_7

URL : http://www.win.tue.nl/~berry/papers/euro96.pdf

C. J. Cremers, The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols, Computer Aided Verification, 20th International Conference, pp.414-418, 2008.
DOI : 10.1007/978-3-540-70545-1_38

S. Deering, Multicast Routing in a Datagram Internetwork, 1992.

G. Denker and J. Millen, CAPSL integrated protocol environment, Proceedings DARPA Information Survivability Conference and Exposition. DISCEX'00, pp.207-221, 2000.
DOI : 10.1109/DISCEX.2000.824980

URL : http://www.csl.sri.com/~millen/capsl/cipe.ps

W. Diffie and M. Hellman, New directions in cryptography, IEEE Transactions on Information Theory, vol.22, issue.6, pp.22644-654, 1976.
DOI : 10.1109/TIT.1976.1055638

D. Dolev and A. Yao, On the security of public key protocols, IEEE Transactions on Information Theory, vol.29, issue.2, pp.198-207, 1983.
DOI : 10.1109/TIT.1983.1056650

B. Donovan, P. Norris, and G. Lowe, Analyzing a Library of Security Protocols using Casper and FDR, Proceedings of the Workshop on Formal Methods and Security Protocols, 1999.

N. Durgin, P. Lincoln, J. Mitchell, and A. Scedrov, Undecidability of Bounded Security Protocols, Workshop on Formal Methods and Security Protocols, 1999.

J. Garay and P. Mackenzie, Abuse-Free Multi-party Contract Signing, Proceedings of the 13th International Symposium on Distributed Computing, pp.151-165, 1999.
DOI : 10.1007/3-540-48169-9_11

T. Genet and F. Klay, Rewriting for Cryptographic Protocol Verification, Proceedings of the 17th International Conference on Automated Deduction, pp.271-290, 2000.
DOI : 10.1007/10721959_21

URL : https://hal.archives-ouvertes.fr/inria-00072731

T. Genet and V. Tong, Reachability Analysis of Term Rewriting Systems with Timbuk, Logic for Programming, Artificial Intelligence, and Reasoning, 8th International Conference, pp.695-706, 2001.
DOI : 10.1007/3-540-45653-8_48

URL : https://hal.archives-ouvertes.fr/inria-00072321

M. Hirt and K. Sako, Efficient Receipt-Free Voting Based on Homomorphic Encryption, EUROCRYPT, pp.539-556, 2000.
DOI : 10.1007/3-540-45539-6_38

A. Huima, Efficient infinite-state analysis of security protocols, Proceeding of the Workshop on Formal Methods and Security Protocols (FLOC'99), 1999.

D. Jackson, Alloy: a lightweight object modelling notation, ACM Transactions on Software Engineering and Methodology, vol.11, issue.2, pp.256-290, 2002.
DOI : 10.1145/505145.505149

J. Katz and J. S. Shin, Modeling insider attacks on group key-exchange protocols, Proceedings of the 12th ACM conference on Computer and communications security , CCS '05, pp.180-189, 2005.
DOI : 10.1145/1102120.1102146

Y. Kim, A. Perrig, and G. Tsudik, Communication-efficient group key agreement, Sec '01 : Proceedings of the 16th international conference on Information security : Trusted information, pp.229-244, 2001.

Y. Kim, A. Perrig, G. Tsudik, S. Kremer, A. Mercier et al., Tree-based group key agreement, Proceedings of the 4th International Joint Conference on Automated Reasoning (IJCAR'08), pp.60-96, 2004.
DOI : 10.1145/984334.984337

K. Kürtz, R. Küsters, and T. Wilke, Selecting theories and nonce generation for recursive protocols, FMSE '07 : Proceedings of the 2007 ACM workshop on Formal methods in security engineering, pp.61-70, 2007.

R. Küsters and T. Truderung, On the Automatic Analysis of Recursive Security Protocols with XOR, Proceedings of the 24th Symposium on Theoretical Aspects of Computer Science, pp.646-657, 2007.
DOI : 10.1007/978-3-540-70918-3_55

R. Küsters and T. Wilke, Automata-Based Analysis of Recursive Cryptographic Protocols, 21st Symposium on Theoretical Aspects of Computer Science, pp.382-393, 2004.
DOI : 10.1007/978-3-540-24749-4_34

G. Lowe, Breaking and fixing the Needham-Schroeder Public-Key Protocol using FDR, TACAS'96 : Proceedings of the Second International Workshop on Tools and Algorithms for Construction and Analysis of Systems, pp.147-166, 1996.
DOI : 10.1007/3-540-61042-1_43

G. Lowe, Towards a completeness result for model checking of security protocols, Proceedings of the 11th IEEE Computer Security Foundations Workshop (CSF), pp.96-105, 1998.

M. Manulis, Survey on Security Requirements and Models for Group Key Exchange, 2006.

C. Meadows, The NRL Protocol Analyzer: An Overview, The Journal of Logic Programming, vol.26, issue.2, pp.113-131, 1996.
DOI : 10.1016/0743-1066(95)00095-X

C. Meadows, Extending Formal Cryptographic Protocol Analysis Techniques for Group Protocols and Low-Level Cryptographic Primitives, Proceedings of the 1st Workshop on Issues in the Theory of Security, WITS, pp.87-92, 2000.
DOI : 10.21236/ADA464085

C. Meadows and P. Syverson, Formalizing GDOI group key management requirements in NPATRL, Proceedings of the 8th ACM conference on Computer and Communications Security , CCS '01, pp.235-244, 2001.
DOI : 10.1145/501983.502016

A. J. Menezes, P. C. Van-oorschot, and S. A. Vanstone, Handbook of Applied Cryptography , chapter Key Establishment Protocols, 1996.

J. Millen and V. Shmatikov, Constraint solving for bounded-process cryptographic protocol analysis, Proceedings of the 8th ACM conference on Computer and Communications Security , CCS '01, pp.166-175, 2001.
DOI : 10.1145/501983.502007

J. C. Mitchell, M. Mitchell, and U. Stern, Automated analysis of cryptographic protocols using Murphi, SP'97 : Proceedings of the 1997 IEEE Symposium on Security and Privacy, p.141, 1997.

S. Mittra, Iolus : A Framework for Scalable Secure Multicasting, Proceedings of the ACM SIGCOMM'97 Conference on Applications, Technologies, Architectures, and Protocols for Computer Communication, pp.277-288, 1997.

D. Monniaux, Abstracting cryptographic protocols with tree automata, Science of Computer Programming, vol.47, issue.2-3, pp.177-202, 2003.
DOI : 10.1016/S0167-6423(02)00132-6

URL : https://doi.org/10.1016/s0167-6423(02)00132-6

J. Nam, S. Kim, and D. Won, Attacks on Bresson-Chevassut-Essiari-Pointcheval's Group Key Agreement Scheme for Low-Power Mobile Devices, Cryptology ePrint Archive Report, vol.251, 2004.

J. Nam, S. Kim, and D. Won, A Weakness in the Bresson-Chevassut-Essiari-Pointcheval's Group Key Agreement Scheme for Low-Power Mobile Devices, IEEE Communication Letters, vol.9, issue.5, pp.429-431, 2005.

R. M. Needham and M. D. Schroeder, Using encryption for authentication in large networks of computers, Communications of the ACM, vol.21, issue.12, pp.993-999, 1978.
DOI : 10.1145/359657.359659

L. C. Paulson, Isabelle : a Generic Theorem Prover, Lecture Notes in Computer Science, vol.828, 1994.
DOI : 10.1007/BFb0030541

L. C. Paulson, Mechanized proofs for a recursive authentication protocol, Proceedings 10th Computer Security Foundations Workshop, pp.84-95, 1997.
DOI : 10.1109/CSFW.1997.596790

L. C. Paulson, The inductive approach to verifying cryptographic protocols, Journal of Computer Security, vol.6, issue.1-2, pp.85-128, 1998.
DOI : 10.3233/JCS-1998-61-205

O. Pereira, Modelling and Security Analysis of Authenticated Group Key Agreement Protocols, 2003.

O. Pereira and J. Quisquater, Security Analysis of the Cliques Protocols Suites: First Results, IFIP/Sec '01 : Proceedings of the IFIP TC11 Sixteenth Annual Working Conference on Information Security, pp.151-166, 2001.
DOI : 10.1007/0-306-46998-7_11

O. Pereira and J. Quisquater, Some attacks upon authenticated group key agreement protocols, Journal of Computer Security, vol.11, issue.4, pp.555-580, 2003.
DOI : 10.3233/JCS-2003-11404

URL : http://www.dice.ucl.ac.be/crypto/publications/2002/PQ_JCS.ps

O. Pereira and J. Quisquater, Generic insecurity of cliques-type authenticated group key agreement protocols, Proceedings. 17th IEEE Computer Security Foundations Workshop, 2004., pp.16-19, 2004.
DOI : 10.1109/CSFW.2004.1310729

G. L. Peterson, Myths about the mutual exclusion problem, Information Processing Letters, vol.12, issue.3, pp.115-116, 1981.
DOI : 10.1016/0020-0190(81)90106-X

A. Pettorossi, M. Proietti, and V. Senni, Transformational Verification of Parameterized Protocols Using Array Formulas, 15th International Symposium, LOPSTR 2005, pp.23-43, 2005.
DOI : 10.1016/j.cl.2004.02.006

S. Rafaeli and D. Hutchison, A survey of key management for secure group communication, ACM Computing Surveys, vol.35, issue.3, pp.309-329, 2003.
DOI : 10.1145/937503.937506

H. R. Hassan, A. Bouabdallah, H. Bettahar, and Y. Challal, HI-KD : Hash-based hierarchical key distribution for group communication, IEEE-INFOCOM'05, 2005.

R. Ramanujam and S. Suresh, Tagging Makes Secrecy Decidable with Unbounded Nonces as Well, FST TCS 2003 : Foundations of Software Technology and Theoretical Computer Science, 23rd Conference, pp.363-374, 2003.
DOI : 10.1007/978-3-540-24597-1_31

R. L. Rivest, A. Shamir, and L. M. Adleman, A method for obtaining digital signatures and public-key cryptosystems, Communications of the ACM, vol.21, issue.2, pp.120-126, 1978.
DOI : 10.1145/359340.359342

M. Rusinowitch and M. Turuani, Protocol insecurity with a finite number of sessions and composed keys is NP-complete, Theoretical Computer Science, vol.299, issue.1-3, pp.1-3451, 2003.
DOI : 10.1016/S0304-3975(02)00490-5

P. Ryan and S. Schneider, The modelling and analysis of security protocols : the csp approach, 2000.

A. T. Sherman and D. A. Mcgrew, Key establishment in large dynamic groups using one-way function trees, IEEE Transactions on Software Engineering, vol.29, issue.5, pp.444-458, 2003.
DOI : 10.1109/TSE.2003.1199073

D. X. Song, S. Berezin, and A. Perrig, Athena: a novel approach to efficient automatic security protocol analysis1, Journal of Computer Security, vol.9, issue.1-2, pp.47-74, 2001.
DOI : 10.3233/JCS-2001-91-203

G. Steel and A. Bundy, Attacking Group Multicast Key Management Protocols using CO- RAL, Proceedings of the Workshop on Automated Reasoning for Security Protocol Analysis of Electronic Notes in Theoretical Computer Science, pp.125-144, 2004.

G. Steel, A. Bundy, and M. Maidl, Attacking a Protocol for Group Key Agreement by Refuting Incorrect Inductive Conjectures, Proceedings of 2nd Int. Joint Conference on Automated Reasoning, IJCAR, pp.137-151, 2004.
DOI : 10.1007/978-3-540-25984-8_8

M. Steiner, G. Tsudik, and M. Waidner, CLIQUES: a new approach to group key agreement, Proceedings. 18th International Conference on Distributed Computing Systems (Cat. No.98CB36183), pp.380-387, 1998.
DOI : 10.1109/ICDCS.1998.679745

M. Taghdiri and D. Jackson, A Lightweight Formal Analysis of a Multicast Key Management Scheme, Formal Techniques for Networked and Distributed Systems, pp.240-256, 2003.
DOI : 10.1109/ICOIN.2001.905598

S. Tanaka and F. Sato, A key distribution and rekeying framework with totally ordered multicast protocols, Proceedings 15th International Conference on Information Networking, pp.831-838, 2001.
DOI : 10.1109/ICOIN.2001.905598

F. J. Thayer, J. C. Herzog, and J. D. Guttman, Strand spaces: proving security protocols correct, Journal of Computer Security, vol.7, issue.2-3, pp.191-230, 1999.
DOI : 10.3233/JCS-1999-72-304

T. Truderung, Selecting Theories and Recursive Protocols, Concurrency Theory, 16th International Conference, CONCUR 2005, pp.217-232, 2005.
DOI : 10.1007/11539452_19

G. Tsudik, Secure and Minimal Protocols for Authenticated Key Distribution, Computer Communications Journal, vol.18, pp.645-653, 1995.

M. Turuani, Sécurité des protocoles cryptographiques : décidabilité et complexité, 2003.

M. Turuani, The CL-Atse Protocol Analyser, Term Rewriting and Applications -Proc. of RTA, pp.277-286, 2006.
DOI : 10.1007/11805618_21

URL : https://hal.archives-ouvertes.fr/inria-00103573

C. Weidenbach, Towards an Automatic Analysis of Security Protocols in First-Order Logic, 16th International Conference on Automated Deduction, pp.314-328, 1999.
DOI : 10.1007/3-540-48660-7_29

E. Wolfstetter, AUCTIONS: AN INTRODUCTION, Journal of Economic Surveys, vol.60, issue.4, pp.367-420, 1996.
DOI : 10.2307/2296904

C. Wong, M. Gouda, and S. Lam, Secure Group Communications Using Key Graphs, Proceedings of the ACM SIGCOMM'98 Conference on Applications, Technologies, Architectures , and Protocols for Computer Communication, pp.68-79, 1998.

J. Xu, Automatic Verification of Parameterized Systems

=. State, \ secret(CGKm',id1,{L,M}) end role %% Second Role: The Leader of the group role leader (L: agent, LongTermKey: (agent.symmetric_key) set, Snd, Rcv: channel(dy)) played_by L def= local State: nat, GroupMembers: (agent) set, GroupIndivMembers,GpInMembers: (agent.symmetric_key) set, symmetric_key const id1,id2: protocol_id init State:=0 /\ GroupMembers := {L} /\ GroupIndivMembers := {} /\ GpInMembers :={} transition step0. State=0 /\ Rcv(start) =|> CGk' := new(

/. Groupindivmembers, Im',GroupIndivMembers) /\ State':=2 /\ secret(CGk',id,GroupMembers') step12