Ida Siahaan

Verification of Cryptographic Protocols
Beller-Chang-Yacobi MSR Protocols with ProVerif

The verification of cryptographic protocols is a very
active research area. It is justified by the
seriousness of security flaws of cryptographic
protocols. This research has produces a number of
interesting methods and effective tools.

ProVerif is a protocol checker that can establish
secrecy and authenticity properties of protocols
represented directly as programs in a minimal
programming notation (an extension of the pi-calculus).
The protocols need not be finite-state;
the tool can deal with an unbounded number of protocol
sessions, even executed in parallel. Nevertheless, the
proofs are fully automatic and often fast.

This talk presents the application of this tool in the
verification of three public-key/private-key hybrid
key agreement and authentication protocols
(Beller-Chang-Yacobi MSR protocols). 
These protocols handle the problems relating to 
1) authentication-ensuring service is not obtained
   fraudulently, and 
2) the privacy of information about Portable
   Communications Systems (PCS s) user s location. 

The verification using ProVerif yields the flaws,
which have been discussed in the literature, and
analyzed by the verification tool LySa.

This case study aims to demonstrate the ability and
applicability of ProVerif. It also serves for
describing the transformation from the extended
pi-calculus to Horn clauses.