Unreliable communication channels are a practical reality. They add to the complexity of protocol design and verification. In this work, we consider noisy channels which can corrupt messages. We present an approach to model and verify protocols which combine error detection and error control to provide reliable communication over noisy channels. We call these protocols retransmission protocols as they achieve reliable communication through repeated retransmissions of messages. These protocols typically use cyclic redundancy checks and sliding window protocols for error detection and control respectively. We propose models of these protocols as regular transducers operating on bit strings. Deterministic streaming string transducers provide a natural way of modeling these protocols and formalizing correctness requirements. The verification problem is posed as functional equivalence between the protocol transducer and the specification transducer. Functional equivalence checking is decidable for this class of transducers and this makes the transducer models amenable to algorithmic verification. In our transducer models, message lengths and retransmission rounds are unbounded. We present case studies based on TinyOS serial communication and the HDLC retransmission protocol. We further extend our protocol models to capture the effects of a noisy channel with non-determinism. We present two non-deterministic yet decidable extensions of transducer models of retransmission protocols. For one of our models, we achieve decidable verification by bounding the retransmission rounds, whereas for the other, even retransmission rounds are unbounded.

La téléportation quantique promet d'être centrale à de nombreuses applications du futur tels la cryptographique quantique et l'ordinateur quantique. Comme toute mise en œuvre physique s'accompagne inévitablement d'imperfections expérimentales, on étudie la téléportation dans un contexte où la ressource quantique, c'est-à-dire l'intrication, que l'on consomme est brouillée. Pour ce faire, on introduit en premier lieu le formalisme de l'informatique quantique. En seconde partie, on approche les protocoles de téléportation quantique standard, de téléportation avec relais quantiques et de téléportation multi-ports. Notre analyse de la téléportation standard et de la téléportation multi-ports poursuit trois objectifs principaux. Le premier est de comparer l'emploi d'un canal brouillé pour la téléportation d'un état quantique avec l'utilisation de ce même canal pour l'envoi direct de l'état. On trouve ainsi les conditions pour lesquelles les deux protocoles de transmission sont équivalents. Le second but est d'observer le caractère non-local de l'intrication brouillée en regardant quand et comment Alice peut réduire le bruit chez elle à un bruit exclusivement chez Bob. En troisième, on quantifie par une borne inférieure la qualité d'un canal de téléportation en réduisant l'effet de toute intrication brouillée à celui d'un bruit de Pauli à un seul paramètre. On accomplit cette tâche en effaçant au moment approprié l'information classique superflue et en appliquant la wernerisation. Finalement, on analyse la composition de bruits de Pauli et l'effet du taux d'effacement sur la téléportation avec relais quantiques pour mieux comprendre comment se combinent les effets de l'intrication brouillée dans un réseau de téléportation quantique. La suite logique est d'établir des protocoles plus robustes de téléportation quantique qui prennent en compte l'effet de l'intrication brouillée. / Quantum teleportation will be a centerpiece of practical quantum cryptography and quantum computing in a soon to be future. As no physical implementation is perfect, we study quantum teleportation in the context of impaired quantum resources which we call noisy entanglement. In a first part, we introduce how quantum mechanics is formalized by quantum information theory. In the second part, we study standard quantum teleportation, in both the absence and presence of quantum repeaters, as well as port-based teleportation. Our analysis of standard quantum teleportation and port-based teleportation follows three main directions. The first goal is to compare the use of a noisy channel for teleportation to the one of the same channel for direct transmission. We thus find the conditions under which the two cases are equivalent. Our second objective is to observe the non-local properties of noisy entanglement by finding when and how Alice can blame Bob for her noise. Thirdly, we quantify, in the worst-case scenario, the quality of a teleportation channel by reducing the effect of any noisy entanglement to the one of a one-parameter Pauli channel that can be interpreted as a depolarizing channel in most instances. We achieve this task by erasing unneeded classical information at the appropriate time and by twirling either the entanglement or the teleported state. Finally, we analyze the composition of Pauli noises and the impact of the erasure channel parameter on the protocol of teleportation with quantum repeaters. We thus aim to understand how the effects of noisy entanglement cumulate in a teleportation network. The next logical step is to create robust teleportation schemes that take into account the effects of noisy entanglement.