2026-07-21T20:03:20Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5658 2024-03-06T10:36:47Z ddc:004 open_access

Secure Refinements of Communication Channels Cheval, Vincent Cortier, Véronique le Morvan, Eric Protocol Composition Formal methods Channels Implementation 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Vincent Cheval and Véronique Cortier and Eric le Morvan 2015 Is Part Of LIPIcs, Volume 45, 35th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2015) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2015.575 urn:nbn:de:0030-drops-56583 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2015.575 eng https://creativecommons.org/licenses/by/3.0/legalcode