5 Search Results for "Chadha, Rohit"

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-dev.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-dev.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.2014.505
Computing Information Flow Using Symbolic Model-Checking

Authors: Rohit Chadha, Umang Mathur, and Stefan Schwoon

Published in: LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

Abstract
Several measures have been proposed in literature for quantifying the information leaked by the public outputs of a program with secret inputs. We consider the problem of computing information leaked by a deterministic or probabilistic program when the measure of information is based on (a) min-entropy and (b) Shannon entropy. The key challenge in computing these measures is that we need the total number of possible outputs and, for each possible output, the number of inputs that lead to it. A direct computation of these quantities is infeasible because of the state-explosion problem. We therefore propose symbolic algorithms based on binary decision diagrams (BDDs). The advantage of our approach is that these symbolic algorithms can be easily implemented in any BDD-based model-checking tool that checks for reachability in deterministic non-recursive programs by computing program summaries. We demonstrate the validity of our approach by implementing these algorithms in a tool Moped-QLeak, which is built upon Moped, a model checker for Boolean programs. Finally, we show how this symbolic approach extends to probabilistic programs.
Cite as

Rohit Chadha, Umang Mathur, and Stefan Schwoon. Computing Information Flow Using Symbolic Model-Checking. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 505-516, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{chadha_et_al:LIPIcs.FSTTCS.2014.505,
  author =	{Chadha, Rohit and Mathur, Umang and Schwoon, Stefan},
  title =	{{Computing Information Flow Using Symbolic Model-Checking}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{505--516},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Raman, Venkatesh and Suresh, S. P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.505},
  URN =		{urn:nbn:de:0030-drops-48676},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.505},
  annote =	{Keywords: Information leakage, Min Entropy, Shannon Entropy, Abstract decision diagrams, Program summaries}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2012.534
The Complexity of Quantitative Information Flow in Recursive Programs

Authors: Rohit Chadha and Michael Ummels

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

Abstract
Information-theoretic measures based upon mutual information can be employed to quantify the information that an execution of a program reveals about its secret inputs. The information leakage bounding problem asks whether the information leaked by a program does not exceed a given threshold. We consider this problem for two scenarios: a) the outputs of the program are revealed, and b)the timing (measured in the number of execution steps) of the program is revealed. For both scenarios, we establish complexity results in the context of deterministic boolean programs, both for programs with and without recursion. In particular, we prove that for recursive programs the information leakage bounding problem is no harder than checking reachability.
Cite as

Rohit Chadha and Michael Ummels. The Complexity of Quantitative Information Flow in Recursive Programs. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 18, pp. 534-545, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{chadha_et_al:LIPIcs.FSTTCS.2012.534,
  author =	{Chadha, Rohit and Ummels, Michael},
  title =	{{The Complexity of Quantitative Information Flow in Recursive Programs}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)},
  pages =	{534--545},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-47-7},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{18},
  editor =	{D'Souza, Deepak and Radhakrishnan, Jaikumar and Telikepalli, Kavitha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2012.534},
  URN =		{urn:nbn:de:0030-drops-38872},
  doi =		{10.4230/LIPIcs.FSTTCS.2012.534},
  annote =	{Keywords: quantitative information flow, recursive programs, program analysis, verification, computational complexity}
}
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-dev.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}
}
  • Refine by Author
  • 4 Chadha, Rohit
  • 3 Sistla, A. Prasad
  • 2 Viswanathan, Mahesh
  • 1 Mathur, Umang
  • 1 Schwoon, Stefan
  • Show More...

  • Refine by Classification
  • 1 Theory of computation → Logic and verification
  • 1 Theory of computation → Probabilistic computation

  • Refine by Keyword
  • 1 Abstract decision diagrams
  • 1 Ambiguity
  • 1 Information leakage
  • 1 Min Entropy
  • 1 Probabilistic Finite Automata
  • Show More...

  • Refine by Type
  • 5 document

  • Refine by Publication Year
  • 2 2018
  • 1 2010
  • 1 2012
  • 1 2014

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 Imprint Privacy Contact