Formalização em PVS de Propriedades de
Balanceamento para Protocolos em Cascata
Yuri Santos Rêgo∗ 1
Maurı́cio Ayala-Rincón
† 1,2
1
2
Departamento de Matemática, Universidade de Brası́lia
Departamento de Ciência da Computação, Universidade de Brası́lia
Uma das vertentes de matemática aplicada à computação refere-se à criptografia e aos
protocolos criptográficos.
Protocolos criptográficos são, em termos abstratos, aplicações de operadores de codificação-decodificação feitas e distribuı́das de acordo com um dado algoritmo. Tais protocolos requerem cautelosa análise de suas propriedades para que se garanta que um dado
sistema proposto seja eficaz e seguro, face às definições de segurança do mesmo.
No âmbito da formalização e do rigor matemático, trabalhados mais enfaticamente
desde Hilbert, desde a modelagem de problemas às bases axiomáticas e demonstrações de
teoremas mostra-se necessária uma fundamentação rigorosa da matemática envolvida no
desenvolvimento de cada teoria. A matemática aplicada não é exceção.
O Modelo de Protocolos em Cascata de Dolev-Yao ([1]) é conhecido e utilizado há quase
3 décadas como um dos modelos base para protocolos criptográficos, tendo propriedades
básicas comuns a uma grande parte dos protocolos hoje utilizados.
Promove-se aqui uma formalização integral de tal modelo, especificado e caracterizado
em um assistente de provas, o PVS (Prototype Verification System, [3]). Tal formalização
foi feita através da utilização de técnicas algébricas, onde os operadores criptográficos aparecem como os geradores do monóide livremente gerado por estes. Com isso formaliza-se,
tanto analiticamente quanto como uma teoria em PVS, uma caracterização de segurança
para tal modelo, como um Teorema que garante sob quais condições o mesmo é seguro.
Noções Iniciais
O Modelo baseia-se em sistemas de chave pública bipartidos, onde todo usuário u ∈ U
(conjunto de usuários) possui um operador de encriptação Eu e um operador de decriptação
Du . Um diretório público seguro contém todos os pares (u, Eu ) mas, ∀u ∈ U , apenas u
tem conhecimento sobre Du . Assume-se que o usuário malicioso é também usuário do
sistema, e que o mesmo pode extrair informações de maneira passiva ou ativa na rede.
Os operadores de encriptação-decriptação satisfazem a propriedade algébrica de serem
elementos inversos: ∀u ∈ U, Eu Du = Du Eu = λ, onde λ denota a palavra vazia (elemento
neutro do monóide). As informações trocadas entre usuários são arbitrárias, codificadas
e decodificadas com uso de encrypts e decrypts. Por isso, trata-se do monóide livremente
gerado pelos operadores criptográficos e de sua especificação módulo usuários, induzida
∗
†
Graduando em Matemática, bolsista CNPq. [email protected]
Orientador, parcialmente financiado pelo CNPq. [email protected]
1
pelos operadores, e trabalha-se aqui apenas com as palavras (strings) formadas pelos
mesmos, i.e., sequências finitas formadas pela concatenação de tais operadores.
Seja Σ = E ∪ D = {Eu | u ∈ U } ∪ {Du | u ∈ U }. Σ∗ denota o conjunto de todas as
palavras finitas sobre os sı́mbolos de Σ. ∀γ ∈ Σ∗ , |γ| indica o tamanho da palavra γ, i.e.,
número de elementos (operadores) presentes na sequência finita.
Adiciona-se aqui a noção de Normalização, que pode ser vista como uma aplicação.
Quando uma palavra σ ∈ Σ∗ é tal que σ = σ ′ Eu Du σ ′′ = σ ′ Du Eu σ ′′ , para alguns u ∈
U, σ ′ , σ ′′ ∈ Σ∗ , dizemos que σ pode ser normalizada com respeito a u, e denotamos por
σ u a normalização de σ com respeito a u, e σ como σ normalizada com respeito a todos
os usuários. Normalização então significa eliminar de uma dada palavra todos os pares de
operadores que possam ser cancelados, i.e., pares que resultem em λ.
Definição 1 (Protocolo em Cascata Bipartido) Determina como pares de usuários
devem comunicar-se na rede usada, e é definido por uma sequência finita não-vazia α =
αn−1 αn−2 · · · α2 α1 α0 , n ≥ 1, sendo αi : U × U → Σ∗ , ∀i tal que 0 ≤ i < n. Além disso,
∀x, y ∈ U , o protocolo goza das propriedades: αi (x, y) 6= λ, e está na forma normalizada,
αi (x, y) ∈ {Ex , Dx , Ey }∗ (i par) ou {Ey , Dy , Ex }∗ (i ı́mpar), e os passos de protocolo
executado entre quaisquer pares de usuários são exatamente os mesmos.
Ou seja, dados x, y ∈ U e M , a comunicação se dá da seguinte maneira: x envia a
y a mensagem α0 (x, y)M, y responde a x com α1 (x, y)α0 (x, y)M, x responde a y com
α2 (x, y)α1 (x, y)α0 (x, y)M , e assim sucessivamente.
Caracterização de Segurança
Seja z ∈ U um possı́vel sabotador. O interesse de z é conseguir informações na rede
a fim de obter conhecimento sobre os operadores decrypt de outros usuários ([1], [2]).
Denote por Σ(z) o conjunto de todas as palavras que z pode construir. Com isso, elaborase uma definição de segurança: se z puder construir uma palavra γ tal que ela “anule”
uma composição de um certo número de α’s, então z poderá decifrar alguma mensagem
arbitrária M que estiver sendo trocada entre dois usuários.
Definição 2 Um Protocolo em Cascata T satisfaz a Condição Inicial (CI) se o Passo
Inicial de T inclui operador(es) de encriptação em sua composição.
Definição 3 Uma palavra σ ∈ Σ∗ possui a Propriedade de Balanceamento (PB) com
respeito a u ∈ U se, caso exista algum Du em σ, então existe pelo menos um Eu em σ.
Definição 4 Um Protocolo em Cascata T é dito Balanceado se, ∀x, y ∈ U, ∀ i ≥ 0, temse que αi (x, y) satisfaz PB com respeito a x (se i é par) e satisfaz PB com respeito a y
(se i é ı́mpar), ou seja, se todo passo do protocolo satisfaz PB.
Teorema 1 (Caracterização da Segurança) Seja T um Protocolo em Cascata Bipartido. T é seguro se, e somente se, satisfaz CI e é um Protocolo Balanceado.
O Lema 1 e a Formalização em PVS
A demonstração do Teorema 1, tanto analı́tica quanto em PVS, requer uso do seguinte:
2
Lema 1 Sejam T um Protocolo em Cascata Balanceado e u ∈ U . Então, ∀η ∈ Σ(u), η
satisfaz PB com respeito a todo a ∈ U, a 6= u.
A prova analı́tica do Lema 1 faz uso direto de mais dois Lemas, e uso indireto de
mais outro (Lemas 9, 10 e 11, como vistos em [1]). Tanto o Lema 1 quanto os últimos
dizem respeito a propriedades de balanceamento de palavras da linguagem admissı́vel.
Tais propriedades são cruciais para determinarmos certas caracterı́sticas dessas palavras.
O PVS é um sistema cuja linguagem é construı́da com base em lógica de ordem superior,
e quantificação pode ser aplicada a variáveis de funções. Além disso, a biblioteca do PVS
disponibiliza uma ampla gama de tipos e a possibilidade de construção de tipos, bem como
uma poderosa noção de subtipos. As noções de PVS usadas para especificar os conceitos
aqui necessários são tiradas da teoria do prelude para finite sequences e sets ([3]).
Exemplifica-se o uso do PVS na teoria em questão com a especificação do Lema 1:
userBalancing : LEMMA FORALL (prot : welldefined protocol, z :
w /= z, gamma : gammaT | gamma welldef?(prot,gamma, z)) :
balanced cascade protocol?(prot) =>
balancedseq wrt?(normalizeseq(extract gamma(gamma)), w)
U, w :
U |
A formalização em PVS do Modelo de Dolev-Yao já vinha sendo feita pelo Grupo de
Teoria da Computação (GTC/UnB, [2]). Boa parte de sua especificação e verificação está
concretizada. A prova do Teorema 1 já foi realizada em PVS. Entretanto, isto se deu
através da axiomatização do Lema 1, que ainda não havia sido demonstrado em PVS.
Este trabalho concentra-se no estudo, na formalização e na especificação em PVS de
propriedades de balanceamento e algumas de suas variantes. Para tanto, vários resultados
a respeito de estruturas de palavras que possuam restrições quanto a usuários ou operadores nela presentes, vêm sendo obtidos e empregados na elaboração e prova de lemas. Na
teoria geral, tais lemas representam incrementos, correções e a base necessária para que
sejam verificados e provados os lemas conhecidos ([1]) sobre balanceamento.
Em particular, o Lema 1 pode ser visto como a generalização de certos resultados a
respeito dessas propriedades. Ainda que todos os lemas e teoremas aqui mencionados
já estejam demonstrados analiticamente, nem todas as provas em PVS estão concluı́das.
Um dos resultados deste trabalho foi a prova do Lema 1, iniciada de maneira análoga
à demonstração analı́tica, mas onde fez-se necessário o uso de um novo lema, resultado
de desenvolvimentos aqui realizados. Ainda que axiomatizando-se os Lemas 9, 10 e 11
para tal demonstração, verificou-se que a especificação da teoria, como vem sendo feita,
mostra-se extremamente eficaz. Trabalha-se agora na conclusão das provas (em PVS) dos
outros 3 lemas centrais (9, 10 e 11) sobre balanceamento. Com isso obteremos a completa
especificação e verificação do Modelo de Dolev-Yao.
Referências
[1] D. Dolev and A. C. Yao. On The Security Of Public Key Protocols. IEEE Transactions of
Information Theory, 1983, 29 (2).
[2] R. B. Nogueira, F. L. C. Moura, A. Nascimento and M. Ayala-Rincón. Formalization Of Security
Proofs Using PVS in the Dolev-Yao Model. In Proc. (Booklet) Computability in Europe CiE,
2010.
[3] S. Owre and N. Shankar. The Formal Semantics Of PVS. SRI International, Computer Science
Laboratory Menlo Park CA, USA, 1997.
3