Ferramentas de verificação formal de protocolos criptográficos

Abstract

Ao longo destes anos o número de aplicações distribuídas e o uso da Internet têm aumentado consideravelmente. Muitas destas aplicações críticas efetuam um conjunto de operações sensíveis, manipulando frequentemente dados privados e confidenciais. Torna-se deste modo importante que, antes de usufruir de uma estrutura deste tipo, se averigúe quais são as políticas de segurança da aplicação em questão de modo a que, mais tarde, o utilizador não tenha surpresas indesejadas.

Os protocolos criptográficos constituem um recurso importante nos componentes dos sistemas encarregues de fornecer as garantias de segurança pretendidas. Tratam-se de protocolos de comunicação normalmente pequenos, que fazem uso de técnicas criptográficas, e que têm objectivos bem especificados como sejam o estabelecimento de uma chave de sessão ou de garantias de autenticidade na comunicação. A natureza crítica desses protocolos justifica que se invista numa análise rigorosa (i.e., formal) desses protocolos, garantindo dessa forma que eles cumprem a função para que foram desenhados. No entanto, a análise desses protocolos tem-se revelado um problema complexo, mesmo quando se atribui um comportamento idealizado às operações criptográficas empregues. Por esse motivo, a comunidade científica tem vindo a propor novas metodologias e ferramentas que auxiliam no processo de verificação formal de protocolos criptográficos.

Neste trabalho, iremos apresentar um conjunto representativo de ferramentas para a verificação formal de protocolos criptográficos. Após a exposição das suas principais características e dos respetivos modelos que as suportam, iremos emprega-las na análise de fragmentos de um protocolo concreto que se tem implantado como um standard de facto na internet: o protocolo de autenticação centralizada (Single Sign-On) “OpenID”.

Over these years the number of distributed applications and the Internet use have increased considerably. Many of these critical applications perform a set of sensitive operations that often manipulate private and confidential data. In this way, it’s important before we use one of these critical applications, determine the security policies of the application in question, just to the user doesn’t have surprises later. The cryptographic protocols are an important resource of the systems components that have the charge of provide the desired security guarantees. These cryptographic protocols, usually small, make use of cryptographic techniques, whose aims are well specified, such as the settlement of a session key or some guarantees of communication authenticity. The critical nature of these protocols justifies that we must do a rigorous analysis (i.e. formal) of these protocols. In this way, we guarantee that they fit the function for what they were designed. However, the analysis of these protocols has showed to be a complex problem, even when it is attributed an idealized behavior for the cryptographic operations employed. That’s why the scientific community has proposed new methodologies and tools that help in the formal verification process of cryptographic protocols. In this work, we introduce a representative set of tools for the formal verification of cryptographic protocols. After we demonstrate their main characteristics and models that support them, we will use those tools in the analysis of the fragments of one concrete protocol that has implemented like a standard indeed on the internet: the centralized authentication protocol (Single Sign-On) “OpenID”.