Automated Analysis of Security Protocols with Global State

Steve Kremer and Robert Künnemann. Automated Analysis of Security Protocols with Global State. In Proceedings of the 35th IEEE Symposium on Security and Privacy (S&P'14), pp. 163–178, IEEE Computer Society Press, San Jose, CA, USA, May 2014.
doi:10.1109/SP.2014.18

Download

[PDF] [PDF (long version)] [HTML] 

Abstract

Security APIs, key servers and protocols that need to keep the status of transactions, require to maintain a global, non-monotonic state, e.g., in the form of a database or register. However, most existing automated verification tools do not support the analysis of such stateful security protocols - sometimes because of fundamental reasons, such as the encoding of the protocol as Horn clauses, which are inherently monotonic. A notable exception is the recent tamarin prover which allows specifying protocols as multiset rewrite (MSR) rules, a formalism expressive enough to encode state. As multiset rewriting is a "low-level" specification language with no direct support for concurrent message passing, encoding protocols correctly is a difficult and error-prone process.
We propose a process calculus which is a variant of the applied pi calculus with constructs for manipulation of a global state by processes running in parallel. We show that this language can be translated to MSR rules whilst preserving all security properties expressible in a dedicated first-order logic for security properties. The translation has been implemented in a prototype tool which uses the tamarin prover as a backend. We apply the tool to several case studies among which a simplified fragment of PKCS#11, the Yubikey security token, and an optimistic contract signing protocol.

BibTeX

@inproceedings{KK-sp14,
  abstract =      {Security APIs, key servers and protocols that need
                  to keep the status of transactions, require to
                  maintain a global, non-monotonic state, e.g., in the
                  form of a database or register. However, most
                  existing automated verification tools do not support
                  the analysis of such stateful security protocols -
                  sometimes because of fundamental reasons, such as
                  the encoding of the protocol as Horn clauses, which
                  are inherently monotonic. A notable exception is the
                  recent tamarin prover which allows specifying
                  protocols as multiset rewrite (MSR) rules, a
                  formalism expressive enough to encode state. As
                  multiset rewriting is a "low-level" specification
                  language with no direct support for concurrent
                  message passing, encoding protocols correctly is a
                  difficult and error-prone process.\par We propose a
                  process calculus which is a variant of the applied
                  pi calculus with constructs for manipulation of a
                  global state by processes running in parallel. We
                  show that this language can be translated to MSR
                  rules whilst preserving all security properties
                  expressible in a dedicated first-order logic for
                  security properties. The translation has been
                  implemented in a prototype tool which uses the
                  tamarin prover as a backend. We apply the tool to
                  several case studies among which a simplified
                  fragment of PKCS#11, the Yubikey security token, and
                  an optimistic contract signing protocol.},
  address =       {San Jose, CA, USA},
  author =	  {Kremer, Steve and K{\"u}nnemann, Robert},
  booktitle =     {{P}roceedings of the 35th IEEE Symposium on Security and Privacy (S\&P'14)},
  DOI =           {10.1109/SP.2014.18},
  month =         may,
  pages     =     {163--178},
  publisher =     {{IEEE} Computer Society Press},
  title =         {Automated Analysis of Security Protocols with Global State},
  year =          {2014},
  acronym =       {{S\&P}'14},
  nmonth =        {5},
  url =           {https://members.loria.fr/skremer/files/Papers/KK-sp14.pdf},
}