salle A. Turing CE4
6 February 2014 - 15h00
Formal Security Analysis for Routing Protocols and E-exams
by Ali Kassem from Verimag
Abstract: Security protocols aim at securing communications over public net-
works. Their design is error-prone and not an easy task. Formal
methods have shown their usefulness for providing a careful security
analysis and discovering flaws if exist. We make some contributions
in security analysis of routing protocols and e-exams.
First, we work on route validity in ad-hoc networks. We consider
the non-cooperative attacker model to analysis the route validity prop-
erty. In such networks the presence of an attack depends on the net-
work topology. Thus, we have to verify an infinite number of topolo-
gies which is not tractable. We show that verifying the route validity
under the non-cooperative model requires to verify only five topologies.
In a fixed network topology, the problem of verifying route validity can
be reduced to a satisfiability of non-well-formed constraints system.
Currently, we are working in a novel constraint reduction procedure
for this general class of non-well-formed constraints.
Second, we consider electronic exams protocols. E-exams are com-
puter based systems meant to evaluate skills of people taking tests
remotely and often via the Internet. E-exams are claimed secure since
they rely upon cryptographic protocols running under optimistic trust
assumptions. This security is mostly unproven. We provide the means
to check whether an e-exam protocol is secure or not. In the formal
framework of the applied pi calculus, we define authentication, privacy
and verification properties for e-exams. As proof of concept we model
a recently proposed secure electronic exam system and we verify it
intensively with ProVerif, and we find some flaws on it.
