Diffie-Hellman

使用 ProVerif 證明 TLS 握手的安全性

  • April 4, 2022

背景

對於我的論文，我正在研究一個需要 TLS 會話的應用程序協議。我希望實現完美前向保密，這意味著我選擇了短暫的 Diffie-Hellman 密碼套件。當我完成模型時，我打算偏愛橢圓曲線密碼學而不是正常 DHE。我希望這在我的模型中很容易互換。我發現了一個用 Pi 演算編寫的模型，它使用了 RSA，我已經適應了 DH。密切關注RFC 5246，我來到了下面的模型。

問題

不知何故，大部分似乎是死程式碼。我在死程式碼檢查失敗之前的行中添加了註釋。請幫助我了解出了什麼問題並導致 ProVerif 報告“無法證明”。

模型

(**************************************************************************
* DEFINITIONS                                                            *
**************************************************************************)

param verboseClauses = explained.
param traceDisplay = long.

(* A public channel *)
free net.

(* Message tags *)
free ClientHello, ClientKeyExchange, ClientCertificate, ServerHello, ServerCertificate, CertificateVerify, ServerKeyExchange.

(* Agent initialization is done over a private channel *)
private free initialClientData, initialServerData.

(* The cryptographic constructors *)
fun hash/1.     (* hashing *)
fun encrypt/2.  (* symmetric key encryption *)
fun pencrypt/2. (* Public key encryption *)
fun sign/2.     (* Public key signing *)
fun enc/1.      (* Extracts encryption key from a keypair *)
fun dec/1.      (* Extracts decryption key from a keypair *)

(* The cryptographic destructors *)
reduc decrypt(encrypt(x, y), y) = x.
reduc pdecrypt(pencrypt(x, enc(y)), dec(y)) = x.
reduc unsign(sign(x, enc(y)), dec(y)) = x.

(* A constructor that maps agents to their secret keypairs *)
private fun signkeypair/1.

(* Pseudo−random−number function *)
fun PRF/1.

(* Symmetric key construction *)
fun clientK/3.
fun serverK/3.

(* Certificates *)
private fun cert/2.

(* If cert(x, y) establishes x as owner of key y, y is returned *)
reduc verify(cert(x, y), x) = y.
   
(* Diffie-Hellman functions *)
fun f/2.
fun g/1.
equation f(x, g(y)) = f(y, g(x)).

(**************************************************************************
* QUERIES                                                                *
**************************************************************************)

(* secrecy Pre Master secret *)
query attacker: PMS.

(* secrecy Master secret *)
query attacker: MSa.
query attacker: MSb.

(* secrecy Finished message from the client *)
query attacker: FinishedAFlag.

(* secrecy Finished message from the server *)
query attacker: FinishedBFlag.

(* authenticity of the server *)
query evinj: endServerAuth(x, y, z) ==> evinj: beginServerAuth(x, y, z).

(* authenticity of the client *)
query evinj: endClientAuth(x, y, z) ==> evinj: beginClientAuth(x, y, z).

(* Dead code check *)
query attacker: clientFinished.
query attacker: serverFinished.

(**************************************************************************
* CLIENT PROCESS, this client is the initiator of the protocol.          *
**************************************************************************)
let client =
   (** Initial agent data from a trusted channel **)
   in(initialClientData, (A, keypair, clientCert));
   
   let SKc = enc(keypair) in
   let PKc = dec(keypair) in
       
   (** Replication to model arbitrary sessions **)
   !
   
   (** Get the server’s name, perhaps as user input **)
   in(net, B);
   
   (* A generates fresh nonce Na *)
   new Na;
   
   (* A determines Sid, session is randomly generated in basic model *)
   new Sid;
   
   (* A chooses options Pa, options are just random data for our model *)
   new Pa;
   
   (* A −> B : ClientHello *)
   let CH = (ClientHello, A, Na, Sid, Pa) in out(net, CH);
   
   (* B −> A : ServerHello *)
   in(net, SH); let (=ServerHello, Nb, =Sid, Pb) = SH in
   
   (* B −> A : ServerCertificate *)
   in(net, SC); let (=ServerCertificate, serverCert) = SC in
   
   (* Receiving Server DH Key Parameters and checking integrity *)
   in(net, SKE); let (=ServerKeyExchange, G, N, GY, DHSignature) = SKE in
   let unsignKey = verify(serverCert, B) in
   
   (** THE LINE BELOW CAUSES PROVERIF TO CLAIM "CANNOT BE PROVED" WHEN CHECKING DEAD CODE **)
   let (=Na, =Nb, =G, =N, =GY) = unsign(DHSignature, unsignKey) in
   
   (** dead code check **)
   new clientFinished; out(net, clientFinished);
   
   (* A −> B: ClientCertificate *)
   let CC = (ClientCertificate, clientCert) in out(net, CC);
   
   (* A −> B : ClientKeyExchange *)
   new X;
   let CKE = (ClientKeyExchange, g(X)) in out(net, CKE);
   
   let cvHash = hash((CH, SH, SC, SKE, CC, CKE)) in
   
   (** begin client authentication **)
   event beginClientAuth(A, B, cvHash);
   
   (* A −> B: CertificateVerify *)
   let CV = sign((CertificateVerify, cvHash), SKc) in out(net, CV);
   
   (* Compute the pre-master secret (g^xy) *)
   let PMS = f(GY, g(X)) in
   
   (* A calculates the Master secret M *)
   let M = PRF((PMS, Na, Nb)) in
   
   (* A calculates Finished *)
   let Finished = hash((CH, SH, SC, CC, CKE, CV, M)) in
   
   (* A −> B : Finished *)
   out(net, encrypt(Finished, clientK(Na, Nb, M)));
   
   (* B −> A : Finished *)
   in(net, FB);
   
   (* A verifies received finished *)
   let =Finished = decrypt(FB, serverK(Na, Nb, M)) in
   
   (** end server authentication **)
   event endServerAuth(A, B, PMS);
   
   (** secrecy check on the Master secret **)
   new MSa; out(M, MSa) |
   
   (** secrecy check on the Finished message **)
   new FinishedAFlag; out(Finished, FinishedAFlag).
   
(**************************************************************************
* THE SERVER PROCESS                                                     *
**************************************************************************)
let server =
   (** THE LINE BELOW CAUSES PROVERIF TO CLAIM "CANNOT BE PROVED" WHEN CHECKING DEAD CODE **)
   (** Initial agent data from a trusted channel **)
   in(initialServerData, (B, keypair, serverCert));
   
   (** dead code check **)
   new serverFinished; out(net, serverFinished);
   
   let PKs = dec(keypair) in
   let SKs = enc(keypair) in
   
   (** Replication to model arbitrary sessions **)
   !
   
   (* A −> B : ClientHello *)
   in(net, CH); let (=ClientHello, A, Na, Sid, Pa) = CH in
   
   (* B generates fresh nonce Nb *)
   new Nb;
   
   (* B chooses options Pb, just some random data in our model *)
   new Pb;
   
   (* B −> A : ServerHello *)
   let SH = (ServerHello, Nb, Sid, Pb) in out(net, SH);
   
   (* B −> A : ServerCertificate *)
   let SC = (ServerCertificate, serverCert) in out(net, SC);
   
   (* Generate Diffie-Hellman Key Exchange parameters *)
   new G; (* Generator, public *)
   new N; (* Modulus (prime), public *)
   new Y; (* Server's secret exponent *)
   
   (* B -> A: ServerKeyExchange *)
   let SKE = (ServerKeyExchange, G, N, g(Y), sign((Na, Nb, G, N, g(Y)), SKs)) in out(net, SKE);
   
   (* A −> B : ClientCertificate *)
   in(net, CC); let (=ClientCertificate, clientCert) = CC in
   
   (* A −> B : ClientKeyExchange *)
   in(net, CKE); let(=ClientKeyExchange, GX) = CKE in
   
   (* A −> B : CertificateVerify *)
   let unsignKey = verify(clientCert, A) in
   in(net, CV); let (=CertificateVerify, cvHash) = unsign(CV, unsignKey) in
   
   (* B verifies client signature *)
   let =cvHash = hash((CH, SH, SC, SKE, CC, CKE)) in
   
   (** end client authentication **)
   event endClientAuth(A, B, cvHash);
   
   (* Calculating the Pre-Master Secret *)
   let PMS = f(GX, g(Y)) in
   
   (* A −> B : Finished *)
   in(net, FA);
       
   (* B calculates M *)
   let M = PRF((PMS, Na, Nb)) in
   
   (* B calculates Finished *)
   let Finished = hash((CH, SH, SC, SKE, CC, CKE, CV, M)) in
   
   (** server authentication **)
   event beginServerAuth(A, B, PMS);
   
   (* B −> A : Finished *)
   out(net, encrypt(Finished, serverK(Na, Nb, M)));
   
   (* B verifies received Finished *)
   let =Finished = decrypt(FA, clientK(Na, Nb, M)) in
   
   (** secrecy check on the Master secret **)
   new MSb; out(M, MSb) |
   
   (** secrecy check on the finished **)
   new FinishedBFlag; out(Finished, FinishedBFlag).
   
(**************************************************************************
* THE INITIALIZER PROCESS                                                *
**************************************************************************)
let initializer =
   new C; (* Generate agent name *)
   new S; (* Generate agent name *)
   let clientKeyPair = signkeypair(C) in (* Generate client key *)
   let serverKeyPair = signkeypair(S) in (* Generate server key *)
   let clientCert = cert(C, dec(clientKeyPair)) in
   let serverCert = cert(S, dec(serverKeyPair)) in
   out(initialClientData, (C, clientKeyPair, clientCert));
   out(initialServerData, (S, serverKeyPair, serverCert));
   out(net, S).
   
(**************************************************************************
* THE SYSTEM                                                             *
**************************************************************************)
process
   !initializer | !client | !server

按照評論中的建議，我已將此問題發送到 ProVerif 郵件列表。我從布魯諾·布蘭切特那裡得到的答復如下。

實際上，ProVerif 並沒有說程式碼死了，它只是說它不能證明它沒有死。（它說“RESULT not attacker:serverFinished_96[...]無法證明”。）如果它說“ RESULT not attacker:serverFinished_96[...] is true.”，那麼程式碼肯定會死。

程式碼真的沒有死。ProVerif 無法證明此屬性的原因來自於 Horn 子句在協議的內部表示中所做的抽象。更準確地說，你有

let initializer =
   ...
   out(initialClientData, (C, clientKeyPair, clientCert));
   out(initialServerData, (S, serverKeyPair, serverCert));
   ...

let server =
   (** Initial agent data from a trusted channel **)
   in(initialServerData, (B, keypair, serverCert));
   (** dead code check **)
   new serverFinished; out(net, serverFinished);
   ...

let client =
   (** Initial agent data from a trusted channel **)
   in(initialClientData, (A, keypair, clientCert));
   ...

在 Horn 子句級別，ProVerif 設法輸出serverFinished，如下文所述：

  1. 消息(S_12356,signkeypair(S_12356),cert(S_12356,dec(signkeypair(S_12356))))可以initialServerData[]在輸出 {9} 的通道上發送。 mess:initialServerData[], (S_12356,signkeypair(S_12356),cert(S_12356,dec(signkeypair(S_12356)))).
  2. 可以在輸入 {53} 處接收可由 1(S_12356,signkeypair(S_12356),cert(S_12356,dec(signkeypair(S_12356))))在通道上發送的消息。initialServerData[]因此消息serverFinished_12357可能會在輸出 {55} 處發送給攻擊者。 attacker:serverFinished_12357.

ProVerif 認為它只需要執行初始化程序來發送消息initialServerData（上面的步驟 1），然後伺服器接收它以便輸出serverFinished（上面的步驟 2）。ProVerif 然後嘗試在 pi 演算級別重建軌跡。但是，要initialServerData在初始化程序中執行輸出，它首先需要在 上輸出一條消息initialClientData。由於initialClientData是私人頻道，因此需要輸入才能接收此消息。此輸入位於客戶端中。然而，它根本沒有出現在上面的 Horn 子句推導中。這就是跟踪重建失敗的原因，ProVerif 說它無法證明程式碼沒有死。

更一般地說，Horn 子句表示在存在私有通道的情況下引入了更多抽象，即使在相當簡單的情況下，有時也會導致跟踪重建失敗，例如上述情況。

在您的範例中，避免該問題的一種方法是重寫初始化程序過程，以便它並行而不是按順序執行最終輸出：

(out(initialClientData, (C, clientKeyPair, clientCert)) | out(initialServerData, (S, serverKeyPair, serverCert)) | out(net, S)).

引用自：https://crypto.stackexchange.com/questions/27389

相關問答

Diffie-Hellman

將 DH / DHE p & g 參數映射到組

  • November 8, 2022
檢視問答
Diffie-Hellman

是否有一種標準化的方法來評估密鑰交換算法的安全性？

  • March 18, 2022
檢視問答
Diffie-Hellman

為什麼 SSH 協議會生成兩個密鑰：客戶端到伺服器通信和伺服器到客戶端通信的加密密鑰？

  • March 8, 2022
檢視問答
Rsa

RSA 和 Diffie-Hellman 有什麼區別？

  • January 10, 2022
檢視問答
Public-Key

如何辨識 TLS 會話中使用的 ECDHE 組值

  • January 9, 2022
檢視問答
Authentication

安全證明，遊戲序列

  • December 20, 2021
檢視問答