📎

ProVerif Syntax

Syntax

declaring a process describing the protocol

<decl>* process <process>

Variables

Variables are the identifiers used in let and in(c,x) .

One can bind names to them (which turns them to names.)

Names

globally declared free identifiers.

undeclared free identifiers (avoid these).

Syntactic sugar: instead of using new to declare new names one can use these shortcuts:

Free names:

[private] free id1, ... idn

Free names are public by default - here they are declared as private.

Constructor declarations

Defining a constructor with nn arguments

[private] fun constructor_name/n

Examples:

  • fun encrypt / 2
  • fun sign / 2
  • fun hash / 1
  • private fun serverkey / 1

Destructor declarations

Defining a destructor with its own reduction rule.

[private] reduc destructor_name(M1,M2,...,Mn) = M

Where M1,…,Mn,MM_1,\dots,M_n, M are variables.

Example:

  • reduc decrypt(encrypt(x,y),y) = x

Equational rule declarations

Translated by proVerif into rewriting rules.

Example:

  • exp(exp(x,z),z) → exp(exp(x,z),y)

Process macros and pattern-matching

syntactic sugar

let process_name = <process>

then one can refer to the process by process_name .

For pattern matching we must = and for binding we must leave it out, like so:

  • let (=tag, =B, x) = decrypt (ctext, k) in ...

Events

Used for logging (as seen before, for begin / end events ...).

Logging = security related protocol points.

Used for authenticity properties .

Examples:

  • eventbeginSend(A,B,m)
  • eventendSend(A,B,m)

Queries

You can ask whether something is known to a process.

Example:

  • query attacker: MIs M known to the attacker?
  • query ev:M ==> ev:NDoes event N always follow after event N?
  • query evinj:M ==> evinj:NSpecifically for injective agreements.

Variables in queries

Variables in correspondence queries are universally quantified:

query ev:endSend(x,y,z) ==> ev:beginSend(x,y,z)

is equivalent to

(∀x,y,z) ev:endSend(x,y,z) ==> ev:beginSend(x,y,z)

Variables in secrecy queries are existentially qunatified:

query attacker:x

is equivalent to

(∃x) attacker:x

Which is always true! You want to ask for the existence of names, not variables.