32 research outputs found
Schnorr protocol in Jasmin
No full textWe implement the Schnorr protocol in assembler via the Jasmin toolchain, and prove the security (proof-of-knowledge and zero-knowledge properties) and the absence of leakage through timing side-channels of that implementation in EasyCrypt.
In order to do so, we provide a semantic characterization of leakage-freeness for probabilistic Jasmin programs (that are not constant-time). We design a library for multiple-precision integer arithmetic in Jasmin -- the libjbn\u27\u27 library. Among others, we implement and verify algorithms for fast constant-time modular multiplication and exponentiation (using Barrett reduction and Montgomery ladder). We also implement and verify correctness and leakage-freeness of the rejection sampling algorithm. And finally, we put it all together and show the security of the overall implementation (end-to-end verification) of the Schnorr protocol, by connecting our implementation to prior security analyses in EasyCrypt (Firsov, Unruh, CSF~2023)
Reflection, Rewinding, and Coin-Toss in EasyCrypt
No full textIn this paper we derive a suite of lemmas which allows users to
internally reflect EasyCrypt programs into distributions which
correspond to their denotational semantics (probabilistic
reflection). Based on this we develop techniques for reasoning about
rewinding of adversaries in EasyCrypt. (A widely used technique in
cryptology.) We use our reflection and rewindability results to prove
the security of a coin-toss protocol
The Ouroboros of ZK: Why Verifying the Verifier Unlocks Longer-Term ZK Innovation
No full textVerifying the verifier in the context of zero-knowledge proof is an essential part of ensuring the long-term integrity of the zero-knowledge ecosystem. This is vital for both zero-knowledge rollups and also other industrial applications of ZK. In addition to further minimizing the required trust and reducing the trusted computing base (TCB), having a verified verifier opens the door to decentralized proof generation by potentially untrusted parties. We outline a research program and justify the need for more work at the intersection of ZK and formal verification research
Forking Lemma in EasyCrypt
No full textFormal methods are becoming an important tool for ensuring correctness and security of cryptographic constructions. However, the support for certain advanced proof techniques, namely rewinding, is scarce among existing verification frameworks, which hinders their application to complex schemes such as multi-party signatures and zero-knowledge proofs.
We expand the support for rewinding in EasyCrypt by implementing a version of the general forking lemma by Bellare and Neven. We demonstrate its usability by proving EUF-CMA security of Schnorr signatures
Zero-Knowledge in EasyCrypt
No full textWe formalize security properties of zero-knowledge protocols and
their proofs in EasyCrypt. Specifically, we focus on sigma-protocols
(three-round protocols). Most importantly, we also cover properties
whose security proofs require the use of rewinding; prior work has
focused on properties that do not need this more advanced technique.
On our way we give generic definitions of the main properties
associated with sigma protocols, both in the computational and
information-theoretical setting. We give generic derivations of
soundness, (malicious-verifier) zero-knowledge, and proof of
knowledge from simpler assumptions with proofs which rely on
rewinding. Also, we address sequential composition of sigma
protocols. Finally, we illustrate the applicability of our results
on three zero-knowledge protocols: Fiat-Shamir (for quadratic
residues), Schnorr (for discrete logarithms), and Blum (for Hamiltonian
cycles, NP-complete)
SOCIAL EDUCATION AT HIGHER MEDICAL SCHOOL
No full textThe development of social education in modern Russia became an important part of an overall process of social and innovative modernization of Russian society. Implementing of the educational standardin thefield of social workin Yaroslavl State Medical Academy confirms propriety of the development of socially oriented educational programs at higher medical school
Efficient Foreign-Field Arithmetic in PLONK
No full textPLONK is a prominent universal and updatable zk-SNARK for general circuit satisfiability, which allows a prover to produce a short certificate of the validity of a certain statement/computation. Its expressive model of computation and its highly efficient verifier complexity make PLONK a powerful tool for a wide range of blockchain applications.
Supporting standard cryptographic primitives (such us ECDSA over SECP256k1) or advanced recursive predicates (e.g. incrementally verifiable computation) on a SNARK presents a significant challenge. It requires so-called foreign-field arithmetic (enforcing constraints over algebraic fields that differ from the SNARK native field) which was previously believed to incur an overhead of two or three orders of magnitude.
We build on the techniques by Lubarov and Baylina and observe that, by considering tight bounds on their encoding of foreign-field multiplication, the number of PLONK constraints can be significantly reduced. We show that these techniques also extend to elliptic curve emulation, with an overhead of just one order of magnitude (with respect to its native counterpart). We validate soundness and completeness of our main results in EasyCrypt. Finally, we implement an open-source library with support for foreign-field arithmetic. Our experimental results showcase the generality of our techniques and confirm their suitability for real-world applications
Verified Multiple-Time Signature Scheme from One-Time Signatures and Timestamping
No full textBuldas, Laanoja, and Truu designed a family of server-assisted digital
signature schemes (BLT signatures) built around cryptographic
timestamping and forward-resistant tag systems. The original
constructions had either expensive key generation phase or stateful
client-side computations.
In this paper, we construct a stateless tag system with efficient key
generation from one-time signature schemes. We prove that the proposed
tag system is forward-resistant and when combined with cryptographic
timestamping, it induces a secure (existentially unforgeable)
multiple-time signature scheme. Our constructions are developed and
verified using the EasyCrypt framework
Formal Analysis of Non-Malleability for Commitments in EasyCrypt
No full textIn this work, we perform a formal analysis of definitions of
non-malleability for commitment schemes in the EasyCrypt theorem
prover. There are two distinct formulations of non-malleability found
in the literature: the comparison-based definition and the simulation-
based definition. In this paper, we do a formal analysis of both. We
start by formally proving that the comparison-based definition which was
originally introduced by Laur et al. is unsatisfiable. Also, we propose a
novel formulation of simulation-based non-malleability and show that it
is satisfiable in the Random Oracle Model. Moreover, we validate our
definition by proving that it implies hiding and binding of the commitment
scheme. Finally, we relate the novel definition to the existing definitions
of non-malleability
O impacto da digitalização no desenvolvimento do trabalho social e pedagógico
No full textThe article presents the results of an empirical study conducted by the authors according to the method of an online questionnaire survey (n = 157) in 2020. The respondents are Russian social workers. The study is aimed at identifying the specifics of the use of digital technologies in the professional activities of social workers and managers in the social sphere. The article analyses the effectiveness of the use of digital tools and highlights the problems in this activity. The authors also try to identify ways of solving these problems for the possible increase of the efficiency of digitalization in social work. The analysis of the respondents’ opinions has shown that among the main advantages are the increase in the efficiency of a labour organization (acceleration of data processing, automation of document management, online purchases and delivery) and obtaining the necessary information, including from other departments.El artículo presenta los resultados de un estudio empírico realizado por los autores en una encuesta de cuestionario en línea (n = 157) en 2020 con trabajadores sociales rusos. El estudio tiene como objetivo identificar las especificidades del uso de las tecnologías digitales en las actividades profesionales de los trabajadores sociales y administradores en el ámbito social. El artículo analiza la efectividad del uso de herramientas digitales y destaca los problemas en esta actividad e intenta identificar formas de resolver estos problemas para el posible aumento de la eficiencia de la digitalización en el trabajo social. El análisis de las opiniones de los encuestados ha mostrado que entre las principales ventajas se encuentran el aumento de la eficiencia de una organización laboral (aceleración del procesamiento de datos, automatización de la gestión documental, compras y entregas en línea) y la obtención de la información necesaria, incluso de otros departamentos.O artigo apresenta os resultados de um estudo empírico realizado pelos autores de acordo com o método de um questionário online (n = 157) em 2020. Os entrevistados são assistentes sociais russos. O estudo visa identificar as especificidades do uso das tecnologias digitais nas atividades profissionais de assistentes sociais e gestores na esfera social. O artigo analisa a eficácia do uso de ferramentas digitais e destaca os problemas nessa atividade. Os autores também tentam identificar formas de resolver esses problemas para o possível aumento da eficiência da digitalização no serviço social. A análise das opiniões dos respondentes mostrou que entre as principais vantagens estão o aumento da eficiência de uma organização trabalhista (aceleração do processamento de dados, automação da gestão de documentos, compras e entregas online) e a obtenção das informações necessárias, inclusive de outros departamentos
