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.