Finite probability distributions in Coq

Abstract

When building safety-critical systems, guaranteeing properties like correctness and security are one of the most important goals to achieve. Thus, from a scientific point of view, one of the hardest problems in cryptography is to build systems whose security properties can be formally demonstrated. In the last few years we have assisted an exponential growth in the use of tools to formalize security proofs of primitives and cryptographic protocols, clearly showing the strong connection between cryptography and formal methods. This necessity comes from the great complexity and sometimes careless presentation of many security proofs, which often contain holes or rely on hidden assumptions that may reveal unknown weaknesses. In this context, interactive theorem provers appear as the perfect tool to aid in the formal certification of programs due to their capability of producing proofs without glitches and providing additional evidence that the proof process is correct. Hence, it is the purpose of this thesis to document the development of a framework for reasoning over information theoretic concepts, which are particularly useful to derive results on the security properties of cryptographic systems. For this it is first necessary to understand, and formalize, the underlying probability theoretic notions. The framework is implemented on top of the fintype and finfun modules of SSREFLECT, which is a small scale reflection extension for the COQ proof assistant, in order to take advantage of the formalization of big operators and finite sets that are available.

Na construção de sistemas críticos, a garantia de propriedades como a correção e segurança assume-se como um dos principais objetivos. Deste modo, e de um ponto de vista científico, um dos problemas criptográficos mais complicados é o de construir sistemas cujas propriedades possam ser demonstradas formalmente.

Nos últimos anos temos assistido a um crescimento enorme no uso de ferramentas para formalizar provas de segurança de primitivas e protocolos criptográficos, o que revela a forte ligação entre a criptografia e os métodos formais. Urge esta necessidade devido à grande complexidade, e apresentação por vezes descuidada, de algumas provas de segurança que muitas vezes contêm erros ou se baseiam em pressupostos escondidos que podem revelar falhas desconhecidas. Desta forma, os provers interativos revelam-se como a ferramenta ideal para certificar programas formalmente devido à sua capacidade de produzir provas sem erros e de conferir uma maior confiança na correção dos processos de prova.

Neste contexto, o propósito deste documento é o de documentar e apresentar o desenvolvimento de uma plataforma para raciocinar sobre conceitos da teoria de informação, que são particularmente úteis para derivar resultados sobre as propriedades de sistemas criptográficos. Para tal é necessário, em primeiro lugar, entender e formalizar os conceitos de teoria de probabilidades subjacentes. A plataforma é implementada sobre as bibliotecas fintype e finfun do SSREFLECT, que é uma extensão à ferramenta de provas assistidas COQ, por forma a aproveitar a formalização dos somatórios e conjuntos finitos disponíveis.