Abstract

Abstract
MPC-in-the-Head (MitH) is a general framework that enables constructing efficient zero-knowledge (ZK) protocols for NP relations from secure multiparty computation (MPC) protocols. In this paper we present the first machine-checked implementations of MitH. We begin with an EasyCrypt formalization that preserves the modular structure of the original construction and can be instantiated with arbitrary MPC protocols, and secret sharing and commitment schemes satisfying standard notions of security. We then formalize various suitable components, which we use to obtain full-fledged ZK protocols for general relations. We compare two approaches for obtaining verified executable implementations. The first uses a fully automated extraction from EasyCrypt to OCaml. The second reduces the trusted computing base (TCB) and provides better performance by combining code extraction with formally verified manual low-level components implemented in the Jasmin language. We conclude with a discussion of the trade-off between the formal verification effort and the performance of resulting executables, and how our approach opens the way for fully verified implementations of state-of the-art optimized protocols based on MitH.

Abstract
Wikipedia is a free, multilingual, and collaborative online encyclopedia. Nowadays, it is one of the largest sources of online knowledge, often appearing at the top of the results of the major search engines, being one of the most sought-after resources by the public searching for health information. The collaborative nature of Wikipedia raises security concerns since this information is used for decision-making, especially in the health area. Despite being available in hundreds of idioms, there are asymmetries between idioms, namely regarding their quality. In this work, we compare the quality of health information on Wikipedia between idioms with 100 million native speakers or more, and also in Greek, Italian, Korean, Turkish, Persian, Catalan and Hebrew, for historical tradition. Quality metrics are applied to health and medical articles in English, maintained by WikiProject Medicine, and their versions in the above idioms. With this, we contribute to a clarification of the role of Wikipedia in the access to health information. We demonstrate differences in both the quantity and quality of information available between idioms. English is the idiom with the highest quality in general. Urdu, Greek, Indonesian, and Hindi achieved lower values of quality.

Abstract
Huge efforts and resources are spent every year on prevention and recovery of cyberattacks targeting users, services and network infrastructures. Software-Defined Networking (SDN) is a technology providing advances to the field of security with the ability of programming the network, promoting high-performance solutions and efficient resource utilization at low costs, as the use of specialized hardware is avoided. The present paper aims at exploring the SDN paradigm to develop an SDN-based framework for prevention and mitigation of malicious attacks throuhgt the network. The framework design and proposal has concerns regarding the efficient use of network and computational resources, distributing the inspection of suspicious flows by distinct Intrusion Detection Systems. For this purpose, a load-balancing strategy for traffic inspection is devised, allowing to balance both the usage of resources and the analysis of traffic flows. In this way, this paper also sheds light on the usage of OpenFlow messages to build distributed SDN-based applications with the mentioned properties.

Abstract
Virtual Reality (VR) has been showing potential in new and diverse areas, notably in education. However, there is a lack of studies in the Foreign Language Teaching and Learning field, particularly in listening comprehension. Therefore, this study investigated the effects of avatar animations and lip synchronization, and user interaction; features deemed relevant in this broader area. A sociodemographic, a quick CEFR-Common European Framework of Reference for Languages-15-minute English test, and questionnaire were used to evaluate the participants' Presence, Quality of Experience, Cybersickness and Knowledge Retention. Results show that, overall, the use of avatars with realistic animations and movements, and featuring lip synchronization have a positive influence on the users' sense of presence, knowledge retention and a more enjoyable overall quality of experience. The same can be said for the use of object interaction and navigation in the cultural representative environment, which had an overall positive impact.

Abstract
Polar codes have been shown to provide an effective mechanism for achieving physical-layer security over various wiretap channels. A majority of these schemes require channel state information (CSI) at the encoder for both intended receivers and eavesdroppers. In this paper, we consider a polar coding scheme for secrecy over a Gaussian wiretap channel when no CSI is available. We show that the availability of a shared keystream between friendly parties allows polar codes to be used for both secure and reliable communications, even when the eavesdropper knows a large fraction of the keystream. The scheme relies on a predetermined strategy for partitioning the bits to be encoded into a set of frozen bits and a set of information bits. The frozen bits are filled with bits from the keystream, and we evaluate the security gap when the cyclic redundancy check-aided successive cancellation list decoder is used at both receivers in the wiretap channel model.