Download ProVerif 1.85: Automatic Cryptographic Protocol Verifier, User

7
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
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 ] .
event evCocks .
event evRSA .
query event ( evCocks ) ==> event ( evRSA ) .
process
out ( c , RSA ) ;
in ( c , x : b i t s t r i n g ) ;
i f x = Cocks then
event evCocks ;
event evRSA
else
event evRSA
Lines 1-7 should be familiar. Lines 8-9 declare events evCocks and evRSA. Intuition suggests that Line 11
is some form of query. Lines 13-14 should again be standard. Line 15 contains a message input of type
bitstring on channel c which it binds to the variable x. Lines 16-20 denote an if-then-else statement;
the body of the then branch can be found on Lines 17-18 and the else branch on Line 20. We remark
that the code presented is a shorthand for the more verbose
i f x = Cocks then event evCocks ; event evRSA ; 0 e l s e event evRSA ; 0
where 0 denotes the end of a branch (termination of a process). The statement event evCocks (similarly
event evRSA) declares an event and the query
query event ( evCocks ) ==> event ( evRSA )
is true if and only if, for all executions of the protocol, if the event evCocks has been executed, then the
event evRSA has also been executed before. Executing the script produces the output:
Process:
{1}out(c, RSA);
{2}in(c, x: bitstring);
{3}if x = Cocks then
{4}event evCocks;
{5}event evRSA
else
{6}event evRSA
-- Query event(evCocks) ==> event(evRSA)
Completing...
Starting query event(evCocks) ==> event(evRSA)
RESULT event(evCocks) ==> event(evRSA) is true.
As expected, it is not possible to witness the event evCocks without having previously executing the event
evRSA and hence the correspondence event(evCocks) ==> event(evRSA) is true. In fact, a stronger
property is true: the event evCocks is unreachable. The reader can verify this claim with the addition of
query event(evCocks). (The authors remark that writing code with unreachable points is a common
source of errors for new users. Advice on avoiding such pitfalls will be presented in Section 4.3.1.)