文件名称：Saatana:加密框架，经验证可正确处理SPARK
文件大小：312KB
文件格式：ZIP
更新时间：2024-04-25 03:42:39
cryptography encryption ada formal-verification spark-ada
针对高级网络应用的SPARK / Ada算法 加密框架，经验证可正确处理SPARK 由于我们正在使用SPARK的 ，因此需要GNAT社区2020。 包含的算法 单个密码基元中的快速加密和身份验证 道格·惠廷（Doug Whiting），布鲁斯·施耐尔（Bruce Schneier），斯特凡·卢克斯（Stefan Lucks）和弗雷德里克·穆勒（FrédéricMuller） ECRYPT流密码项目报告2005 / 027，2005。 摘要：Phelix¹是具有内置MAC功能的高速流密码。 它在硬件和软件上都是高效的。 在当前的奔腾CPU上，Phelix的每数据包开销少于900个时钟，加上每字节的成本远低于每字节8个时钟，与最佳AES（仅加密）实现相比，即使对于小数据包，也非常有利。 ¹发音为“ felix”（与“ helix”成韵）。
【文件预览】：
Saatana-master
----artifacts()
--------gnatprove.out(19KB)
--------test_phelix.out(231KB)
----saatana.gpr(1KB)
----alire.toml(752B)
----.github()
--------scripts()
--------workflows()
----src()
--------saatana.ads(871B)
--------phelix()
--------saatana-crypto.adb(2KB)
--------saatana-crypto.ads(4KB)
----doc()
--------phelix()
----LICENSE(482B)
----README.md(2KB)
----SECURITY.md(436B)
----alire.lock(547B)
----tests()
--------phelix()
--------saatana-crypto-stream_tools.adb(2KB)
--------saatana-crypto-stream_tools.ads(1KB)
----.gitignore(7B)
----_config.yml(163B)
----rules()
--------restrictions.ads(903B)
--------coding-standards.txt(1KB)
----lemmas()
--------saatana-crypto-lemmas.ads(3KB)
----_build()
--------.gitignore(15B)