Steve Kremer: Epistemic Logic for the Applied Pi Calculus

Epistemic Logic for the Applied Pi Calculus

Rohit Chadha, Stéphanie Delaune, and Steve Kremer. Epistemic Logic for the Applied Pi Calculus. In Proceedings of IFIP International Conference on Formal Techniques for Distributed Systems (FMOODS/FORTE'09), pp. 182–197, Lecture Notes in Computer Science 5522, Springer, Lisbon, Portugal, June 2009.
doi:10.1007/978-3-642-02138-1_12

Download

[PDF] [PS] [HTML]

Abstract

We propose an epistemic logic for the applied pi calculus, which is a variant of the pi calculus with extensions for modeling cryptographic protocols. In such a calculus, the security guarantees are usually stated as equivalences. While process calculi provide a natural means to describe the protocols themselves, epistemic logics are often better suited for expressing certain security properties such as secrecy and anonymity.
We intend to bridge the gap between these two approaches: using the set of traces generated by a process as models, we define a logic which has constructs for reasoning about both intruder's epistemic knowledge and the set of messages in possession of the intruder. As an example we consider two formalizations of privacy in electronic voting and study the relationship between them.

BibTeX

@inproceedings{CDK-forte09,
  abstract =      {We propose an epistemic logic for the applied pi
                   calculus, which is a variant of the pi calculus with
                   extensions for modeling cryptographic protocols. In
                   such a calculus, the security guarantees are usually
                   stated as equivalences. While process calculi provide
                   a natural means to describe the protocols themselves,
                   epistemic logics are often better suited for
                   expressing certain security properties such as
                   secrecy and anonymity.\par We intend to bridge the
                   gap between these two approaches: using the set of
                   traces generated by a process as models, we define a
                   logic which has constructs for reasoning about both
                   intruder's epistemic knowledge and the set of
                   messages in possession of the intruder. As an example
                   we consider two formalizations of privacy in
                   electronic voting and study the relationship between
                   them.},
  address =       {Lisbon, Portugal},
  author =        {Chadha, Rohit and Delaune, St{\'e}phanie and
                   Kremer, Steve},
  booktitle =     {{P}roceedings of {IFIP} {I}nternational {C}onference
                   on {F}ormal {T}echniques for {D}istributed {S}ystems
                   ({FMOODS/FORTE}'09)},
  DOI =           {10.1007/978-3-642-02138-1_12},
  editor =        {Lee, David and Lopes, Ant{\'o}nia and
                   Poetzsch-Heffter, Arnd},
  month =         jun,
  pages =         {182-197},
  publisher =     {Springer},
  series =        {Lecture Notes in Computer Science},
  title =         {Epistemic Logic for the Applied Pi Calculus},
  volume =        {5522},
  year =          {2009},
  acronym =       {{FMOODS/FORTE}'09},
  nmonth =        {6},
  url =           {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/cdk-forte09.pdf},
}