Document Open Access Logo

Secure Refinements of Communication Channels

Authors Vincent Cheval, Véronique Cortier, Eric le Morvan

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSTTCS.2015.575.pdf
  • Filesize: 0.5 MB
  • 15 pages

Document Identifiers

Subject Classification

Keywords
  • Protocol
  • Composition
  • Formal methods
  • Channels
  • Implementation

Metrics

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

Abstract

It is a common practice to design a protocol (say Q) assuming some secure channels. Then the secure channels are implemented using any standard protocol, e.g. TLS. In this paper, we study when such a practice is indeed secure.
We provide a characterization of both confidential and authenticated channels. As an application, we study several protocols of the literature including TLS and BAC protocols. Thanks to our result, we can consider a larger number of sessions when analyzing complex protocols resulting from explicit implementation of the secure channels of some more abstract protocol Q.

Cite As Get BibTex

Vincent Cheval, Véronique Cortier, and Eric le Morvan. Secure Refinements of Communication Channels. In 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 45, pp. 575-589, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.FSTTCS.2015.575

Author Details

Vincent Cheval
Véronique Cortier
Eric le Morvan

References

  1. Machine readable travel document. Technical Report 9303, International Civil Aviation Organization, 2008. Google Scholar
  2. M. Abadi and C. Fournet. Mobile values, new names, and secure communication. In Proc. of the 28th ACM Symposium on Principles of Programming Languages (POPL'01), pages 104-115, January 2001. Google Scholar
  3. Bruno Blanchet. An efficient cryptographic protocol verifier based on prolog rules. In Proc. CSFW'01, 2001. Google Scholar
  4. Bruno Blanchet and Andreas Podelski. Verification of cryptographic protocols: Tagging enforces termination. In Andrew Gordon, editor, Foundations of Software Science and Computation Structures (FoSSaCS'03), volume 2620 of LNCS, April 2003. Google Scholar
  5. V. Cheval, V. Cortier, and E. Le-Morvan. Secure refinements of communication channels. Research report RR-8790, Inria, 2015. Google Scholar
  6. Ştefan Ciobâcă and Véronique Cortier. Protocol composition for arbitrary primitives. In Proceedings of the 23rd IEEE Computer Security Foundations Symposium (CSF'10), pages 322-336, Edinburgh, Scotland, UK, July 2010. IEEE Computer Society Press. Google Scholar
  7. Véronique Cortier and Stéphanie Delaune. Safely composing security protocols. Formal Methods in System Design, 34(1):1-36, February 2009. Google Scholar
  8. Anupam Datta, Ante Derek, John C. Mitchell, and Arnab Roy. Protocol composition logic (PCL). Electr. Notes Theoretical Computer Science, 172:311-358, 2007. Google Scholar
  9. T. Dierks and E. Rescorla. The transport layer security (tls) protocol version 1.2 (rfc 5246). Technical report, IETF, 2008. Google Scholar
  10. Thomas Gibson-Robinson, Allaa Kamil, and Gavin Lowe. Verifying layered security protocols. Journal of Computer Security, 23(3), 2015. Google Scholar
  11. Joshua D. Guttman. Authentication tests and disjoint encryption: a design method for security protocols. Journal of Computer Security, 12(3-4):409-433, 2004. Google Scholar
  12. Joshua D. Guttman. Establishing and preserving protocol security goals. Journal of Computer Security, 22(2):203-267, 2004. Google Scholar
  13. Joshua D. Guttman and F. Javier Thayer. Protocol independence through disjoint encryption. In Proc. 13th Computer Security Foundations Workshop (CSFW'00), pages 24-34. IEEE Comp. Soc. Press, 2000. Google Scholar
  14. Simon Meier, Benedikt Schmidt, Cas Cremers, and David Basin. The TAMARIN Prover for the Symbolic Analysis of Security Protocols. In Natasha Sharygina and Helmut Veith, editors, Computer Aided Verification, 25th International Conference, CAV 2013, Princeton, USA, Proc., volume 8044 of Lecture Notes in Computer Science, pages 696-701. Springer, 2013. Google Scholar
  15. Christopher Meyer and Jorg Schwenk. Lessons learned from previous ssl/tls attacks : A brief chronology of attacks and weaknesses. In IACR Cryptology ePrint, 2013. Google Scholar
  16. Sebastian Moedersheim and Luca Viganò. Sufficient conditions for vertical composition of security protocols. In ASIACCS, pages 435-446, 2014. Google Scholar
  17. Vijayakrishnan Pasupathinathan, Josef Pieprzyk, Huaxiong Wang, and Joo Yeon Cho. Formal analysis of card-based payment systems in mobile services. In Fourth Australian information security workshop, conferences in research and practise in information security, pages 213-220, 2006. Google Scholar
  18. Mathieu Turuani. The CL-Atse Protocol Analyser. In Term Rewriting and Applications - Proc. of RTA, volume 4098 of Lecture Notes in Computer Science, pages 277-286, Seattle, WA, USA, 2006. Google Scholar
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact