License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2018.2
URN: urn:nbn:de:0030-drops-99018
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/9901/
Go to the corresponding LIPIcs Volume Portal

Sistla, A. Prasad

Model Checking Randomized Security Protocols (Invited Paper)

pdf-format:
LIPIcs-FSTTCS-2018-2.pdf (0.2 MB)

Abstract

The design of security protocols is extremely subtle and is prone to serious faults. Many tools for automatic analysis of such protocols have been developed. However, none of them have the ability to model protocols that use explicit randomization. Such randomized protocols are being increasingly used in systems to provide privacy and anonymity guarantees. In this talk we consider the problem of automatic verification of randomized security protocols. We consider verification of secrecy and indistinguishability properties under a powerful threat model of Dolev-Yao adversary. We present some complexity bounds on verification of these properties. We also describe practical algorithms for checking indistinguishability. These algorithms have been implemented in the tool SPAN and have been experimentally evaluated. The talk concludes with future challenges.
(Joint work with: Matt Bauer, Rohit Chadha and Mahesh Viswanathan)

BibTeX - Entry

@InProceedings{sistla:LIPIcs:2018:9901,
  author =	{A. Prasad Sistla},
  title =	{{Model Checking Randomized Security Protocols (Invited Paper)}},
  booktitle =	{38th IARCS Annual Conference on Foundations of Software  Technology and Theoretical Computer Science (FSTTCS 2018)},
  pages =	{2:1--2:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-093-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{122},
  editor =	{Sumit Ganguly and Paritosh Pandya},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/9901},
  URN =		{urn:nbn:de:0030-drops-99018},
  doi =		{10.4230/LIPIcs.FSTTCS.2018.2},
  annote =	{Keywords: Randomized Protocols, Verification}
}

Keywords: Randomized Protocols, Verification
Collection: 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)
Issue Date: 2018
Date of publication: 05.12.2018

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI