Information flow analysis plays a vital role in obtaining quantitative bounds on information leakage due to external attacks. Traditionally, information flow analysis is done using paper-and-pencil based proofs or computer simulations based on the Shannon entropy and mutual information. However, these metrics sometimes provide misleading information. For example, in the case of a specific threat model where the secret is correctly guessed in one try, a random variable with high vulnerability to be guessed can have larger Shannon entropy. Moreover, due to its inherent limitations, simulation cannot ascertain accurate analysis. In order to overcome these shortcomings, we propose to formalize min-entropy and belief-min-entropy in higher-order-logic and use them to perform information flow analysis within the sound core of the HOL theorem prover. These entropy measures allow us to model and analyze the information leakage in deterministic and probabilistic systems and can deal with the above mentioned threat model more effectively. Moreover, the usage of theorem proving ensures the correctness of analysis, which is a very useful feature of analyzing security-critical applications. For illustration purposes, we use the proposed formalization to evaluate the information leakage of a cascade of channels in HOL.

HOL Script

Foundational Formalization

• min-beliefTheo.sml (This file contains formalization of Min-Entropy and Belief Min-Entropy theories)

Application: Min-Entropy Leakage of Cascade of Channels

• cascChann.sml (This file contains the formal verification of the information leakage in a Cascade of Channels)