Encontrados 25 documentos, a visualizar página 1 de 3
Ferramentas de suporte ao estudo da Disciplina de Sistemas Digitais: Mapas de K...
Sérgio Barbosa; Manuel Bernardo Cunha; Augusto SilvaThis article intends to reveal a tool for Boolean functions simplification, developed in the scope of the DigitalSystems program, part of the Mathematical EducationProject.The document begins by showing some work examples,describes the technology used in the project, it enunciates and describes (with examples) all the steps of the algorithm and finishes by illustrating graphically the results gathered inlaborat...
Ferramentas de suporte ao estudo da Disciplina de Sistemas Digitais: Carta de I...
Sérgio Barbosa; Manuel Bernardo Cunha; Augusto SilvaThe Implication Chart is an algorithm used to simplify Finite State Machines which is a lectured part of the Digital Systems course, under the Engineering Electronics, Telecommunication and Informatics Department responsibility.The result of all the work presented here is an efficient toolused at the project stage of sequential components and useful in the learning support.Developed for Microsoft platforms, it ...
On the semantic security of functional encryption schemes
Barbosa, Manuel Bernardo; Farshim, PooyaFunctional encryption (FE) is a powerful cryptographic primitive that generalizes many asymmetric encryption systems proposed in recent years. Syntax and security definitions for FE were proposed by Boneh, Sahai, and Waters (BSW) (TCC 2011) and independently by O’Neill (ePrint 2010/556). In this paper we revisit these definitions, identify several shortcomings in them, and propose a new definitional approach th...
A certifying compiler for zero-knowledge proofs of knowledge based on sigma-pro...
Almeida, José Bacelar; Bangerter, Endre; Barbosa, Manuel Bernardo; Krenn, Stephan; Sadeghi, Ahmad-Reza; Schneider, ThomasZero-knowledge proofs of knowledge (ZK-PoK) are important building blocks for numerous cryptographic applications. Although ZK-PoK have a high potential impact, their real world deployment is typically hindered by their significant complexity compared to other (non-interactive) crypto primitives. Moreover, their design and implementation are time-consuming and error-prone. We contribute to overcoming these chal...
Delegatable homomorphic encryption with applications to secure outsourcing of c...
Barbosa, Manuel Bernardo; Farshim, P.In this work we propose a new cryptographic primitive called Delegatable Homomorphic Encryption (DHE). This allows a Trusted Authority to control/delegate the capability to evaluate circuits over encrypted data to untrusted workers/evaluators by issuing tokens. This primitive can be both seen as a public-key counterpart to Verifiable Computation, where input generation and output verification are performed by d...
Practical realisation and elimination of an ECC-related software bug attack
Brumley, B. B.; Barbosa, Manuel Bernardo; Page, D.; Vercauteren, F.We analyse and exploit implementation features in OpenSSL version 0.9.8g which permit an attack against ECDH-based functionality. The attack, although more general, can recover the entire (static) private key from an associated SSL server via $633$ adaptive queries when the NIST curve P-256 is used. One can view it as a software-oriented analogue of the bug attack concept due to Biham et al. and, consequently, ...
Type checking cryptography implementations
Barbosa, Manuel Bernardo; Page, D.; Moss, Andrew; Rodrigues, Nuno F.; Silva, PauloProceedings da conferência Fundamentals of Software Engineering 2011 ; Cryptographic software development is a challenging field: high performance must be achieved, while ensuring correctness and compliance with low-level security policies. CAO is a domain specific language designed to assist development of cryptographic software. An important feature of this language is the design of a novel type system intr...
Formal verification of side channel countermeasures using self-composition
Almeida, José Bacelar; Barbosa, Manuel Bernardo; Pinto, Jorge Sousa; Vieira, BárbaraFormal verification of cryptographic software implementations poses significant challenges for off-the-shelf tools. This is due to the domain-specific characteristics of the code, involving aggressive optimisations and non-functional security requirements, namely the critical aspect of countermeasures against side-channel attacks. In this paper we extend previous results supporting the practicality of self-comp...
A deductive verification platform for cryptographic software
Barbosa, Manuel Bernardo; Filliâtre, Jean-Christophe; Pinto, Jorge Sousa; Vieira, BárbaraIn this paper we describe a deductive verification platform for the CAO language. CAO is a domain-specific language for cryptography. We show that this language presents interesting challenges for formal verification, not only in the rich mathematical type system that it introduces, but also in the cryptography-oriented language constructions that it offers. We describe how we tackle these problems, and also de...
Deductive verification of cryptographic software
Almeida, José Bacelar; Barbosa, Manuel Bernardo; Pinto, Jorge Sousa; Vieira, BárbaraWe apply state-of-the art deductive verification tools to check security-relevant properties of cryptographic software, including safety, absence of error propagation, and correctness with respect to reference implementations. We also develop techniques to help us in our task, focusing on methods oriented towards increased levels of automation, in scenarios where there are clear obvious limits to such automatio...
| Financiadores do RCAAP | |||||||
|
|
|
|
|
|
||