Download ProVerif User Manual. - Prosecco

12
CHAPTER 3. USING PROVERIF
Asymmetric encryption. For asymmetric cryptography, we consider the unary constructor pk, which
takes an argument of type skey (private key) and returns a pkey (public key), to capture the notion of
constructing a key pair. Decryption is captured in a similar manner to symmetric cryptography with a
public/private key pair used in place of a symmetric key.
5
6
7
8
9
10
11
type s k e y .
type pkey .
fun pk ( s k e y ) : pkey .
fun aenc ( b i t s t r i n g , pkey ) : b i t s t r i n g .
reduc f o r a l l m: b i t s t r i n g , k : s k e y ; adec ( aenc (m, pk ( k ) ) , k ) = m.
Digital signatures. In a similar manner to asymmetric encryption, digital signatures rely on a pair of
signing keys of types sskey (private signing key) and spkey (public signing key). We will consider digital
signatures with message recovery:
12
13
14
15
16
17
18
19
type s s k e y .
type spkey .
fun spk ( s s k e y ) : spkey .
fun s i g n ( b i t s t r i n g , s s k e y ) : b i t s t r i n g .
reduc f o r a l l m: b i t s t r i n g , k : s s k e y ; ge t m e s s ( s i g n (m, k ) ) = m.
reduc f o r a l l m: b i t s t r i n g , k : s s k e y ; c h e c k s i g n ( s i g n (m, k ) , spk ( k ) ) = m.
The constructors spk, for creating public keys, and sign, for constructing signatures, are standard.
The destructors permit message recovery and signature verification. The destructor getmess allows the
adversary to get the message m from the signature, even without having the key. The destructor checksign
checks the signature, and returns m only when the signature is correct. Honest processes typically use
only checksign. This model of signatures assumes that the signature is always accompanied with the
message m. It is also possible to model signatures that do not reveal the message m, see Section 4.2.5.
Tuples and typing. For convenience, ProVerif has built-in support for tupling. A tuple of length
n > 1 is defined as (M1 , . . . , Mn ) where M1 , . . . , Mn are terms of any type. Once in possession of a tuple,
the adversary has the ability to recover the ith element. The inverse is also true: if the adversary is
in possession of terms M1 , . . . , Mn , then it can construct the tuple (M1 , . . . , Mn ). Tuples are always of
type bitstring. Accordingly, constructors that take arguments of type bitstring may be applied to tuples.
Note that the term (M ) is not a tuple and is equivalent to M . (Parentheses are needed to override the
default precedence of infix operators.) It follows that (M ) and M have the same type and that tuples of
arity one do not exist.
3.1.3
Process macros
To facilitate development, protocols need not be encoded into a single main process (as we did in
Section 2). Instead, sub-processes may be specified in the declarations using macros of the form
l e t R(x1 : t1 , . . . , xn : tn ) = P .
where R is the macro name, P is the sub-process being defined, and x1 , . . . , xn , of types t1 , . . . , tn
respectively, are the free variables of P . The macro expansion R(M1 , . . . , Mn ) will then expand to P with
M1 substituted for x1 , . . . , Mn substituted for xn . As an example, consider a variant docs/hello var.pv
of docs/hello.pv (previously presented in Chapter 2):
free c : channel .
f r e e Cocks : b i t s t r i n g [ private ] .
f r e e RSA : b i t s t r i n g [ private ] .