Symbolic verification of privacy-type properties for security protocols with XOR

David Baelde, Stéphanie Delaune, Ivan Gazeau, and Steve Kremer. Symbolic verification of privacy-type properties for security protocols with XOR. In Proceedings of the 30th IEEE Computer Security Foundations Symposium (CSF'17), pp. 234–248, IEEE Computer Society Press, Santa Barbara, USA, August 2017.
doi:10.1109/CSF.2017.22

Download

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

Abstract

In symbolic verification of security protocols, process equivalences have recently been used extensively to model strong secrecy, anonymity and unlinkability properties. However, tool support for automated analysis of equivalence properties is limited compared to trace properties, \eg modeling authentication and weak notions of secrecy. In this paper, we present a novel procedure for verifying equivalences on finite processes, i.e., without replication, for protocols that rely on various cryptographic primitives including exclusive or (xor). We have implemented our procedure in the tool AKISS, and successfully used it on several case studies that are outside the scope of existing tools, e.g., unlinkability on various RFID protocols, and resistance against guessing attacks on protocols that use xor.

BibTeX

@inproceedings{BDGK-csf17,
  abstract =	 {In symbolic verification of security protocols,
                  process equivalences have recently been used
                  extensively to model strong secrecy, anonymity and
                  unlinkability properties. However, tool support for
                  automated analysis of equivalence properties is
                  limited compared to trace properties, \eg modeling
                  authentication and weak notions of secrecy. In this
                  paper, we present a novel procedure for verifying
                  equivalences on finite processes, i.e., without
                  replication, for protocols that rely on various
                  cryptographic primitives including exclusive or
                  (xor). We have implemented our procedure in the tool
                  AKISS, and successfully used it on several case
                  studies that are outside the scope of existing
                  tools, e.g., unlinkability on various RFID
                  protocols, and resistance against guessing attacks
                  on protocols that use xor. },
  address =	 {Santa Barbara, USA},
  author =	 {Baelde, David and Delaune, St{\'e}phanie and Gazeau,
                  Ivan and Kremer, Steve},
  booktitle =	 {{P}roceedings of the 30th {IEEE} {C}omputer
                  {S}ecurity {F}oundations {S}ymposium ({CSF}'17)},
  pages =        {234--248},
  doi =          {10.1109/CSF.2017.22},
  month =	 aug,
  publisher =	 {{IEEE} Computer Society Press},
  title =	 {Symbolic verification of privacy-type properties for
                  security protocols with XOR},
  year =	 2017,
  acronym =	 {{CSF}'17},
  nmonth =	 8,
}