Formal analysis for robust anti-SPIT protection using model checking
Identifieur interne : 000061 ( Main/Curation ); précédent : 000060; suivant : 000062Formal analysis for robust anti-SPIT protection using model checking
Auteurs : Dimitris Gritzalis [Grèce] ; Panagiotis Katsaros [Grèce] ; Stylianos Basagiannis [Grèce] ; Yannis Soupionis [Grèce]Source :
- 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 toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: Pour aller vers cette notice dans l'étape Curation :000233
- to stream Istex, to step Curation: Pour aller vers cette notice dans l'étape Curation :000233
- to stream Istex, to step Checkpoint: Pour aller vers cette notice dans l'étape Curation :000014
- to stream Main, to step Merge: Pour aller vers cette notice dans l'étape Curation :000061
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>
</author>
<author><name sortKey="Katsaros, Panagiotis" sort="Katsaros, Panagiotis" uniqKey="Katsaros P" first="Panagiotis" last="Katsaros">Panagiotis Katsaros</name>
</author>
<author><name sortKey="Basagiannis, Stylianos" sort="Basagiannis, Stylianos" uniqKey="Basagiannis S" first="Stylianos" last="Basagiannis">Stylianos Basagiannis</name>
</author>
<author><name sortKey="Soupionis, Yannis" sort="Soupionis, Yannis" uniqKey="Soupionis Y" first="Yannis" last="Soupionis">Yannis Soupionis</name>
</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>
<idno type="wicri:Area/Istex/Curation">000233</idno>
<idno type="wicri:Area/Istex/Checkpoint">000014</idno>
<idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">000014</idno>
<idno type="wicri:doubleKey">1615-5262:2012:Gritzalis D:formal:analysis:for</idno>
<idno type="wicri:Area/Main/Merge">000061</idno>
<idno type="wicri:Area/Main/Curation">000061</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 wicri:level="3"><country xml:lang="fr">Grèce</country>
<wicri:regionArea>Information Security and Critical Infrastructure Protection Research Laboratory, Department of Informatics, Athens University of Economics and Business (AUEB), 76 Patission Ave., 10434, Athens</wicri:regionArea>
<placeName><settlement type="city">Athènes</settlement>
<region nuts="2" type="region">Attique (région)</region>
</placeName>
</affiliation>
<affiliation wicri:level="1"><country wicri:rule="url">Grèce</country>
</affiliation>
</author>
<author><name sortKey="Katsaros, Panagiotis" sort="Katsaros, Panagiotis" uniqKey="Katsaros P" first="Panagiotis" last="Katsaros">Panagiotis Katsaros</name>
<affiliation wicri:level="1"><country xml:lang="fr">Grèce</country>
<wicri:regionArea>Dependability and Security Group, Department of Informatics, Aristotle University of Thessaloniki (AUTh), 54124, Thessaloniki</wicri:regionArea>
<wicri:noRegion>Thessaloniki</wicri:noRegion>
</affiliation>
<affiliation wicri:level="1"><country wicri:rule="url">Grèce</country>
</affiliation>
</author>
<author><name sortKey="Basagiannis, Stylianos" sort="Basagiannis, Stylianos" uniqKey="Basagiannis S" first="Stylianos" last="Basagiannis">Stylianos Basagiannis</name>
<affiliation wicri:level="1"><country xml:lang="fr">Grèce</country>
<wicri:regionArea>Dependability and Security Group, Department of Informatics, Aristotle University of Thessaloniki (AUTh), 54124, Thessaloniki</wicri:regionArea>
<wicri:noRegion>Thessaloniki</wicri:noRegion>
</affiliation>
<affiliation wicri:level="1"><country wicri:rule="url">Grèce</country>
</affiliation>
</author>
<author><name sortKey="Soupionis, Yannis" sort="Soupionis, Yannis" uniqKey="Soupionis Y" first="Yannis" last="Soupionis">Yannis Soupionis</name>
<affiliation wicri:level="3"><country xml:lang="fr">Grèce</country>
<wicri:regionArea>Information Security and Critical Infrastructure Protection Research Laboratory, Department of Informatics, Athens University of Economics and Business (AUEB), 76 Patission Ave., 10434, Athens</wicri:regionArea>
<placeName><settlement type="city">Athènes</settlement>
<region nuts="2" type="region">Attique (région)</region>
</placeName>
</affiliation>
<affiliation wicri:level="1"><country wicri:rule="url">Grèce</country>
</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>
</record>
Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Musique/explor/XenakisV1/Data/Main/Curation
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000061 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Curation/biblio.hfd -nk 000061 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien |wiki= Wicri/Musique |area= XenakisV1 |flux= Main |étape= Curation |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. |