Protocol-Design
是否有正式的語言來定義加密協議？
我想從事一個個人項目，試圖找出加密協議中的缺陷。現在為了讓它正常工作，程序應該理解協議定義的語法（如果有的話）。所以我想知道是否有任何正式的語言來定義加密協議。
我找到了一篇論文，但我不知道是否每個人都真正遵循這一點。
**免責聲明：**我每天都使用 Coq…
關於工具
當您正在尋找形式驗證時，我建議您看一下Coq。儘管主要由學者使用，但它提供了一個邏輯框架和一個介面來編寫正式和互動式證明。
基於這種語言，存在一些專用於密碼證明的庫：
證明範例：
PHD：基於遊戲的密碼證明的正式認證
可以使用其他形式化工具（互動式證明者），例如Isabelle、Agda、Fstar和HOL。還有一些讀數：
正如 Mikeazo 所說，Cryptol可能是另一種可能性，但我不能說更多。
關於形式化
我也建議你看看 $ \pi $ -演算，主要用於探索並發程序的驗證，但可以應用於協議的情況。
因為這些證明中的大多數都是基於遊戲的，所以在這種情況下應用的概念之一是機率耦合。
一些有趣的讀物：
鑑於您項目的性質，我強烈建議您查看 David Basin 的作品，因為他們的軟體似乎可以完成您打算從事的工作（據我所知）。