Search Results

Documents authored by Sistla, A. Prasad

Document
Invited Paper
DOI: 10.4230/LIPIcs.FSTTCS.2018.2
Model Checking Randomized Security Protocols (Invited Paper)

Authors: A. Prasad Sistla

Published in: LIPIcs, Volume 122, 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018)

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)
Cite as

A. Prasad Sistla. Model Checking Randomized Security Protocols (Invited Paper). In 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 122, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{sistla:LIPIcs.FSTTCS.2018.2,
  author =	{Sistla, A. Prasad},
  title =	{{Model Checking Randomized Security Protocols}},
  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 =	{Ganguly, Sumit and Pandya, Paritosh},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2018.2},
  URN =		{urn:nbn:de:0030-drops-99018},
  doi =		{10.4230/LIPIcs.FSTTCS.2018.2},
  annote =	{Keywords: Randomized Protocols, Verification}
}
Document
DOI: 10.4230/LIPIcs.CSL.2018.14
Approximating Probabilistic Automata by Regular Languages

Authors: Rohit Chadha, A. Prasad Sistla, and Mahesh Viswanathan

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
A probabilistic finite automaton (PFA) A is said to be regular-approximable with respect to (x,y), if there is a regular language that contains all words accepted by A with probability at least x+y, but does not contain any word accepted with probability at most x. We show that the problem of determining if a PFA A is regular-approximable with respect to (x,y) is not recursively enumerable. We then show that many tractable sub-classes of PFAs identified in the literature - hierarchical PFAs, polynomially ambiguous PFAs, and eventually weakly ergodic PFAs - are regular-approximable with respect to all (x,y). Establishing the regular-approximability of a PFA has the nice consequence that its value can be effectively approximated, and the emptiness problem can be decided under the assumption of isolation.
Cite as

Rohit Chadha, A. Prasad Sistla, and Mahesh Viswanathan. Approximating Probabilistic Automata by Regular Languages. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 14:1-14:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{chadha_et_al:LIPIcs.CSL.2018.14,
  author =	{Chadha, Rohit and Sistla, A. Prasad and Viswanathan, Mahesh},
  title =	{{Approximating Probabilistic Automata by Regular Languages}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{14:1--14:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.14},
  URN =		{urn:nbn:de:0030-drops-96815},
  doi =		{10.4230/LIPIcs.CSL.2018.14},
  annote =	{Keywords: Probabilistic Finite Automata, Regular Languages, Ambiguity}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2010.364
Model Checking Concurrent Programs with Nondeterminism and Randomization

Authors: Rohit Chadha, A. Prasad Sistla, and Mahesh Viswanathan

Published in: LIPIcs, Volume 8, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)

Abstract
For concurrent probabilistic programs having process-level nondeterminism, it is often necessary to restrict the class of schedulers that resolve nondeterminism to obtain sound and precise model checking algorithms. In this paper, we introduce two classes of schedulers called view consistent and locally Markovian schedulers and consider the model checking problem of concurrent, probabilistic programs under these alternate semantics. Specifically, given a B\"{u}chi automaton $Spec$, a threshold $x$ in $[0,1]$, and a concurrent program $P$, the model checking problem asks if the measure of computations of $P$ that satisfy $Spec$ is at least $x$, under all view consistent (or locally Markovian) schedulers. We give precise complexity results for the model checking problem (for different classes of B\"{u}chi automata specifications) and contrast it with the complexity under the standard semantics that considers all schedulers.
Cite as

Rohit Chadha, A. Prasad Sistla, and Mahesh Viswanathan. Model Checking Concurrent Programs with Nondeterminism and Randomization. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010). Leibniz International Proceedings in Informatics (LIPIcs), Volume 8, pp. 364-375, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{chadha_et_al:LIPIcs.FSTTCS.2010.364,
  author =	{Chadha, Rohit and Sistla, A. Prasad and Viswanathan, Mahesh},
  title =	{{Model Checking Concurrent Programs with Nondeterminism and  Randomization}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)},
  pages =	{364--375},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-23-1},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{8},
  editor =	{Lodaya, Kamal and Mahajan, Meena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2010.364},
  URN =		{urn:nbn:de:0030-drops-28788},
  doi =		{10.4230/LIPIcs.FSTTCS.2010.364},
  annote =	{Keywords: view consistent scheduler, locally Markovian scheduler, model-checking, probabilistic program}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact