Evaluation of anonymity and confidentiality protocols using theorem proving

详细信息    查看全文

• 作者：Tarek Mhamdi ; Osman Hasan ; Sofiène Tahar
• 关键词：Information leakage ; Anonymity ; Confidentiality ; Theorem proving ; Dependable systems and software
• 刊名：Formal Methods in System Design
• 出版年：2015
• 出版时间：December 2015
• 年：2015
• 卷：47
• 期：3
• 页码：265-286
• 全文大小：591 KB
• 参考文献：1.Andrews PB (2002) An introduction to mathematical logic and type theory: to truth through proof. Springer, HeidelbergCrossRef
  2.Chatzikokolakis K, Palamidessi C, Panangaden P (2007) Anonymity protocols as noisy channels. In: Trustworthy global computing, LNCS, vol 4661. Springer-Verlag, Heidelberg, pp 281–300
  3.Church A (1940) A formulation of the simple theory of types. J Symb Log 5:56–68MathSciNet CrossRef
  4.Coble AR (2008) Formalized information-theoretic proofs of privacy using the HOL4 theorem-prover. In: Privacy enhancing technologies, LNCS, vol 5134. Springer-Verlag, Heidelberg, pp 77–98
  5.Coble AR (2010) Anonymity, information, and machine-assisted proof. PhD Thesis, University of Cambridge
  6.Cover TM, Thomas JA (1991) Elements of information theory. Wiley-Interscience, New YorkMATH CrossRef
  7.Deng Y, Pang J, Wu P (2007) Measuring anonymity with relative entropy. In: Formal aspects in security and trust, LNCS, vol 4691. Springer, pp 65–79
  8.Diaz C, Seys S, Claessens J, Preneel B (2003) Towards measuring anonymity. In: Privacy enhancing technologies, LNCS, vol 2482. Springer, Heidelberg, pp 54–68
  9.Dingledine R, Mathewson N, Syverson P (2004) Tor: the second-generation onion router. In: Proceedings of the 13th USENIX security symposium
  10.Goldberg RR (1976) Methods of real analysis. Wiley, New YorkMATH
  11.Gordon MJC (1989) Mechanizing programming logics in higher-order logic. In: Current trends in hardware verification and automated theorem proving. Springer, New York, pp 387–439
  12.Harrison J (1996) Formalized mathematics. Technical Report 36. Turku Centre for Computer Science, Finland
  13.Harrison J (2009) Handbook of practical logic and automated reasoning. Cambridge University Press, CambridgeMATH CrossRef
  14.Kolmogorov AN (1933) Grundbegriffe der Wahrscheinlichkeitsrechnung. Springer, Berlin. English translation (1950): foundations of the theory of probability. Chelsea, New York
  15.Kwiatkowska M, Norman G, Parker D (2005) Quantitative analysis with the probabilistic model checker PRISM. Electron Notes Theor Comput Sci 153(2):5–31CrossRef
  16.Malacaria P (2007) Assessing security threats of looping constructs. SIGPLAN Notes 42(1):225–235CrossRef
  17.Mhamdi T (2013) Probability and information theories in HOL. Hardware Verification Group (HVG), Concordia University, Montreal, QC. https://​github.​com/​mn200/​hol/​tree/​master/​src/​probability
  18.Mhamdi T, Hasan O, Tahar S (2010) On the formalization of the Lebesgue integration theory in HOL. In: Interactive theorem proving, LNCS, vol 6172. Springer, Heidelberg, pp 387–402
  19.Mhamdi T, Hasan O, Tahar S (2011) Formalization of entropy measures in HOL. In: Interactive theorem proving, LNCS, vol 6898. Springer, Heidelberg, pp 233–248
  20.Mhamdi T, Hasan O, Tahar S (2012) Quantitative analysis of information flow using theorem proving. In: International conference on formal engineering methods, LNCS, vol 7635. Springer-Verlag, Heidelberg, pp 119–134
  21.Miller F (1882) Telegraphic code to insure privacy and secrecy in the transmission of telegrams. C.M. Cornwell, New York
  22.Milner R (1977) A theory of type polymorphism in programming. J Comput Syst Sci 17:348–375MathSciNet CrossRef
  23.Paulson LC (1996) ML for the working programmer. Cambridge University Press, CambridgeMATH CrossRef
  24.Reiter MK, Rubin AD (1998) Crowds: anonymity for web transactions. ACM Trans Inf Syst Secur 1(1):66–92CrossRef
  25.Rijmenants D (2004) One-time pad. Cipher Machines and Cryptology. http://​users.​telenet.​be/​d.​rijmenants/​en/​table.​htm
  26.Sabelfeld A, Myers AC (2003) Language-based information-flow security. IEEE J Sel Areas Commun 21(1):5–19CrossRef
  27.Serjantov A, Danezis G (2003) Towards an information theoretic metric for anonymity. In: Privacy enhancing technologies, LNCS, vol 2482. Springer, Heidelberg , pp 259–263
  28.Smith G (2009) On the foundations of quantitative information flow. In: Foundations of software science and computational structures, LNCS, vol 5504. Springer, York, pp 288–302
  29.Zhu Y, Bettati R (2009) Information leakage as a model for quality of anonymity networks. IEEE Trans Parallel Distrib Syst 20(4):540–552CrossRef
  
• 作者单位：Tarek Mhamdi (1)
  Osman Hasan (1)
  Sofiène Tahar (1)
  
  1. Department of Electrical and Computer Engineering, Concordia University, Montreal, QC, Canada
  
• 刊物类别：Engineering
• 刊物主题：Circuits and Systems
  Electronic and Computer Engineering
  Computer-Aided Engineering and Design
  Software Engineering, Programming and Operating Systems
  
• 出版者：Springer Netherlands
• ISSN：1572-8102

文摘

Anonymity and confidentiality protocols constitute crucial parts in many network applications as they ensure anonymous communications between entities in a network or provide security in insecure communication channels. Evaluating the properties of these protocols is therefore of paramount importance, especially in the case of safety-critical applications. However, traditional analysis techniques, like simulation, cannot ascertain accurate analysis in this domain. We propose to overcome this limitation by conducting an information leakage analysis of anonymity and cryptographic protocols within the trusted kernel of a higher-order-logic theorem prover. For this purpose, we first introduce two novel measures of information leakage, namely the information leakage degree and the conditional information leakage degree and then present a higher-order-logic formalization of information measures and the underlying required theories of measure, probability and information. For illustration purposes, we use the proposed framework to evaluate the security properties of the one-time pad encryption system as well as the properties of an anonymity-based single MIX. We show how this formal analysis allowed us to find a counter-example for a theorem that was reported in the literature to describe the leakage properties of this single MIX. Keywords Information leakage Anonymity Confidentiality Theorem proving Dependable systems and software