密碼學中的形式驗證
我在某些地方看到人們使用形式驗證和/或電腦輔助驗證進行密碼學（ProVerif、CryptoVerif 等工具）。
這些方法如何運作？
**免責聲明：**我每天都使用Coq …
我在某些地方看到人們使用形式驗證和/或電腦輔助驗證進行密碼學。
據我所知，做這種事情的地方並不多。
首先，讓我們定義我們的概念：
形式驗證：使用形式化數學方法證明算法關於某個形式規範或屬性的正確性的行為。
電腦輔助證明：至少部分由電腦生成的證明。
一些例子（在密碼學中）：
- 加密原語的驗證：SHA-256（論文）
- 基於遊戲的密碼證明(PHD)的正式認證
還有一些閱讀：
- 通過抽象解釋對電腦系統的形式驗證進行簡要介紹（論文）
- 密碼學基礎證明框架(PHD)
- 密碼學中的電腦驗證（論文）
- 密碼實現的機率關係驗證（論文）
它是如何工作的？
在正式方法（無論是哪個領域）中，有兩種方法：
- 規格 $ \rightarrow $ 軟體
- 規格 $ \wedge $ 軟體 $ \rightarrow $ 證明軟體的正確性。
在大多數情況下，第一種方法是使用的方法。為什麼？因為從正式的規範開始，然後逐步通過經過驗證的步驟，最終獲得軟體（因此經過驗證）更容易。例如，這個經過認證的編譯器：
例如在方法 B中，過程如下： $$ DEFINE\ /\ SPECIFY \rightarrow PROVE \rightarrow REFINE \rightarrow PROVE \rightarrow \ldots \rightarrow IMPLEMENT $$
形式驗證使用Hoare 邏輯，這是一組允許我們對程序進行推理的規則。它基於連續演算和自然演繹。它依賴於 Hoare 三元組： $$ {P}\ C\ {Q} $$ 目前*提條件* $ {P} $ 滿足，執行命令 $ C $ 建立*後置條件* $ {Q} $ . 如果命令 $ C $ 從一個州出發 $ s $ 到一個狀態 $ s’ $ . $$ C: s \rightarrow s’ $$ 然後你必須證明： $$ \forall\ s\ s’, P[s] \implies C : s \rightarrow s’ \implies Q[s’] $$ 但我們更喜歡 Hoare 三重表示法（較輕）。
例如，這是規則 $ SKIP $ （又名什麼都不做）： $$ \frac{}{{P}\ SKIP\ {P}} $$
這是序列的規則： $$ \frac{{P}\ C_1\ {Q}\ \ \ \ \ \ \ {Q}\ C_2\ {R}}{{P}\ C_1 ; C_2\ {R}} $$ 這個符號讀作：“如果 $ {P}\ C_1\ {Q} $ （是 $ \text{True} $ ） 而如果 $ {Q}\ C_2\ {R} $ , 我可以推斷 $ {P}\ C_1 ; C_2\ {R} $ .
因此，一個證明是自下而上建構的：如果你想證明 $ {P}\ C_1 ; C_2\ {R} $ ，你需要證明有 $ Q $ 如 $ {P}\ C_1\ {Q} $ 和 $ {Q}\ C_2\ {R} $ .
霍爾邏輯的一些讀物：
- 霍爾邏輯背景閱讀（課程）
- 講義 C2：關於程式碼的推理（霍爾邏輯）（課程）
- 軟體基礎（自學課程，如果您想進入該領域，強烈推薦）。
工具
在形式化方法中，有兩種工具：
- 全自動證明者
- 證明助理
第一種主要基於SMT（可滿足性模理論），例如Atelier B和Alt-Ergo。
第二種是基於純邏輯的。您為其提供引理（幫助定理），這將確保您在證明中所做的每一步都是正確的。這是一個非常徹底的過程，非常緩慢。但最後你知道你的證明是如何工作的並且它是正確的，因為你沒有錯過任何假設。該過程可能令人沮喪，但將確保證明有效。主要的證明助手如下：Coq、 Isabelle、Agda、Fstar和HOL。
您提到的工具（ProVerif，CryptoVerif）不是專用於加密原語，而是協議驗證。我不認識他們，所以我不會評論。確實存在關於同一主題的其他工具。例如：
是的，它們基於 Coq。
在 C 中，為了能夠驗證您的程式碼是否符合您的規範（例如已經為 $ \text{SHA-}256 $ )，需要從程式碼中提取語義。這可以使用Verifiable Tool Chain或Why3來完成。第一個將為您提供一個 Coq 文件，您可以從該文件開始您的證明。第二個，給定C ASCL檢測程式碼，將使用frama-c並嘗試使用上面提到的 SMT 證明者證明屬性。如果失敗，它會生成目標並要求您使用 Coq 來證明它們。
在密碼學（和數學）
我已經提到了證明協議的想法（參見 EasyCrypt 等人），對於密碼證明，想法基本相同。使用邏輯屬性指定。
Coq 範例（對於本科生來說用手證明很簡單）： $$ \forall\ f g, f \text{ is injective} \implies g \text{ is injective} \implies g \circ f \text{ is injective} $$
Require Import Coq.Sets.Image. Theorem injective_trans: forall A B C (f: A -> B) (g:B -> C) (h:A -> C), (forall x, h x = g (f x)) -> injective A B f -> injective B C g -> injective A C h. Proof. intros A B C f g h H_h_equal_g_f H_f_injective H_g_injective. unfold injective in *. intros x y H_h_x_y. apply H_f_injective. apply H_g_injective. rewrite <- H_h_equal_g_f. rewrite <- H_h_equal_g_f. apply H_h_x_y. Qed.這是 Coq 中著名的已證明定理的列表。
最後的話
Keccak 的安全界限已在電腦的幫助下得到證明。但是他們的過程不同：他們詳盡地生成了軌跡並顯示了屬性。因此，它是電腦輔助的，但未經驗證。
最後，來自 FSE 2016 的最新論文：加密實現的可驗證側通道安全性：恆定時間 MEE-CBC
正如 SEJPM 所指出的，本文也是另一種方法（更多基於遊戲）。他們創建了一個分析器，可以生成滿足 AE 方案的密碼方案。但是，我不知道他們是否已經手動證明了他們的屬性或使用了證明助手（這可能是因為他們使用 Ocaml 來編寫他們的分析器）。
您可能還對Gilles Barthe（EasyCrypt 團隊）在這裡完成的課程感興趣。
我不知道我的回答是否有幫助。我知道它並不主要關注密碼學，但我希望它能讓您對事物的工作原理有所了解。
