Information-Theoretic Analysis using Theorem Proving
Contact: mhamdi@ece.concordia.ca
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 work 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 (KL) 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 propose two new measures of information leakage, namely the information leakage degree and the conditional information leakage degree and compare them with the existing ones.
We illustrate the usefulness of the proposed framework by tackling various applications including the performance analysis of a typical encoder which is used in the proof of the Shannon source coding theorem, the quantitative analysis of privacy properties of an anonymity-based MIX channel and the one-time pad encryption system using information-theoretic measures.
The formalization in this work is now part of the official release (Kananaskis 8) of the HOL4 theorem prover.
Tarek Mhamdi, "Information-Theoretic Analysis using Theorem Proving", PhD Department of Electrical and Computer Engineering, Concordia University, Montreal, Quebec, Canada, December 2012.
[2] T. Mhamdi, O. Hasan, and S. Tahar: Formalization of Entropy Measures in HOL M. V. Eekelen, H. Geuvers, J. Schmaltz and F. Wiedijk (Eds.), Interactive Theorem Proving, Lecture Notes in Computer Science 6898, Springer Verlag, 2011, pp. 233-248. [Proc. Second International Conference on Interactive Theorem Proving (ITP 2011), Berg en Dal, The Netherlands, August 2011.]
[3] T. Mhamdi, O. Hasan, and S. Tahar: On the Formalization of the Lebesgue Integration Theory in HOL M. Kaufmann, L. C. Paulson (Eds.), Interactive Theorem Proving, Lecture Notes in Computer Science 6172, Springer Verlag, 2010, pp. 387-402. [Proc. First International Conference on Interactive Theorem Proving (ITP 2010), Edinburgh, UK, July 2010.]
[4] T. Mhamdi, O. Hasan, and S. Tahar. Formalization of Measure Theory and Lebesgue Integration for Probabilistic Analysis in HOL, ACM Transactions on Embedded Computing Systems, Accepted in June 2011. [25 pages].
[2] T. Mhamdi, O. Hasan, and S. Tahar. On the Formalization of the Lebesgue Integration Theory in HOL, Technical Report, Department of Electrical and Computer Engineering, Concordia University, January 2010. [25 Pages].
In order to overcome the inaccuracy limitations of these techniques, this work 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 (KL) 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 propose two new measures of information leakage, namely the information leakage degree and the conditional information leakage degree and compare them with the existing ones.
We illustrate the usefulness of the proposed framework by tackling various applications including the performance analysis of a typical encoder which is used in the proof of the Shannon source coding theorem, the quantitative analysis of privacy properties of an anonymity-based MIX channel and the one-time pad encryption system using information-theoretic measures.
The formalization in this work is now part of the official release (Kananaskis 8) of the HOL4 theorem prover.
Thesis
Publications
Journal Papers
[1] T. Mhamdi, O. Hasan, and S. Tahar. Performance Evaluation of Anonymity and Security Protocols using Theorem Proving, IEEE Transactions on Parallel and Distributed Systems, Submitted in September 2012. [12 pages].Conference Papers
[1] T. Mhamdi, O. Hasan, and S. Tahar. Quantitative Analysis of Information Flow using Theorem Proving, In International Conference on Formal Engineering Methods (ICFEM 2012), volume 7635 of LNCS, pages 119–134. Springer, 2012.[2] T. Mhamdi, O. Hasan, and S. Tahar: Formalization of Entropy Measures in HOL M. V. Eekelen, H. Geuvers, J. Schmaltz and F. Wiedijk (Eds.), Interactive Theorem Proving, Lecture Notes in Computer Science 6898, Springer Verlag, 2011, pp. 233-248. [Proc. Second International Conference on Interactive Theorem Proving (ITP 2011), Berg en Dal, The Netherlands, August 2011.]
[3] T. Mhamdi, O. Hasan, and S. Tahar: On the Formalization of the Lebesgue Integration Theory in HOL M. Kaufmann, L. C. Paulson (Eds.), Interactive Theorem Proving, Lecture Notes in Computer Science 6172, Springer Verlag, 2010, pp. 387-402. [Proc. First International Conference on Interactive Theorem Proving (ITP 2010), Edinburgh, UK, July 2010.]
[4] T. Mhamdi, O. Hasan, and S. Tahar. Formalization of Measure Theory and Lebesgue Integration for Probabilistic Analysis in HOL, ACM Transactions on Embedded Computing Systems, Accepted in June 2011. [25 pages].
Technical Reports
[1] T. Mhamdi, O. Hasan, and S. Tahar, Formalization of Measure and Lebesgue Integration over Extended Reals in HOL, Technical Report, Department of Electrical and Computer Engineering, Concordia University, January 2011. [120 Pages].[2] T. Mhamdi, O. Hasan, and S. Tahar. On the Formalization of the Lebesgue Integration Theory in HOL, Technical Report, Department of Electrical and Computer Engineering, Concordia University, January 2010. [25 Pages].
HOL Scripts
Download Files