Document Open Access Logo

Analysing Privacy-Type Properties in Cryptographic Protocols (Invited Talk)

Author Stéphanie Delaune

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2018.1.pdf
  • Filesize: 0.5 MB
  • 21 pages

Document Identifiers

Author Details

Stéphanie Delaune
  • Univ Rennes, CNRS, IRISA, France

Funding

This work has been partially supported by the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation program (grant agreement No 714955-POPSTAR) and the ANR project TECAP.

Cite AsGet BibTex

Stéphanie Delaune. Analysing Privacy-Type Properties in Cryptographic Protocols (Invited Talk). In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 1:1-1:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.FSCD.2018.1

Abstract

Cryptographic protocols aim at securing communications over insecure networks such as the Internet, where dishonest users may listen to communications and interfere with them. For example, passports are no more pure paper documents. Instead, they contain a chip that stores additional information such as pictures and fingerprints of their holder. In order to ensure privacy, these chips include a mechanism, i.e. a cryptographic protocol, that does not let the passport disclose private information to external users except the intended terminal. This is just a single example but of course privacy appears in many other contexts such as RFIDs technologies or electronic voting. Formal methods have been successfully applied to automatically analyse traditional protocols and discover their flaws. Privacy-type security properties (e.g. anonymity, unlinkability, vote secrecy, ...) are expressed relying on a notion of behavioural equivalence, and are actually more difficult to analyse than confidentiality and authentication properties. We will discuss some recent advances that have been done to analyse automatically equivalence-based security properties, and we will review some issues that remain to be solved in this field.

Subject Classification

ACM Subject Classification
  • Security and privacy → Logic and verification
Keywords
  • cryptographic protocols
  • symbolic models
  • privacy-related properties
  • behavioural equivalence

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. M. Abadi and V. Cortier. Deciding knowledge in security protocols under equational theories. Theoretical Computer Science, 387(1-2):2-32, 2006. Google Scholar
  2. M. Abadi and C. Fournet. Mobile values, new names, and secure communication. In Proc. 28th Symposium on Principles of Programming Languages (POPL'01), pages 104-115. ACM Press, 2001. Google Scholar
  3. Martín Abadi and Andrew D Gordon. A calculus for cryptographic protocols: The spi calculus. In Proc. of the 4th ACM conference on Computer and communications security, pages 36-47. ACM, 1997. Google Scholar
  4. Myrto Arapinis, Tom Chothia, Eike Ritter, and Mark Ryan. Analysing unlinkability and anonymity using the applied pi calculus. In Proc. 23rd Computer Security Foundations Symposium (CSF'10), pages 107-121. IEEE Computer Society Press, 2010. Google Scholar
  5. A. Armando et al. The AVANTSSAR platform for the automated validation of trust and security of service-oriented architectures. In Proc. 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'12), volume 7214, pages 267-282. Springer, 2012. Google Scholar
  6. Alessandro Armando, Roberto Carbone, and Luca Compagna. SATMC: a SAT-based model checker for security-critical systems. In Proc. 20th international Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'14), pages 31-45. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-642-54862-8_3.
  7. Alessandro Armando, Roberto Carbone, Luca Compagna, Jorge Cuellar, and Llanos Tobarra Abad. Formal analysis of saml 2.0 web browser single sign-on: Breaking the saml-based single sign-on for google apps. In Proc. 6th ACM Workshop on Formal Methods in Security Engineering (FMSE 2008), pages 1-10, 2008. Google Scholar
  8. David Baelde, Stéphanie Delaune, Ivan Gazeau, and Steve Kremer. Symbolic verification of privacy-type properties for security protocols with xor. In Proc. 30th IEEE Computer Security Foundations Symposium (CSF'17), pages 234-248. IEEE Computer Society Press, 2017. Google Scholar
  9. David Baelde, Stéphanie Delaune, and Lucca Hirschi. Partial order reduction for security protocols. In Proc. 26th International Conference on Concurrency Theory (CONCUR'15), volume 42 of LIPIcs, pages 497-510. Leibniz-Zentrum für Informatik, 2015. Google Scholar
  10. David Baelde, Stéphanie Delaune, and Lucca Hirschi. A reduced semantics for deciding trace equivalence. Logical Methods in Computer Science, 2017. Google Scholar
  11. David Baelde, Stéphanie Delaune, and Lucca Hirschi. POR for Security Protocols Equivalences - Beyond Action-Determinism. arXiv, 2018. URL: http://arxiv.org/abs/1804.03650.
  12. David Basin, Jannik Dreier, and Ralf Sasse. Automated symbolic proofs of observational equivalence. In Proc. 22nd Conference on Computer and Communications Security (CCS'15), pages 1144-1155. ACM, 2015. Google Scholar
  13. Mathieu Baudet. Deciding security of protocols against off-line guessing attacks. In Proc. 12th ACM conference on Computer and communications security (CCS'05), pages 16-25. ACM, 2005. Google Scholar
  14. Bruno Blanchet. Automatic proof of strong secrecy for security protocols. In Proc. . 2004 Symposium on Security and Privacy, pages 86-100. IEEE Computer Society Press, 2004. Google Scholar
  15. Bruno Blanchet. An automatic security protocol verifier based on resolution theorem proving (invited tutorial). In Proc. 20th International Conference on Automated Deduction (CADE-20), July 2005. Google Scholar
  16. Bruno Blanchet, Martín Abadi, and Cédric Fournet. Automated verification of selected equivalences for security protocols. Journal of Logic and Algebraic Programming, 75(1):3-51, 2008. Google Scholar
  17. Bruno Blanchet and Ben Smyth. Automated reasoning for equivalences in the applied pi calculus with barriers. In Proc. 29th Computer Security Foundations Symposium (CSF'16), 2016. Google Scholar
  18. Mayla Brusó, Konstantinos Chatzikokolakis, and Jerry Den Hartog. Formal verification of privacy for RFID systems. In Proc. 23rd Computer Security Foundations Symposium (CSF'10), pages 75-88. IEEE Computer Society Press, 2010. Google Scholar
  19. I. Cervesato, N. Durgin, P. Lincoln, J. Mitchell, and A. Scedrov. A meta-notation for protocol analysis. In Proc. 12th Computer Security Foundations Workshop (CSFW'99), pages 55-69. IEEE Computer Society Press, 1999. Google Scholar
  20. Rohit Chadha, Ştefan Ciobâcă, and Steve Kremer. Automated verification of equivalence properties of cryptographic protocols. In Proc. European Symposium on Programming (ESOP'12), pages 108-127. Springer, 2012. Google Scholar
  21. Vincent Cheval. Apte: an algorithm for proving trace equivalence. In Proc. 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'14), volume 8413 of LNCS, pages 587-592, 2014. Google Scholar
  22. Vincent Cheval and Bruno Blanchet. Proving more observational equivalences with ProVerif. In Proc. 2nd Conference on Principles of Security and Trust (POST'13), volume 7796 of LNCS, pages 226-246. Springer, 2013. Google Scholar
  23. Vincent Cheval, Hubert Comon-Lundh, and Stéphanie Delaune. Trace equivalence decision: Negative tests and non-determinism. In Proc. 18th ACM Conference on Computer and Communications Security (CCS'11), pages 321-330. ACM Press, 2011. Google Scholar
  24. Vincent Cheval and Véronique Cortier. Timing attacks in security protocols: symbolic framework and proof techniques. In Proc. 4th Conference on Principles of Security and Trust (POST'15), pages 280-299. Springer, 2015. Google Scholar
  25. Vincent Cheval, Véronique Cortier, and Antoine Plet. Lengths may break privacy - or how to check for equivalences with length. In Proc. 25th International Conference on Computer Aided Verification (CAV'13), volume 8044 of LNCS, pages 708-723. Springer Berlin Heidelberg, 2013. Google Scholar
  26. Vincent Cheval, Steve Kremer, and Itsaka Rakotonirina. Deepsec: Deciding equivalence properties in security protocols - theory and practice. In Proc. 39th IEEE Symposium on Security and Privacy (S&P'18). IEEE Computer Society Press, 2018. Accepted for publication. Google Scholar
  27. Y. Chevalier, R. Küsters, M. Rusinowitch, and M. Turuani. Deciding the security of protocols with Diffie-Hellman exponentiation and product in exponents. In Proc. 23rd Conference on Foundations of Software Technology and Theoretical Computer Science (FST&TCS'03), volume 2914 of LNCS, pages 124-135. Springer-Verlag, 2003. Google Scholar
  28. Yannick Chevalier and Michael Rusinowitch. Decidability of symbolic equivalence of derivations. Journal of Automated Reasoning, 48(2):263-292, 2012. Google Scholar
  29. Tom Chothia and Vitaliy Smirnov. A traceability attack against e-passports. In Proc. 14th International Conference on Financial Cryptography and Data Security (FC'10), 2010. Google Scholar
  30. Rémy Chrétien, Véronique Cortier, and Stéphanie Delaune. Typing messages for free in security protocols: the case of equivalence properties. In Proc. 25th International Conference on Concurrency Theory (CONCUR'14), volume 8704 of LNCS, pages 372-386. Springer, 2014. Google Scholar
  31. Rémy Chrétien, Véronique Cortier, and Stéphanie Delaune. Decidability of trace equivalence for protocols with nonces. In Proc. 28th Computer Security Foundations Symposium (CSF'15), pages 170-184. IEEE Computer Society Press, 2015. Google Scholar
  32. Rémy Chrétien, Véronique Cortier, and Stéphanie Delaune. From security protocols to pushdown automata. ACM Transactions on Computational Logic, 17(1:3), 2015. Google Scholar
  33. Ştefan Ciobâcă, Stéphanie Delaune, and Steve Kremer. Computing knowledge in security protocols under convergent equational theories. Journal of Automated Reasoning, 48(2):219-262, 2012. Google Scholar
  34. Hubert Comon-Lundh and Stéphanie Delaune. The finite variant property: How to get rid of some algebraic properties. In Proc. International Conference on Rewriting Techniques and Applications (RTA'05), pages 294-307. Springer, 2005. Google Scholar
  35. Bruno Conchinha, David A. Basin, and Carlos Caleiro. FAST: an efficient decision procedure for deduction and static equivalence. In Proc. 22nd International Conference on Rewriting Techniques and Applications, RTA 2011, volume 10 of LIPIcs, pages 11-20. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2011. Google Scholar
  36. Ricardo Corin, Jeroen Doumen, and Sandro Etalle. Analysing password protocol security against off-line dictionary attacks. Electonic Notes in Theoretical Computer Science, 121:47-63, 2005. Google Scholar
  37. Véronique Cortier. Vérification automatique des protocoles cryptographiques. Thèse de doctorat (PhD thesis), Laboratoire Spécification et Vérification, ENS Cachan, France, mar 2003. Google Scholar
  38. Véronique Cortier, Antoine Dallon, and Stéphanie Delaune. Sat-equiv: an efficient tool for equivalence properties. In Proc. 30th IEEE Computer Security Foundations Symposium (CSF'17). IEEE Computer Society Press, aug 2017. Google Scholar
  39. Véronique Cortier and Stéphanie Delaune. Decidability and combination results for two notions of knowledge in security protocols. Journal of Automated Reasoning, 48(4):441-487, 2012. Google Scholar
  40. Véronique Cortier, Niklas Grimm, Joseph Lallemand, and Matteo Maffei. A type system for privacy properties. In 24th ACM Conference on Computer and Communications Security (CCS'17), pages 409-423. ACM, October 2017. Google Scholar
  41. Véronique Cortier, Niklas Grimm, Joseph Lallemand, and Matteo Maffei. Equivalence properties by typing in cryptographic branching protocols. In Proc. 7th International Conference on Principles of Security and Trust (POST'18), pages 160-187, April 2018. Google Scholar
  42. Véronique Cortier and Ben Smyth. Attacking and fixing helios: An analysis of ballot secrecy. In Proc. 24th Computer Security Foundations Symposium (CSF'11), pages 297-311. IEEE Computer Society Press, 2011. Google Scholar
  43. Stéphanie Delaune. Easy intruder deduction problems with homomorphisms. Information Processing Letters, 97(6):213-218, 2006. URL: http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/SD-ipl05.pdf.
  44. Stéphanie Delaune, Steve Kremer, and Mark D. Ryan. Symbolic bisimulation for the applied pi calculus. Journal of Computer Security, 18(2):317-377, mar 2010. Google Scholar
  45. D. Dolev and A. C. Yao. On the security of public key protocols. In Proc. 22nd Symposium on Foundations of Computer Science (FCS'81), pages 350-357. IEEE Computer Society Press, 1981. Google Scholar
  46. Jannik Dreier, Lucca Hirschi, Saša Radomirovic, and Sasse Ralf. Automated unbounded verification of stateful cryptographic protocols with exclusive OR operations. In Proc. 31st IEEE Computer Security Foundations Symposium (CSF'18). IEEE Computer Society Press, 2018. Google Scholar
  47. Ivan Gazeau and Steve Kremer. Automated analysis of equivalence properties for security protocols using else branches. In Proc. 22nd European Symposium on Research in Computer Security (ESORICS'17), volume 10493 of Lecture Notes in Computer Science, pages 1-20. Springer, sep 2017. URL: http://dx.doi.org/10.1007/978-3-319-66399-9_1.
  48. Lucca Hirschi, David Baelde, and Stéphanie Delaune. A method for verifying privacy-type properties: the unbounded case. In Proc. 37th Symposium on Security and Privacy (S&P'16), 2016. Google Scholar
  49. C. A. R. Hoare. Communicating sequential processes. Commun. ACM, 21(8):666-677, 1978. URL: http://dx.doi.org/10.1145/359576.359585.
  50. Hans Hüttel. Deciding framed bisimilarity. Electronic Notes in Theoretical Computer Science, 68(6):1-18, 2003. Google Scholar
  51. Il-Jung Kim, Eun Young Choi, and Dong Hoon Lee. Secure mobile RFID system against privacy and security problems. In Third International Workshop on Security, Privacy and Trust in Pervasive and Ubiquitous Computing, SECPerU 2007, Istanbul, Turkey, July 19, 2007, pages 67-72. IEEE Computer Society, 2007. Google Scholar
  52. Pascal Lafourcade, Denis Lugiez, and Ralf Treinen. Intruder deduction for AC-like equational theories with homomorphisms. In Proc. 16th International Conference on Rewriting Techniques and Applications (RTA'05), volume 3467 of LNCS, pages 308-322. Springer, 2005. Google Scholar
  53. G. Lowe. An attack on the Needham-Schroeder public key authentication protocol. Information Processing Letters, 56(3):131-133, 1995. Google Scholar
  54. Robin Milner. Communicating and mobile systems - the Pi-calculus. Cambridge University Press, 1999. Google Scholar
  55. R. Needham and M. Schroeder. Using encryption for authentification in large networks of computers. Communications of the ACM, 21(12):993-999, 1978. Google Scholar
  56. Technical advisory group on machine readable travel documents (tag/mrtd). URL: http://www.icao.int/Meetings/TAG-MRTD/TagMrtd22/TAG-MRTD-22_WP05.pdf.
  57. Sonia Santiago, Santiago Escobar, Catherine Meadows, and José Meseguer. A formal definition of protocol indistinguishability and its verification using Maude-NPA. In Security and Trust Management, pages 162-177. Springer, 2014. Google Scholar
  58. Benedikt Schmidt, Simon Meier, C. J. F. Cremers, and David Basin. Automated analysis of Diffie-Hellman protocols and advanced security properties. In Proc. 25th Computer Security Foundations Symposium (CSF'12), pages 78-94. IEEE Computer Society Press, 2012. Google Scholar
  59. F. Javier Thayer, Jonathan C. Herzog, and Joshua D. Guttman. Strand spaces: Proving security protocols correct. Journal of Computer Security, 7(1):191-230, 1999. Google Scholar
  60. Alwen Tiu. A trace based bisimulation for the spi calculus. In Programming Languages and Systems, pages 367-382. Springer, 2007. Google Scholar
  61. Ton van Deursen and Sasa Radomirovic. Attacks on RFID protocols. IACR Cryptology ePrint Archive - Report 2008/310, 2008. URL: http://eprint.iacr.org/2008/310.
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