Formal analysis for robust anti-SPIT protection using model checking
Identifieur interne : 000233 ( Istex/Corpus ); précédent : 000232; suivant : 000234Formal analysis for robust anti-SPIT protection using model checking
Auteurs : Dimitris Gritzalis ; Panagiotis Katsaros ; Stylianos Basagiannis ; Yannis SoupionisSource :
- International Journal of Information Security [ 1615-5262 ] ; 2012-04-01.
English descriptors
Abstract
Abstract: Anti-SPIT policies counter the SPam over Internet Telephony (SPIT) by distinguishing bots launching unsolicited bulks of VoIP calls from human beings. We propose an Anti-SPIT Policy Management mechanism (aSPM) that detects spam calls and prevents VoIP session establishment by the Session Initiation Protocol (SIP). The SPIN model checker is used to formally model and analyze the robustness of the aSPM mechanism in execution scenarios with parallel SIP sessions. In case of a possible design flaw, the model checker provides a trace of the caught unexpected behavior (counterexample), that can be used for the revision of the mechanism’s design. Our SPIN model is parameterized, based on measurements from experiments with VoIP users. Non-determinism plays a key role in representing all possible anti-SPIT policy decisions, in terms of the SIP messages that may be exchanged. The model checking results provide evidence for the timeliness of the parallel SIP sessions, the absence of deadlocks or livelocks, and the fairness for the VoIP service users. These findings ensure robust anti-SPIT protection, meaning that the aSPM mechanism operates as expected, despite the occurrence of random SPIT calls and communication error messages. To the best of our knowledge, this is the first analysis for exhaustively searching security policy flaws, due to complex interactions between anti-SPIT measures and the SIP protocol services.
Url:
DOI: 10.1007/s10207-012-0159-4
Links to Exploration step
ISTEX:B25A57002A7BE4BBB9F4DE934CE147BA6365546CLe document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Formal analysis for robust anti-SPIT protection using model checking</title><author><name sortKey="Gritzalis, Dimitris" sort="Gritzalis, Dimitris" uniqKey="Gritzalis D" first="Dimitris" last="Gritzalis">Dimitris Gritzalis</name><affiliation><mods:affiliation>Information Security and Critical Infrastructure Protection Research Laboratory, Department of Informatics, Athens University of Economics and Business (AUEB), 76 Patission Ave., 10434, Athens, Greece</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: dgrit@aueb.gr</mods:affiliation></affiliation></author><author><name sortKey="Katsaros, Panagiotis" sort="Katsaros, Panagiotis" uniqKey="Katsaros P" first="Panagiotis" last="Katsaros">Panagiotis Katsaros</name><affiliation><mods:affiliation>Dependability and Security Group, Department of Informatics, Aristotle University of Thessaloniki (AUTh), 54124, Thessaloniki, Greece</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: katsaros@csd.auth.gr</mods:affiliation></affiliation></author><author><name sortKey="Basagiannis, Stylianos" sort="Basagiannis, Stylianos" uniqKey="Basagiannis S" first="Stylianos" last="Basagiannis">Stylianos Basagiannis</name><affiliation><mods:affiliation>Dependability and Security Group, Department of Informatics, Aristotle University of Thessaloniki (AUTh), 54124, Thessaloniki, Greece</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: basags@csd.auth.gr</mods:affiliation></affiliation></author><author><name sortKey="Soupionis, Yannis" sort="Soupionis, Yannis" uniqKey="Soupionis Y" first="Yannis" last="Soupionis">Yannis Soupionis</name><affiliation><mods:affiliation>Information Security and Critical Infrastructure Protection Research Laboratory, Department of Informatics, Athens University of Economics and Business (AUEB), 76 Patission Ave., 10434, Athens, Greece</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: jsoup@aueb.gr</mods:affiliation></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:B25A57002A7BE4BBB9F4DE934CE147BA6365546C</idno><date when="2012" year="2012">2012</date><idno type="doi">10.1007/s10207-012-0159-4</idno><idno type="url">https://api.istex.fr/document/B25A57002A7BE4BBB9F4DE934CE147BA6365546C/fulltext/pdf</idno><idno type="wicri:Area/Istex/Corpus">000233</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">000233</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Formal analysis for robust anti-SPIT protection using model checking</title><author><name sortKey="Gritzalis, Dimitris" sort="Gritzalis, Dimitris" uniqKey="Gritzalis D" first="Dimitris" last="Gritzalis">Dimitris Gritzalis</name><affiliation><mods:affiliation>Information Security and Critical Infrastructure Protection Research Laboratory, Department of Informatics, Athens University of Economics and Business (AUEB), 76 Patission Ave., 10434, Athens, Greece</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: dgrit@aueb.gr</mods:affiliation></affiliation></author><author><name sortKey="Katsaros, Panagiotis" sort="Katsaros, Panagiotis" uniqKey="Katsaros P" first="Panagiotis" last="Katsaros">Panagiotis Katsaros</name><affiliation><mods:affiliation>Dependability and Security Group, Department of Informatics, Aristotle University of Thessaloniki (AUTh), 54124, Thessaloniki, Greece</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: katsaros@csd.auth.gr</mods:affiliation></affiliation></author><author><name sortKey="Basagiannis, Stylianos" sort="Basagiannis, Stylianos" uniqKey="Basagiannis S" first="Stylianos" last="Basagiannis">Stylianos Basagiannis</name><affiliation><mods:affiliation>Dependability and Security Group, Department of Informatics, Aristotle University of Thessaloniki (AUTh), 54124, Thessaloniki, Greece</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: basags@csd.auth.gr</mods:affiliation></affiliation></author><author><name sortKey="Soupionis, Yannis" sort="Soupionis, Yannis" uniqKey="Soupionis Y" first="Yannis" last="Soupionis">Yannis Soupionis</name><affiliation><mods:affiliation>Information Security and Critical Infrastructure Protection Research Laboratory, Department of Informatics, Athens University of Economics and Business (AUEB), 76 Patission Ave., 10434, Athens, Greece</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: jsoup@aueb.gr</mods:affiliation></affiliation></author></analytic><monogr></monogr><series><title level="j">International Journal of Information Security</title><title level="j" type="abbrev">Int. J. Inf. Secur.</title><idno type="ISSN">1615-5262</idno><idno type="eISSN">1615-5270</idno><imprint><publisher>Springer-Verlag</publisher><pubPlace>Berlin/Heidelberg</pubPlace><date type="published" when="2012-04-01">2012-04-01</date><biblScope unit="volume">11</biblScope><biblScope unit="issue">2</biblScope><biblScope unit="page" from="121">121</biblScope><biblScope unit="page" to="135">135</biblScope></imprint><idno type="ISSN">1615-5262</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">1615-5262</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Anti-SPIT security policies</term><term>Model checking</term><term>Robustness analysis</term><term>Voice over IP (VoIP)</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: Anti-SPIT policies counter the SPam over Internet Telephony (SPIT) by distinguishing bots launching unsolicited bulks of VoIP calls from human beings. We propose an Anti-SPIT Policy Management mechanism (aSPM) that detects spam calls and prevents VoIP session establishment by the Session Initiation Protocol (SIP). The SPIN model checker is used to formally model and analyze the robustness of the aSPM mechanism in execution scenarios with parallel SIP sessions. In case of a possible design flaw, the model checker provides a trace of the caught unexpected behavior (counterexample), that can be used for the revision of the mechanism’s design. Our SPIN model is parameterized, based on measurements from experiments with VoIP users. Non-determinism plays a key role in representing all possible anti-SPIT policy decisions, in terms of the SIP messages that may be exchanged. The model checking results provide evidence for the timeliness of the parallel SIP sessions, the absence of deadlocks or livelocks, and the fairness for the VoIP service users. These findings ensure robust anti-SPIT protection, meaning that the aSPM mechanism operates as expected, despite the occurrence of random SPIT calls and communication error messages. To the best of our knowledge, this is the first analysis for exhaustively searching security policy flaws, due to complex interactions between anti-SPIT measures and the SIP protocol services.</div></front></TEI><istex><corpusName>springer-journals</corpusName><author><json:item><name>Dimitris Gritzalis</name><affiliations><json:string>Information Security and Critical Infrastructure Protection Research Laboratory, Department of Informatics, Athens University of Economics and Business (AUEB), 76 Patission Ave., 10434, Athens, Greece</json:string><json:string>E-mail: dgrit@aueb.gr</json:string></affiliations></json:item><json:item><name>Panagiotis Katsaros</name><affiliations><json:string>Dependability and Security Group, Department of Informatics, Aristotle University of Thessaloniki (AUTh), 54124, Thessaloniki, Greece</json:string><json:string>E-mail: katsaros@csd.auth.gr</json:string></affiliations></json:item><json:item><name>Stylianos Basagiannis</name><affiliations><json:string>Dependability and Security Group, Department of Informatics, Aristotle University of Thessaloniki (AUTh), 54124, Thessaloniki, Greece</json:string><json:string>E-mail: basags@csd.auth.gr</json:string></affiliations></json:item><json:item><name>Yannis Soupionis</name><affiliations><json:string>Information Security and Critical Infrastructure Protection Research Laboratory, Department of Informatics, Athens University of Economics and Business (AUEB), 76 Patission Ave., 10434, Athens, Greece</json:string><json:string>E-mail: jsoup@aueb.gr</json:string></affiliations></json:item></author><subject><json:item><lang><json:string>eng</json:string></lang><value>Voice over IP (VoIP)</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>Anti-SPIT security policies</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>Robustness analysis</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>Model checking</value></json:item></subject><articleId><json:string>159</json:string><json:string>s10207-012-0159-4</json:string></articleId><arkIstex>ark:/67375/VQC-WMP3Z5Q9-1</arkIstex><language><json:string>eng</json:string></language><originalGenre><json:string>OriginalPaper</json:string></originalGenre><abstract>Abstract: Anti-SPIT policies counter the SPam over Internet Telephony (SPIT) by distinguishing bots launching unsolicited bulks of VoIP calls from human beings. We propose an Anti-SPIT Policy Management mechanism (aSPM) that detects spam calls and prevents VoIP session establishment by the Session Initiation Protocol (SIP). The SPIN model checker is used to formally model and analyze the robustness of the aSPM mechanism in execution scenarios with parallel SIP sessions. In case of a possible design flaw, the model checker provides a trace of the caught unexpected behavior (counterexample), that can be used for the revision of the mechanism’s design. Our SPIN model is parameterized, based on measurements from experiments with VoIP users. Non-determinism plays a key role in representing all possible anti-SPIT policy decisions, in terms of the SIP messages that may be exchanged. The model checking results provide evidence for the timeliness of the parallel SIP sessions, the absence of deadlocks or livelocks, and the fairness for the VoIP service users. These findings ensure robust anti-SPIT protection, meaning that the aSPM mechanism operates as expected, despite the occurrence of random SPIT calls and communication error messages. To the best of our knowledge, this is the first analysis for exhaustively searching security policy flaws, due to complex interactions between anti-SPIT measures and the SIP protocol services.</abstract><qualityIndicators><score>9.592</score><pdfWordCount>7627</pdfWordCount><pdfCharCount>47606</pdfCharCount><pdfVersion>1.4</pdfVersion><pdfPageCount>15</pdfPageCount><pdfPageSize>595.276 x 790.866 pts</pdfPageSize><refBibsNative>false</refBibsNative><abstractWordCount>216</abstractWordCount><abstractCharCount>1441</abstractCharCount><keywordCount>4</keywordCount></qualityIndicators><title>Formal analysis for robust anti-SPIT protection using model checking</title><genre><json:string>research-article</json:string></genre><host><title>International Journal of Information Security</title><language><json:string>unknown</json:string></language><publicationDate>2012</publicationDate><copyrightDate>2012</copyrightDate><issn><json:string>1615-5262</json:string></issn><eissn><json:string>1615-5270</json:string></eissn><journalId><json:string>10207</json:string></journalId><volume>11</volume><issue>2</issue><pages><first>121</first><last>135</last></pages><genre><json:string>journal</json:string></genre><subject><json:item><value>Data Encryption</value></json:item><json:item><value>Communications Engineering, Networks</value></json:item><json:item><value>Operating Systems</value></json:item><json:item><value>Coding and Information Theory</value></json:item><json:item><value>Management of Computing and Information Systems</value></json:item><json:item><value>Computer Communication Networks</value></json:item></subject></host><ark><json:string>ark:/67375/VQC-WMP3Z5Q9-1</json:string></ark><publicationDate>2012</publicationDate><copyrightDate>2012</copyrightDate><doi><json:string>10.1007/s10207-012-0159-4</json:string></doi><id>B25A57002A7BE4BBB9F4DE934CE147BA6365546C</id><score>1</score><fulltext><json:item><extension>pdf</extension><original>true</original><mimetype>application/pdf</mimetype><uri>https://api.istex.fr/document/B25A57002A7BE4BBB9F4DE934CE147BA6365546C/fulltext/pdf</uri></json:item><json:item><extension>zip</extension><original>false</original><mimetype>application/zip</mimetype><uri>https://api.istex.fr/document/B25A57002A7BE4BBB9F4DE934CE147BA6365546C/fulltext/zip</uri></json:item><json:item><extension>txt</extension><original>false</original><mimetype>text/plain</mimetype><uri>https://api.istex.fr/document/B25A57002A7BE4BBB9F4DE934CE147BA6365546C/fulltext/txt</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/document/B25A57002A7BE4BBB9F4DE934CE147BA6365546C/fulltext/tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">Formal analysis for robust anti-SPIT protection using model checking</title><respStmt><resp>Références bibliographiques récupérées via GROBID</resp><name resp="ISTEX-API">ISTEX-API (INIST-CNRS)</name></respStmt></titleStmt><publicationStmt><authority>ISTEX</authority><publisher scheme="https://publisher-list.data.istex.fr">Springer-Verlag</publisher><pubPlace>Berlin/Heidelberg</pubPlace><availability><licence><p>Springer-Verlag, 2012</p></licence><p scheme="https://loaded-corpus.data.istex.fr/ark:/67375/XBH-3XSW68JL-F">springer</p></availability><date>2012</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><note>Regular Contribution</note></notesStmt><sourceDesc><biblStruct type="inbook"><analytic><title level="a" type="main" xml:lang="en">Formal analysis for robust anti-SPIT protection using model checking</title><author xml:id="author-0000" corresp="yes"><persName><forename type="first">Dimitris</forename><surname>Gritzalis</surname></persName><email>dgrit@aueb.gr</email><affiliation>Information Security and Critical Infrastructure Protection Research Laboratory, Department of Informatics, Athens University of Economics and Business (AUEB), 76 Patission Ave., 10434, Athens, Greece</affiliation></author><author xml:id="author-0001"><persName><forename type="first">Panagiotis</forename><surname>Katsaros</surname></persName><email>katsaros@csd.auth.gr</email><affiliation>Dependability and Security Group, Department of Informatics, Aristotle University of Thessaloniki (AUTh), 54124, Thessaloniki, Greece</affiliation></author><author xml:id="author-0002"><persName><forename type="first">Stylianos</forename><surname>Basagiannis</surname></persName><email>basags@csd.auth.gr</email><affiliation>Dependability and Security Group, Department of Informatics, Aristotle University of Thessaloniki (AUTh), 54124, Thessaloniki, Greece</affiliation></author><author xml:id="author-0003"><persName><forename type="first">Yannis</forename><surname>Soupionis</surname></persName><email>jsoup@aueb.gr</email><affiliation>Information Security and Critical Infrastructure Protection Research Laboratory, Department of Informatics, Athens University of Economics and Business (AUEB), 76 Patission Ave., 10434, Athens, Greece</affiliation></author><idno type="istex">B25A57002A7BE4BBB9F4DE934CE147BA6365546C</idno><idno type="ark">ark:/67375/VQC-WMP3Z5Q9-1</idno><idno type="DOI">10.1007/s10207-012-0159-4</idno><idno type="article-id">159</idno><idno type="article-id">s10207-012-0159-4</idno></analytic><monogr><title level="j">International Journal of Information Security</title><title level="j" type="abbrev">Int. J. Inf. Secur.</title><idno type="pISSN">1615-5262</idno><idno type="eISSN">1615-5270</idno><idno type="journal-ID">true</idno><idno type="journal-SPIN">30643369</idno><idno type="issue-article-count">4</idno><idno type="volume-issue-count">6</idno><imprint><publisher>Springer-Verlag</publisher><pubPlace>Berlin/Heidelberg</pubPlace><date type="published" when="2012-04-01"></date><biblScope unit="volume">11</biblScope><biblScope unit="issue">2</biblScope><biblScope unit="page" from="121">121</biblScope><biblScope unit="page" to="135">135</biblScope></imprint></monogr></biblStruct></sourceDesc></fileDesc><profileDesc><creation><date>2012</date></creation><langUsage><language ident="en">en</language></langUsage><abstract xml:lang="en"><p>Abstract: Anti-SPIT policies counter the SPam over Internet Telephony (SPIT) by distinguishing bots launching unsolicited bulks of VoIP calls from human beings. We propose an Anti-SPIT Policy Management mechanism (aSPM) that detects spam calls and prevents VoIP session establishment by the Session Initiation Protocol (SIP). The SPIN model checker is used to formally model and analyze the robustness of the aSPM mechanism in execution scenarios with parallel SIP sessions. In case of a possible design flaw, the model checker provides a trace of the caught unexpected behavior (counterexample), that can be used for the revision of the mechanism’s design. Our SPIN model is parameterized, based on measurements from experiments with VoIP users. Non-determinism plays a key role in representing all possible anti-SPIT policy decisions, in terms of the SIP messages that may be exchanged. The model checking results provide evidence for the timeliness of the parallel SIP sessions, the absence of deadlocks or livelocks, and the fairness for the VoIP service users. These findings ensure robust anti-SPIT protection, meaning that the aSPM mechanism operates as expected, despite the occurrence of random SPIT calls and communication error messages. To the best of our knowledge, this is the first analysis for exhaustively searching security policy flaws, due to complex interactions between anti-SPIT measures and the SIP protocol services.</p></abstract><textClass xml:lang="en"><keywords scheme="keyword"><list><head>Keywords</head><item><term>Voice over IP (VoIP)</term></item><item><term>Anti-SPIT security policies</term></item><item><term>Robustness analysis</term></item><item><term>Model checking</term></item></list></keywords></textClass><textClass><keywords scheme="Journal Subject"><list><head>Computer Science</head><item><term>Data Encryption</term></item><item><term>Communications Engineering, Networks</term></item><item><term>Operating Systems</term></item><item><term>Coding and Information Theory</term></item><item><term>Management of Computing and Information Systems</term></item><item><term>Computer Communication Networks</term></item></list></keywords></textClass></profileDesc><revisionDesc><change when="2012-04-01">Published</change><change xml:id="refBibs-istex" who="#ISTEX-API" when="2017-12-2">References added</change></revisionDesc></teiHeader></istex:fulltextTEI></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>Springer-Verlag</PublisherName><PublisherLocation>Berlin/Heidelberg</PublisherLocation></PublisherInfo><Journal OutputMedium="All"><JournalInfo JournalProductType="ArchiveJournal" NumberingStyle="ContentOnly"><JournalID>10207</JournalID><JournalPrintISSN>1615-5262</JournalPrintISSN><JournalElectronicISSN>1615-5270</JournalElectronicISSN><JournalSPIN>30643369</JournalSPIN><JournalTitle>International Journal of Information Security</JournalTitle><JournalAbbreviatedTitle>Int. J. Inf. Secur.</JournalAbbreviatedTitle><JournalSubjectGroup><JournalSubject Type="Primary">Computer Science</JournalSubject><JournalSubject Type="Secondary">Data Encryption</JournalSubject><JournalSubject Type="Secondary">Communications Engineering, Networks</JournalSubject><JournalSubject Type="Secondary">Operating Systems</JournalSubject><JournalSubject Type="Secondary">Coding and Information Theory</JournalSubject><JournalSubject Type="Secondary">Management of Computing and Information Systems</JournalSubject><JournalSubject Type="Secondary">Computer Communication Networks</JournalSubject></JournalSubjectGroup></JournalInfo><Volume OutputMedium="All"><VolumeInfo TocLevels="0" VolumeType="Regular"><VolumeIDStart>11</VolumeIDStart><VolumeIDEnd>11</VolumeIDEnd><VolumeIssueCount>6</VolumeIssueCount></VolumeInfo><Issue IssueType="Regular" OutputMedium="All"><IssueInfo IssueType="Regular" TocLevels="0"><IssueIDStart>2</IssueIDStart><IssueIDEnd>2</IssueIDEnd><IssueArticleCount>4</IssueArticleCount><IssueHistory><OnlineDate><Year>2012</Year><Month>3</Month><Day>13</Day></OnlineDate><PrintDate><Year>2012</Year><Month>3</Month><Day>12</Day></PrintDate><CoverDate><Year>2012</Year><Month>4</Month></CoverDate><PricelistYear>2012</PricelistYear></IssueHistory><IssueCopyright><CopyrightHolderName>Springer-Verlag</CopyrightHolderName><CopyrightYear>2012</CopyrightYear></IssueCopyright></IssueInfo><Article ID="s10207-012-0159-4" OutputMedium="All"><ArticleInfo ArticleType="OriginalPaper" ContainsESM="No" Language="En" NumberingStyle="ContentOnly" TocLevels="0"><ArticleID>159</ArticleID><ArticleDOI>10.1007/s10207-012-0159-4</ArticleDOI><ArticleSequenceNumber>4</ArticleSequenceNumber><ArticleTitle Language="En">Formal analysis for robust anti-SPIT protection using model checking</ArticleTitle><ArticleCategory>Regular Contribution</ArticleCategory><ArticleFirstPage>121</ArticleFirstPage><ArticleLastPage>135</ArticleLastPage><ArticleHistory><RegistrationDate><Year>2012</Year><Month>1</Month><Day>25</Day></RegistrationDate><OnlineDate><Year>2012</Year><Month>2</Month><Day>12</Day></OnlineDate></ArticleHistory><ArticleCopyright><CopyrightHolderName>Springer-Verlag</CopyrightHolderName><CopyrightYear>2012</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></ArticleInfo><ArticleHeader><AuthorGroup><Author AffiliationIDS="Aff1" CorrespondingAffiliationID="Aff1"><AuthorName DisplayOrder="Western"><GivenName>Dimitris</GivenName><FamilyName>Gritzalis</FamilyName></AuthorName><Contact><Email>dgrit@aueb.gr</Email></Contact></Author><Author AffiliationIDS="Aff2"><AuthorName DisplayOrder="Western"><GivenName>Panagiotis</GivenName><FamilyName>Katsaros</FamilyName></AuthorName><Contact><Email>katsaros@csd.auth.gr</Email></Contact></Author><Author AffiliationIDS="Aff2"><AuthorName DisplayOrder="Western"><GivenName>Stylianos</GivenName><FamilyName>Basagiannis</FamilyName></AuthorName><Contact><Email>basags@csd.auth.gr</Email></Contact></Author><Author AffiliationIDS="Aff1"><AuthorName DisplayOrder="Western"><GivenName>Yannis</GivenName><FamilyName>Soupionis</FamilyName></AuthorName><Contact><Email>jsoup@aueb.gr</Email></Contact></Author><Affiliation ID="Aff1"><OrgDivision>Information Security and Critical Infrastructure Protection Research Laboratory, Department of Informatics</OrgDivision><OrgName>Athens University of Economics and Business (AUEB)</OrgName><OrgAddress><Street>76 Patission Ave.</Street><Postcode>10434</Postcode><City>Athens</City><Country Code="GR">Greece</Country></OrgAddress></Affiliation><Affiliation ID="Aff2"><OrgDivision>Dependability and Security Group, Department of Informatics</OrgDivision><OrgName>Aristotle University of Thessaloniki (AUTh)</OrgName><OrgAddress><Postcode>54124</Postcode><City>Thessaloniki</City><Country Code="GR">Greece</Country></OrgAddress></Affiliation></AuthorGroup><Abstract ID="Abs1" Language="En"><Heading>Abstract</Heading><Para>Anti-SPIT policies counter the SPam over Internet Telephony (SPIT) by distinguishing bots launching unsolicited bulks of VoIP calls from human beings. We propose an Anti-SPIT Policy Management mechanism (aSPM) that detects spam calls and prevents VoIP session establishment by the Session Initiation Protocol (SIP). The SPIN model checker is used to formally model and analyze the robustness of the aSPM mechanism in execution scenarios with parallel SIP sessions. In case of a possible design flaw, the model checker provides a trace of the caught unexpected behavior (counterexample), that can be used for the revision of the mechanism’s design. Our SPIN model is parameterized, based on measurements from experiments with VoIP users. Non-determinism plays a key role in representing all possible anti-SPIT policy decisions, in terms of the SIP messages that may be exchanged. The model checking results provide evidence for the timeliness of the parallel SIP sessions, the absence of deadlocks or livelocks, and the fairness for the VoIP service users. These findings ensure robust anti-SPIT protection, meaning that the aSPM mechanism operates as expected, despite the occurrence of random SPIT calls and communication error messages. To the best of our knowledge, this is the first analysis for exhaustively searching security policy flaws, due to complex interactions between anti-SPIT measures and the SIP protocol services.</Para></Abstract><KeywordGroup Language="En"><Heading>Keywords</Heading><Keyword>Voice over IP (VoIP)</Keyword><Keyword>Anti-SPIT security policies</Keyword><Keyword>Robustness analysis</Keyword><Keyword>Model checking</Keyword></KeywordGroup></ArticleHeader><NoBody></NoBody></Article></Issue></Volume></Journal></Publisher></istex:document></istex:metadataXml><mods version="3.6"><titleInfo lang="en"><title>Formal analysis for robust anti-SPIT protection using model checking</title></titleInfo><titleInfo type="alternative" contentType="CDATA" lang="en"><title>Formal analysis for robust anti-SPIT protection using model checking</title></titleInfo><name type="personal" displayLabel="corresp"><namePart type="given">Dimitris</namePart><namePart type="family">Gritzalis</namePart><affiliation>Information Security and Critical Infrastructure Protection Research Laboratory, Department of Informatics, Athens University of Economics and Business (AUEB), 76 Patission Ave., 10434, Athens, Greece</affiliation><affiliation>E-mail: dgrit@aueb.gr</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Panagiotis</namePart><namePart type="family">Katsaros</namePart><affiliation>Dependability and Security Group, Department of Informatics, Aristotle University of Thessaloniki (AUTh), 54124, Thessaloniki, Greece</affiliation><affiliation>E-mail: katsaros@csd.auth.gr</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Stylianos</namePart><namePart type="family">Basagiannis</namePart><affiliation>Dependability and Security Group, Department of Informatics, Aristotle University of Thessaloniki (AUTh), 54124, Thessaloniki, Greece</affiliation><affiliation>E-mail: basags@csd.auth.gr</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Yannis</namePart><namePart type="family">Soupionis</namePart><affiliation>Information Security and Critical Infrastructure Protection Research Laboratory, Department of Informatics, Athens University of Economics and Business (AUEB), 76 Patission Ave., 10434, Athens, Greece</affiliation><affiliation>E-mail: jsoup@aueb.gr</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>Springer-Verlag</publisher><place><placeTerm type="text">Berlin/Heidelberg</placeTerm></place><dateIssued encoding="w3cdtf">2012-04-01</dateIssued><dateIssued encoding="w3cdtf">2012</dateIssued><copyrightDate encoding="w3cdtf">2012</copyrightDate></originInfo><language><languageTerm type="code" authority="rfc3066">en</languageTerm><languageTerm type="code" authority="iso639-2b">eng</languageTerm></language><abstract lang="en">Abstract: Anti-SPIT policies counter the SPam over Internet Telephony (SPIT) by distinguishing bots launching unsolicited bulks of VoIP calls from human beings. We propose an Anti-SPIT Policy Management mechanism (aSPM) that detects spam calls and prevents VoIP session establishment by the Session Initiation Protocol (SIP). The SPIN model checker is used to formally model and analyze the robustness of the aSPM mechanism in execution scenarios with parallel SIP sessions. In case of a possible design flaw, the model checker provides a trace of the caught unexpected behavior (counterexample), that can be used for the revision of the mechanism’s design. Our SPIN model is parameterized, based on measurements from experiments with VoIP users. Non-determinism plays a key role in representing all possible anti-SPIT policy decisions, in terms of the SIP messages that may be exchanged. The model checking results provide evidence for the timeliness of the parallel SIP sessions, the absence of deadlocks or livelocks, and the fairness for the VoIP service users. These findings ensure robust anti-SPIT protection, meaning that the aSPM mechanism operates as expected, despite the occurrence of random SPIT calls and communication error messages. To the best of our knowledge, this is the first analysis for exhaustively searching security policy flaws, due to complex interactions between anti-SPIT measures and the SIP protocol services.</abstract><note>Regular Contribution</note><subject lang="en"><genre>Keywords</genre><topic>Voice over IP (VoIP)</topic><topic>Anti-SPIT security policies</topic><topic>Robustness analysis</topic><topic>Model checking</topic></subject><relatedItem type="host"><titleInfo><title>International Journal of Information Security</title></titleInfo><titleInfo type="abbreviated"><title>Int. J. Inf. Secur.</title></titleInfo><genre type="journal" displayLabel="Archive Journal" authority="ISTEX" valueURI="https://publication-type.data.istex.fr/ark:/67375/JMC-0GLKJH51-B">journal</genre><originInfo><publisher>Springer</publisher><dateIssued encoding="w3cdtf">2012-03-13</dateIssued><copyrightDate encoding="w3cdtf">2012</copyrightDate></originInfo><subject><genre>Computer Science</genre><topic>Data Encryption</topic><topic>Communications Engineering, Networks</topic><topic>Operating Systems</topic><topic>Coding and Information Theory</topic><topic>Management of Computing and Information Systems</topic><topic>Computer Communication Networks</topic></subject><identifier type="ISSN">1615-5262</identifier><identifier type="eISSN">1615-5270</identifier><identifier type="JournalID">10207</identifier><identifier type="JournalSPIN">30643369</identifier><identifier type="IssueArticleCount">4</identifier><identifier type="VolumeIssueCount">6</identifier><part><date>2012</date><detail type="volume"><number>11</number><caption>vol.</caption></detail><detail type="issue"><number>2</number><caption>no.</caption></detail><extent unit="pages"><start>121</start><end>135</end></extent></part><recordInfo><recordOrigin>Springer-Verlag, 2012</recordOrigin></recordInfo></relatedItem><identifier type="istex">B25A57002A7BE4BBB9F4DE934CE147BA6365546C</identifier><identifier type="ark">ark:/67375/VQC-WMP3Z5Q9-1</identifier><identifier type="DOI">10.1007/s10207-012-0159-4</identifier><identifier type="ArticleID">159</identifier><identifier type="ArticleID">s10207-012-0159-4</identifier><accessCondition type="use and reproduction" contentType="copyright">Springer-Verlag, 2012</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>Springer-Verlag, 2012</recordOrigin></recordInfo></mods><json:item><extension>json</extension><original>false</original><mimetype>application/json</mimetype><uri>https://api.istex.fr/document/B25A57002A7BE4BBB9F4DE934CE147BA6365546C/metadata/json</uri></json:item></metadata><serie></serie></istex></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Musique/explor/XenakisV1/Data/Istex/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000233 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 000233 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Musique
|area= XenakisV1
|flux= Istex
|étape= Corpus
|type= RBID
|clé= ISTEX:B25A57002A7BE4BBB9F4DE934CE147BA6365546C
|texte= Formal analysis for robust anti-SPIT protection using model checking
}}
| This area was generated with Dilib version V0.6.33. |  |