Login | Register

Information-Theoretic Analysis using Theorem Proving


Information-Theoretic Analysis using Theorem Proving

Mhamdi, Tarek (2012) Information-Theoretic Analysis using Theorem Proving. PhD thesis, Concordia University.

[thumbnail of Mhamdi_PhD_S2013.pdf]
Text (application/pdf)
Mhamdi_PhD_S2013.pdf - Accepted Version


Information theory is widely used for analyzing a wide range of scientific and engineering problems, including cryptography, neurobiology, quantum computing, plagiarism detection and other forms of data analysis. Despite the safety-critical nature of some of these applications, most of the information-theoretic analysis is done using informal techniques, mainly computer simulation and paper-and-pencil analysis, and thus cannot be completely relied upon. The unreliable nature of the produced results poses a serious problem in safety-critical applications and may result in heavy financial losses or even the loss of human life. In order to overcome the inaccuracy limitations of these techniques, this thesis proposes to conduct the analysis within the trusted kernel of a higher-order-logic (HOL) theorem prover. For this purpose, we provide HOL formalizations of the fundamental theories of measure, Lebesgue integration and probability and use them to formalize some of the most widely used information-theoretic principles. We use the Kullback-Leibler divergence as a unified measure of information which is in turn used to define the main measures of information like the Shannon entropy, mutual information and conditional mutual information. Furthermore, we introduce two new measures of information leakage, namely the information leakage degree and the conditional information leakage degree and compare them with existing measures. We illustrate the usefulness of the proposed framework by tackling various applications including the performance analysis of a communication encoder used in the proof of the Shannon source coding theorem, the quantitative analysis of privacy properties of a digital communications mixer and the one-time pad encryption system using information-theoretic measures.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Electrical and Computer Engineering
Item Type:Thesis (PhD)
Authors:Mhamdi, Tarek
Institution:Concordia University
Degree Name:Ph. D.
Program:Electrical and Computer Engineering
Date:4 December 2012
Thesis Supervisor(s):Tahar, Sofiene
Keywords:Information Theory, Theorem Proving, Formal Methods, Quantitative Analysis of Information
ID Code:975027
Deposited On:17 Jun 2013 18:12
Last Modified:18 Jan 2018 17:39
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.

Repository Staff Only: item control page

Downloads per month over past year

Research related to the current document (at the CORE website)
- Research related to the current document (at the CORE website)
Back to top Back to top