[3/3] 话说我当初在博洛尼亚大学读硕的时候,密码学那门课是满分。我不但把整本教材全看完了,还在作为考试一部分的个人项目里仔细研究了 DES 加密算法和针对它的差分攻击(Differential Cryptanalysis),然后还用 Common Lisp 实现了整个算法和破解算法(但是只能攻击不完整的 DES)。我甚至给了这门课的教授一个小惊喜:我找到了 DES 设计者之一 Feistel 本人在 1973 年《科学美国人》上撰写的现代密码学科普文章。现在我要填补一个 HOL4 里面的小空白,形式化 DES(目前 HOL4 里面已有 AES 等算法的形式化)和它的一些主要性质。

Discussion
No replies yet.