## Rosario Giustolisi: *Modelling and Verification of Secure Exams*

Springer, 2018, 133 pages, ISBN 978-3-319-67106-2

https://www.springer.com/gp/book/9783319671062

#### Summary

Exams are an important aspect in assessing people’s skills and as such play a key role to establish meritocracy in modern societies. To be effective, however, exams need to be fair and secure against tampering, which is where Rosario Giustolisi’s book “Modelling and Verification of Secure Exams'' [5] comes to the rescue. Over 133 pages, the book describes the different aspects of exams in detail and identifies various security-related requirements for them. Moreover, the book describes how to formally model an exam using the applied pi-calculus and how to verify security requirements for it using the ProVerif verifier. Finally, the book presents the outcome of modelling and analysing three popular example protocols. This book might be of interest to everyone who wants to learn more about the nature of exams in general, and in particular about how to model and verify them. To fully appreciate the book, however, some familiarity with the applied pi-calculus and in particular the ProVerif verifier is necessary.

This review is written by Diego Marmsoler for FME’s Book Review Committee (BRC). The aim of the BRC is to provide to the formal methods community, and to the scientific community in general, high-quality reviews of books on topics of interest to the community.

**Modelling and Verification of Secure Exams by
Rosario Giustolisi.**

#### Review

The book opens with a description of the key entities relating to
exams — such as *candidates*, *examiners*, *question committee*,
*collector*, and *remaining authorities* — and then shows how they
can be modelled using the applied pi-calculus [1] as the concurrent
execution of corresponding processes. In addition, the author
identifies various security requirements for exams and discusses
possibilities to formalize them. In particular, three types of
security requirements are discussed: *authentication*, *privacy*, and
*verifiability*. Authentication is formalized in terms of
correspondence properties such as “if a certain event happens then
another event must have happened before''. Privacy requirements, on
the other hand, are formalized as a special kind of bisimilarity
requirements. To formalize verifiability requirements, the author
first introduces an alternative definition of an exam — compared to
the process algebraic one — based on basic set theory. Verifiability
is then formalized as a predicate-logic formula over the model.
Finally, the author describes the outcome of applying the approach to
three concrete exam protocols. The first one is the
*Huszti-Pethö* [7] protocol which — according to the author
— was the first protocol proposed in literature that focused on
authentication and privacy, even in the presence of corrupted
candidates and exam authorities. The second protocol described is
*Remark!* [6]: a protocol designed for secure internet-based
exams without relying on a single, trusted authority. The last
protocol is the *Written Authenticated Though Anonymous (WATA)*
exam protocol [2,3], which is actually a family of exam protocols with
different levels of computer assistance. For each of the protocols,
the author formalizes several security properties and analyses them
using the ProVerif [4] verifier. In some of the protocols, the author
found violations for several properties originally claimed to be true.

The book provides a good overview of key elements of various types of exams and their corresponding security requirements, leading to a better understanding of exam protocols in general and in particular how they could be formalized. However, clarity is reduced by the fact that the book uses a mix of two different formalisms: while the applied pi-calculus is used to formalize authentication and privacy requirements, an abstract model based on set theory is used to formalize verifiability. Later on, the abstract formalization of verifiability is again mapped to ProVerif — again a process calculus model — which raises the question why the formalization of verifiability was not given in terms of the pi-calculus in the first place.

The description of the individual exam protocols is very detailed and easy to follow. What is particularly well accomplished is that the most important cryptographic primitives for a certain protocol are explained in detail. The formalization of the protocols, however, is not always discussed in detail and sometimes one would wish additional explanations. Moreover, ProVerif itself is not introduced and thus it is difficult to understand all the details of the formalization of the protocols for an audience not familiar with ProVerif.

In summary, this is a book from an expert to experts and probably best
suited for an audience with a background in Formal Methods as well as
Security wanting to learn more about how Formal Methods can be used
for the design and analysis of exam protocols. A reader with a solid
background in *Formal Methods* and *Security* should be able to grasp
most of the book’s contents. However, to fully appreciate the book,
the reader needs to be familiar with the applied pi-calculus [1] and
in particular the ProVerif [4] protocol analyser.

### References

[1] M. Abadi, C. Fournet. *Mobile values, new names, and secure
communication*. In Proc. POPL’01, pages 104-115. ACM, 2001.

[2] G. Bella, G. Costantino, L. Coles-Kemp, S. Riccobene. *Remote
management of face-to-face written authenticated though anonymous
exams*. In Proc. 3rd Intl. Conf. on Computer Supported Education
(CSEDU), pages 431–437. SciTePress 2011.

[3] G. Bella, G. Costantino, S. Riccobene. *Wata-a system for written
authenticated though anonymous exams*. In Proc. 2nd Intl. Conf. on
Computer Supported Education (CSEDU), pages 132–137. INSTICC
Press 2010.

[4] B. Blanchet. *Modeling and verifying security protocols with the
Applied Pi Calculus and ProVerif*. Foundations and Trends in Privacy
and Security, 1(1-2):1–135, 2016.

[5] R. Giustolisi. *Modelling and Verification of Secure
Exams*. Springer, 2018.

[6] R. Giustolisi, G. Lenzini, P. Y. A. Ryan. *Remark!: A secure protocol
for remote exams*. In Security Protocols XXII, pages 38-48.
LNCS 8809. Springer, 2014.

[7] A. Huszti, A. Petho. *A secure electronic exam
system*. Publicationes Mathematicae Debrecen, 77(3-4):299–312, 2010.