问题标签 [cryptol]

我在 Dobb 博士 2008 年 12 月 29 日的电子邮件报告中看到，有一种用于设计加密系统的新 DSL（特定领域语言）。它被称为Cryptol，可从 Galois 获得。

有人看过吗？有人有使用它的计划吗？值得吗，你觉得呢？

罗伯特·甘布尔指出：

Cryptol 并不新鲜，它已经存在很多年了。新的是它（部分）对公众的可用性，它最初是为 NSA 开发和使用的。

就像布赖恩一样，我没有任何真正的理由使用 Cryptol。如果我需要（重新）验证我们拥有的基于 SSL 的实现，它可能会很有用，尽管我不确定它是否会有所帮助（我们不需要验证 SSL 库；我们可能需要验证我们的（错误）使用 SSL 库）。

我已经从源代码编译并安装了两个 cvc4。按照建议下载并安装了 Cvc4，并从其 git 存储库下载了 Cryptol。沙盒和安装完成且没有错误（使用 GHC 7.8.3 x86_64）。该问题仅在调用cryptol并发出:prove True. 这是一切：

对此的任何帮助都将是巨大的。对我来说，感觉就像找不到共享库。这会导致这个问题吗？谢谢你。

我尝试使用 Cryptol 实现 MAA 算法。这是我到目前为止所做的，但我并不幸运。有任何想法吗？

如何对不同宽度的值进行算术运算？在verilog中，将2位与8位异或没有问题，但cryptol抱怨：

我最初的问题：我想以 64 位值旋转字节，要移动的字节数取决于两位输入。我很难让这个工作：

在解释器中，我可以删除 s 的类型规范，然后它可以工作，但是我需要从文件中获取它，并且 s 实际上是一个 2 位值。

我已经是使用 Cryptol 方言的 Haskell 的新手，我也很恼火，因为我不能使用循环......我想实现这样的数组......初始化矩阵，但我唯一的想法是每 4 个从 [0] 索引开始的元素并将这个新列表加载到 S0。同样从列表的1 个索引开始，每 4 个元素加载到新的 S1 数组。

我目前正在开始一些关于 Cryptol 的工作，但对于 Cryptol，我需要 z3。Z3 甚至需要运行它。我已经从 gitHub 下载了最新的 Z3 版本，但我不确定如何安装/设置它以供 cryptol 使用。我在 Windows 10 电脑上。将不胜感激任何帮助。