ProVerif is a tool for automatically analyzing the security of cryptographic protocols. Support is provided for, but not limited to, cryptographic primitives including:
symmetric and asymmetric encryption; digital signatures; hash functions; bit-commitment; and non-interactive zero-knowledge proofs.
(*
Alice sends a private message to Bob on a
public channel that the attacker cannot read.
*)
set traceDisplay = long.
type private_key .
type public_key .
fun public_key_from_private_key(private_key): public_key .
fun authenticated_encrypt( bitstring, public_key) : bitstring .
reduc forall m: bitstring, k: private_key; authenticated_decrypt(authenticated_encrypt(m, public_key_from_private_key(k)), k) = m .
free alice_private_key: private_key [ private ] .
free alice_message_for_bob: bitstring [ private ] .
free bob_private_key: private_key [ private ] .
free public_messaging_channel : channel .
query attacker ( alice_message_for_bob ).
process
out ( public_messaging_channel, authenticated_encrypt(alice_message_for_bob, public_key_from_private_key(bob_private_key)) ) ;
0
(*
Alice sends a private message to Bob on a
public channel that the attacker cannot read, but Bob publishes his private_key
letting the attacker read alices message.
*)
set traceDisplay = long.
type private_key .
type public_key .
fun public_key_from_private_key(private_key): public_key .
fun authenticated_encrypt( bitstring, public_key) : bitstring .
reduc forall m: bitstring, k: private_key; authenticated_decrypt(authenticated_encrypt(m, public_key_from_private_key(k)), k) = m .
free alice_private_key: private_key [ private ] .
free alice_message_for_bob: bitstring [ private ] .
free bob_private_key: private_key [ private ] .
free public_messaging_channel : channel .
query attacker ( alice_message_for_bob ).
process
out ( public_messaging_channel, authenticated_encrypt(alice_message_for_bob, public_key_from_private_key(bob_private_key)) ) ;
(* Here bob accidentally publishes his private key, giving the attacker access to alice's message. *)
out ( public_messaging_channel, bob_private_key);
0