arXiv subjects

Rosario Giustolisi

Publications and source records attributed to Rosario Giustolisi.

3 recordsLinked to original sources

arXiv2026

Cryptographic Choreographies

We present CryptoChoreo, a choreography language for the specification of cryptographic protocols. Choreographies can be regarded as an extension of Alice-and-Bob notation, providing an intuitive high-level view of the protocol as a whole (rather than specifying each protocol role in isolation). The extensions over standard Alice-and-Bob notation that we consider are non-deterministic choice, conditional branching, and mutable long-term memory. We define the semantics of CryptoChoreo by translation to a process calculus. This semantics entails an understanding of the protocol: it determines how agents parse and check incoming messages and how they construct outgoing messages, in the presence of an arbitrary algebraic theory and non-deterministic choices made by other agents. While this semantics entails algebraic problems that are in general undecidable, we give an implementation for a representative theory. We connect this translation to ProVerif and show on a number of case studies that the approach is practically feasible.

cs.CR↗

arXiv2022

Secure Internet Exams Despite Coercion

We study coercion-resistance for online exams. We propose two properties, Anonymous Submission and Single-Blindness which, if hold, preserve the anonymity of the links between tests, test takers, and examiners even when the parties coerce one another into revealing secrets. The properties are relevant: not even Remark!, a secure exam protocol that satisfied anonymous marking and anonymous examiners results to be coercion resistant. Then, we propose a coercion-resistance protocol which satisfies, in addition to known anonymity properties, the two novel properties we have introduced. We prove our claims formally in ProVerif. The paper has also another contribution: it describes an attack (and a fix) to an exponentiation mixnet that Remark! uses to ensure unlinkability. We use the secure version of the mixnet in our new protocol.

cs.CR↗

arXiv2015

Design and Analysis of Secure Exam Protocols

Except for the traditional threat that candidates may want to cheat, exams have historically not been seen as a serious security problem. That threat is routinely thwarted by having invigilators ensure that candidates do not misbehave during testing. However, as recent exam scandals confirm, also invigilators and exam authorities may have interest in frauds, hence they may pose security threats as well. Moreover, new security issues arise from the recent use of computers, which can facilitate the exam experience for example by allowing candidates to register from home. Thus, exams must be designed with the care normally devoted to security protocols. This dissertation studies exam protocol security and provides an in-depth understanding that can be also useful for the study of the security of similar systems, such as personnel selections, project reviews, and conference management systems. It introduces an unambiguous terminology that leads to the specification of a taxonomy of various exam types, depending on the level of computer assistance. It then establishes a theoretical framework for the formal analysis of exams. The framework defines several authentication, privacy, and verifiability requirements that modern exams should meet, and enables the security of exam protocols to be studied. Using the framework, we formally analyse traditional, computer-assisted, and Internet-based exam protocols. We find some security issues and propose modifications to partially achieve the desired requirements. This dissertation also designs three novel exam protocols that guarantee a wide set of security requirements. Finally, this dissertation looks at exams as carried out through modern browsers. We advance a formal analysis of requirements that are not only logically conditioned on the technology but also on user actions. We conclude with best-practice recommendations to browser vendors.

cs.CR↗