Counter-strategies are key components of coercion-resistant voting schemes, allowing voters to submit votes that represent their own intentions in an environment controlled by a coercer. By deploying a counter-strategy a voter can prevent the coercer from learning if the voter followed the coercer’s instructions or not. Two effective counter-strategies have been proposed in the literature, one based on fake credentials and another on revoting. While fake-credential schemes assume that voters hide cryptographic keys away from the coercer, revoting schemes assume that voters can revote after being coerced.In this work, we present a new counter-strategy technique that enables flexible vote updating, that is, a revoting approach that provides protection against coercion even if the adversary is able to coerce a voter at the very last minute of the voting phase. We demonstrate that our technique is effective by implementing it in Loki, an Internet-based coercion-resistant voting scheme that allows revoting. We prove that Loki satisfies a game-based definition of coercion-resistance that accounts for flexible vote updating. To the best of our knowledge, we provide the first technique that enables deniable coercion-resistant voting and that can evade last-minute voter coercion.

Socio-Technical Systems (STSs) combine the operations of technical systems with the choices and intervention of humans, namely the users of the technical systems. Designing such systems is far from trivial due to the interaction of heterogeneous components, including hardware components and software applications, physical elements such as tickets, user interfaces, such as touchscreens and displays, and notably, humans. While the possible security issues about the technical components are well known yet continuously investigated, the focus of this article is on the various levels of threat that human actors may pose, namely, the focus is on security ceremonies. The approach is to formally model human threats systematically and to formally verify whether they can break the security properties of a few running examples: two currently deployed Deposit-Return Systems (DRSs) and a variant that we designed to strengthen them. The two real-world DRSs are found to support security properties differently, and some relevant properties fail, yet our variant is verified to meet all the properties. Our human threat model is distributed and interacting: it formalises all humans as potential threatening users because they can execute rules that encode specific threats in addition to being honest, that is, to follow the prescribed rules of interaction with the technical system; additionally, humans may exchange information or objects directly, hence practically favour each other although no specific form of collusion is prescribed. We start by introducing four different human threat models, and some security properties are found to succumb against the strongest model, the addition of the four. The question then arises on what meaningful combinations of the four would not break the properties. This leads to the definition of a lattice of human threat models and to a general methodology to traverse it by verifying each node against the properties. The methodology is executed on our running example for the sake of demonstration. Our approach thus is modular and extensible to include additional threats, potentially even borrowed from existing works, and, consequently, to the growth of the corresponding lattice. STSs can easily become very complex, hence we deem modularity and extensibility of the human threat model as key factors. The current computer-assisted tool support is put to test but proves to be sufficient.

The authentication of a web server is a crucial procedure in the security of web browsing. It relies on certificate validation, a process that may require the participation of the user. Thus, the security of certificate validation is socio-technical as it depends on traditional security technology as well as on social elements such as cultural values, trust and human-computer interaction. This manuscript analyzes extensively the socio-technical security of certificate validation as carried out through today’s most popular browsers. First, we model processes, protocols and ceremonies that browsers run with servers and users as UML activity diagrams. We consider both classic and private browsing modes and focus on the certificate validation. We then translate each UML activity diagram to a CSP# model. The model is expanded with the LTL formalization of five socio-technical properties pivoted on user involvement with certificate validation. We automatically check whether the CSP# models are socio-technically secure against Man-in-the-Middle attacks using the PAT model checker. The findings turn out to be far from straightforward. From them, we state best-practice recommendations to browser vendors.

We introduce the notion of privacy-preserving verifiability for security protocols. It holds when a protocol admits a verifiability test that does not reveal, to the verifier that runs it, more pieces of information about the protocol’s execution than those required to run the test. Our definition of privacy-preserving verifiability is general and applies to cryptographic protocols as well as to human security protocols. In this paper we exemplify it in the domain of e-exams. We prove that the notion is meaningful by studying an existing exam protocol that is verifiable but whose verifiability tests are not privacy-preserving. We prove that the notion is applicable: we review the protocol using functional encryption so that it admits a verifiability test that preserves privacy according to our definition. We analyse, in ProVerif, that the verifiability holds despite malicious parties and that the new protocol maintains all the security properties of the original protocol, so proving that our privacy-preserving verifiability can be achieved starting from existing security

The fifth generation wireless system (5G) is expected to handle an unpredictable number of heterogeneous connected devices and to guarantee at least the same level of security provided by the contemporary wireless standards, including the Authentication and Key Agreement (AKA) protocol. The current AKA protocol has not been designed to efficiently support a very large number of devices. Hence, a new group-based AKA protocol is expected to be one of the security enhancement introduced in 5G. In this paper, we advance the group-based AKA threat model, reflecting previously neglected security risks. The threat model presented in the paper paves the way for the design of more secure protocols.

An exam is a practise for assessing the knowledge of a candidate from an examination she takes. Exams are used in various contexts, such as in university tests and public competitions. We begin by identifying various security and privacy requirements that modern exams should meet, especially in the prospect of them being supported by information and communication technologies. These requirements extend well beyond ensuring authenticating the candidate and preventing her from cheating. Cheating is routinely enforced by invigilation by trusted parties, whereas we discuss that an exam should meet its security and privacy requirements against stronger threat models, including malicious exam authorities. Thus exams must be designed with the care normally devoted to security protocols, and in such a mindset we present WATA IV, a new protocol that meets our security and privacy requirements even when an exam manager is malicious.

International audience

Electronic exam systems are pieces of software employed in online educations to assess performances of students. However, both the security of the protocols they reply upon and a general understanding of the possible threats is still to be met. This manuscript outlines a Ph.D. research work wherein we attempt to shed some light in the area. We identify the phases composing a typical exam system, we comments on relevant security properties that should be preserved in the various phases, and we advances an informal though structured definitions of them.

Authenticating a web server is crucial to the security of web browsing. It relies on TLS certificate validation, a property whose enforcement may require getting the user involved. Thus, certificate validation is a socio-technical property - it relies on traditional security technology as well as on social elements such as cultural values, trust and human-computer interaction. Hence the need for an appropriate methodology to study certificate validation from a socio-technical perspective. Certificate validation as carried out through today's most popular browsers - Chrome, Internet Explorer, Firefox and Opera Mini - is first represented by means of UML activity diagrams. It is then translated into CSP#, and expanded with the LTL formalization of four socio-technical properties pivoted on user involvement with certificate validation. The properties are then checked automatically using the PAT model checker. The findings turn out to be far from straightforward and, most importantly, allowed for prototyping a basic methodology for the sociotechnical formal analysis of security properties.