Novo Modelo Baseado em SAT para o Problema de Decisão de Circuito Quântico: Buscando uma Implementação Quântica de Baixo Custo

Nos últimos anos, a tecnologia quântica tem se desenvolvido rapidamente. À medida que análises de segurança para cifras simétricas continuam a surgir, muitas delas requerem uma avaliação dos recursos necessários para a implementação de circuito quântico do algoritmo de criptografia. Nesse sentido, propomos o problema de decisão de circuito quântico, que exige determinar se existe um circuito quântico para uma dada permutação f usando M qubits ancilla e não mais que K portas quânticas dentro da profundidade D do circuito. Primeiramente, investigamos algoritmos heurísticos e modelos clássicos baseados em SAT em trabalhos anteriores, revelando suas limitações na resolução do problema. Assim, propomos de forma inovadora um modelo melhorado baseado em SAT que incorpora três métricas de circuitos quânticos. O modelo nos permite encontrar o circuito quântico ótimo de uma S-box arbitrária de 3 ou 4 bits sob um determinado objetivo de otimização baseado em solucionadores de SAT, que provou a optimalidade de circuitos construídos pela ferramenta, LIGHTER-R. Em seguida, ao combinar diferentes critérios no modelo, encontramos implementações de circuito quântico mais compactas de S-boxes como RECTANGLE e GIFT. Para a S-box GIFT, nosso modelo fornece o circuito quântico ótimo que requer apenas 8 portas com uma profundidade de 31. Além disso, nosso modelo pode ser generalizado para camadas lineares e melhorar o modelo anterior baseado em SAT proposto por Huang et al. no ASIACRYPT 2022, adicionando critérios sobre o número de qubits e a profundidade do circuito.