Strategy for Verifying Security Protocols with Unbounded Message Size
Identifieur interne : 002E74 ( Istex/Corpus ); précédent : 002E73; suivant : 002E75Strategy for Verifying Security Protocols with Unbounded Message Size
Auteurs : Y. Chevalier ; L. VigneronSource :
- Automated Software Engineering [ 0928-8910 ] ; 2004-04-01.
English descriptors
Abstract
Abstract: We present a system for automatically verifying cryptographic protocols. This system manages the knowledge of principals and checks if the protocol is runnable. In this case, it outputs a set of rewrite rules describing the protocol itself, the strategy of an intruder, and the goal to achieve. The protocol specification language permits to express commonly used descriptions of properties (authentication, short term secrecy, and so on) as well as complex data structures such as tables and hash functions. The generated rewrite rules can be used for detecting flaws with various systems: theorem proving in first-order logic, on-the-fly model-checking, or SAT-based state exploration. These three techniques are being experimented in the European Union project AVISPA. The aim of this paper is to describe the analysis process. First, we describe the major steps of the compilation process of a protocol description by our tool Casrul. Then, we describe the behavior of the intruder defined for the analysis. Our intruder is based on a lazy strategy, and is implemented as rewrite rules for the theorem prover daTac. Another advantage of our model is that it permits to handle parallel executions of the protocol and composition of keys. And for sake of completeness, it is possible, using Casrul, to either specify an unbounded number of executions or an unbounded message size. The combination of Casrul and daTac has permitted successful studying of various protocols, such as NSPK, EKE, RSA, Neumann-Stubblebine, Kao-Chow and Otway-Rees. We detail some of these examples in this paper. We are now studying the SET protocol and have already very encouraging results.
Url:
DOI: 10.1023/B:AUSE.0000017741.10347.9b
Links to Exploration step
ISTEX:C4E26DFDE651735571C3245C003C9272FC877F30Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Strategy for Verifying Security Protocols with Unbounded Message Size</title><author><name sortKey="Chevalier, Y" sort="Chevalier, Y" uniqKey="Chevalier Y" first="Y." last="Chevalier">Y. Chevalier</name><affiliation><mods:affiliation>LORIA, UHP, UN2, Campus Scientifique, B.P. 239, 54506, Vandæuvre-lès-Nancy Cedex, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: chevalie@loria.fr</mods:affiliation></affiliation></author><author><name sortKey="Vigneron, L" sort="Vigneron, L" uniqKey="Vigneron L" first="L." last="Vigneron">L. Vigneron</name><affiliation><mods:affiliation>LORIA, UHP, UN2, Campus Scientifique, B.P. 239, 54506, Vandæuvre-lès-Nancy Cedex, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: vigneron@loria.fr</mods:affiliation></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:C4E26DFDE651735571C3245C003C9272FC877F30</idno><date when="2004" year="2004">2004</date><idno type="doi">10.1023/B:AUSE.0000017741.10347.9b</idno><idno type="url">https://api.istex.fr/ark:/67375/VQC-MBZ0V23C-7/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">002E74</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">002E74</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Strategy for Verifying Security Protocols with Unbounded Message Size</title><author><name sortKey="Chevalier, Y" sort="Chevalier, Y" uniqKey="Chevalier Y" first="Y." last="Chevalier">Y. Chevalier</name><affiliation><mods:affiliation>LORIA, UHP, UN2, Campus Scientifique, B.P. 239, 54506, Vandæuvre-lès-Nancy Cedex, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: chevalie@loria.fr</mods:affiliation></affiliation></author><author><name sortKey="Vigneron, L" sort="Vigneron, L" uniqKey="Vigneron L" first="L." last="Vigneron">L. Vigneron</name><affiliation><mods:affiliation>LORIA, UHP, UN2, Campus Scientifique, B.P. 239, 54506, Vandæuvre-lès-Nancy Cedex, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: vigneron@loria.fr</mods:affiliation></affiliation></author></analytic><monogr></monogr><series><title level="j">Automated Software Engineering</title><title level="j" type="sub">An International Journal</title><title level="j" type="abbrev">Automated Software Engineering</title><idno type="ISSN">0928-8910</idno><idno type="eISSN">1573-7535</idno><imprint><publisher>Kluwer Academic Publishers</publisher><pubPlace>Boston</pubPlace><date type="published" when="2004-04-01">2004-04-01</date><biblScope unit="volume">11</biblScope><biblScope unit="issue">2</biblScope><biblScope unit="page" from="141">141</biblScope><biblScope unit="page" to="166">166</biblScope></imprint><idno type="ISSN">0928-8910</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0928-8910</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>automatic strategies</term><term>flaw detection</term><term>intruder model</term><term>security protocols</term><term>verification</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: We present a system for automatically verifying cryptographic protocols. This system manages the knowledge of principals and checks if the protocol is runnable. In this case, it outputs a set of rewrite rules describing the protocol itself, the strategy of an intruder, and the goal to achieve. The protocol specification language permits to express commonly used descriptions of properties (authentication, short term secrecy, and so on) as well as complex data structures such as tables and hash functions. The generated rewrite rules can be used for detecting flaws with various systems: theorem proving in first-order logic, on-the-fly model-checking, or SAT-based state exploration. These three techniques are being experimented in the European Union project AVISPA. The aim of this paper is to describe the analysis process. First, we describe the major steps of the compilation process of a protocol description by our tool Casrul. Then, we describe the behavior of the intruder defined for the analysis. Our intruder is based on a lazy strategy, and is implemented as rewrite rules for the theorem prover daTac. Another advantage of our model is that it permits to handle parallel executions of the protocol and composition of keys. And for sake of completeness, it is possible, using Casrul, to either specify an unbounded number of executions or an unbounded message size. The combination of Casrul and daTac has permitted successful studying of various protocols, such as NSPK, EKE, RSA, Neumann-Stubblebine, Kao-Chow and Otway-Rees. We detail some of these examples in this paper. We are now studying the SET protocol and have already very encouraging results.</div></front></TEI><istex><corpusName>springer-journals</corpusName><author><json:item><name>Y. Chevalier</name><affiliations><json:string>LORIA, UHP, UN2, Campus Scientifique, B.P. 239, 54506, Vandæuvre-lès-Nancy Cedex, France</json:string><json:string>E-mail: chevalie@loria.fr</json:string></affiliations></json:item><json:item><name>L. Vigneron</name><affiliations><json:string>LORIA, UHP, UN2, Campus Scientifique, B.P. 239, 54506, Vandæuvre-lès-Nancy Cedex, France</json:string><json:string>E-mail: vigneron@loria.fr</json:string></affiliations></json:item></author><subject><json:item><lang><json:string>eng</json:string></lang><value>security protocols</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>verification</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>flaw detection</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>intruder model</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>automatic strategies</value></json:item></subject><articleId><json:string>5266195</json:string><json:string>Art3</json:string></articleId><arkIstex>ark:/67375/VQC-MBZ0V23C-7</arkIstex><language><json:string>eng</json:string></language><originalGenre><json:string>OriginalPaper</json:string></originalGenre><abstract>Abstract: We present a system for automatically verifying cryptographic protocols. This system manages the knowledge of principals and checks if the protocol is runnable. In this case, it outputs a set of rewrite rules describing the protocol itself, the strategy of an intruder, and the goal to achieve. The protocol specification language permits to express commonly used descriptions of properties (authentication, short term secrecy, and so on) as well as complex data structures such as tables and hash functions. The generated rewrite rules can be used for detecting flaws with various systems: theorem proving in first-order logic, on-the-fly model-checking, or SAT-based state exploration. These three techniques are being experimented in the European Union project AVISPA. The aim of this paper is to describe the analysis process. First, we describe the major steps of the compilation process of a protocol description by our tool Casrul. Then, we describe the behavior of the intruder defined for the analysis. Our intruder is based on a lazy strategy, and is implemented as rewrite rules for the theorem prover daTac. Another advantage of our model is that it permits to handle parallel executions of the protocol and composition of keys. And for sake of completeness, it is possible, using Casrul, to either specify an unbounded number of executions or an unbounded message size. The combination of Casrul and daTac has permitted successful studying of various protocols, such as NSPK, EKE, RSA, Neumann-Stubblebine, Kao-Chow and Otway-Rees. We detail some of these examples in this paper. We are now studying the SET protocol and have already very encouraging results.</abstract><qualityIndicators><score>10</score><pdfWordCount>10236</pdfWordCount><pdfCharCount>55828</pdfCharCount><pdfVersion>1.4</pdfVersion><pdfPageCount>26</pdfPageCount><pdfPageSize>595 x 842 pts (A4)</pdfPageSize><refBibsNative>false</refBibsNative><abstractWordCount>262</abstractWordCount><abstractCharCount>1682</abstractCharCount><keywordCount>5</keywordCount></qualityIndicators><title>Strategy for Verifying Security Protocols with Unbounded Message Size</title><genre><json:string>research-article</json:string></genre><host><title>Automated Software Engineering</title><language><json:string>unknown</json:string></language><publicationDate>2004</publicationDate><copyrightDate>2004</copyrightDate><issn><json:string>0928-8910</json:string></issn><eissn><json:string>1573-7535</json:string></eissn><journalId><json:string>10515</json:string></journalId><volume>11</volume><issue>2</issue><pages><first>141</first><last>166</last></pages><genre><json:string>journal</json:string></genre><subject><json:item><value>Software Engineering/Programming and Operating Systems</value></json:item><json:item><value>Artificial Intelligence (incl. Robotics)</value></json:item></subject></host><ark><json:string>ark:/67375/VQC-MBZ0V23C-7</json:string></ark><publicationDate>2004</publicationDate><copyrightDate>2004</copyrightDate><doi><json:string>10.1023/B:AUSE.0000017741.10347.9b</json:string></doi><id>C4E26DFDE651735571C3245C003C9272FC877F30</id><score>1</score><fulltext><json:item><extension>pdf</extension><original>true</original><mimetype>application/pdf</mimetype><uri>https://api.istex.fr/ark:/67375/VQC-MBZ0V23C-7/fulltext.pdf</uri></json:item><json:item><extension>zip</extension><original>false</original><mimetype>application/zip</mimetype><uri>https://api.istex.fr/ark:/67375/VQC-MBZ0V23C-7/bundle.zip</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/ark:/67375/VQC-MBZ0V23C-7/fulltext.tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">Strategy for Verifying Security Protocols with Unbounded Message Size</title></titleStmt><publicationStmt><authority>ISTEX</authority><publisher scheme="https://scientific-publisher.data.istex.fr">Kluwer Academic Publishers</publisher><pubPlace>Boston</pubPlace><availability><licence><p>Kluwer Academic Publishers, 2004</p></licence><p scheme="https://loaded-corpus.data.istex.fr/ark:/67375/XBH-3XSW68JL-F">springer</p></availability><date>2004</date></publicationStmt><notesStmt><note type="research-article" scheme="https://content-type.data.istex.fr/ark:/67375/XTP-1JC4F85T-7">research-article</note><note type="journal" scheme="https://publication-type.data.istex.fr/ark:/67375/JMC-0GLKJH51-B">journal</note></notesStmt><sourceDesc><biblStruct type="inbook"><analytic><title level="a" type="main" xml:lang="en">Strategy for Verifying Security Protocols with Unbounded Message Size</title><author xml:id="author-0000"><persName><forename type="first">Y.</forename><surname>Chevalier</surname></persName><email>chevalie@loria.fr</email><affiliation>LORIA, UHP, UN2, Campus Scientifique, B.P. 239, 54506, Vandæuvre-lès-Nancy Cedex, France</affiliation></author><author xml:id="author-0001"><persName><forename type="first">L.</forename><surname>Vigneron</surname></persName><email>vigneron@loria.fr</email><affiliation>LORIA, UHP, UN2, Campus Scientifique, B.P. 239, 54506, Vandæuvre-lès-Nancy Cedex, France</affiliation></author><idno type="istex">C4E26DFDE651735571C3245C003C9272FC877F30</idno><idno type="ark">ark:/67375/VQC-MBZ0V23C-7</idno><idno type="DOI">10.1023/B:AUSE.0000017741.10347.9b</idno><idno type="article-id">5266195</idno><idno type="article-id">Art3</idno></analytic><monogr><title level="j">Automated Software Engineering</title><title level="j" type="sub">An International Journal</title><title level="j" type="abbrev">Automated Software Engineering</title><idno type="pISSN">0928-8910</idno><idno type="eISSN">1573-7535</idno><idno type="journal-ID">true</idno><idno type="issue-article-count">5</idno><idno type="volume-issue-count">4</idno><imprint><publisher>Kluwer Academic Publishers</publisher><pubPlace>Boston</pubPlace><date type="published" when="2004-04-01"></date><biblScope unit="volume">11</biblScope><biblScope unit="issue">2</biblScope><biblScope unit="page" from="141">141</biblScope><biblScope unit="page" to="166">166</biblScope></imprint></monogr></biblStruct></sourceDesc></fileDesc><profileDesc><creation><date>2004</date></creation><langUsage><language ident="en">en</language></langUsage><abstract xml:lang="en"><p>Abstract: We present a system for automatically verifying cryptographic protocols. This system manages the knowledge of principals and checks if the protocol is runnable. In this case, it outputs a set of rewrite rules describing the protocol itself, the strategy of an intruder, and the goal to achieve. The protocol specification language permits to express commonly used descriptions of properties (authentication, short term secrecy, and so on) as well as complex data structures such as tables and hash functions. The generated rewrite rules can be used for detecting flaws with various systems: theorem proving in first-order logic, on-the-fly model-checking, or SAT-based state exploration. These three techniques are being experimented in the European Union project AVISPA. The aim of this paper is to describe the analysis process. First, we describe the major steps of the compilation process of a protocol description by our tool Casrul. Then, we describe the behavior of the intruder defined for the analysis. Our intruder is based on a lazy strategy, and is implemented as rewrite rules for the theorem prover daTac. Another advantage of our model is that it permits to handle parallel executions of the protocol and composition of keys. And for sake of completeness, it is possible, using Casrul, to either specify an unbounded number of executions or an unbounded message size. The combination of Casrul and daTac has permitted successful studying of various protocols, such as NSPK, EKE, RSA, Neumann-Stubblebine, Kao-Chow and Otway-Rees. We detail some of these examples in this paper. We are now studying the SET protocol and have already very encouraging results.</p></abstract><textClass xml:lang="en"><keywords scheme="keyword"><list><item><term>security protocols</term></item><item><term>verification</term></item><item><term>flaw detection</term></item><item><term>intruder model</term></item><item><term>automatic strategies</term></item></list></keywords></textClass><textClass><keywords scheme="Journal Subject"><list><head>Computer Science</head><item><term>Software Engineering/Programming and Operating Systems</term></item><item><term>Artificial Intelligence (incl. Robotics)</term></item></list></keywords></textClass></profileDesc><revisionDesc><change when="2004-04-01">Published</change></revisionDesc></teiHeader></istex:fulltextTEI><json:item><extension>txt</extension><original>false</original><mimetype>text/plain</mimetype><uri>https://api.istex.fr/ark:/67375/VQC-MBZ0V23C-7/fulltext.txt</uri></json:item></fulltext><metadata><istex:metadataXml wicri:clean="corpus springer-journals not found" wicri:toSee="no header"><istex:xmlDeclaration>version="1.0" encoding="UTF-8"</istex:xmlDeclaration><istex:docType PUBLIC="-//Springer-Verlag//DTD A++ V2.4//EN" URI="http://devel.springer.de/A++/V2.4/DTD/A++V2.4.dtd" name="istex:docType"></istex:docType><istex:document><Publisher><PublisherInfo><PublisherName>Kluwer Academic Publishers</PublisherName><PublisherLocation>Boston</PublisherLocation></PublisherInfo><Journal><JournalInfo JournalProductType="ArchiveJournal" NumberingStyle="Unnumbered"><JournalID>10515</JournalID><JournalPrintISSN>0928-8910</JournalPrintISSN><JournalElectronicISSN>1573-7535</JournalElectronicISSN><JournalTitle>Automated Software Engineering</JournalTitle><JournalSubTitle>An International Journal</JournalSubTitle><JournalAbbreviatedTitle>Automated Software Engineering</JournalAbbreviatedTitle><JournalSubjectGroup><JournalSubject Type="Primary">Computer Science</JournalSubject><JournalSubject Type="Secondary">Software Engineering/Programming and Operating Systems</JournalSubject><JournalSubject Type="Secondary">Artificial Intelligence (incl. Robotics)</JournalSubject></JournalSubjectGroup></JournalInfo><Volume><VolumeInfo VolumeType="Regular" TocLevels="0"><VolumeIDStart>11</VolumeIDStart><VolumeIDEnd>11</VolumeIDEnd><VolumeIssueCount>4</VolumeIssueCount></VolumeInfo><Issue IssueType="Regular"><IssueInfo TocLevels="0"><IssueIDStart>2</IssueIDStart><IssueIDEnd>2</IssueIDEnd><IssueTitle Language="En">Special Section on Automated Verification of Infinite-State Systems</IssueTitle><IssueArticleCount>5</IssueArticleCount><IssueHistory><CoverDate><Year>2004</Year><Month>4</Month></CoverDate></IssueHistory><IssueCopyright><CopyrightHolderName>Kluwer Academic Publishers</CopyrightHolderName><CopyrightYear>2004</CopyrightYear></IssueCopyright></IssueInfo><Article ID="Art3"><ArticleInfo Language="En" ArticleType="OriginalPaper" NumberingStyle="Unnumbered" TocLevels="0" ContainsESM="No"><ArticleID>5266195</ArticleID><ArticleDOI>10.1023/B:AUSE.0000017741.10347.9b</ArticleDOI><ArticleSequenceNumber>3</ArticleSequenceNumber><ArticleTitle Language="En">Strategy for Verifying Security Protocols with Unbounded Message Size</ArticleTitle><ArticleFirstPage>141</ArticleFirstPage><ArticleLastPage>166</ArticleLastPage><ArticleHistory><RegistrationDate><Year>2004</Year><Month>10</Month><Day>2</Day></RegistrationDate></ArticleHistory><ArticleCopyright><CopyrightHolderName>Kluwer Academic Publishers</CopyrightHolderName><CopyrightYear>2004</CopyrightYear></ArticleCopyright><ArticleGrants Type="Regular"><MetadataGrant Grant="OpenAccess"></MetadataGrant><AbstractGrant Grant="OpenAccess"></AbstractGrant><BodyPDFGrant Grant="Restricted"></BodyPDFGrant><BodyHTMLGrant Grant="Restricted"></BodyHTMLGrant><BibliographyGrant Grant="Restricted"></BibliographyGrant><ESMGrant Grant="Restricted"></ESMGrant></ArticleGrants><ArticleContext><JournalID>10515</JournalID><VolumeIDStart>11</VolumeIDStart><VolumeIDEnd>11</VolumeIDEnd><IssueIDStart>2</IssueIDStart><IssueIDEnd>2</IssueIDEnd></ArticleContext></ArticleInfo><ArticleHeader><AuthorGroup><Author AffiliationIDS="Aff1"><AuthorName DisplayOrder="Western"><GivenName>Y.</GivenName><FamilyName>Chevalier</FamilyName></AuthorName><Contact><Email>chevalie@loria.fr</Email></Contact></Author><Author AffiliationIDS="Aff1"><AuthorName DisplayOrder="Western"><GivenName>L.</GivenName><FamilyName>Vigneron</FamilyName></AuthorName><Contact><Email>vigneron@loria.fr</Email></Contact></Author><Affiliation ID="Aff1"><OrgDivision>LORIA</OrgDivision><OrgName>UHP, UN2, Campus Scientifique</OrgName><OrgAddress><Postbox>B.P. 239</Postbox><Postcode>54506</Postcode><City>Vandæuvre-lès-Nancy Cedex</City><Country>France</Country></OrgAddress></Affiliation></AuthorGroup><Abstract ID="Abs1" Language="En"><Heading>Abstract</Heading><Para>We present a system for automatically verifying cryptographic protocols. This system manages the knowledge of principals and checks if the protocol is runnable. In this case, it outputs a set of rewrite rules describing the protocol itself, the strategy of an intruder, and the goal to achieve. The protocol specification language permits to express commonly used descriptions of properties (authentication, short term secrecy, and so on) as well as complex data structures such as tables and hash functions. The generated rewrite rules can be used for detecting flaws with various systems: theorem proving in first-order logic, on-the-fly model-checking, or SAT-based state exploration. These three techniques are being experimented in the European Union project AVISPA.</Para><Para>The aim of this paper is to describe the analysis process. First, we describe the major steps of the compilation process of a protocol description by our tool Casrul. Then, we describe the behavior of the intruder defined for the analysis. Our intruder is based on a lazy strategy, and is implemented as rewrite rules for the theorem prover daTac. Another advantage of our model is that it permits to handle parallel executions of the protocol and composition of keys. And for sake of completeness, it is possible, using Casrul, to either specify an unbounded number of executions or an unbounded message size.</Para><Para>The combination of Casrul and daTac has permitted successful studying of various protocols, such as NSPK, EKE, RSA, Neumann-Stubblebine, Kao-Chow and Otway-Rees. We detail some of these examples in this paper. We are now studying the SET protocol and have already very encouraging results.</Para></Abstract><KeywordGroup Language="En"><Keyword>security protocols</Keyword><Keyword>verification</Keyword><Keyword>flaw detection</Keyword><Keyword>intruder model</Keyword><Keyword>automatic strategies</Keyword></KeywordGroup></ArticleHeader><NoBody></NoBody></Article></Issue></Volume></Journal></Publisher></istex:document></istex:metadataXml><mods version="3.6"><titleInfo lang="en"><title>Strategy for Verifying Security Protocols with Unbounded Message Size</title></titleInfo><titleInfo type="alternative" contentType="CDATA"><title>Strategy for Verifying Security Protocols with Unbounded Message Size</title></titleInfo><name type="personal"><namePart type="given">Y.</namePart><namePart type="family">Chevalier</namePart><affiliation>LORIA, UHP, UN2, Campus Scientifique, B.P. 239, 54506, Vandæuvre-lès-Nancy Cedex, France</affiliation><affiliation>E-mail: chevalie@loria.fr</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">L.</namePart><namePart type="family">Vigneron</namePart><affiliation>LORIA, UHP, UN2, Campus Scientifique, B.P. 239, 54506, Vandæuvre-lès-Nancy Cedex, France</affiliation><affiliation>E-mail: vigneron@loria.fr</affiliation><role><roleTerm type="text">author</roleTerm></role></name><typeOfResource>text</typeOfResource><genre type="research-article" displayLabel="OriginalPaper" authority="ISTEX" authorityURI="https://content-type.data.istex.fr" valueURI="https://content-type.data.istex.fr/ark:/67375/XTP-1JC4F85T-7">research-article</genre><originInfo><publisher>Kluwer Academic Publishers</publisher><place><placeTerm type="text">Boston</placeTerm></place><dateIssued encoding="w3cdtf">2004-04-01</dateIssued><copyrightDate encoding="w3cdtf">2004</copyrightDate></originInfo><language><languageTerm type="code" authority="rfc3066">en</languageTerm><languageTerm type="code" authority="iso639-2b">eng</languageTerm></language><abstract lang="en">Abstract: We present a system for automatically verifying cryptographic protocols. This system manages the knowledge of principals and checks if the protocol is runnable. In this case, it outputs a set of rewrite rules describing the protocol itself, the strategy of an intruder, and the goal to achieve. The protocol specification language permits to express commonly used descriptions of properties (authentication, short term secrecy, and so on) as well as complex data structures such as tables and hash functions. The generated rewrite rules can be used for detecting flaws with various systems: theorem proving in first-order logic, on-the-fly model-checking, or SAT-based state exploration. These three techniques are being experimented in the European Union project AVISPA. The aim of this paper is to describe the analysis process. First, we describe the major steps of the compilation process of a protocol description by our tool Casrul. Then, we describe the behavior of the intruder defined for the analysis. Our intruder is based on a lazy strategy, and is implemented as rewrite rules for the theorem prover daTac. Another advantage of our model is that it permits to handle parallel executions of the protocol and composition of keys. And for sake of completeness, it is possible, using Casrul, to either specify an unbounded number of executions or an unbounded message size. The combination of Casrul and daTac has permitted successful studying of various protocols, such as NSPK, EKE, RSA, Neumann-Stubblebine, Kao-Chow and Otway-Rees. We detail some of these examples in this paper. We are now studying the SET protocol and have already very encouraging results.</abstract><subject lang="en"><topic>security protocols</topic><topic>verification</topic><topic>flaw detection</topic><topic>intruder model</topic><topic>automatic strategies</topic></subject><relatedItem type="host"><titleInfo><title>Automated Software Engineering</title><subTitle>An International Journal</subTitle></titleInfo><titleInfo type="abbreviated"><title>Automated Software Engineering</title></titleInfo><genre type="journal" authority="ISTEX" authorityURI="https://publication-type.data.istex.fr" valueURI="https://publication-type.data.istex.fr/ark:/67375/JMC-0GLKJH51-B">journal</genre><originInfo><publisher>Springer</publisher><dateIssued encoding="w3cdtf">2004-04-01</dateIssued><copyrightDate encoding="w3cdtf">2004</copyrightDate></originInfo><subject><genre>Computer Science</genre><topic>Software Engineering/Programming and Operating Systems</topic><topic>Artificial Intelligence (incl. Robotics)</topic></subject><identifier type="ISSN">0928-8910</identifier><identifier type="eISSN">1573-7535</identifier><identifier type="JournalID">10515</identifier><identifier type="IssueArticleCount">5</identifier><identifier type="VolumeIssueCount">4</identifier><part><date>2004</date><detail type="issue"><title>Special Section on Automated Verification of Infinite-State Systems</title></detail><detail type="volume"><number>11</number><caption>vol.</caption></detail><detail type="issue"><number>2</number><caption>no.</caption></detail><extent unit="pages"><start>141</start><end>166</end></extent></part><recordInfo><recordOrigin>Kluwer Academic Publishers, 2004</recordOrigin></recordInfo></relatedItem><identifier type="istex">C4E26DFDE651735571C3245C003C9272FC877F30</identifier><identifier type="ark">ark:/67375/VQC-MBZ0V23C-7</identifier><identifier type="DOI">10.1023/B:AUSE.0000017741.10347.9b</identifier><identifier type="ArticleID">5266195</identifier><identifier type="ArticleID">Art3</identifier><accessCondition type="use and reproduction" contentType="copyright">Kluwer Academic Publishers, 2004</accessCondition><recordInfo><recordContentSource authority="ISTEX" authorityURI="https://loaded-corpus.data.istex.fr" valueURI="https://loaded-corpus.data.istex.fr/ark:/67375/XBH-3XSW68JL-F">springer</recordContentSource><recordOrigin>Kluwer Academic Publishers, 2004</recordOrigin></recordInfo></mods><json:item><extension>json</extension><original>false</original><mimetype>application/json</mimetype><uri>https://api.istex.fr/ark:/67375/VQC-MBZ0V23C-7/record.json</uri></json:item></metadata><serie></serie></istex></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Istex/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 002E74 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 002E74 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Istex
|étape= Corpus
|type= RBID
|clé= ISTEX:C4E26DFDE651735571C3245C003C9272FC877F30
|texte= Strategy for Verifying Security Protocols with Unbounded Message Size
}}
| This area was generated with Dilib version V0.6.33. |  |