Prezados, gostaria de convidá-los a participar da palestra do Prof. Andrew Marshall que ocorrerá no dia 6/11, às 11:00. Os dados estão abaixo:
Join Zoom Meeting https://us02web.zoom.us/j/87296172206?pwd=bHRzNCt2NzZDQnFBZjhQK3V6SFVvdz09 Meeting ID: 872 9617 2206 Passcode: 399468 -------------------------------------------- Symbolic Methods in the Formal Analysis of Automatically Synthesized Cryptographic Algorithms Prof. Andrew Marshall <https://www.google.com/url?q=https%3A%2F%2Fwww.marshallandrew.net%2F&sa=D&sntz=1&usg=AFQjCNHs0lR6glYyI3t3TxVK-BSK24II4Q> University of Mary Washington Abstract: While symbolic methods have long been applied to cryptographic protocol analysis, there has been comparatively little done on developing new classes of symbolic techniques specifically for application to automated synthesis of cryptographic algorithms. However, since the symbolic algebras used in the evaluation of automatically synthesized cryptosystems have much in common with those used in the analysis of cryptographic protocols, a promising direction in research is to build on these previously developed methods combined with new methods to make advances in the symbolic analysis of automatically synthesized cryptosystems. Many of the symbolic characterizations are expressed in terms of the existence or non-existence of solutions to systems of equations. Thus, unification, the process of finding solutions to systems of equations in a symbolic algebra, is an important tool in this approach. However, the unification algorithms in this setting often need to obey certain constraints. For example, the solutions may need to be computable by a probabilistic polynomial-time adversary without access to certain terms (e.g. some cryptographic keys), or a solution may require that certain terms not be identical, thus adding a disunification constraint. Additionally, an authentication algorithm may require that authentication checks (which usually involve checking an inequality) succeed for correctly authenticated data and fail for all other cases. Thus, this area requires the development of new unification methods and algorithms. In this talk we provide some background material to this symbolic approach to the analysis of these types of cryptographic systems. We then detail several new problems and results with a focus on new unification algorithms. We review a new tool for automating some of the above methods. Finally, we outline some future work and open questions. ------------------------ -- Daniele Nantes Grupo de Teoria da Computação Departamentos de Matemática e Computação Universidade de Brasília www.mat.unb.br/~dnantes -- Você está recebendo esta mensagem porque se inscreveu no grupo "LOGICA-L" dos Grupos do Google. Para cancelar inscrição nesse grupo e parar de receber e-mails dele, envie um e-mail para [email protected]. Para ver esta discussão na web, acesse https://groups.google.com/a/dimap.ufrn.br/d/msgid/logica-l/CAMnPOrqod06ovJRAfM3t45Vn4ih4%2B60%2BecrqnsPQTiY7VByRMg%40mail.gmail.com.
