我們最近推出了 Privacy Gateway，這是一種完全託管、可擴展且高效能的 Oblivious HTTP (OHTTP) 轉送。從概念上講，OHTTP 是一個簡單的通訊協定：端到端的加密請求和回應透過轉送裝置在用戶端和伺服器之間轉寄，將_傳送者_與_傳送內容_分離。這是一種常見的模式，Oblivious DoH 和 Apple Private Relay 等部署的技術證明了這一點。儘管如此，OHTTP 仍然是一個新通訊協定，作為一個新通訊協定，我們必須仔細進行分析。
為此，我們進行了由電腦輔助的正式安全性分析，以補充對該通訊協定正在進行的標準化過程和部署。在這篇文章中，我們更深入地描述了這一分析，更深入地挖掘了該通訊協定的加密細節以及我們為分析它而開發的模型。如果您已經熟悉 OHTTP 通訊協定，可請隨時跳到分析區段以深入瞭解。如果不太熟悉，則讓我們首先回顧一下 OHTTP 要實現的目標以及該通訊協定如何設計以實現這些目標。
將傳送者與傳送內容分離
OHTTP 是一種將公開金鑰加密與代理相結合，以將 HTTP 請求（和回應）的內容與 HTTP 請求的傳送者分開的通訊協定。在 OHTTP 中，用戶端產生加密請求並將其傳送到轉送裝置，該轉送裝置將它們轉寄到閘道伺服器，最後閘道解密訊息以處理請求。轉送裝置只能看到加密文字以及用戶端和閘道識別身分，閘道只能看到轉送裝置識別身分和純文字。
這樣，OHTTP 就是一個輕量級的應用程式層代理通訊協定。這意味著它代理應用程式訊息而不是網路層連線。這種區別很重要，所以要確保我們能理解這些差異。代理連線涉及通常建置在 HTTP CONNECT 上的一整套其他通訊協定。（也可以使用 VPN 和 WireGuard 等技術，包括 Cloudflare WARP，但我們著重關注 HTTP CONNECT 以進行比較。）
面向連線的代理描述
由於整個 TCP 連線本身都是代理的，因此面向連線的代理與使用 TCP 的所有應用程式相容。實際上，它們是支援任何類型的應用程式流量的一般目的代理通訊協定。與此相反，代理應用程式訊息與需要在用戶端和伺服器之間傳輸整個物件（訊息）的應用程式使用案例相容。
面向訊息的代理描述
範例包括 DNS 請求和回應，或者在 OHTTP 的情況下，則為 HTTP 請求和回應。換句話說，OHTTP 不是一個一般目的代理通訊協定：它有其用途，專用於用戶端和伺服器之間的交易式互動（例如應用程式級 API）。因此，相比之下，它要簡單得多。
應用程式使用 OHTTP 來確保請求不會連結到以下任一項：
用戶端識別資訊，包括 IP 位址、TLS 指紋等。作為代理通訊協定，這是一個基本要求。
來自同一用戶端的未來請求。這對於不跨請求攜帶狀態的應用程式而言是必需的。
這兩個屬性使 OHTTP 非常適合希望在不損害基本功能的情況下為使用者提供隱私的應用程式。一年多以來，它一直是 Oblivious DoH 廣泛部署的基礎，最近，它成為 Flo Health Inc. 匿名模式功能的基礎。
值得注意的是，這兩個屬性都可以透過面向連線的通訊協定來實現，但代價是用戶端想要傳輸的每條訊息都需要新的端到端 TLS 連線。對於參與該通訊協定的所有實體來說，這可能非常昂貴。
那麼 OHTTP 究竟是如何實現這些目標的？讓我們更深入地研究 OHTTP 以找出答案。
Oblivious HTTP 通訊協定設計
OHTTP 中的單個交易涉及以下步驟：
用戶端使用閘道伺服器的公開金鑰封裝 HTTP 請求，並透過 client<>relay HTTPS 連線將其傳送至轉送裝置。
轉送裝置透過其自己的 relay<>gateway HTTPS 連線將請求轉寄到伺服器。
閘道解封請求，將其轉寄到可以產生資源的目標伺服器。
閘道向轉送裝置傳回封裝的回應，然後後者將結果轉寄給用戶端。
請注意，在此交期中，轉送裝置只能看到用戶端和閘道身分識別（分別是用戶端 IP 位址和閘道 URL），但看不到任何應用程式資料。相反，閘道能看到應用程式資料和轉送裝置 IP 位址，但看不到用戶端 IP 位址。任何一方都無法窺見全貌，除非轉送裝置和閘道勾結，否則它會保持這種狀態。
上述交易中轉寄請求和回應的 HTTP 詳細資料在技術上並不有趣——訊息是使用 POST 透過 HTTPS 從傳送者處傳送給接收者的——所以我們將跳過此過程。令人著迷的部分是請求和回應封裝，它建立在 HPKE 之上，這是最近批准的混合公開金鑰加密標準。
讓我們從請求封裝開始，它是混合公開金鑰加密。用戶端首先將其 HTTP 請求轉換為二進位格式，稱為二進位 HTTP，如 RFC9292 所指定。顧名思義，二進位 HTTP 是一種用於對 HTTP 訊息進行編碼的二進位格式。此表示讓用戶端能夠將 HTTP 請求編碼為二進位編碼值，並讓閘道反轉此過程，從二進位編碼值恢復 HTTP 請求。二進位編碼是必需的，因為公開金鑰加密層需要二進位編碼的輸入。
在 HTTP 請求以二進位格式進行編碼後，它將被饋送到 HPKE 以產生加密訊息，然後用戶端將其傳送到轉送裝置以轉寄到閘道。閘道解密此訊息，將二進位編碼的請求轉換回其等效的 HTTP 請求，然後將其轉寄到目標伺服器進行處理。
來自閘道的回應以非常相似的方式封裝傳回用戶端。閘道先將回應編碼為等效的二進位 HTTP 訊息，使用只有用戶端和閘道知道的對稱金鑰對其進行加密，然後將其傳回給轉送裝置以轉寄給用戶端。用戶端解密並轉換此訊息以復原結果。
簡化的模型和安全性目標
在我們的正式分析中，我們想要確保 OHTTP 使用加密和代理實現上述所需的隱私目標。
為了推動分析，考慮以下簡化模型，其中存在兩個用戶端 C1 和 C2、一個轉送裝置 R 和一個閘道 G。OHTTP 假設攻擊者可以觀察所有網路活動且能夠自適應地入侵 R 或 G，但不能入侵 C1 或 C2。OHTTP 假設 R 和 G 不串通，因此我們假設 R 和 G 中只有一個遭到入侵。在入侵後，攻擊者就可以存取被入侵方的所有工作階段資訊和私密金鑰材料。攻擊者被禁止向閘道傳送用戶端識別資訊，例如 IP 位址。（這將允許攻擊者輕易地將查詢連結到相應的用戶端。）
在此模型中，C1 和 C2 分別透過 R 向 G 傳送 OHTTP 請求 Q1 和 Q2，G 提供答案 A1 和 A2。攻擊者的目標是分別將 C1 連結到 (Q1, A1)，將 C2 連結到 (Q2, A2)。如果無需任何其他互動即可實現此連結性，則攻擊者成功。OHTTP 會阻止這種連結性。簡單來說，這意味著：
只有擁有相應回應金鑰和 HPKE 金鑰材料的用戶端和閘道知道請求和回應的內容。
如果沒有每個用戶端唯一的金鑰，閘道無法區分從同一用戶端產生的兩個相同請求和從不同用戶端產生的兩個相同請求。
非正式地說，我們很清楚是 OHTTP 實現了這些屬性。但我們想正式證明這一點，這意味著如果完美實作，設計將具有這些屬性。這種類型的形式分析與形式驗證不同，在形式驗證中，您採用通訊協定設計並證明某些程式碼正確實作了該設計。雖然兩者都很有用，但它們是不同的過程，在這篇部落格文章中，我們將談論前者。但首先，讓我們給出一些形式分析的背景。
形式分析程式設計模型
在我們的設定中，形式分析涉及產生通訊協定的代數描述，然後使用數學證明該代數描述具有我們想要的屬性。最終結果證明，對於我們想要防禦的攻擊者，我們理想中的通訊協定代數版本是「安全的」，即具有所需的屬性。在我們的案例中，我們選擇使用名為 Tamarin 的工具對我們理想中的 OHTTP 代數版本進行建模，Tamarin 是一種以安全為中心的定理證明器和模型檢查器。Tamarin 是一種使用起來令人生畏的工具，但一旦您熟悉了它，就會有直觀的感覺。我們將在下面的 OHTTP 模型環境中分解 Tamarin 模型的各個部分。
通訊協定行為建模
Tamarin 使用一種稱為多重集重寫的技術來描述通訊協定。通訊協定描述由一系列「規則」組成，當滿足某些要求時，就可以「觸發」這些規則。每條規則代表通訊協定中的一個獨立步驟，當一條規則觸發時，意味著該步驟已被執行。例如，我們有一個規則表示閘道產生其長期公開封裝金鑰，並為通訊協定中的不同各方建立安全的 TLS 連線。這些規則幾乎可以隨時觸發，因為它們沒有任何要求。
產生 OHTTP 閘道金鑰的基本規則
Tamarin 將這些要求表示為「事實」。當正確的事實可用時，即會觸發規則。Tamarin 將所有可用的事實儲存在「袋」或多重集中。多重集與普通集相似，因為它以無序方式儲存物件的集合，但與普通集不同的是，它允許重複物件。這是「多重集重寫」的「多重集」部分。
重寫部分是指我們規則的輸出。當規則觸發時，它會從袋中取出一些可用的事實，並在完成後將一些新的事實插入袋中。這些新事實可能會滿足一些其他規則的要求，然後可以觸發這些規則，產生更多新事實，以此類推1。這樣，我們可以透過通訊協定來表示進度。使用輸入和輸出事實，我們可以描述我們用於纏身長期公開封裝金鑰的規則，它沒有要求，且會產生一個長期金鑰作為輸出，如下所示。
如果存在與規則的輸入事實匹配的輸出事實，則滿足規則要求。例如，在 OHTTP 中，用於產生請求的用戶端規則的一個要求是存在長期公開封裝金鑰。此匹配如下所示。
讓我們把其中一些片段放在一起，來展示 OHTTP 的一個非常小但具體的部分作為範例：用戶端產生其封裝的請求並將其傳送到轉送裝置。此步驟應為轉送裝置產生一條訊息，以及處理來自轉送裝置的最終回應所需的任何相應狀態。作為先決條件，用戶端需要 (1) 閘道公開金鑰和 (2) 到轉送裝置的 TLS 連線。如前所述，產生公開金鑰和 TLS 連線不需要任何輸入，因此隨時可以完成。
按時間對事件進行建模
除了耗用和產生新的事實之外，每個 Tamarin 規則還可能產生副作用，稱為「動作事實」。Tamarin 會記錄每次觸發規則時的動作事實。動作事實可能類似於「在時間 t 傳送了包含內容 m 的用戶端訊息」。有時規則只能按嚴格的順序觸發，因此我們可以將它們的動作事實放在固定的時間順序中。在其他時候，多個規則的先決條件可能同時滿足，因此我們無法將其動作事實放入嚴格的時間順序中。我們可以將這種部分有序含義的模式表示為有向非循環圖，簡稱 DAG。
總之，多重集重寫規則描述通訊協定的步驟，產生的 DAG 記錄與通訊協定描述關聯的動作。我們將動作的 DAG 稱為動作圖表。如果我們的工作完成得不錯，就可以遵循這些規則，並產生通訊協定允許的訊息或動作的所有可能組合，以及它們相應的動作圖表。
作為動作圖表的範例，我們可以考慮一下當用戶端成功完成通訊協定時會發生什麼。當滿足此規則的要求時，規則觸發，標示用戶端已完成且回應有效。由於通訊協定是在此時完成的，因此不會產生輸出事實。
終端用戶端回應處理常式規則的動作圖表
對攻擊者進行建模
動作圖表是推理通訊協定安全屬性的核心。我們可以檢查圖表中的各種屬性，例如「轉送裝置執行的第一個動作是否發生在用戶端執行的第一個動作之後？」。我們的規則允許同時多次執行通訊協定。這是非常強大的。我們可以查看一個圖表，並詢問「這裡是否發生了可能破壞通訊協定安全屬性的糟糕事情？」
特別是，我們可以透過查詢此圖表或透過判斷與之相關的各種屬性來證明（安全性和正確性）屬性。例如，我們可以說「對於通訊協定的所有執行，如果用戶端完成通訊協定並且可以解密來自閘道的回應，則回應肯定是由具有相應共用金鑰的實體產生和加密。」
這是一個有用的聲明，但它並沒有說太多關於安全性的事情。例如，如果閘道私密金鑰被洩露，會發生什麼？為了證明安全屬性，我們需要定義我們的威脅模型，其中包括對手及其能力。在 Tamarin 中，我們將威脅模型編碼為通訊協定模型的一部分。例如，當我們定義從用戶端傳遞到轉送裝置的訊息時，我們可以新增一個特殊規則，允許攻擊者在訊息經過時讀取它。這使我們能夠描述諸如「對於我們語言中通訊協定的所有執行，攻擊者永遠不會知曉祕密金鑰」之類的屬性。
對於安全性通訊協定，我們通常賦予攻擊者讀取、修改、捨棄和重播任何訊息的能力。這有時被描述為「攻擊者控製網路」，或 Dolev-Yao 攻擊者。然而，攻擊者有時也可以入侵通訊協定中的不同實體，瞭解與該實體關聯的狀態。這有時被稱為擴展的 Dolev-Yao 攻擊者，這正是我們在模型中考慮的攻擊者類型。
回到我們的模型，我們使攻擊者能夠根據需要透過不同的規則入侵長期金鑰對和 TLS 工作階段。這些設定了各種動作事實，標誌著發生入侵的事實。
金鑰洩露規則的動作圖表
將所有內容放在一起，我們就有了一種對通訊協定行為、攻擊者能力和安全屬性進行建模的方法。現在讓我們深入剖析我們如何套用這些來證明 OHTTP 的安全性。
OHTTP Tamarin 模型
在我們的模型中，我們使攻擊者能夠入侵伺服器的長期金鑰以及用戶端和轉送裝置之間的金鑰。針對這個攻擊者，我們旨在證明上述兩個非正式聲明：
只有擁有相應回應金鑰和 HPKE 金鑰材料的用戶端和閘道知道請求和回應的內容。
如果沒有每個用戶端唯一的金鑰，閘道無法區分從同一用戶端產生的兩個請求和從不同用戶端產生的兩個請求。
為了正式證明這些，我們以不同的方式表達它們。首先，我們斷言通訊協定實際上已完成。這是一個重要的步驟，因為如果您的模型中有一個錯誤，通訊協定甚至無法按預期執行，那麼 Tamarin 可能會說它是「安全的」，因為沒有什麼不好的事情發生。
對於核心安全屬性，我們將期望的目標轉譯為有關模型的問題。這樣，形式分析只能為我們提供所詢問之問題的證明（或反駁！），而不是我們應該提出的問題，因此這種轉譯依賴於經驗和專業知識。我們將針對下面要問的每個問題分解此轉譯，從閘道驗證開始。
閘道驗證除非攻擊者入侵了閘道的長期金鑰，否則如果用戶端完成通訊協定並能夠解密閘道的回應，那麼它就知道：回應者是它打算使用的閘道，閘道衍生了相同的金鑰， 閘道看到了用戶端傳送的請求，且用戶端收到的回應是閘道傳送的回應。
這告訴我們通訊協定確實有效，並且按原樣傳送和接收了訊息。驗證的一個方面可能是參與者就某些資料達成一致，因此儘管此通訊協定看起來像一堆屬性混雜在一起，但它們都是一個驗證屬性的一部分。
接下來，我們需要證明請求和回應是保密的。有多種方法可能破壞保密性，例如，如果加密或解密金鑰被洩露。我們透過證明以下屬性來做到這一點。
請求和回應都是保密的，即攻擊者永遠不會知曉它們，除非攻擊者入侵了閘道的長期金鑰。
從某種意義上說，請求和回應保密涵蓋了閘道是惡意的情況，因為如果閘道是惡意的，那麼「攻擊者」就知道閘道的長期金鑰。
用戶端和轉送裝置的連線內容是祕密的，除非攻擊者入侵了轉送裝置。
如果用戶端遭到入侵，我們不必擔心連線的保密性，因為在這種情況下，攻擊者甚至在查詢傳送之前就已經知曉其內容，並且可以透過自己進行真實查詢來獲得回應。如果您的用戶端遭到入侵，那麼遊戲就結束了。
如果閘道向用戶端傳送一條訊息，並且攻擊者發現了使用相同金鑰和隨機數加密的另一條訊息，則表示攻擊者已經入侵了閘道，或者他們已經知道查詢。
在轉譯中，此屬性意味著回應加密是正確的並且不易受到攻擊，例如透過 AEAD 隨機數重用。這對 OHTTP 來說顯然是一場災難，所以我們仔細檢查，確保這種情況永遠不會發生，尤其是我們已經在 ODoH 中偵測到這個問題。
最後，也許也是最重要的一點，我們希望證明攻擊者無法將特定查詢連結到用戶端。我們證明了一個略有不同的屬性，該屬性有效地證明，除非轉送裝置和閘道串通，否則攻擊者無法將加密查詢與其解密查詢連結到一起。尤其是，我們證明了以下內容：
如果攻擊者知道查詢和傳送到轉送裝置的連線內容（即加密查詢），那麼它一定已經入侵了閘道和轉送裝置。
這通常不能證明不可區分性。攻擊者可以使用兩種技術來連結兩個查詢：直接推理和統計分析。由於匿名三難困境，我們知道我們無法防禦統計分析，因此我們必須宣佈它超出範圍並繼續前進。為了防止直接推理，我們需要確保攻擊者不會入侵用戶端，或者同時入侵轉送裝置和閘道，從而直接連結查詢。那麼，我們可以做些什麼來進行防範？值得慶幸的是，我們可以做一件事。我們可以確保惡意閘道無法識別單個用戶端傳送了兩條訊息。我們透過不保留連線之間的任何狀態來證明這一點。如果傳回用戶端的行為方式與新用戶端完全相同，並且在請求之間不攜帶任何狀態，則惡意閘道無需分析任何內容。
就是這樣！如果您想親自嘗試證明其中一些屬性，我們的模型和證明以及我們的 ODoH 模型和證據都可以在 GitHub 上找到。Tamarin 證明器也是免費提供的，因此您可以仔細檢查我們的所有工作。希望這篇文章能讓您瞭解，當我們說我們已經證明通訊協定安全時，這意味著什麼，同時也能激勵您自行嘗試。如果您想從事這樣的偉大專案，請查看我們的招聘頁面。
1根據模型的不同，此過程可能導致搜尋空間呈指數級爆炸，從而無法自動證明任何事情。此外，如果新的輸出事實不滿足任何剩餘規則的要求，則程序將懸置。