ProVerif: verificação automatizada de protocolos
Especifique e verifique propriedades do handshake do TLS com ProVerif.
ProVerif: verificação automatizada de protocolos é uma aula grátis de Cryptology Academy no CoddyKit. Esta é a aula 3 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 ProVerif?
ProVerif (Bruno Blanchet, 2001) é um verificador automatizado de protocolos criptográficos. Ele recebe um protocolo descrito no cálculo pi aplicado e decide automaticamente propriedades de sigilo e autenticação.
Como o ProVerif Funciona
O ProVerif traduz o protocolo em cláusulas de Horn e aplica um algoritmo baseado em resolução para derivar o que o atacante pode aprender. Se um fato de sigilo puder ser derivado, o protocolo está comprometido; caso contrário, sua segurança é PROVED.
Linguagem de Entrada do ProVerif
Os protocolos são descritos de forma declarativa: declare canais, tipos, funções (enc, dec, sign, verify), equações (dec(enc(m,k),k)=m) e processos que se comunicam por canais.
Declaração de Primitivas Criptográficas
Exemplo de declarações do ProVerif:
(* Symmetric encryption *)
fun senc(bitstring, key): bitstring.
fun sdec(bitstring, key): bitstring.
equation forall m: bitstring, k: key; sdec(senc(m, k), k) = m.
(* Asymmetric encryption *)
fun pk(skey): pkey.
fun aenc(bitstring, pkey): bitstring.
fun adec(bitstring, skey): bitstring.
equation forall m: bitstring, sk: skey; adec(aenc(m, pk(sk)), sk) = m.Escrita de um Processo de Protocolo Simples
Modele Alice e Bob como processos paralelos:
(* Alice sends nonce to Bob, encrypted *)
let Alice(skA: skey, pkB: pkey) =
new na: nonce;
out(c, aenc((na, pk(skA)), pkB));
in(c, m: bitstring);
let nb = adec(m, skA) in
out(c, aenc(nb, pkB)).
(* Main process: run attacker with full channel control *)
process
new skA: skey; new skB: skey;
out(c, pk(skA)); out(c, pk(skB)); (* publish public keys *)
(Alice(skA, pk(skB)) | Bob(skB, pk(skA)))Declaração de Consultas de Segurança
O ProVerif verifica consultas como:
(* Secrecy: attacker cannot learn na *)
query attacker(na).
(* Authentication: if Bob completes, Alice started *)
query event(BobFinished(nb)) ==> event(AliceStarted(nb)).Interpretação da Saída do ProVerif
O ProVerif exibe "RESULT ... é verdadeiro" (segurança comprovada) ou "RESULT ... é falso" e imprime um rastro de ataque como contraexemplo, mostrando as mensagens do atacante. O rastro mostra exatamente como o ataque funciona.
Verificação do TLS 1.3 com o ProVerif
Bhargavan et al. (2016) usaram o ProVerif para analisar um modelo do TLS 1.3. Eles encontraram e relataram um ataque ao mecanismo de retomada 0-RTT, que foi corrigido antes da finalização da RFC.
Limitações: Aproximação e Laços
O ProVerif produz uma superaproximação: pode relatar ataques falsos (dizer "falso" quando o protocolo é, na verdade, seguro), mas nunca deixa de detectar ataques reais. Sessões de protocolo ilimitadas podem não terminar — o ProVerif desenrola os laços heurísticamente.
Quando o ProVerif Diz "Não Pode Ser Comprovado"
Se o ProVerif não puder determinar o resultado dentro da sua aproximação, ele exibirá "CANNOT BE PROVED.". Isso não é uma prova de insegurança — significa que a ferramenta esgotou sua capacidade heurística. O Tamarin pode ter êxito nesses casos.
Verificação de Conhecimento
O que significa uma saída do ProVerif como "RESULT ... é falso" para uma consulta de sigilo?
Recapitulação da Lição
O ProVerif automatiza a verificação de protocolos usando resolução de cláusulas de Horn. Os protocolos são escritos no cálculo pi aplicado com equações criptográficas. As consultas questionam propriedades de sigilo e autenticação. Falso significa segurança comprovada; verdadeiro significa que o protocolo está comprometido (com um rastro de ataque). Limitações: as aproximações podem resultar em "não pode ser comprovado".
Perguntas Frequentes
A aula “ProVerif: verificação automatizada de protocolos” é grátis?
Sim — o texto completo de “ProVerif: verificação automatizada de protocolos” é 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 “ProVerif: verificação automatizada de protocolos”?
Especifique e verifique propriedades do handshake do TLS com ProVerif. 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 3 de 4.
Quanto tempo leva a aula “ProVerif: verificação automatizada de protocolos”?
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