Tamarin e provas computacionais
Use o provador Tamarin para reescrita de multiconjuntos e verificação baseada em rastros.
Tamarin e provas computacionais é uma aula grátis de Cryptology Academy no CoddyKit. Esta é a aula 4 de 4. Você pode ler a aula completa abaixo gratuitamente — depois pratica ao vivo no navegador com um editor de código integrado e um tutor de IA 24/7. Faz parte do caminho de aprendizado de Cryptology Academy, e seu progresso é sincronizado entre a web e o app CoddyKit. O curso de Cryptology Academy inclui 4 aulas no total.
O que é o Tamarin?
Tamarin (ETH Zurich, 2012) é um verificador de protocolos de segurança baseado em reescrita de multiconjuntos. Diferentemente da abordagem por cláusulas de Horn do ProVerif, o Tamarin raciocina sobre rastros de execuções de protocolos com um provador interativo.
Tamarin vs. ProVerif
ProVerif: totalmente automatizado, pode dizer "não pode ser comprovado". Tamarin: assistente interativo de provas + modo automatizado, lida com teorias equacionais (XOR, Diffie-Hellman, mapas bilineares). É mais expressivo, mas tem uma curva de aprendizagem mais acentuada.
Regras de Reescrita de Multiconjuntos
O Tamarin modela protocolos como regras de reescrita sobre fatos. Os fatos representam o estado. Uma regra [ L ] --[ A ]-> [ R ] consome os fatos do lado esquerdo L, produz os fatos do lado direito R e registra a ação A no rastro.
Linguagem de Entrada do Tamarin (.spthy)
Um arquivo de teoria do Tamarin declara funções, equações, regras e lemas:
/* Diffie-Hellman key exchange */
builtins: diffie-hellman
rule Alice_1:
[ Fr(~a) ] /* fresh random a */
--[ AliceSent($A, $B, 'g'^~a) ]->
[ Alice_St($A, $B, ~a), Out('g'^~a) ]
rule Bob_1:
[ In(ga), Fr(~b) ]
--[ BobReceived($A, $B, ga) ]->
[ Bob_St($A, $B, ~b, ga^~b), Out('g'^~b) ]Declaração de Lemas
Os objetivos de segurança são expressos como lemas sobre rastros:
/* Secrecy: shared secret not known to attacker */
lemma secret_key:
"All A B k #i #j.
AliceKey(A, B, k) @ i &
BobKey(A, B, k) @ j
==> not (Ex #r. K(k) @ r)"
/* Authentication: if Bob has key, Alice sent it */
lemma authentication:
"All A B k #j. BobKey(A, B, k) @ j
==> Ex #i. AliceKey(A, B, k) @ i & i < j"Execução do Tamarin
Inicie a GUI interativa do Tamarin: tamarin-prover interactive my_protocol.spthy. A interface do navegador mostra as obrigações de prova; você orienta as estratégias automatizadas ou aplica etapas manuais nos casos que não terminam.
Solidez Computacional
Provas simbólicas (ProVerif, Tamarin) garantem segurança sob as hipóteses de criptografia perfeita. Os teoremas de solidez computacional (Cortier, Backes) elevam as provas simbólicas à segurança computacional quando instanciadas com primitivas cuja segurança foi comprovada.
F* e HACL*: Implementações Verificadas
F* (Microsoft Research) é uma linguagem de programação orientada a provas. HACL* é uma biblioteca criptográfica escrita em F*, com provas verificadas por máquina de correção e resistência a canais laterais. É usada no Firefox NSS e no mbedTLS.
EasyCrypt: Provas Computacionais Baseadas em Jogos
O EasyCrypt permite provas de segurança totalmente computacionais (baseadas em jogos) para construções criptográficas — não apenas para protocolos. A camada de registros do TLS 1.3 e o ChaCha20-Poly1305 foram verificados no EasyCrypt.
Impacto Prático
A criptografia verificada formalmente está chegando à produção: o NSS (Firefox) usa HACL*, a AWS usa s2n-tls com asserções acompanhadas de provas, e o protocolo Signal foi verificado no ProVerif e no Tamarin. Os métodos formais já não são apenas acadêmicos.
Verificação de Conhecimento
Como o Tamarin difere do ProVerif ao lidar com casos em que a automação falha?
Recapitulação da Lição
O Tamarin usa reescrita de multiconjuntos e raciocínio baseado em rastros com uma GUI interativa de provas. Ele lida com teorias equacionais de DH e XOR. Os lemas expressam objetivos de sigilo e autenticação. A solidez computacional estabelece uma ponte entre provas simbólicas e segurança real. HACL* e EasyCrypt ampliam a verificação para implementações e construções.
Perguntas Frequentes
A aula “Tamarin e provas computacionais” é grátis?
Sim — o texto completo de “Tamarin e provas computacionais” é grátis para ler aqui na web. Para praticá-la interativamente (um editor de código integrado e um tutor de IA 24/7) e desbloquear o restante do curso de Cryptology Academy, atualize para CoddyKit PRO. O curso de Cryptology Academy inclui 4 aulas no total.
O que vou aprender em “Tamarin e provas computacionais”?
Use o provador Tamarin para reescrita de multiconjuntos e verificação baseada em rastros. Você pratica Cryptology Academy com código prático que executa diretamente no navegador, e um tutor de IA 24/7 responde suas dúvidas enquanto trabalha na aula.
Preciso ter experiência prévia para começar Cryptology Academy?
Nenhuma experiência prévia é necessária. Cryptology Academy no CoddyKit é estruturado para alunos iniciantes até avançados, então você pode começar aqui ou desde o início e aprender no seu ritmo. Esta é a aula 4 de 4.
Quanto tempo leva a aula “Tamarin e provas computacionais”?
A maioria das aulas CoddyKit leva cerca de 5–10 minutos. Cada uma é compacta e interativa, então você faz progresso constante e retoma exatamente de onde parou entre web e app.
Posso escrever e executar código nesta aula de Cryptology Academy?
Sim. Cada aula de Cryptology Academy inclui um editor de código integrado, então você escreve e executa código real direto no navegador e recebe feedback de IA instantaneamente — nenhuma configuração local necessária.
Todas as aulas deste curso
- Por que provas informais não são suficientes
- Modelo de atacante Dolev-Yao e criptografia simbólica
- ProVerif: verificação automatizada de protocolos
- Tamarin e provas computacionais