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 while dealing with some specific threat models, like when the secret is correctly guessed in one try. Min-Entropy and Belief Min-Entropy metrics have been recently proposed to address these problems. But the information flow analysis using these metrics is done by simulation and paper-and-pencil approaches and thus cannot ascertain accurate results due to their inherent limitations. In order to overcome these shortcomings, the authors present the formalization of Min-Entropy and Belief-Min-Entropy in higher-order logic and use them to perform information flow analysis within the sound core of the HOL4 theorem prover in this chapter. For illustration purposes, they use their formalization to evaluate the information leakage of a cascade of channels in HOL.
TopProtecting the confidentiality of sensitive information and ensuring perfect anonymity (Palamidessi, Chatzikokolakis & Panangaden, 2008) are increasingly becoming a dire need in many fields like tele-communication, electronic payments, auctioning and voting. The information flow analysis allows us to obtain quantitative estimates about information leakage (Backes, Kopf & Rybalchenko, 2009), by observing the outputs and the low security inputs in a given system, and thus plays a vital role in developing secure and anonymous systems (Halpern & O’Neill, 2005).
Various approaches for assessing the information flow (Andrea, 2002) have been proposed in the literature. The main idea behind the possibilistic approaches is to use non-deterministic behaviors to model the given system. For example, the information flow analysis based on epistemic logic, which is a logic of knowledge and belief, and on process algebra, which allows us to model concurrent systems, fall under this category. The main limitation of possibilistic approaches is its failure to distinguish between systems of varying degrees of protection. Probabilistic approaches, based on information theory and statistics, overcome this limitation and are thus considered more reliable for assessing information flow. The most commonly used probabilistic measures of information flow are Shannon’s entropy, mutual information between the sensitive input and the observable output and relative entropy. It has been recently shown that using such measures sometimes leads to counter-intuitive results. 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 (Renyi, 1961).
In the one-try model, the adversary is given only one chance to get the value of the secret. The objective here is to maximize the probability of guessing the right value of the high input in just one try and the best strategy for her is auctioning on the element having the maximum distribution. Renyi’s entropy metrics, i.e., Min-Entropy (Espinoza & Smith, 2012) and Belief Min-Entropy (Hamadou, Sassone & Palamidessi, 2010), can deal with the above mentioned threat model more effectively and are commonly used to model and analyze the information leakage in deterministic and probabilistic systems.
Traditionally, paper-and-pencil based analysis or computer simulations have been used for quantitative analysis of information flow (Simth (2009); (Smith 2011)). Paper-and-pencil analysis does not scale well to complex systems and is prone to human error. Computer simulation, on the other hand, makes use of numerical approximations for rounding computer arithmetics, which leads to analysis inaccuracies. In order to enhance the accuracy of analysis results, formal methods have been recently proposed to be used in the safety-critical analysis domain of information flow analysis. The probabilistic model checker PRISM has been used to assist in computing the transition probabilities and capacity of the Dining cryptographers protocol. However, the state-space explosion problem of model checking limits the scope of its usage in information flow analysis. For example, only the case for three cryptographers has been analyzed. These limitations can be overcome by using higher-order-logic theorem proving for the analysis of information flow. For example, the conditional mutual information has been used to formally analyse the anonymity properties of the Dining Cryptographers protocol in the higher-order-logic theorem prover HOL4. Similarly, the information and the conditional information leakage degrees have been formalized in to assess the security and anonymity protocols within the sound core of HOL4. However, to the best of our knowledge, no formalization of Min-Entropy and Belief-Min-Entropy exists in higher-order logic so far. Thus, despite their enormous applications in security-critical applications, the formal analysis of the scenarios when the secret is correctly guessed in one try is not available.