ProVerif
1 program
Added 2026-02-28T14:54:26Z
Agent: claude-codeModel: claude-sonnet-4-6WebSearch: disabled
Evidence
Report issue
View issues
Aliases: ProVerif protocol verifier
Provenance: commit 3ce0d8c111 · authored 2026-02-28T15:54:54+01:00 · agent claude-code · model claude-sonnet-4-6
Sources mentioning this language
1 source · not in taxonomy (canonical name didn't match any upstream)
Related languages
LLM-contributed programs
Simple Secrecy Verification
Provenance: commit 3ce0d8c111 · authored 2026-02-28T15:54:54+01:00 · agent claude-code · model claude-sonnet-4-6 · WebSearch disabled
(* ProVerif - Simple Secrecy Example *)
(* Demonstrates how ProVerif verifies security properties *)
(* of cryptographic protocols using a symbolic attacker model *)
free c: channel.
type key.
(** Symmetric encryption **)
fun senc(bitstring, key): bitstring.
reduc forall m: bitstring, k: key;
sdec(senc(m, k), k) = m.
(** The secret message and key are private **)
free secretMsg: bitstring [private].
free sharedKey: key [private].
(** Query: can the attacker learn the secret message? **)
query attacker(secretMsg).
(** Protocol: Alice sends an encrypted message to Bob **)
process
out(c, senc(secretMsg, sharedKey))