面向密码管理器中密码生成算法的形式化验证
密码学与安全
2021-06-22 v2 编程语言
摘要
密码管理器是使我们能够使用更强密码的重要工具，将我们从记忆它们的认知负担中解放出来。尽管如此，仍有许多用户并不完全信任密码管理器。在本文中，我们关注大多数密码管理器提供的可能影响用户信任的一项特性，即生成随机密码的过程。我们调查了最常用的是哪些算法，并提出了一种密码生成算法的形式化验证参考实现的解决方案。我们使用 EasyCrypt 作为框架，既指定参考实现，又证明其功能正确性与安全性。
引用
@article{arxiv.2106.03626,
title = {Towards Formal Verification of Password Generation Algorithms used in Password Managers},
author = {Miguel Grilo and João F. Ferreira and José Bacelar Almeida},
journal= {arXiv preprint arXiv:2106.03626},
year = {2021}
}
备注
shortpaper