Uma análise orientada a modelo das propriedades de segurança do Mimblewimble e suas implementações de protocolo
DOI:
https://doi.org/10.36561/ING.24.10Palavras-chave:
Segurança, Verificação formal, Mimblewimble, Modelo idealizado, CriptomoedaResumo
Mimblewimble é uma tecnologia de criptomoeda orientada para a privacidade que fornece propriedades de segurança e escalabilidade que a distinguem de outros protocolos. A abordagem criptográfica do Mimblewimble é baseada na Elliptic Curve Cryptography, que permite verificar uma transação sem revelar nenhuma informação sobre o valor da transação ou as partes envolvidas. O Mimblewimble combina transações confidenciais, CoinJoin e cut-through para alcançar um nível mais alto de privacidade, segurança e escalabilidade. Neste trabalho, apresentamos e discutimos essas propriedades de segurança e delineamos a base de uma abordagem de verificação orientada por modelo para abordar a certificação da correção das implementações de protocolo. Em particular, propomos um modelo idealizado que é chave no processo de verificação descrito. Em seguida, identificamos e declaramos com precisão as condições de nosso modelo para garantir a verificação das propriedades de segurança relevantes do Mimblewimble. Além disso, analisamos as implementações Grin e Beam do Mimblewimble em seu estado atual de desenvolvimento. Apresentamos conexões detalhadas entre nosso modelo e suas implementações em relação à estrutura Mimblewimble e suas propriedades de segurança.