InforLorV4, PascalFrancis, Corpus, bibRecord, 000544

The AVISPA tool for the automated validation of internet security protocols and applications

Identifieur interne : 000544 ( PascalFrancis/Corpus ); précédent : 000543; suivant : 000545

The AVISPA tool for the automated validation of internet security protocols and applications

Auteurs : A. Armando ; D. Basin ; Y. Boichut ; Y. Chevalier ; L. Compagna ; J. Cuellar ; P. Hankes Drielsma ; P. C. Heam ; O. Kouchnarenko ; J. Mantovani ; S. Mödersheim ; D. Von Oheimb ; M. Rusinowitch ; J. Santiago ; M. Turuani ; L. Vigano ; L. Vigneron

Source :

Lecture notes in computer science [ 0302-9743 ] ; 2005.

RBID : Pascal:05-0349048

Descripteurs français

Pascal (Inist)
- Vérification programme, Protocole internet, Protocole transmission, Sécurité, Langage formel, Extensibilité, Validation, Analyse automatique, Robustesse.

English descriptors

KwdEn :
- Automatic analysis, Formal language, Internet protocol, Program verification, Robustness, Safety, Scalability, Transmission protocol, Validation.

Abstract

AVISPA is a push-button tool for the automated validation of Internet security-sensitive protocols and applications. It provides a modular and expressive formal language for specifying protocols and their security properties, and integrates different back-ends that implement a variety of state-of-the-art automatic analysis techniques. To the best of our knowledge, no other tool exhibits the same level of scope and robustness while enjoying the same performance and scalability.

Notice en format standard (ISO 2709)

Pour connaître la documentation sur le format Inist Standard.

A01	`01`	`1`		`@0 0302-9743`
A05				`@2 3576`
A08	`01`	`1`	`ENG`	`@1 The AVISPA tool for the automated validation of internet security protocols and applications`
A09	`01`	`1`	`ENG`	`@1 CAV 2005 : computer aided verification : Edinburgh, 6-10 July 2005`
A11	`01`	`1`		`@1 ARMANDO (A.)`
A11	`02`	`1`		`@1 BASIN (D.)`
A11	`03`	`1`		`@1 BOICHUT (Y.)`
A11	`04`	`1`		`@1 CHEVALIER (Y.)`
A11	`05`	`1`		`@1 COMPAGNA (L.)`
A11	`06`	`1`		`@1 CUELLAR (J.)`
A11	`07`	`1`		`@1 DRIELSMA (P. Hankes)`
A11	`08`	`1`		`@1 HEAM (P. C.)`
A11	`09`	`1`		`@1 KOUCHNARENKO (O.)`
A11	`10`	`1`		`@1 MANTOVANI (J.)`
A11	`11`	`1`		`@1 MÖDERSHEIM (S.)`
A11	`12`	`1`		`@1 VON OHEIMB (D.)`
A11	`13`	`1`		`@1 RUSINOWITCH (M.)`
A11	`14`	`1`		`@1 SANTIAGO (J.)`
A11	`15`	`1`		`@1 TURUANI (M.)`
A11	`16`	`1`		`@1 VIGANO (L.)`
A11	`17`	`1`		`@1 VIGNERON (L.)`
A12	`01`	`1`		`@1 ETESSAMI (Kousha) @9 ed.`
A12	`02`	`1`		`@1 RAJAMANI (Sriram K.) @9 ed.`
A14	`01`			`@1 AI-Lab, DIST, Università di Genova @3 ITA @Z 1 aut. @Z 5 aut. @Z 10 aut.`
A14	`02`			`@1 Information Security Group, ETH Zurich @3 CHE @Z 2 aut. @Z 7 aut. @Z 11 aut. @Z 16 aut.`
A14	`03`			`@1 LIFC, Université de Franche-Comté @2 Besancon @3 FRA @Z 3 aut. @Z 8 aut. @Z 9 aut.`
A14	`04`			`@1 LORIA-INRIA-Lorraine @2 Nancy @3 FRA @Z 4 aut. @Z 13 aut. @Z 14 aut. @Z 15 aut. @Z 17 aut.`
A14	`05`			`@1 Siemens AG, CT IC 3 @2 Munich @3 DEU @Z 6 aut. @Z 12 aut.`
A20				`@1 281-285`
A21				`@1 2005`
A23	`01`			`@0 ENG`
A26	`01`			`@0 3-540-27231-3`
A43	`01`			`@1 INIST @2 16343 @5 354000124488910260`
A44				`@0 0000 @1 © 2005 INIST-CNRS. All rights reserved.`
A45				`@0 14 ref.`
A47	`01`	`1`		`@0 05-0349048`
A60				`@1 P @2 C`
A61				`@0 A`
A64	`01`	`1`		`@0 Lecture notes in computer science`
A66	`01`			`@0 DEU`
C01	`01`		`ENG`	`@0 AVISPA is a push-button tool for the automated validation of Internet security-sensitive protocols and applications. It provides a modular and expressive formal language for specifying protocols and their security properties, and integrates different back-ends that implement a variety of state-of-the-art automatic analysis techniques. To the best of our knowledge, no other tool exhibits the same level of scope and robustness while enjoying the same performance and scalability.`
C02	`01`	`X`		`@0 001D02B04`
C02	`02`	`X`		`@0 001D02B09`
C03	`01`	`X`	`FRE`	`@0 Vérification programme @5 01`
C03	`01`	`X`	`ENG`	`@0 Program verification @5 01`
C03	`01`	`X`	`SPA`	`@0 Verificación programa @5 01`
C03	`02`	`X`	`FRE`	`@0 Protocole internet @5 06`
C03	`02`	`X`	`ENG`	`@0 Internet protocol @5 06`
C03	`02`	`X`	`SPA`	`@0 Protocolo internet @5 06`
C03	`03`	`X`	`FRE`	`@0 Protocole transmission @5 07`
C03	`03`	`X`	`ENG`	`@0 Transmission protocol @5 07`
C03	`03`	`X`	`SPA`	`@0 Protocolo transmisión @5 07`
C03	`04`	`X`	`FRE`	`@0 Sécurité @5 08`
C03	`04`	`X`	`ENG`	`@0 Safety @5 08`
C03	`04`	`X`	`SPA`	`@0 Seguridad @5 08`
C03	`05`	`X`	`FRE`	`@0 Langage formel @5 09`
C03	`05`	`X`	`ENG`	`@0 Formal language @5 09`
C03	`05`	`X`	`SPA`	`@0 Lenguaje formal @5 09`
C03	`06`	`X`	`FRE`	`@0 Extensibilité @5 10`
C03	`06`	`X`	`ENG`	`@0 Scalability @5 10`
C03	`06`	`X`	`SPA`	`@0 Estensibilidad @5 10`
C03	`07`	`X`	`FRE`	`@0 Validation @5 23`
C03	`07`	`X`	`ENG`	`@0 Validation @5 23`
C03	`07`	`X`	`SPA`	`@0 Validación @5 23`
C03	`08`	`X`	`FRE`	`@0 Analyse automatique @5 24`
C03	`08`	`X`	`ENG`	`@0 Automatic analysis @5 24`
C03	`08`	`X`	`SPA`	`@0 Análisis automático @5 24`
C03	`09`	`X`	`FRE`	`@0 Robustesse @5 25`
C03	`09`	`X`	`ENG`	`@0 Robustness @5 25`
C03	`09`	`X`	`SPA`	`@0 Robustez @5 25`
N21				`@1 241`
N44	`01`			`@1 OTO`
N82				`@1 OTO`

A30	`01`	`1`	`ENG`	`@1 Computer aided verification. International conference @2 17 @3 Edinburgh GBR @4 2005-07-06`

Format Inist (serveur)

NO :	PASCAL 05-0349048 INIST
ET :	The AVISPA tool for the automated validation of internet security protocols and applications
AU :	ARMANDO (A.); BASIN (D.); BOICHUT (Y.); CHEVALIER (Y.); COMPAGNA (L.); CUELLAR (J.); DRIELSMA (P. Hankes); HEAM (P. C.); KOUCHNARENKO (O.); MANTOVANI (J.); MÖDERSHEIM (S.); VON OHEIMB (D.); RUSINOWITCH (M.); SANTIAGO (J.); TURUANI (M.); VIGANO (L.); VIGNERON (L.); ETESSAMI (Kousha); RAJAMANI (Sriram K.)
AF :	AI-Lab, DIST, Università di Genova/Italie (1 aut., 5 aut., 10 aut.); Information Security Group, ETH Zurich/Suisse (2 aut., 7 aut., 11 aut., 16 aut.); LIFC, Université de Franche-Comté/Besancon/France (3 aut., 8 aut., 9 aut.); LORIA-INRIA-Lorraine/Nancy/France (4 aut., 13 aut., 14 aut., 15 aut., 17 aut.); Siemens AG, CT IC 3/Munich/Allemagne (6 aut., 12 aut.)
DT :	Publication en série; Congrès; Niveau analytique
SO :	Lecture notes in computer science; ISSN 0302-9743; Allemagne; Da. 2005; Vol. 3576; Pp. 281-285; Bibl. 14 ref.
LA :	Anglais
EA :	AVISPA is a push-button tool for the automated validation of Internet security-sensitive protocols and applications. It provides a modular and expressive formal language for specifying protocols and their security properties, and integrates different back-ends that implement a variety of state-of-the-art automatic analysis techniques. To the best of our knowledge, no other tool exhibits the same level of scope and robustness while enjoying the same performance and scalability.
CC :	001D02B04; 001D02B09
FD :	Vérification programme; Protocole internet; Protocole transmission; Sécurité; Langage formel; Extensibilité; Validation; Analyse automatique; Robustesse
ED :	Program verification; Internet protocol; Transmission protocol; Safety; Formal language; Scalability; Validation; Automatic analysis; Robustness
SD :	Verificación programa; Protocolo internet; Protocolo transmisión; Seguridad; Lenguaje formal; Estensibilidad; Validación; Análisis automático; Robustez
LO :	INIST-16343.354000124488910260
ID :	05-0349048

Links to Exploration step

Pascal:05-0349048

Le document en format XML

<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">The AVISPA tool for the automated validation of internet security protocols and applications</title>
<author><name sortKey="Armando, A" sort="Armando, A" uniqKey="Armando A" first="A." last="Armando">A. Armando</name>
<affiliation><inist:fA14 i1="01"><s1>AI-Lab, DIST, Università di Genova</s1>
<s3>ITA</s3>
<sZ>1 aut.</sZ>
<sZ>5 aut.</sZ>
<sZ>10 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Basin, D" sort="Basin, D" uniqKey="Basin D" first="D." last="Basin">D. Basin</name>
<affiliation><inist:fA14 i1="02"><s1>Information Security Group, ETH Zurich</s1>
<s3>CHE</s3>
<sZ>2 aut.</sZ>
<sZ>7 aut.</sZ>
<sZ>11 aut.</sZ>
<sZ>16 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Boichut, Y" sort="Boichut, Y" uniqKey="Boichut Y" first="Y." last="Boichut">Y. Boichut</name>
<affiliation><inist:fA14 i1="03"><s1>LIFC, Université de Franche-Comté</s1>
<s2>Besancon</s2>
<s3>FRA</s3>
<sZ>3 aut.</sZ>
<sZ>8 aut.</sZ>
<sZ>9 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Chevalier, Y" sort="Chevalier, Y" uniqKey="Chevalier Y" first="Y." last="Chevalier">Y. Chevalier</name>
<affiliation><inist:fA14 i1="04"><s1>LORIA-INRIA-Lorraine</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>4 aut.</sZ>
<sZ>13 aut.</sZ>
<sZ>14 aut.</sZ>
<sZ>15 aut.</sZ>
<sZ>17 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Compagna, L" sort="Compagna, L" uniqKey="Compagna L" first="L." last="Compagna">L. Compagna</name>
<affiliation><inist:fA14 i1="01"><s1>AI-Lab, DIST, Università di Genova</s1>
<s3>ITA</s3>
<sZ>1 aut.</sZ>
<sZ>5 aut.</sZ>
<sZ>10 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Cuellar, J" sort="Cuellar, J" uniqKey="Cuellar J" first="J." last="Cuellar">J. Cuellar</name>
<affiliation><inist:fA14 i1="05"><s1>Siemens AG, CT IC 3</s1>
<s2>Munich</s2>
<s3>DEU</s3>
<sZ>6 aut.</sZ>
<sZ>12 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Drielsma, P Hankes" sort="Drielsma, P Hankes" uniqKey="Drielsma P" first="P. Hankes" last="Drielsma">P. Hankes Drielsma</name>
<affiliation><inist:fA14 i1="02"><s1>Information Security Group, ETH Zurich</s1>
<s3>CHE</s3>
<sZ>2 aut.</sZ>
<sZ>7 aut.</sZ>
<sZ>11 aut.</sZ>
<sZ>16 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Heam, P C" sort="Heam, P C" uniqKey="Heam P" first="P. C." last="Heam">P. C. Heam</name>
<affiliation><inist:fA14 i1="03"><s1>LIFC, Université de Franche-Comté</s1>
<s2>Besancon</s2>
<s3>FRA</s3>
<sZ>3 aut.</sZ>
<sZ>8 aut.</sZ>
<sZ>9 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Kouchnarenko, O" sort="Kouchnarenko, O" uniqKey="Kouchnarenko O" first="O." last="Kouchnarenko">O. Kouchnarenko</name>
<affiliation><inist:fA14 i1="03"><s1>LIFC, Université de Franche-Comté</s1>
<s2>Besancon</s2>
<s3>FRA</s3>
<sZ>3 aut.</sZ>
<sZ>8 aut.</sZ>
<sZ>9 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Mantovani, J" sort="Mantovani, J" uniqKey="Mantovani J" first="J." last="Mantovani">J. Mantovani</name>
<affiliation><inist:fA14 i1="01"><s1>AI-Lab, DIST, Università di Genova</s1>
<s3>ITA</s3>
<sZ>1 aut.</sZ>
<sZ>5 aut.</sZ>
<sZ>10 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Modersheim, S" sort="Modersheim, S" uniqKey="Modersheim S" first="S." last="Mödersheim">S. Mödersheim</name>
<affiliation><inist:fA14 i1="02"><s1>Information Security Group, ETH Zurich</s1>
<s3>CHE</s3>
<sZ>2 aut.</sZ>
<sZ>7 aut.</sZ>
<sZ>11 aut.</sZ>
<sZ>16 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Von Oheimb, D" sort="Von Oheimb, D" uniqKey="Von Oheimb D" first="D." last="Von Oheimb">D. Von Oheimb</name>
<affiliation><inist:fA14 i1="05"><s1>Siemens AG, CT IC 3</s1>
<s2>Munich</s2>
<s3>DEU</s3>
<sZ>6 aut.</sZ>
<sZ>12 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Rusinowitch, M" sort="Rusinowitch, M" uniqKey="Rusinowitch M" first="M." last="Rusinowitch">M. Rusinowitch</name>
<affiliation><inist:fA14 i1="04"><s1>LORIA-INRIA-Lorraine</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>4 aut.</sZ>
<sZ>13 aut.</sZ>
<sZ>14 aut.</sZ>
<sZ>15 aut.</sZ>
<sZ>17 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Santiago, J" sort="Santiago, J" uniqKey="Santiago J" first="J." last="Santiago">J. Santiago</name>
<affiliation><inist:fA14 i1="04"><s1>LORIA-INRIA-Lorraine</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>4 aut.</sZ>
<sZ>13 aut.</sZ>
<sZ>14 aut.</sZ>
<sZ>15 aut.</sZ>
<sZ>17 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Turuani, M" sort="Turuani, M" uniqKey="Turuani M" first="M." last="Turuani">M. Turuani</name>
<affiliation><inist:fA14 i1="04"><s1>LORIA-INRIA-Lorraine</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>4 aut.</sZ>
<sZ>13 aut.</sZ>
<sZ>14 aut.</sZ>
<sZ>15 aut.</sZ>
<sZ>17 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Vigano, L" sort="Vigano, L" uniqKey="Vigano L" first="L." last="Vigano">L. Vigano</name>
<affiliation><inist:fA14 i1="02"><s1>Information Security Group, ETH Zurich</s1>
<s3>CHE</s3>
<sZ>2 aut.</sZ>
<sZ>7 aut.</sZ>
<sZ>11 aut.</sZ>
<sZ>16 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Vigneron, L" sort="Vigneron, L" uniqKey="Vigneron L" first="L." last="Vigneron">L. Vigneron</name>
<affiliation><inist:fA14 i1="04"><s1>LORIA-INRIA-Lorraine</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>4 aut.</sZ>
<sZ>13 aut.</sZ>
<sZ>14 aut.</sZ>
<sZ>15 aut.</sZ>
<sZ>17 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">05-0349048</idno>
<date when="2005">2005</date>
<idno type="stanalyst">PASCAL 05-0349048 INIST</idno>
<idno type="RBID">Pascal:05-0349048</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000544</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">The AVISPA tool for the automated validation of internet security protocols and applications</title>
<author><name sortKey="Armando, A" sort="Armando, A" uniqKey="Armando A" first="A." last="Armando">A. Armando</name>
<affiliation><inist:fA14 i1="01"><s1>AI-Lab, DIST, Università di Genova</s1>
<s3>ITA</s3>
<sZ>1 aut.</sZ>
<sZ>5 aut.</sZ>
<sZ>10 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Basin, D" sort="Basin, D" uniqKey="Basin D" first="D." last="Basin">D. Basin</name>
<affiliation><inist:fA14 i1="02"><s1>Information Security Group, ETH Zurich</s1>
<s3>CHE</s3>
<sZ>2 aut.</sZ>
<sZ>7 aut.</sZ>
<sZ>11 aut.</sZ>
<sZ>16 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Boichut, Y" sort="Boichut, Y" uniqKey="Boichut Y" first="Y." last="Boichut">Y. Boichut</name>
<affiliation><inist:fA14 i1="03"><s1>LIFC, Université de Franche-Comté</s1>
<s2>Besancon</s2>
<s3>FRA</s3>
<sZ>3 aut.</sZ>
<sZ>8 aut.</sZ>
<sZ>9 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Chevalier, Y" sort="Chevalier, Y" uniqKey="Chevalier Y" first="Y." last="Chevalier">Y. Chevalier</name>
<affiliation><inist:fA14 i1="04"><s1>LORIA-INRIA-Lorraine</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>4 aut.</sZ>
<sZ>13 aut.</sZ>
<sZ>14 aut.</sZ>
<sZ>15 aut.</sZ>
<sZ>17 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Compagna, L" sort="Compagna, L" uniqKey="Compagna L" first="L." last="Compagna">L. Compagna</name>
<affiliation><inist:fA14 i1="01"><s1>AI-Lab, DIST, Università di Genova</s1>
<s3>ITA</s3>
<sZ>1 aut.</sZ>
<sZ>5 aut.</sZ>
<sZ>10 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Cuellar, J" sort="Cuellar, J" uniqKey="Cuellar J" first="J." last="Cuellar">J. Cuellar</name>
<affiliation><inist:fA14 i1="05"><s1>Siemens AG, CT IC 3</s1>
<s2>Munich</s2>
<s3>DEU</s3>
<sZ>6 aut.</sZ>
<sZ>12 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Drielsma, P Hankes" sort="Drielsma, P Hankes" uniqKey="Drielsma P" first="P. Hankes" last="Drielsma">P. Hankes Drielsma</name>
<affiliation><inist:fA14 i1="02"><s1>Information Security Group, ETH Zurich</s1>
<s3>CHE</s3>
<sZ>2 aut.</sZ>
<sZ>7 aut.</sZ>
<sZ>11 aut.</sZ>
<sZ>16 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Heam, P C" sort="Heam, P C" uniqKey="Heam P" first="P. C." last="Heam">P. C. Heam</name>
<affiliation><inist:fA14 i1="03"><s1>LIFC, Université de Franche-Comté</s1>
<s2>Besancon</s2>
<s3>FRA</s3>
<sZ>3 aut.</sZ>
<sZ>8 aut.</sZ>
<sZ>9 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Kouchnarenko, O" sort="Kouchnarenko, O" uniqKey="Kouchnarenko O" first="O." last="Kouchnarenko">O. Kouchnarenko</name>
<affiliation><inist:fA14 i1="03"><s1>LIFC, Université de Franche-Comté</s1>
<s2>Besancon</s2>
<s3>FRA</s3>
<sZ>3 aut.</sZ>
<sZ>8 aut.</sZ>
<sZ>9 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Mantovani, J" sort="Mantovani, J" uniqKey="Mantovani J" first="J." last="Mantovani">J. Mantovani</name>
<affiliation><inist:fA14 i1="01"><s1>AI-Lab, DIST, Università di Genova</s1>
<s3>ITA</s3>
<sZ>1 aut.</sZ>
<sZ>5 aut.</sZ>
<sZ>10 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Modersheim, S" sort="Modersheim, S" uniqKey="Modersheim S" first="S." last="Mödersheim">S. Mödersheim</name>
<affiliation><inist:fA14 i1="02"><s1>Information Security Group, ETH Zurich</s1>
<s3>CHE</s3>
<sZ>2 aut.</sZ>
<sZ>7 aut.</sZ>
<sZ>11 aut.</sZ>
<sZ>16 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Von Oheimb, D" sort="Von Oheimb, D" uniqKey="Von Oheimb D" first="D." last="Von Oheimb">D. Von Oheimb</name>
<affiliation><inist:fA14 i1="05"><s1>Siemens AG, CT IC 3</s1>
<s2>Munich</s2>
<s3>DEU</s3>
<sZ>6 aut.</sZ>
<sZ>12 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Rusinowitch, M" sort="Rusinowitch, M" uniqKey="Rusinowitch M" first="M." last="Rusinowitch">M. Rusinowitch</name>
<affiliation><inist:fA14 i1="04"><s1>LORIA-INRIA-Lorraine</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>4 aut.</sZ>
<sZ>13 aut.</sZ>
<sZ>14 aut.</sZ>
<sZ>15 aut.</sZ>
<sZ>17 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Santiago, J" sort="Santiago, J" uniqKey="Santiago J" first="J." last="Santiago">J. Santiago</name>
<affiliation><inist:fA14 i1="04"><s1>LORIA-INRIA-Lorraine</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>4 aut.</sZ>
<sZ>13 aut.</sZ>
<sZ>14 aut.</sZ>
<sZ>15 aut.</sZ>
<sZ>17 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Turuani, M" sort="Turuani, M" uniqKey="Turuani M" first="M." last="Turuani">M. Turuani</name>
<affiliation><inist:fA14 i1="04"><s1>LORIA-INRIA-Lorraine</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>4 aut.</sZ>
<sZ>13 aut.</sZ>
<sZ>14 aut.</sZ>
<sZ>15 aut.</sZ>
<sZ>17 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Vigano, L" sort="Vigano, L" uniqKey="Vigano L" first="L." last="Vigano">L. Vigano</name>
<affiliation><inist:fA14 i1="02"><s1>Information Security Group, ETH Zurich</s1>
<s3>CHE</s3>
<sZ>2 aut.</sZ>
<sZ>7 aut.</sZ>
<sZ>11 aut.</sZ>
<sZ>16 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Vigneron, L" sort="Vigneron, L" uniqKey="Vigneron L" first="L." last="Vigneron">L. Vigneron</name>
<affiliation><inist:fA14 i1="04"><s1>LORIA-INRIA-Lorraine</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>4 aut.</sZ>
<sZ>13 aut.</sZ>
<sZ>14 aut.</sZ>
<sZ>15 aut.</sZ>
<sZ>17 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
</analytic>
<series><title level="j" type="main">Lecture notes in computer science</title>
<idno type="ISSN">0302-9743</idno>
<imprint><date when="2005">2005</date>
</imprint>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><title level="j" type="main">Lecture notes in computer science</title>
<idno type="ISSN">0302-9743</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Automatic analysis</term>
<term>Formal language</term>
<term>Internet protocol</term>
<term>Program verification</term>
<term>Robustness</term>
<term>Safety</term>
<term>Scalability</term>
<term>Transmission protocol</term>
<term>Validation</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Vérification programme</term>
<term>Protocole internet</term>
<term>Protocole transmission</term>
<term>Sécurité</term>
<term>Langage formel</term>
<term>Extensibilité</term>
<term>Validation</term>
<term>Analyse automatique</term>
<term>Robustesse</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">AVISPA is a push-button tool for the automated validation of Internet security-sensitive protocols and applications. It provides a modular and expressive formal language for specifying protocols and their security properties, and integrates different back-ends that implement a variety of state-of-the-art automatic analysis techniques. To the best of our knowledge, no other tool exhibits the same level of scope and robustness while enjoying the same performance and scalability.</div>
</front>
</TEI>
<inist><standard h6="B"><pA><fA01 i1="01" i2="1"><s0>0302-9743</s0>
</fA01>
<fA05><s2>3576</s2>
</fA05>
<fA08 i1="01" i2="1" l="ENG"><s1>The AVISPA tool for the automated validation of internet security protocols and applications</s1>
</fA08>
<fA09 i1="01" i2="1" l="ENG"><s1>CAV 2005 : computer aided verification : Edinburgh, 6-10 July 2005</s1>
</fA09>
<fA11 i1="01" i2="1"><s1>ARMANDO (A.)</s1>
</fA11>
<fA11 i1="02" i2="1"><s1>BASIN (D.)</s1>
</fA11>
<fA11 i1="03" i2="1"><s1>BOICHUT (Y.)</s1>
</fA11>
<fA11 i1="04" i2="1"><s1>CHEVALIER (Y.)</s1>
</fA11>
<fA11 i1="05" i2="1"><s1>COMPAGNA (L.)</s1>
</fA11>
<fA11 i1="06" i2="1"><s1>CUELLAR (J.)</s1>
</fA11>
<fA11 i1="07" i2="1"><s1>DRIELSMA (P. Hankes)</s1>
</fA11>
<fA11 i1="08" i2="1"><s1>HEAM (P. C.)</s1>
</fA11>
<fA11 i1="09" i2="1"><s1>KOUCHNARENKO (O.)</s1>
</fA11>
<fA11 i1="10" i2="1"><s1>MANTOVANI (J.)</s1>
</fA11>
<fA11 i1="11" i2="1"><s1>MÖDERSHEIM (S.)</s1>
</fA11>
<fA11 i1="12" i2="1"><s1>VON OHEIMB (D.)</s1>
</fA11>
<fA11 i1="13" i2="1"><s1>RUSINOWITCH (M.)</s1>
</fA11>
<fA11 i1="14" i2="1"><s1>SANTIAGO (J.)</s1>
</fA11>
<fA11 i1="15" i2="1"><s1>TURUANI (M.)</s1>
</fA11>
<fA11 i1="16" i2="1"><s1>VIGANO (L.)</s1>
</fA11>
<fA11 i1="17" i2="1"><s1>VIGNERON (L.)</s1>
</fA11>
<fA12 i1="01" i2="1"><s1>ETESSAMI (Kousha)</s1>
<s9>ed.</s9>
</fA12>
<fA12 i1="02" i2="1"><s1>RAJAMANI (Sriram K.)</s1>
<s9>ed.</s9>
</fA12>
<fA14 i1="01"><s1>AI-Lab, DIST, Università di Genova</s1>
<s3>ITA</s3>
<sZ>1 aut.</sZ>
<sZ>5 aut.</sZ>
<sZ>10 aut.</sZ>
</fA14>
<fA14 i1="02"><s1>Information Security Group, ETH Zurich</s1>
<s3>CHE</s3>
<sZ>2 aut.</sZ>
<sZ>7 aut.</sZ>
<sZ>11 aut.</sZ>
<sZ>16 aut.</sZ>
</fA14>
<fA14 i1="03"><s1>LIFC, Université de Franche-Comté</s1>
<s2>Besancon</s2>
<s3>FRA</s3>
<sZ>3 aut.</sZ>
<sZ>8 aut.</sZ>
<sZ>9 aut.</sZ>
</fA14>
<fA14 i1="04"><s1>LORIA-INRIA-Lorraine</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>4 aut.</sZ>
<sZ>13 aut.</sZ>
<sZ>14 aut.</sZ>
<sZ>15 aut.</sZ>
<sZ>17 aut.</sZ>
</fA14>
<fA14 i1="05"><s1>Siemens AG, CT IC 3</s1>
<s2>Munich</s2>
<s3>DEU</s3>
<sZ>6 aut.</sZ>
<sZ>12 aut.</sZ>
</fA14>
<fA20><s1>281-285</s1>
</fA20>
<fA21><s1>2005</s1>
</fA21>
<fA23 i1="01"><s0>ENG</s0>
</fA23>
<fA26 i1="01"><s0>3-540-27231-3</s0>
</fA26>
<fA43 i1="01"><s1>INIST</s1>
<s2>16343</s2>
<s5>354000124488910260</s5>
</fA43>
<fA44><s0>0000</s0>
<s1>© 2005 INIST-CNRS. All rights reserved.</s1>
</fA44>
<fA45><s0>14 ref.</s0>
</fA45>
<fA47 i1="01" i2="1"><s0>05-0349048</s0>
</fA47>
<fA60><s1>P</s1>
<s2>C</s2>
</fA60>
<fA61><s0>A</s0>
</fA61>
<fA64 i1="01" i2="1"><s0>Lecture notes in computer science</s0>
</fA64>
<fA66 i1="01"><s0>DEU</s0>
</fA66>
<fC01 i1="01" l="ENG"><s0>AVISPA is a push-button tool for the automated validation of Internet security-sensitive protocols and applications. It provides a modular and expressive formal language for specifying protocols and their security properties, and integrates different back-ends that implement a variety of state-of-the-art automatic analysis techniques. To the best of our knowledge, no other tool exhibits the same level of scope and robustness while enjoying the same performance and scalability.</s0>
</fC01>
<fC02 i1="01" i2="X"><s0>001D02B04</s0>
</fC02>
<fC02 i1="02" i2="X"><s0>001D02B09</s0>
</fC02>
<fC03 i1="01" i2="X" l="FRE"><s0>Vérification programme</s0>
<s5>01</s5>
</fC03>
<fC03 i1="01" i2="X" l="ENG"><s0>Program verification</s0>
<s5>01</s5>
</fC03>
<fC03 i1="01" i2="X" l="SPA"><s0>Verificación programa</s0>
<s5>01</s5>
</fC03>
<fC03 i1="02" i2="X" l="FRE"><s0>Protocole internet</s0>
<s5>06</s5>
</fC03>
<fC03 i1="02" i2="X" l="ENG"><s0>Internet protocol</s0>
<s5>06</s5>
</fC03>
<fC03 i1="02" i2="X" l="SPA"><s0>Protocolo internet</s0>
<s5>06</s5>
</fC03>
<fC03 i1="03" i2="X" l="FRE"><s0>Protocole transmission</s0>
<s5>07</s5>
</fC03>
<fC03 i1="03" i2="X" l="ENG"><s0>Transmission protocol</s0>
<s5>07</s5>
</fC03>
<fC03 i1="03" i2="X" l="SPA"><s0>Protocolo transmisión</s0>
<s5>07</s5>
</fC03>
<fC03 i1="04" i2="X" l="FRE"><s0>Sécurité</s0>
<s5>08</s5>
</fC03>
<fC03 i1="04" i2="X" l="ENG"><s0>Safety</s0>
<s5>08</s5>
</fC03>
<fC03 i1="04" i2="X" l="SPA"><s0>Seguridad</s0>
<s5>08</s5>
</fC03>
<fC03 i1="05" i2="X" l="FRE"><s0>Langage formel</s0>
<s5>09</s5>
</fC03>
<fC03 i1="05" i2="X" l="ENG"><s0>Formal language</s0>
<s5>09</s5>
</fC03>
<fC03 i1="05" i2="X" l="SPA"><s0>Lenguaje formal</s0>
<s5>09</s5>
</fC03>
<fC03 i1="06" i2="X" l="FRE"><s0>Extensibilité</s0>
<s5>10</s5>
</fC03>
<fC03 i1="06" i2="X" l="ENG"><s0>Scalability</s0>
<s5>10</s5>
</fC03>
<fC03 i1="06" i2="X" l="SPA"><s0>Estensibilidad</s0>
<s5>10</s5>
</fC03>
<fC03 i1="07" i2="X" l="FRE"><s0>Validation</s0>
<s5>23</s5>
</fC03>
<fC03 i1="07" i2="X" l="ENG"><s0>Validation</s0>
<s5>23</s5>
</fC03>
<fC03 i1="07" i2="X" l="SPA"><s0>Validación</s0>
<s5>23</s5>
</fC03>
<fC03 i1="08" i2="X" l="FRE"><s0>Analyse automatique</s0>
<s5>24</s5>
</fC03>
<fC03 i1="08" i2="X" l="ENG"><s0>Automatic analysis</s0>
<s5>24</s5>
</fC03>
<fC03 i1="08" i2="X" l="SPA"><s0>Análisis automático</s0>
<s5>24</s5>
</fC03>
<fC03 i1="09" i2="X" l="FRE"><s0>Robustesse</s0>
<s5>25</s5>
</fC03>
<fC03 i1="09" i2="X" l="ENG"><s0>Robustness</s0>
<s5>25</s5>
</fC03>
<fC03 i1="09" i2="X" l="SPA"><s0>Robustez</s0>
<s5>25</s5>
</fC03>
<fN21><s1>241</s1>
</fN21>
<fN44 i1="01"><s1>OTO</s1>
</fN44>
<fN82><s1>OTO</s1>
</fN82>
</pA>
<pR><fA30 i1="01" i2="1" l="ENG"><s1>Computer aided verification. International conference</s1>
<s2>17</s2>
<s3>Edinburgh GBR</s3>
<s4>2005-07-06</s4>
</fA30>
</pR>
</standard>
<server><NO>PASCAL 05-0349048 INIST</NO>
<ET>The AVISPA tool for the automated validation of internet security protocols and applications</ET>
<AU>ARMANDO (A.); BASIN (D.); BOICHUT (Y.); CHEVALIER (Y.); COMPAGNA (L.); CUELLAR (J.); DRIELSMA (P. Hankes); HEAM (P. C.); KOUCHNARENKO (O.); MANTOVANI (J.); MÖDERSHEIM (S.); VON OHEIMB (D.); RUSINOWITCH (M.); SANTIAGO (J.); TURUANI (M.); VIGANO (L.); VIGNERON (L.); ETESSAMI (Kousha); RAJAMANI (Sriram K.)</AU>
<AF>AI-Lab, DIST, Università di Genova/Italie (1 aut., 5 aut., 10 aut.); Information Security Group, ETH Zurich/Suisse (2 aut., 7 aut., 11 aut., 16 aut.); LIFC, Université de Franche-Comté/Besancon/France (3 aut., 8 aut., 9 aut.); LORIA-INRIA-Lorraine/Nancy/France (4 aut., 13 aut., 14 aut., 15 aut., 17 aut.); Siemens AG, CT IC 3/Munich/Allemagne (6 aut., 12 aut.)</AF>
<DT>Publication en série; Congrès; Niveau analytique</DT>
<SO>Lecture notes in computer science; ISSN 0302-9743; Allemagne; Da. 2005; Vol. 3576; Pp. 281-285; Bibl. 14 ref.</SO>
<LA>Anglais</LA>
<EA>AVISPA is a push-button tool for the automated validation of Internet security-sensitive protocols and applications. It provides a modular and expressive formal language for specifying protocols and their security properties, and integrates different back-ends that implement a variety of state-of-the-art automatic analysis techniques. To the best of our knowledge, no other tool exhibits the same level of scope and robustness while enjoying the same performance and scalability.</EA>
<CC>001D02B04; 001D02B09</CC>
<FD>Vérification programme; Protocole internet; Protocole transmission; Sécurité; Langage formel; Extensibilité; Validation; Analyse automatique; Robustesse</FD>
<ED>Program verification; Internet protocol; Transmission protocol; Safety; Formal language; Scalability; Validation; Automatic analysis; Robustness</ED>
<SD>Verificación programa; Protocolo internet; Protocolo transmisión; Seguridad; Lenguaje formal; Estensibilidad; Validación; Análisis automático; Robustez</SD>
<LO>INIST-16343.354000124488910260</LO>
<ID>05-0349048</ID>
</server>
</inist>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/PascalFrancis/Corpus

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000544 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Corpus/biblio.hfd -nk 000544 | SxmlIndent | more

Pour mettre un lien sur cette page dans le réseau Wicri

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    PascalFrancis
   |étape=   Corpus
   |type=    RBID
   |clé=     Pascal:05-0349048
   |texte=   The AVISPA tool for the automated validation of internet security protocols and applications
}}

This area was generated with Dilib version V0.6.33.
Data generation: Mon Jun 10 21:56:28 2019. Site generation: Fri Feb 25 15:29:27 2022

	Serveur d'exploration sur la recherche en informatique en Lorraine
	Attention, ce site est en cours de développement ! Attention, site généré par des moyens informatiques à partir de corpus bruts. Les informations ne sont donc pas validées.

Serveur d'exploration sur la recherche en informatique en Lorraine

The AVISPA tool for the automated validation of internet security protocols and applications

The AVISPA tool for the automated validation of internet security protocols and applications

Source :

Descripteurs français

English descriptors

Abstract

Notice en format standard (ISO 2709)

Format Inist (serveur)

Links to Exploration step

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

Pour mettre un lien sur cette page dans le réseau Wicri