From 3e8c40e17750ec96fa5b6eb94d6b118d75bcd5b7 Mon Sep 17 00:00:00 2001 From: MM45 Date: Tue, 5 May 2026 13:13:43 +0200 Subject: [PATCH] Import `Distr`, remove aux file --- proof/security/DigitalSignatures.eca | 1526 ++++++++-------- proof/security/DigitalSignaturesROM.eca | 2 +- proof/security/HashThenSignAux.eca | 2154 ----------------------- 3 files changed, 764 insertions(+), 2918 deletions(-) delete mode 100644 proof/security/HashThenSignAux.eca diff --git a/proof/security/DigitalSignatures.eca b/proof/security/DigitalSignatures.eca index 99a84f24..6f296b5e 100644 --- a/proof/security/DigitalSignatures.eca +++ b/proof/security/DigitalSignatures.eca @@ -4,7 +4,7 @@ (* - "A Digital Signature Scheme Secure Against Adaptive *) (* Chosen-Message Attack" *) (* DOI: 10.1137/0217017 *) -(* - "Digital Signatures" *) +(* - "Digital Signatures" *) (* DOI: 10.1007/978-0-387-27712-7. *) (**************************************************************************) @@ -12,7 +12,7 @@ (* --- Require/Import Theories --- *) (* -- Built-in (i.e, standard library) -- *) -require import AllCore List. +require import AllCore List Distr. @@ -28,15 +28,15 @@ type sk_t. (* -- Oracles -- *) -(* +(* Default implementation of the shared functionality, comprised of checking for freshness and computing the number of queries, shared by all oracles throughout *) module O_Base_Default = { var qs : msg_t list - (* + (* Check whether given message m is fresh, i.e., whether m is not contained in - the list of oracle queries qs + the list of oracle queries qs *) proc fresh(m : msg_t) : bool = { return ! m \in qs; @@ -59,8 +59,8 @@ theory Stateless. proc sign(sk : sk_t, m : msg_t) : sig_t proc verify(pk : pk_t, m : msg_t, s : sig_t) : bool }. - - + + (* -- Correctness -- *) (* Probabilistic program formalizing the correctness of stateless signature schemes *) module Correctness(S : Scheme) = { @@ -69,59 +69,59 @@ theory Stateless. var sk : sk_t; var sig : sig_t; var is_valid : bool; - + (pk, sk) <@ S.keygen(); sig <@ S.sign(sk, m); - is_valid <@ S.verify(pk, m, sig); - + is_valid <@ S.verify(pk, m, sig); + return is_valid; } }. - - + + (* - -- + -- Key-Only Attack (KOA). Attacks in which the adversary is only given the public/verification key - -- + -- *) (* - - - UnBreakability under Key-Only Attack (UB-KOA). + - + UnBreakability under Key-Only Attack (UB-KOA). Given the public/verification key, the adversary is tasked with computing the corresponding secret key - *) (* Class of adversaries against UB-KOA *) module type Adv_UBKOA = { - proc break(pk : pk_t) : sk_t + proc break(pk : pk_t) : sk_t }. - + (* UB-KOA game *) module UB_KOA(S : Scheme, A : Adv_UBKOA) = { proc main() : bool = { var pk : pk_t; var sk, sk' : sk_t; var sig : sig_t; - + (* Generate a key pair using the considered signature scheme *) (pk, sk) <@ S.keygen(); - - (* Ask adversary to compute the secret key sk given the public key pk *) + + (* Ask adversary to compute the secret key sk given the public key pk *) sk' <@ A.break(pk); - + (* Success iff the adversary correctly computed the secret key *) return sk' = sk; } }. - - - (* - - + + + (* + - Universal UnForgeability under Key-Only Attack (UUF-KOA). - Given the public/verification key and an arbitrary message, the adversary is tasked + Given the public/verification key and an arbitrary message, the adversary is tasked with forging a signature for the given message - - + - *) abstract theory UUFKOA. (* (Proper) distribution over type of to-be-signed artifacts ('messages') *) @@ -150,9 +150,9 @@ theory Stateless. (* Ask the adversary to forge a signature for m given the public key pk (and m) *) sig <@ A.forge(pk, m); - (* - Verify (w.r.t. message m) the signature sig provided by the adversary - using the verification algorithm of the considered signature scheme + (* + Verify (w.r.t. message m) the signature sig provided by the adversary + using the verification algorithm of the considered signature scheme *) is_valid <@ S.verify(pk, m, sig); @@ -161,9 +161,9 @@ theory Stateless. } }. end UUFKOA. - + (* - - + - Selective UnForgeability under Key-Only Attack (SUF-KOA). After picking a message, the adversary is given the public/verification key and tasked with forging a signature for the picked message @@ -172,7 +172,7 @@ theory Stateless. (* Class of adversaries SUF-KOA *) module type Adv_SUFKOA = { proc pick() : msg_t - proc forge(pk : pk_t) : sig_t + proc forge(pk : pk_t) : sig_t }. (* SUF-KOA game *) @@ -190,15 +190,15 @@ theory Stateless. (* Generate a key pair using the considered signature scheme *) (pk, sk) <@ S.keygen(); - (* + (* Ask the adversary to forge a signature for the previously picked message m given the public key pk *) sig <@ A.forge(pk); - (* - Verify (w.r.t. message m) the signature sig provided by the adversary - using the verification algorithm of the considered signature scheme + (* + Verify (w.r.t. message m) the signature sig provided by the adversary + using the verification algorithm of the considered signature scheme *) is_valid <@ S.verify(pk, m, sig); @@ -207,7 +207,7 @@ theory Stateless. } }. - + (* - Existential UnForgeability under Key-Only Attack (EUF-KOA). @@ -217,7 +217,7 @@ theory Stateless. *) (* Class of adversaries against EUF-KOA *) module type Adv_EUFKOA = { - proc forge(pk : pk_t) : msg_t * sig_t + proc forge(pk : pk_t) : msg_t * sig_t }. (* EUF-KOA game *) @@ -232,15 +232,15 @@ theory Stateless. (* Generate a key pair using the considered signature scheme *) (pk, sk) <@ S.keygen(); - (* + (* Ask adversary to forge a signature on any message (and provide both the - message and the signature) given the public key pk + message and the signature) given the public key pk *) (m, sig) <@ A.forge(pk); - (* - Verify (w.r.t. message m) the signature sig provided by the adversary - using the verification algorithm of the considered signature scheme + (* + Verify (w.r.t. message m) the signature sig provided by the adversary + using the verification algorithm of the considered signature scheme *) is_valid <@ S.verify(pk, m, sig); @@ -250,18 +250,18 @@ theory Stateless. }. - (* - -- + (* + -- Random-Message Attack (RMA). - Attacks in which the adversary is given the public/verification key as well as + Attacks in which the adversary is given the public/verification key as well as the signatures for a set of random messages *known* to it, but not *chosen* by it - -- - *) - (* - - - UnBreakability under Random-Message Attack (UB-RMA). - Given the public/verification key and the signatures for a set of known random messages, - the adversary is tasked with computing the secret key corresponding to the + -- + *) + (* + - + UnBreakability under Random-Message Attack (UB-RMA). + Given the public/verification key and the signatures for a set of known random messages, + the adversary is tasked with computing the secret key corresponding to the public/verification key - *) @@ -274,7 +274,7 @@ theory Stateless. (* Class of adversaries against UB-RMA *) module type Adv_UBRMA = { - proc break(pk : pk_t, msigl : (msg_t * sig_t) list) : sk_t + proc break(pk : pk_t, msigl : (msg_t * sig_t) list) : sk_t }. (* UB-RMA game *) @@ -290,10 +290,10 @@ theory Stateless. (* Generate a key pair using the considered signature scheme *) (pk, sk) <@ S.keygen(); - (* + (* Construct a list of n_ubrma (message, signature) pairs. To this end, for each pair, randomly sample a message and, subsequently, create - (with the previously generated secret key) a corresponding signature by + (with the previously generated secret key) a corresponding signature by using the signing algorithm of the considered signature scheme. *) msigl <- []; @@ -306,10 +306,10 @@ theory Stateless. msigl <- rcons msigl msig; } - (* + (* Ask adversary to compute the secret key sk given the public key pk and list of (message, signature) pairs msigl - *) + *) sk' <@ A.break(pk, msigl); (* Success iff the adversary correctly computed the secret key sk *) @@ -317,13 +317,13 @@ theory Stateless. } }. end UBRMA. - - - (* - - + + + (* + - Universal UnForgeability under Random-Message Attack (UUF-RMA). - Given the public/verification key, the signatures for a set of known random messages, - and an arbitrary message, the adversary is tasked with forging a signature for + Given the public/verification key, the signatures for a set of known random messages, + and an arbitrary message, the adversary is tasked with forging a signature for the given (latter) message - *) @@ -356,10 +356,10 @@ theory Stateless. (* Generate a key pair using the considered signature scheme *) (pk, sk) <@ S.keygen(); - (* + (* Construct a list of n_uufrma (message, signature) pairs. To this end, for each pair, randomly sample a message and, subsequently, create - (with the previously generated secret key) a corresponding signature by + (with the previously generated secret key) a corresponding signature by using the signing algorithm of the considered signature scheme. *) msigl <- []; @@ -372,27 +372,27 @@ theory Stateless. msigl <- rcons msigl msig; } - (* + (* Ask the adversary to forge a signature for m' given the public key pk, a list of (message, signature) pairs msigl, and m' *) sig' <@ A.forge(pk, msigl, m'); - (* - Verify (w.r.t. message m') the signature sig' provided by the adversary - using the verification algorithm of the considered signature scheme + (* + Verify (w.r.t. message m') the signature sig' provided by the adversary + using the verification algorithm of the considered signature scheme *) is_valid <@ S.verify(pk, m', sig'); - (* - Check whether message for which the adversary forged a signature is fresh - (i.e., check whether message is not included in the set of messages for which + (* + Check whether message for which the adversary forged a signature is fresh + (i.e., check whether message is not included in the set of messages for which the adversary received signatures) *) is_fresh <- ! m' \in (map fst msigl); - (* - Success iff + (* + Success iff (1) "is_valid": the forged signature provided by the adversary is valid, and (2) "is_fresh": the message for which the adversary forged a signature is fresh. *) @@ -405,7 +405,7 @@ theory Stateless. (* - Selective UnForgeability under Random-Message Attack (SUF-RMA). - After picking a message, the adversary is given the public/verification key, + After picking a message, the adversary is given the public/verification key, the signatures for a set of known random messages, and an arbitrary message, and is tasked with forging a signature for the picked message - @@ -440,10 +440,10 @@ theory Stateless. (* Generate a key pair using the considered signature scheme *) (pk, sk) <@ S.keygen(); - (* + (* Construct a list of n_sufrma (message, signature) pairs. To this end, for each pair, randomly sample a message and, subsequently, create - (with the previously generated secret key) a corresponding signature by + (with the previously generated secret key) a corresponding signature by using the signing algorithm of the considered signature scheme. *) msigl <- []; @@ -456,27 +456,27 @@ theory Stateless. msigl <- rcons msigl msig; } - (* - Ask the adversary to forge a signature for m' given the public key pk and + (* + Ask the adversary to forge a signature for m' given the public key pk and a list of (message, signature) pairs msigl *) sig' <@ A.forge(pk, msigl); - (* - Verify (w.r.t. message m') the signature sig' provided by the adversary - using the verification algorithm of the considered signature scheme + (* + Verify (w.r.t. message m') the signature sig' provided by the adversary + using the verification algorithm of the considered signature scheme *) is_valid <@ S.verify(pk, m', sig'); - (* - Check whether message for which the adversary forged a signature is fresh - (i.e., check whether message is not included in the set of messages for which + (* + Check whether message for which the adversary forged a signature is fresh + (i.e., check whether message is not included in the set of messages for which the adversary received signatures) *) is_fresh <- ! m' \in (map fst msigl); - (* - Success iff + (* + Success iff (1) "is_valid": the forged signature provided by the adversary is valid, and (2) "is_fresh": the message for which the adversary forged a signature is fresh. *) @@ -484,8 +484,8 @@ theory Stateless. } }. end SUFRMA. - - + + (* - Existential UnForgeability under Random-Message Attack (EUF-RMA) @@ -506,7 +506,7 @@ theory Stateless. }. (* EUF-RMA game *) - module EUF_RMA(S : Scheme, A : Adv_EUFRMA) = { + module EUF_RMA(S : Scheme, A : Adv_EUFRMA) = { proc main() : bool = { var pk : pk_t; var sk : sk_t; @@ -519,10 +519,10 @@ theory Stateless. (* Generate a key pair using the considered signature scheme *) (pk, sk) <@ S.keygen(); - (* + (* Construct a list of n_eufrma (message, signature) pairs. To this end, for each pair, randomly sample a message and, subsequently, create - (with the previously generated secret key) a corresponding signature by + (with the previously generated secret key) a corresponding signature by using the signing algorithm of the considered signature scheme. *) msigl <- []; @@ -535,47 +535,47 @@ theory Stateless. msigl <- rcons msigl msig; } - (* + (* Ask the adversary to forge a signature for any message (and provide both the - message and signature) given the public key pk and a list of (message, signature) + message and signature) given the public key pk and a list of (message, signature) pairs msigl *) (m', sig') <@ A.forge(pk, msigl); - (* - Verify (w.r.t. message m') the signature sig' provided by the adversary - using the verification algorithm of the considered signature scheme + (* + Verify (w.r.t. message m') the signature sig' provided by the adversary + using the verification algorithm of the considered signature scheme *) is_valid <@ S.verify(pk, m', sig'); - (* - Check whether message for which the adversary forged a signature is fresh - (i.e., check whether message is not included in the set of messages for which + (* + Check whether message for which the adversary forged a signature is fresh + (i.e., check whether message is not included in the set of messages for which the adversary received signatures) *) is_fresh <- ! m' \in (map fst msigl); - (* - Success iff + (* + Success iff (1) "is_valid": the forged signature provided by the adversary is valid, and (2) "is_fresh": the message for which the adversary forged a signature is fresh. *) return is_valid /\ is_fresh; } }. - - + + (* - Interactive Existential UnForgeability under Random-Message Attack (I-EUF-RMA) Given the public/verification key and the signatures for a set of random messages - (obtained one-by-one upon request), the adversary is tasked with forging a signature + (obtained one-by-one upon request), the adversary is tasked with forging a signature for any fresh message - *) - (* - Type for signing oracles used in I-EUF-RMA, including procedures - for initialization and auxiliary tasks + (* + Type for signing oracles used in I-EUF-RMA, including procedures + for initialization and auxiliary tasks *) module type Oracle_RMA(S : Scheme) = { proc init(sk_init : sk_t) : unit @@ -583,54 +583,54 @@ theory Stateless. proc fresh(m : msg_t) : bool proc nr_queries() : int }. - - (* - Type for signing oracles used in I-EUF-RMA, only exposing the - procedure for signing + + (* + Type for signing oracles used in I-EUF-RMA, only exposing the + procedure for signing *) module type SOracle_RMA = { proc sign() : msg_t * sig_t }. - - (* - Default implementation of a signing oracle used in I-EUF-RMA, including procedures - for initialization and auxiliary tasks + + (* + Default implementation of a signing oracle used in I-EUF-RMA, including procedures + for initialization and auxiliary tasks *) module (O_RMA_Default : Oracle_RMA) (S : Scheme) = { include var O_Base_Default var sk : sk_t - + (* Initialize secret/signing key and oracle query list qs *) proc init(sk_init : sk_t) : unit = { sk <- sk_init; qs <- []; } - - (* + + (* Sign given message m using the considered signature scheme with the secret/signing key sk and append m to the list of oracle queries qs *) proc sign() : msg_t * sig_t = { var sig : sig_t; var m : msg_t; - + m <$ dmsg; - + sig <@ S.sign(sk, m); - + qs <- rcons qs m; - + return (m, sig); } }. - + (* Class of adversaries against I-EUF-RMA *) module type Adv_I_EUFRMA(O : SOracle_RMA) = { proc forge(pk : pk_t) : msg_t * sig_t }. - + (* I-EUF-RMA game *) - module I_EUF_RMA(S : Scheme, A : Adv_I_EUFRMA, O: Oracle_RMA) = { + module I_EUF_RMA(S : Scheme, A : Adv_I_EUFRMA, O: Oracle_RMA) = { proc main() : bool = { var pk : pk_t; var sk : sk_t; @@ -639,46 +639,46 @@ theory Stateless. var msig : msg_t * sig_t; var nrqs : int; var is_valid, is_fresh : bool; - + (* Generate a key pair using the considered signature scheme *) (pk, sk) <@ S.keygen(); - + (* Initialize oracle *) O(S).init(sk); - - (* + + (* Ask the adversary to forge a signature for any message (and provide both the - message and signature) given the public key pk and a list of (message, signature) + message and signature) given the public key pk and a list of (message, signature) pairs, the latter of which is provided one-by-one upon request *) (m', sig') <@ A(O(S)).forge(pk); - - (* - Verify (w.r.t. message m') the signature sig' provided by the adversary - using the verification algorithm of the considered signature scheme + + (* + Verify (w.r.t. message m') the signature sig' provided by the adversary + using the verification algorithm of the considered signature scheme *) is_valid <@ S.verify(pk, m', sig'); - - (* Check that message was not one of the messages sampled by the signing oracle. *) + + (* Check that message was not one of the messages sampled by the signing oracle. *) is_fresh <@ O(S).fresh(m'); - - (* Get the total number of oracle queries that the adversary made *) + + (* Get the total number of oracle queries that the adversary made *) nrqs <@ O(S).nr_queries(); - - (* + + (* Success iff (1) "nrqs <= n_eufrma": the adversary made at most n_eufrma oracle queries, and (2) "is_valid": the forged signature provided by the adversary is valid, and (3) "is_fresh": the message for which the adversary forged a signature is fresh. *) - return nrqs <= n_eufrma /\ is_valid /\ is_fresh; + return nrqs <= n_eufrma /\ is_valid /\ is_fresh; } }. end EUFRMA. - + (* - -- + -- Generic Chosen-Message Attack (GCMA). Attacks in which the adversary is given the public/verification key as well as the signatures for a set of *chosen* messages. Here, all messages are chosen @@ -686,12 +686,12 @@ theory Stateless. (2) independently of the public key; that is, without knowing the public key at the time of choosing the messages -- - *) - (* - - - UnBreakability under Generic Chosen-Message Attack (UB-GCMA). + *) + (* + - + UnBreakability under Generic Chosen-Message Attack (UB-GCMA). Given the public/verification key and the signatures for a set of messages chosen - non-adaptively and indepedently of the public key, the adversary is tasked with + non-adaptively and indepedently of the public key, the adversary is tasked with computing the secret key corresponding to the public/verification key - *) @@ -702,7 +702,7 @@ theory Stateless. (* Class of adversaries against UB-CMA *) module type Adv_UBGCMA = { proc choose() : msg_t list - proc break(pk : pk_t, sigl : sig_t list) : sk_t + proc break(pk : pk_t, sigl : sig_t list) : sk_t }. (* UB-GCMA game *) @@ -721,7 +721,7 @@ theory Stateless. (* Generate a key pair using the considered signature scheme *) (pk, sk) <@ S.keygen(); - (* + (* Construct a list sigl of at most n_ubgcma signatures. Here, the i-th signature is a signature for the i-th message in the list ml previously provided by the adversary. Naturally, the signatures are created using the signing algorithm @@ -738,11 +738,11 @@ theory Stateless. sigl <- rcons sigl sig; } - (* + (* Ask adversary to compute the secret key sk given the public key pk and a list of signatures sigl for the messages previously chosen by the adversary - (i.e., the messages in list ml) - *) + (i.e., the messages in list ml) + *) sk' <@ A.break(pk, sigl); (* Success iff the adversary correctly computed the secret key sk *) @@ -750,20 +750,20 @@ theory Stateless. } }. end UBGCMA. - - + + (* - Universal UnForgeability under Generic Chosen-Message Attack (UUF-GCMA). Given the public/verification key, the signatures for a set of messages chosen - non-adaptively and indepedently of the public key, and an arbitrary message, + non-adaptively and indepedently of the public key, and an arbitrary message, the adversary is tasked with forging a signature for the given (latter) message - *) abstract theory UUFGCMA. (* (Proper) distribution over type of to-be-signed artifacts ('messages') *) op [lossless] dmsg : msg_t distr. - + (* Number of messages the adversary obtains signatures for in UUF-GCMA game *) const n_uufgcma : { int | 0 <= n_uufgcma } as ge0_nuufgcma. @@ -784,7 +784,7 @@ theory Stateless. var sigl : sig_t list; var is_valid, is_fresh : bool; - (* Sample message for which the adversary must forge a signature *) + (* Sample message for which the adversary must forge a signature *) m' <$ dmsg; (* Ask adversary to choose a list of messages for which to receive signatures *) @@ -793,7 +793,7 @@ theory Stateless. (* Generate a key pair using the considered signature scheme *) (pk, sk) <@ S.keygen(); - (* + (* Construct a list sigl of at most n_uufgcma signatures. Here, the i-th signature is a signature for the i-th message in the list ml previously provided by the adversary. Naturally, the signatures are created using the signing algorithm @@ -811,26 +811,26 @@ theory Stateless. } (* - Ask the adversary to forge a signature for message m' given the public key pk + Ask the adversary to forge a signature for message m' given the public key pk and a list of signatures sigl for the messages previously chosen by the adversary - (i.e., the messages in list ml) + (i.e., the messages in list ml) *) sig' <@ A.forge(pk, sigl, m'); - (* - Verify (w.r.t. message m') the signature sig' provided by the adversary - using the verification algorithm of the considered signature scheme + (* + Verify (w.r.t. message m') the signature sig' provided by the adversary + using the verification algorithm of the considered signature scheme *) is_valid <@ S.verify(pk, m', sig'); - (* - Check whether message for which the adversary forged a signature is fresh - (i.e., check whether message is not included in the set of messages for which + (* + Check whether message for which the adversary forged a signature is fresh + (i.e., check whether message is not included in the set of messages for which the adversary received signatures) *) is_fresh <- ! m' \in (take (size sigl) ml); - (* + (* Success iff (1) "is_valid": the forged signature provided by the adversary is valid, and (2) "is_fresh": the message for which the adversary forged a signature is fresh. @@ -840,12 +840,12 @@ theory Stateless. }. end UUFGCMA. - - (* - - + + (* + - Selective UnForgeability under Generic Chosen-Message Attack (SUF-GCMA). After picking a message, the adversary is given the public/verification key and - the signatures for a set of messages chosen non-adaptively and indepedently + the signatures for a set of messages chosen non-adaptively and indepedently of the public key, and is tasked with forging a signature for the picked message - *) @@ -880,7 +880,7 @@ theory Stateless. (* Generate a key pair using the considered signature scheme *) (pk, sk) <@ S.keygen(); - (* + (* Construct a list sigl of at most n_sufgcma signatures. Here, the i-th signature is a signature for the i-th message in the list ml previously provided by the adversary. Naturally, the signatures are created using the signing algorithm @@ -898,41 +898,41 @@ theory Stateless. } (* - Ask the adversary to forge a signature for the previously picked message m' - given the public key pk and a list of signatures sigl for the messages - previously chosen by the adversary (i.e., the messages in list ml) + Ask the adversary to forge a signature for the previously picked message m' + given the public key pk and a list of signatures sigl for the messages + previously chosen by the adversary (i.e., the messages in list ml) *) sig' <@ A.forge(pk, sigl); - (* - Verify (w.r.t. message m') the signature sig' provided by the adversary - using the verification algorithm of the considered signature scheme + (* + Verify (w.r.t. message m') the signature sig' provided by the adversary + using the verification algorithm of the considered signature scheme *) is_valid <@ S.verify(pk, m', sig'); - (* - Check whether message for which the adversary forged a signature is fresh - (i.e., check whether message is not included in the set of messages for which + (* + Check whether message for which the adversary forged a signature is fresh + (i.e., check whether message is not included in the set of messages for which the adversary received signatures) *) is_fresh <- ! m' \in (take (size sigl) ml); - (* + (* Success iff (1) "is_valid": the forged signature provided by the adversary is valid, and (2) "is_fresh": the message for which the adversary forged a signature is fresh. *) - return is_valid /\ is_fresh; + return is_valid /\ is_fresh; } }. end SUFGCMA. - - + + (* - Existential UnForgeability under Generic Chosen-Message Attack (EUF-GCMA) - Given the public/verification key and the signatures for a set of messages - chosen non-adaptively and indepedently of the public key, the adversary is tasked + Given the public/verification key and the signatures for a set of messages + chosen non-adaptively and indepedently of the public key, the adversary is tasked with forging a signature for any fresh message - *) @@ -947,7 +947,7 @@ theory Stateless. }. (* EUF-GCMA game *) - module EUF_GCMA(S : Scheme, A : Adv_EUFGCMA) = { + module EUF_GCMA(S : Scheme, A : Adv_EUFGCMA) = { proc main() : bool = { var pk : pk_t; var sk : sk_t; @@ -955,7 +955,7 @@ theory Stateless. var ml : msg_t list; var sigl : sig_t list; var sig, sig': sig_t; - var is_valid, is_fresh : bool; + var is_valid, is_fresh : bool; (* Ask adversary to choose a list of messages for which to receive signatures *) ml <@ A.choose(); @@ -963,7 +963,7 @@ theory Stateless. (* Generate a key pair using the considered signature scheme *) (pk, sk) <@ S.keygen(); - (* + (* Construct a list sigl of at most n_eufgcma signatures. Here, the i-th signature is a signature for the i-th message in the list ml previously provided by the adversary. Naturally, the signatures are created using the signing algorithm @@ -982,38 +982,38 @@ theory Stateless. (* Ask the adversary to forge a signature for the any message (and provide both - the message and the signature) given the public key pk and a list of - signatures sigl for the messages previously chosen by the adversary - (i.e., the messages in list ml) + the message and the signature) given the public key pk and a list of + signatures sigl for the messages previously chosen by the adversary + (i.e., the messages in list ml) *) (m', sig') <@ A.forge(pk, sigl); - (* - Verify (w.r.t. message m') the signature sig' provided by the adversary - using the verification algorithm of the considered signature scheme + (* + Verify (w.r.t. message m') the signature sig' provided by the adversary + using the verification algorithm of the considered signature scheme *) is_valid <@ S.verify(pk, m', sig'); - (* - Check whether message for which the adversary forged a signature is fresh - (i.e., check whether message is not included in the set of messages for which + (* + Check whether message for which the adversary forged a signature is fresh + (i.e., check whether message is not included in the set of messages for which the adversary received signatures) *) is_fresh <- ! m' \in (take (size sigl) ml); - (* + (* Success iff (1) "is_valid": the forged signature provided by the adversary is valid, and (2) "is_fresh": the message for which the adversary forged a signature is fresh. *) - return is_valid /\ is_fresh; - } + return is_valid /\ is_fresh; + } }. end EUFGCMA. - - + + (* - -- + -- Non-Adaptive Chosen-Message Attack (NACMA)/Directed Chosen-Message Attack (DCMA). Attacks in which the adversary is given the public/verification key as well as the signatures for a set of *chosen* messages. Here, all messages are chosen @@ -1021,12 +1021,12 @@ theory Stateless. messages may depend on the public key; i.e., the adversary is given the public key when asked to provide the messages -- - *) - (* - - - UnBreakability under Non-Adaptive Chosen-Message Attack (UB-NACMA). + *) + (* + - + UnBreakability under Non-Adaptive Chosen-Message Attack (UB-NACMA). Given the public/verification key and the signatures for a set of non-adaptively - chosen messages, the adversary is tasked with computing the secret key + chosen messages, the adversary is tasked with computing the secret key corresponding to the public/verification key - *) @@ -1037,7 +1037,7 @@ theory Stateless. (* Class of adversaries against UB-NACMA *) module type Adv_UBNACMA = { proc choose(pk : pk_t) : msg_t list - proc break(sigl : sig_t list) : sk_t + proc break(sigl : sig_t list) : sk_t }. (* UB-NACMA game *) @@ -1053,13 +1053,13 @@ theory Stateless. (* Generate a key pair using the considered signature scheme *) (pk, sk) <@ S.keygen(); - (* + (* Ask adversary to choose a list of messages for which to receive signatures - given the public key pk + given the public key pk *) ml <@ A.choose(pk); - (* + (* Construct a list sigl of at most n_ubnacma signatures. Here, the i-th signature is a signature for the i-th message in the list ml previously provided by the adversary. Naturally, the signatures are created using the signing algorithm @@ -1076,11 +1076,11 @@ theory Stateless. sigl <- rcons sigl sig; } - (* + (* Ask adversary to compute the secret key sk given the public key pk (in the - call to A.choose(pk)) and a list of signatures sigl for the messages previously - chosen by the adversary (i.e., the messages in list ml) - *) + call to A.choose(pk)) and a list of signatures sigl for the messages previously + chosen by the adversary (i.e., the messages in list ml) + *) sk' <@ A.break(sigl); (* Success iff the adversary correctly computed the secret key sk *) @@ -1088,20 +1088,20 @@ theory Stateless. } }. end UBNACMA. - - + + (* - - + - Universal UnForgeability under Non-Adaptive Chosen-Message Attack (UUF-NACMA). Given the public/verification key, the signatures for a set of non-adaptively - chosen messages, and an arbitrary message, the adversary is tasked with forging + chosen messages, and an arbitrary message, the adversary is tasked with forging a signature for the given (latter) message - *) abstract theory UUFNACMA. (* (Proper) distribution over type of to-be-signed artifacts ('messages') *) op [lossless] dmsg : msg_t distr. - + (* Number of messages the adversary obtains signatures for in UUF-RMA game *) const n_uufnacma : { int | 0 <= n_uufnacma } as ge0_nuufnacma. @@ -1122,19 +1122,19 @@ theory Stateless. var sigl : sig_t list; var is_valid, is_fresh : bool; - (* Sample message for which the adversary must forge a signature *) + (* Sample message for which the adversary must forge a signature *) m' <$ dmsg; (* Generate a key pair using the considered signature scheme *) (pk, sk) <@ S.keygen(); - (* + (* Ask adversary to choose a list of messages for which to receive signatures - given the public key pk + given the public key pk *) ml <@ A.choose(pk); - (* + (* Construct a list sigl of at most n_uufnacma signatures. Here, the i-th signature is a signature for the i-th message in the list ml previously provided by the adversary. Naturally, the signatures are created using the signing algorithm @@ -1153,25 +1153,25 @@ theory Stateless. (* Ask the adversary to forge a signature for message m' given the public key pk - (in the call to A.choose(pk)) and a list of signatures sigl for the messages - previously chosen by the adversary (i.e., the messages in list ml) + (in the call to A.choose(pk)) and a list of signatures sigl for the messages + previously chosen by the adversary (i.e., the messages in list ml) *) sig' <@ A.forge(sigl, m'); - (* - Verify (w.r.t. message m') the signature sig' provided by the adversary - using the verification algorithm of the considered signature scheme + (* + Verify (w.r.t. message m') the signature sig' provided by the adversary + using the verification algorithm of the considered signature scheme *) is_valid <@ S.verify(pk, m', sig'); - (* - Check whether message for which the adversary forged a signature is fresh - (i.e., check whether message is not included in the set of messages for which + (* + Check whether message for which the adversary forged a signature is fresh + (i.e., check whether message is not included in the set of messages for which the adversary received signatures) *) is_fresh <- ! m' \in (take (size sigl) ml); - (* + (* Success iff (1) "is_valid": the forged signature provided by the adversary is valid, and (2) "is_fresh": the message for which the adversary forged a signature is fresh. @@ -1181,12 +1181,12 @@ theory Stateless. }. end UUFNACMA. - - (* - - + + (* + - Selective UnForgeability under Non-Adaptive Chosen-Message Attack (SUF-NACMA). After picking a message, the adversary is given the public/verification key and - the signatures for a set of non-adaptively chosen messages, and is tasked with + the signatures for a set of non-adaptively chosen messages, and is tasked with forging a signature for the picked message - *) @@ -1221,19 +1221,19 @@ theory Stateless. (* Generate a key pair using the considered signature scheme *) (pk, sk) <@ S.keygen(); - (* + (* Ask adversary to choose a list of messages for which to receive signatures - given the public key pk + given the public key pk *) ml <@ A.choose(pk); - (* + (* Construct a list sigl of at most n_sufnacma signatures. Here, the i-th signature is a signature for the i-th message in the list ml previously provided by the adversary. Naturally, the signatures are created using the signing algorithm of the considered signature scheme with the previously generated secret key. Note that, in case the adversary provided less than n_sufnacma messages in ml, the - resulting list of signatures will have the same size as ml + resulting list of signatures will have the same size as ml (and, hence, less than n_sufnacma). *) sigl <- []; @@ -1247,25 +1247,25 @@ theory Stateless. (* Ask the adversary to forge a signature for message m' given the public key pk - (in the call to A.choose(pk)) and a list of signatures sigl for the messages - previously chosen by the adversary (i.e., the messages in list ml) + (in the call to A.choose(pk)) and a list of signatures sigl for the messages + previously chosen by the adversary (i.e., the messages in list ml) *) sig' <@ A.forge(sigl); - (* - Verify (w.r.t. message m') the signature sig' provided by the adversary - using the verification algorithm of the considered signature scheme + (* + Verify (w.r.t. message m') the signature sig' provided by the adversary + using the verification algorithm of the considered signature scheme *) is_valid <@ S.verify(pk, m', sig'); - (* - Check whether message for which the adversary forged a signature is fresh - (i.e., check whether message is not included in the set of messages for which + (* + Check whether message for which the adversary forged a signature is fresh + (i.e., check whether message is not included in the set of messages for which the adversary received signatures) *) is_fresh <- ! m' \in (take (size sigl) ml); - (* + (* Success iff (1) "is_valid": the forged signature provided by the adversary is valid, and (2) "is_fresh": the message for which the adversary forged a signature is fresh. @@ -1274,8 +1274,8 @@ theory Stateless. } }. end SUFNACMA. - - + + (* - Existential UnForgeability under Non-Adaptive Chosen-Message Attack (EUF-NACMA). @@ -1294,7 +1294,7 @@ theory Stateless. }. (* EUF-NACMA game *) - module EUF_NACMA(S : Scheme, A : Adv_EUFNACMA) = { + module EUF_NACMA(S : Scheme, A : Adv_EUFNACMA) = { proc main() : bool = { var pk : pk_t; var sk : sk_t; @@ -1302,18 +1302,18 @@ theory Stateless. var ml : msg_t list; var sigl : sig_t list; var sig, sig': sig_t; - var is_valid, is_fresh : bool; + var is_valid, is_fresh : bool; (* Generate a key pair using the considered signature scheme *) (pk, sk) <@ S.keygen(); - (* + (* Ask adversary to choose a list of messages for which to receive signatures - given the public key pk + given the public key pk *) ml <@ A.choose(pk); - (* + (* Construct a list sigl of at most n_eufnacma signatures. Here, the i-th signature is a signature for the i-th message in the list ml previously provided by the adversary. Naturally, the signatures are created using the signing algorithm @@ -1333,50 +1333,50 @@ theory Stateless. (* Ask the adversary to forge a signature for the any message (and provide both the message and the signature) given the public key pk (in the call to A.choose(pk)) - and a list of signatures sigl for the messages previously chosen by the adversary - (i.e., the messages in list ml) + and a list of signatures sigl for the messages previously chosen by the adversary + (i.e., the messages in list ml) *) (m', sig') <@ A.forge(sigl); - (* - Verify (w.r.t. message m') the signature sig' provided by the adversary - using the verification algorithm of the considered signature scheme + (* + Verify (w.r.t. message m') the signature sig' provided by the adversary + using the verification algorithm of the considered signature scheme *) is_valid <@ S.verify(pk, m', sig'); - (* - Check whether message for which the adversary forged a signature is fresh - (i.e., check whether message is not included in the set of messages for which + (* + Check whether message for which the adversary forged a signature is fresh + (i.e., check whether message is not included in the set of messages for which the adversary received signatures) *) is_fresh <- ! m' \in (take (size sigl) ml); - (* + (* Success iff (1) "is_valid": the forged signature provided by the adversary is valid, and (2) "is_fresh": the message for which the adversary forged a signature is fresh. *) - return is_valid /\ is_fresh; - } + return is_valid /\ is_fresh; + } }. end EUFNACMA. - + (* - -- + -- (Adaptive) Chosen-Message Attack (CMA). Attacks in which the adversary is given the public/verification key as well as the signatures for a set of *chosen* messages. Here, all messages are chosen - adaptively and may depend on the public key; that is, the adversary - (1) immediately receives a signature for a chosen message before choosing the + adaptively and may depend on the public key; that is, the adversary + (1) immediately receives a signature for a chosen message before choosing the subsequent message, and (2) is given the public key when asked to provide the messages. -- *) (* - General - *) - (* - Type for signing oracles used in (adaptive) CMA games, including procedures - for initialization and auxiliary tasks + (* + Type for signing oracles used in (adaptive) CMA games, including procedures + for initialization and auxiliary tasks *) module type Oracle_CMA(S : Scheme) = { proc init(sk_init : sk_t) : unit @@ -1385,49 +1385,49 @@ theory Stateless. proc nr_queries() : int }. - (* - Type for signing oracles used in (adaptive) CMA games, only exposing the - procedure for signing + (* + Type for signing oracles used in (adaptive) CMA games, only exposing the + procedure for signing *) module type SOracle_CMA = { proc sign(m : msg_t) : sig_t }. - - (* - Default implementation of a signing oracle including procedures for - initialization and auxiliary tasks + + (* + Default implementation of a signing oracle including procedures for + initialization and auxiliary tasks *) module (O_CMA_Default : Oracle_CMA) (S : Scheme) = { include var O_Base_Default var sk : sk_t - + (* Initialize secret/signing key and oracle query list qs *) proc init(sk_init : sk_t) : unit = { sk <- sk_init; qs <- []; } - (* + (* Sign given message m using the considered signature scheme with the secret/signing key sk and append m to the list of oracle queries qs *) proc sign(m : msg_t) : sig_t = { var sig : sig_t; - + sig <@ S.sign(sk, m); qs <- rcons qs m; - + return sig; } }. - - (* - - - UnBreakability under (Adaptive) Chosen-Message Attack (UB-CMA). + + (* + - + UnBreakability under (Adaptive) Chosen-Message Attack (UB-CMA). Given the public/verification key and the signatures for a set of adaptively - chosen messages, the adversary is tasked with computing the secret key + chosen messages, the adversary is tasked with computing the secret key corresponding to the public/verification key - *) @@ -1435,36 +1435,36 @@ theory Stateless. module type Adv_UBCMA(O : SOracle_CMA) = { proc break(pk : pk_t) : sk_t }. - + (* UB-CMA game *) module UB_CMA(S : Scheme, A : Adv_UBCMA, O : Oracle_CMA) = { proc main() : bool = { var pk : pk_t; var sk, sk' : sk_t; - + (* Generate a key pair using the considered signature scheme *) (pk, sk) <@ S.keygen(); - + (* Initialize the signing oracle with the generated secret key *) O(S).init(sk); - (* + (* Ask adversary to compute the secret key sk given the public key pk and access to a signing oracle that it can query an unlimited number of times - *) + *) sk' <@ A(O(S)).break(pk); - + (* Success iff the adversary correctly computed the secret key sk. *) - return sk' = sk; + return sk' = sk; } }. - - + + (* - - + - Universal UnForgeability under (Adaptive) Chosen-Message Attack (UUF-CMA) Given the public/verification key, the signatures for a set of adaptively - chosen messages, and an arbitrary message, the adversary is tasked with forging + chosen messages, and an arbitrary message, the adversary is tasked with forging a signature for the given (latter) message - *) @@ -1486,7 +1486,7 @@ theory Stateless. var sig : sig_t; var is_valid, is_fresh : bool; - (* Sample message for which the adversary must forge a signature *) + (* Sample message for which the adversary must forge a signature *) m <$ dmsg; (* Generate a key pair using the considered signature scheme *) @@ -1496,40 +1496,40 @@ theory Stateless. O(S).init(sk); (* - Ask the adversary to forge a signature for message m given the public key pk + Ask the adversary to forge a signature for message m given the public key pk and and access to a signing oracle that it can query an unlimited number of times *) sig <@ A(O(S)).forge(pk, m); - (* - Verify (w.r.t. message m) the signature sig provided by the adversary - using the verification algorithm of the considered signature scheme + (* + Verify (w.r.t. message m) the signature sig provided by the adversary + using the verification algorithm of the considered signature scheme *) is_valid <@ S.verify(pk, m, sig); - (* - Check whether message for which the adversary forged a signature is fresh - (i.e., check whether message is not included in the list of messages for which + (* + Check whether message for which the adversary forged a signature is fresh + (i.e., check whether message is not included in the list of messages for which the adversary received signatures through an oracle query) *) is_fresh <@ O(S).fresh(m); - (* + (* Success iff (1) "is_valid": the forged signature provided by the adversary is valid, and (2) "is_fresh": the message for which the adversary forged a signature is fresh. *) - return is_valid /\ is_fresh; + return is_valid /\ is_fresh; } }. end UUFCMA. - + (* - Selective UnForgeability under Chosen-Message Attack (SUF-CMA). - After picking a message, the adversary is given the public/verification key - and the signatures for a set of adaptively chosen messages, and is tasked with + After picking a message, the adversary is given the public/verification key + and the signatures for a set of adaptively chosen messages, and is tasked with forging a signature for the picked message - *) @@ -1538,7 +1538,7 @@ theory Stateless. proc pick() : msg_t proc forge(pk : pk_t) : sig_t }. - + (* SUF-CMA game *) module SUF_CMA(S : Scheme, A : Adv_SUFCMA, O : Oracle_CMA) = { proc main() : bool = { @@ -1547,49 +1547,49 @@ theory Stateless. var m : msg_t; var sig : sig_t; var is_valid, is_fresh : bool; - - (* Ask the adversary to pick a message to forge a signature for *) + + (* Ask the adversary to pick a message to forge a signature for *) m <@ A(O(S)).pick(); - + (* Generate a key pair using the considered signature scheme *) (pk, sk) <@ S.keygen(); - + (* Initialize the signing oracle with the generated secret key *) O(S).init(sk); (* - Ask the adversary to forge a signature for message m given the public key pk + Ask the adversary to forge a signature for message m given the public key pk and and access to a signing oracle that it can query an unlimited number of times *) sig <@ A(O(S)).forge(pk); - (* - Verify (w.r.t. message m) the signature sig provided by the adversary - using the verification algorithm of the considered signature scheme + (* + Verify (w.r.t. message m) the signature sig provided by the adversary + using the verification algorithm of the considered signature scheme *) is_valid <@ S.verify(pk, m, sig); - - (* - Check whether message for which the adversary forged a signature is fresh - (i.e., check whether message is not included in the list of messages for which + + (* + Check whether message for which the adversary forged a signature is fresh + (i.e., check whether message is not included in the list of messages for which the adversary received signatures through an oracle query) *) is_fresh <@ O(S).fresh(m); - - (* + + (* Success iff (1) "is_valid": the forged signature provided by the adversary is valid, and (2) "is_fresh": the message for which the adversary forged a signature is fresh. *) - return is_valid /\ is_fresh; + return is_valid /\ is_fresh; } }. - + (* - Existential UnForgeability under Chosen-Message Attack (EUF-CMA) - Given the public/verification key and the signatures for a set of adaptively + Given the public/verification key and the signatures for a set of adaptively chosen messages, the adversary is tasked with forging a signature for any fresh message - *) @@ -1606,53 +1606,53 @@ theory Stateless. var m : msg_t; var sig : sig_t; var is_valid, is_fresh : bool; - + (* Generate a key pair using the considered signature scheme *) (pk, sk) <@ S.keygen(); - + (* Initialize the signing oracle with the generated secret key *) O(S).init(sk); (* Ask the adversary to forge a signature for any message (and provide both the - message and the signature) given the public key pk and access to a signing oracle + message and the signature) given the public key pk and access to a signing oracle that it can query an unlimited number of times *) (m, sig) <@ A(O(S)).forge(pk); - (* - Verify (w.r.t. message m) the signature sig provided by the adversary - using the verification algorithm of the considered signature scheme + (* + Verify (w.r.t. message m) the signature sig provided by the adversary + using the verification algorithm of the considered signature scheme *) is_valid <@ S.verify(pk, m, sig); - - (* - Check whether message for which the adversary forged a signature is fresh - (i.e., check whether message is not included in the list of messages for which + + (* + Check whether message for which the adversary forged a signature is fresh + (i.e., check whether message is not included in the list of messages for which the adversary received signatures through an oracle query) *) is_fresh <@ O(S).fresh(m); - - (* + + (* Success iff (1) "is_valid": the forged signature provided by the adversary is valid, and (2) "is_fresh": the message for which the adversary forged a signature is fresh. *) - return is_valid /\ is_fresh; + return is_valid /\ is_fresh; } }. - + (* - - + - Strong Existential UnForgeability under Chosen-Message Attack (SEUF-CMA). - Given the public/verification key and the signatures for a set of adaptively + Given the public/verification key and the signatures for a set of adaptively chosen messages, the adversary is tasked with forging a fresh signature for any message - *) - (* - Type for signing oracles used in the SEUF-CMA game, including procedures - for initialization and auxiliary tasks + (* + Type for signing oracles used in the SEUF-CMA game, including procedures + for initialization and auxiliary tasks *) module type Oracle_SEUFCMA(S : Scheme) = { proc init(sk_init : sk_t) : unit @@ -1661,52 +1661,52 @@ theory Stateless. proc nr_queries() : int }. - (* - Type for signing oracles used in the SEUF-CMA game, only exposing the - procedure for signing + (* + Type for signing oracles used in the SEUF-CMA game, only exposing the + procedure for signing *) module type SOracle_SEUFCMA = { proc sign(m : msg_t) : sig_t }. - - (* - Default implementation of a signing oracle including procedures for - initialization and auxiliary tasks + + (* + Default implementation of a signing oracle including procedures for + initialization and auxiliary tasks *) module (O_SEUFCMA_Default : Oracle_SEUFCMA) (S : Scheme) = { var sk : sk_t var qs : (msg_t * sig_t) list - + (* Initialize secret/signing key and oracle query list qs *) proc init(sk_init : sk_t) : unit = { sk <- sk_init; qs <- []; } - (* + (* Sign given message m using the considered signature scheme with the secret/signing key sk and append m to the list of oracle queries qs *) proc sign(m : msg_t) : sig_t = { var sig : sig_t; var msig : msg_t * sig_t; - + sig <@ S.sign(sk, m); msig <- (m, sig); qs <- rcons qs msig; - + return sig; } - (* + (* Check whether given (message, signature) pair msig is fresh, i.e., whether this pair - is not contained in the list of oracle queries qs + is not contained in the list of oracle queries qs *) proc fresh(msig : msg_t * sig_t) : bool = { return ! msig \in qs; } - + (* Get the number of oracle queries, i.e., the size of the oracle query list qs *) proc nr_queries() : int = { return size qs; @@ -1726,39 +1726,39 @@ theory Stateless. var m : msg_t; var sig : sig_t; var is_valid, is_fresh : bool; - + (* Generate a key pair using the considered signature scheme *) (pk, sk) <@ S.keygen(); - + (* Initialize the signing oracle with the generated secret key *) O(S).init(sk); (* Ask the adversary to forge a signature for any message (and provide both the - message and the signature) given the public key pk and access to a signing oracle + message and the signature) given the public key pk and access to a signing oracle that it can query an unlimited number of times *) (m, sig) <@ A(O(S)).forge(pk); - (* - Verify (w.r.t. message m) the signature sig provided by the adversary - using the verification algorithm of the considered signature scheme + (* + Verify (w.r.t. message m) the signature sig provided by the adversary + using the verification algorithm of the considered signature scheme *) is_valid <@ S.verify(pk, m, sig); - - (* + + (* Check whether (message, signature) pair (m, sig) returned by the adversary is fresh (i.e., check whether this pair is not included in the list of (message, signature) pairs of the signing oracle) *) is_fresh <@ O(S).fresh((m, sig)); - - (* + + (* Success iff (1) "is_valid": the forged signature provided by the adversary is valid, and (2) "is_fresh": the (message, signature) pair provided by the adversary is fresh. *) - return is_valid /\ is_fresh; + return is_valid /\ is_fresh; } }. end Stateless. @@ -1774,13 +1774,13 @@ theory KeyUpdating. proc sign(sk : sk_t, m : msg_t) : sig_t * sk_t proc verify(pk : pk_t, m : msg_t, sig : sig_t) : bool }. - - + + (* -- Correctness -- *) abstract theory Correctness. (* Maximum number of signatures for which the scheme should be correct *) const n_corr : { int | 0 <= n_corr } as ge0_ncorr. - + (* Probabilistic program formalizing the correctness of key-updating signature schemes *) module Correctness(S : Scheme) = { proc main(ml : msg_t list) : bool = { @@ -1790,17 +1790,17 @@ theory KeyUpdating. var sig : sig_t; var i : int; var is_valid, are_valid : bool; - + (pk, sk) <@ S.keygen(); i <- 0; are_valid <- true; while (i < min (size ml) n_corr) { m <- nth witness ml i; - + (sig, sk) <@ S.sign(sk, m); is_valid <@ S.verify(pk, m, sig); - + are_valid <- are_valid /\ is_valid; i <- i + 1; } @@ -1810,50 +1810,50 @@ theory KeyUpdating. }. end Correctness. - + (* - -- + -- Key-Only Attack (KOA). Attacks in which the adversary is only given the public/verification key - -- + -- *) (* - - - UnBreakability under Key-Only Attack (UB-KOA). + - + UnBreakability under Key-Only Attack (UB-KOA). Given the public/verification key, the adversary is tasked with computing the corresponding secret key - *) (* Class of adversaries against UB-KOA *) module type Adv_UBKOA = { - proc break(pk : pk_t) : sk_t + proc break(pk : pk_t) : sk_t }. - + (* UB-KOA game *) module UB_KOA(S : Scheme, A : Adv_UBKOA) = { proc main() : bool = { var pk : pk_t; var sk, sk' : sk_t; var sig : sig_t; - + (* Generate a key pair using the considered signature scheme *) (pk, sk) <@ S.keygen(); - - (* Ask adversary to compute the secret key sk given the public key pk *) + + (* Ask adversary to compute the secret key sk given the public key pk *) sk' <@ A.break(pk); - + (* Success iff the adversary correctly computed the secret key *) return sk' = sk; } }. - - - (* - - + + + (* + - Universal UnForgeability under Key-Only Attack (UUF-KOA). - Given the public/verification key and an arbitrary message, the adversary is tasked + Given the public/verification key and an arbitrary message, the adversary is tasked with forging a signature for the given message - - + - *) abstract theory UUFKOA. (* (Proper) distribution over type of to-be-signed artifacts ('messages') *) @@ -1882,9 +1882,9 @@ theory KeyUpdating. (* Ask the adversary to forge a signature for m given the public key pk (and m) *) sig <@ A.forge(pk, m); - (* - Verify (w.r.t. message m) the signature sig provided by the adversary - using the verification algorithm of the considered signature scheme + (* + Verify (w.r.t. message m) the signature sig provided by the adversary + using the verification algorithm of the considered signature scheme *) is_valid <@ S.verify(pk, m, sig); @@ -1893,9 +1893,9 @@ theory KeyUpdating. } }. end UUFKOA. - + (* - - + - Selective UnForgeability under Key-Only Attack (SUF-KOA). After picking a message, the adversary is given the public/verification key and tasked with forging a signature for the picked message @@ -1904,7 +1904,7 @@ theory KeyUpdating. (* Class of adversaries SUF-KOA *) module type Adv_SUFKOA = { proc pick() : msg_t - proc forge(pk : pk_t) : sig_t + proc forge(pk : pk_t) : sig_t }. (* SUF-KOA game *) @@ -1922,15 +1922,15 @@ theory KeyUpdating. (* Generate a key pair using the considered signature scheme *) (pk, sk) <@ S.keygen(); - (* + (* Ask the adversary to forge a signature for the previously picked message m given the public key pk *) sig <@ A.forge(pk); - (* - Verify (w.r.t. message m) the signature sig provided by the adversary - using the verification algorithm of the considered signature scheme + (* + Verify (w.r.t. message m) the signature sig provided by the adversary + using the verification algorithm of the considered signature scheme *) is_valid <@ S.verify(pk, m, sig); @@ -1939,7 +1939,7 @@ theory KeyUpdating. } }. - + (* - Existential UnForgeability under Key-Only Attack (EUF-KOA). @@ -1949,7 +1949,7 @@ theory KeyUpdating. *) (* Class of adversaries against EUF-KOA *) module type Adv_EUFKOA = { - proc forge(pk : pk_t) : msg_t * sig_t + proc forge(pk : pk_t) : msg_t * sig_t }. (* EUF-KOA game *) @@ -1964,15 +1964,15 @@ theory KeyUpdating. (* Generate a key pair using the considered signature scheme *) (pk, sk) <@ S.keygen(); - (* + (* Ask adversary to forge a signature on any message (and provide both the - message and the signature) given the public key pk + message and the signature) given the public key pk *) (m, sig) <@ A.forge(pk); - (* - Verify (w.r.t. message m) the signature sig provided by the adversary - using the verification algorithm of the considered signature scheme + (* + Verify (w.r.t. message m) the signature sig provided by the adversary + using the verification algorithm of the considered signature scheme *) is_valid <@ S.verify(pk, m, sig); @@ -1982,18 +1982,18 @@ theory KeyUpdating. }. - (* - -- + (* + -- Random-Message Attack (RMA). - Attacks in which the adversary is given the public/verification key as well as + Attacks in which the adversary is given the public/verification key as well as the signatures for a set of random messages *known* to it, but not *chosen* by it - -- - *) - (* - - - UnBreakability under Random-Message Attack (UB-RMA). - Given the public/verification key and the signatures for a set of known random messages, - the adversary is tasked with computing the secret key corresponding to the + -- + *) + (* + - + UnBreakability under Random-Message Attack (UB-RMA). + Given the public/verification key and the signatures for a set of known random messages, + the adversary is tasked with computing the secret key corresponding to the public/verification key - *) @@ -2006,7 +2006,7 @@ theory KeyUpdating. (* Class of adversaries against UB-RMA *) module type Adv_UBRMA = { - proc break(pk : pk_t, msigl : (msg_t * sig_t) list) : sk_t + proc break(pk : pk_t, msigl : (msg_t * sig_t) list) : sk_t }. (* UB-RMA game *) @@ -2022,10 +2022,10 @@ theory KeyUpdating. (* Generate a key pair using the considered signature scheme *) (pk, sk) <@ S.keygen(); - (* + (* Construct a list of n_ubrma (message, signature) pairs. To this end, for each pair, randomly sample a message and, subsequently, create - (with the previously generated secret key) a corresponding signature by + (with the previously generated secret key) a corresponding signature by using the signing algorithm of the considered signature scheme. *) msigl <- []; @@ -2038,10 +2038,10 @@ theory KeyUpdating. msigl <- rcons msigl msig; } - (* + (* Ask adversary to compute the secret key sk given the public key pk and list of (message, signature) pairs msigl - *) + *) sk' <@ A.break(pk, msigl); (* Success iff the adversary correctly computed the secret key sk *) @@ -2049,13 +2049,13 @@ theory KeyUpdating. } }. end UBRMA. - - - (* - - + + + (* + - Universal UnForgeability under Random-Message Attack (UUF-RMA). - Given the public/verification key, the signatures for a set of known random messages, - and an arbitrary message, the adversary is tasked with forging a signature for + Given the public/verification key, the signatures for a set of known random messages, + and an arbitrary message, the adversary is tasked with forging a signature for the given (latter) message - *) @@ -2088,10 +2088,10 @@ theory KeyUpdating. (* Generate a key pair using the considered signature scheme *) (pk, sk) <@ S.keygen(); - (* + (* Construct a list of n_uufrma (message, signature) pairs. To this end, for each pair, randomly sample a message and, subsequently, create - (with the previously generated secret key) a corresponding signature by + (with the previously generated secret key) a corresponding signature by using the signing algorithm of the considered signature scheme. *) msigl <- []; @@ -2104,27 +2104,27 @@ theory KeyUpdating. msigl <- rcons msigl msig; } - (* + (* Ask the adversary to forge a signature for m' given the public key pk, a list of (message, signature) pairs msigl, and m' *) sig' <@ A.forge(pk, msigl, m'); - (* - Verify (w.r.t. message m') the signature sig' provided by the adversary - using the verification algorithm of the considered signature scheme + (* + Verify (w.r.t. message m') the signature sig' provided by the adversary + using the verification algorithm of the considered signature scheme *) is_valid <@ S.verify(pk, m', sig'); - (* - Check whether message for which the adversary forged a signature is fresh - (i.e., check whether message is not included in the set of messages for which + (* + Check whether message for which the adversary forged a signature is fresh + (i.e., check whether message is not included in the set of messages for which the adversary received signatures) *) is_fresh <- ! m' \in (map fst msigl); - (* - Success iff + (* + Success iff (1) "is_valid": the forged signature provided by the adversary is valid, and (2) "is_fresh": the message for which the adversary forged a signature is fresh. *) @@ -2137,7 +2137,7 @@ theory KeyUpdating. (* - Selective UnForgeability under Random-Message Attack (SUF-RMA). - After picking a message, the adversary is given the public/verification key, + After picking a message, the adversary is given the public/verification key, the signatures for a set of known random messages, and an arbitrary message, and is tasked with forging a signature for the picked message - @@ -2172,10 +2172,10 @@ theory KeyUpdating. (* Generate a key pair using the considered signature scheme *) (pk, sk) <@ S.keygen(); - (* + (* Construct a list of n_sufrma (message, signature) pairs. To this end, for each pair, randomly sample a message and, subsequently, create - (with the previously generated secret key) a corresponding signature by + (with the previously generated secret key) a corresponding signature by using the signing algorithm of the considered signature scheme. *) msigl <- []; @@ -2188,27 +2188,27 @@ theory KeyUpdating. msigl <- rcons msigl msig; } - (* - Ask the adversary to forge a signature for m' given the public key pk and + (* + Ask the adversary to forge a signature for m' given the public key pk and a list of (message, signature) pairs msigl *) sig' <@ A.forge(pk, msigl); - (* - Verify (w.r.t. message m') the signature sig' provided by the adversary - using the verification algorithm of the considered signature scheme + (* + Verify (w.r.t. message m') the signature sig' provided by the adversary + using the verification algorithm of the considered signature scheme *) is_valid <@ S.verify(pk, m', sig'); - (* - Check whether message for which the adversary forged a signature is fresh - (i.e., check whether message is not included in the set of messages for which + (* + Check whether message for which the adversary forged a signature is fresh + (i.e., check whether message is not included in the set of messages for which the adversary received signatures) *) is_fresh <- ! m' \in (map fst msigl); - (* - Success iff + (* + Success iff (1) "is_valid": the forged signature provided by the adversary is valid, and (2) "is_fresh": the message for which the adversary forged a signature is fresh. *) @@ -2216,8 +2216,8 @@ theory KeyUpdating. } }. end SUFRMA. - - + + (* - Existential UnForgeability under Random-Message Attack (EUF-RMA) @@ -2238,7 +2238,7 @@ theory KeyUpdating. }. (* EUF-RMA game *) - module EUF_RMA(S : Scheme, A : Adv_EUFRMA) = { + module EUF_RMA(S : Scheme, A : Adv_EUFRMA) = { proc main() : bool = { var pk : pk_t; var sk : sk_t; @@ -2251,10 +2251,10 @@ theory KeyUpdating. (* Generate a key pair using the considered signature scheme *) (pk, sk) <@ S.keygen(); - (* + (* Construct a list of n_eufrma (message, signature) pairs. To this end, for each pair, randomly sample a message and, subsequently, create - (with the previously generated secret key) a corresponding signature by + (with the previously generated secret key) a corresponding signature by using the signing algorithm of the considered signature scheme. *) msigl <- []; @@ -2267,47 +2267,47 @@ theory KeyUpdating. msigl <- rcons msigl msig; } - (* + (* Ask the adversary to forge a signature for any message (and provide both the - message and signature) given the public key pk and a list of (message, signature) + message and signature) given the public key pk and a list of (message, signature) pairs msigl *) (m', sig') <@ A.forge(pk, msigl); - (* - Verify (w.r.t. message m') the signature sig' provided by the adversary - using the verification algorithm of the considered signature scheme + (* + Verify (w.r.t. message m') the signature sig' provided by the adversary + using the verification algorithm of the considered signature scheme *) is_valid <@ S.verify(pk, m', sig'); - (* - Check whether message for which the adversary forged a signature is fresh - (i.e., check whether message is not included in the set of messages for which + (* + Check whether message for which the adversary forged a signature is fresh + (i.e., check whether message is not included in the set of messages for which the adversary received signatures) *) is_fresh <- ! m' \in (map fst msigl); - (* - Success iff + (* + Success iff (1) "is_valid": the forged signature provided by the adversary is valid, and (2) "is_fresh": the message for which the adversary forged a signature is fresh. *) return is_valid /\ is_fresh; } }. - - + + (* - Interactive Existential UnForgeability under Random-Message Attack (I-EUF-RMA) Given the public/verification key and the signatures for a set of random messages - (obtained one-by-one upon request), the adversary is tasked with forging a signature + (obtained one-by-one upon request), the adversary is tasked with forging a signature for any fresh message - *) - (* - Type for signing oracles used in I-EUF-RMA, including procedures - for initialization and auxiliary tasks + (* + Type for signing oracles used in I-EUF-RMA, including procedures + for initialization and auxiliary tasks *) module type Oracle_RMA(S : Scheme) = { proc init(sk_init : sk_t) : unit @@ -2315,53 +2315,53 @@ theory KeyUpdating. proc fresh(m : msg_t) : bool proc nr_queries() : int }. - - (* - Type for signing oracles used in I-EUF-RMA, only exposing the - procedure for signing + + (* + Type for signing oracles used in I-EUF-RMA, only exposing the + procedure for signing *) module type SOracle_RMA = { proc sign() : msg_t * sig_t }. - - (* - Default implementation of a signing oracle used in I-EUF-RMA, including procedures - for initialization and auxiliary tasks + + (* + Default implementation of a signing oracle used in I-EUF-RMA, including procedures + for initialization and auxiliary tasks *) module (O_RMA_Default : Oracle_RMA) (S : Scheme) = { include var O_Base_Default var sk : sk_t - + (* Initialize secret/signing key and oracle query list qs *) proc init(sk_init : sk_t) : unit = { sk <- sk_init; qs <- []; } - - (* + + (* Sign given message m using the considered signature scheme with the secret/signing key sk and append m to the list of oracle queries qs *) proc sign() : msg_t * sig_t = { var sig : sig_t; var m : msg_t; - + m <$ dmsg; (sig, sk) <@ S.sign(sk, m); - + qs <- rcons qs m; - + return (m, sig); } }. - + (* Class of adversaries against I-EUF-RMA *) module type Adv_I_EUFRMA(O : SOracle_RMA) = { proc forge(pk : pk_t) : msg_t * sig_t }. - + (* I-EUF-RMA game *) - module I_EUF_RMA(S : Scheme, A : Adv_I_EUFRMA, O: Oracle_RMA) = { + module I_EUF_RMA(S : Scheme, A : Adv_I_EUFRMA, O: Oracle_RMA) = { proc main() : bool = { var pk : pk_t; var sk : sk_t; @@ -2370,45 +2370,45 @@ theory KeyUpdating. var msig : msg_t * sig_t; var nrqs : int; var is_valid, is_fresh : bool; - + (* Generate a key pair using the considered signature scheme *) (pk, sk) <@ S.keygen(); - + (* Initialize oracle *) O(S).init(sk); - - (* + + (* Ask the adversary to forge a signature for any message (and provide both the - message and signature) given the public key pk and a list of (message, signature) + message and signature) given the public key pk and a list of (message, signature) pairs, the latter of which is provided one-by-one upon request *) (m', sig') <@ A(O(S)).forge(pk); - - (* - Verify (w.r.t. message m') the signature sig' provided by the adversary - using the verification algorithm of the considered signature scheme + + (* + Verify (w.r.t. message m') the signature sig' provided by the adversary + using the verification algorithm of the considered signature scheme *) is_valid <@ S.verify(pk, m', sig'); - - (* Check that message was not one of the messages sampled by the signing oracle. *) + + (* Check that message was not one of the messages sampled by the signing oracle. *) is_fresh <@ O(S).fresh(m'); - - (* Get the total number of oracle queries that the adversary made *) + + (* Get the total number of oracle queries that the adversary made *) nrqs <@ O(S).nr_queries(); - - (* + + (* Success iff (1) "nrqs <= n_eufrma": the adversary made at most n_eufrma oracle queries, and (2) "is_valid": the forged signature provided by the adversary is valid, and (3) "is_fresh": the message for which the adversary forged a signature is fresh. *) - return nrqs <= n_eufrma /\ is_valid /\ is_fresh; + return nrqs <= n_eufrma /\ is_valid /\ is_fresh; } }. end EUFRMA. (* - -- + -- Generic Chosen-Message Attack (GCMA). Attacks in which the adversary is given the public/verification key as well as the signatures for a set of *chosen* messages. Here, all messages are chosen @@ -2416,12 +2416,12 @@ theory KeyUpdating. (2) independently of the public key; that is, without knowing the public key at the time of choosing the messages -- - *) - (* - - - UnBreakability under Generic Chosen-Message Attack (UB-GCMA). + *) + (* + - + UnBreakability under Generic Chosen-Message Attack (UB-GCMA). Given the public/verification key and the signatures for a set of messages chosen - non-adaptively and indepedently of the public key, the adversary is tasked with + non-adaptively and indepedently of the public key, the adversary is tasked with computing the secret key corresponding to the public/verification key - *) @@ -2432,7 +2432,7 @@ theory KeyUpdating. (* Class of adversaries against UB-CMA *) module type Adv_UBGCMA = { proc choose() : msg_t list - proc break(pk : pk_t, sigl : sig_t list) : sk_t + proc break(pk : pk_t, sigl : sig_t list) : sk_t }. (* UB-GCMA game *) @@ -2451,7 +2451,7 @@ theory KeyUpdating. (* Generate a key pair using the considered signature scheme *) (pk, sk) <@ S.keygen(); - (* + (* Construct a list sigl of at most n_ubgcma signatures. Here, the i-th signature is a signature for the i-th message in the list ml previously provided by the adversary. Naturally, the signatures are created using the signing algorithm @@ -2468,11 +2468,11 @@ theory KeyUpdating. sigl <- rcons sigl sig; } - (* + (* Ask adversary to compute the secret key sk given the public key pk and a list of signatures sigl for the messages previously chosen by the adversary - (i.e., the messages in list ml) - *) + (i.e., the messages in list ml) + *) sk' <@ A.break(pk, sigl); (* Success iff the adversary correctly computed the secret key sk *) @@ -2480,20 +2480,20 @@ theory KeyUpdating. } }. end UBGCMA. - - + + (* - Universal UnForgeability under Generic Chosen-Message Attack (UUF-GCMA). Given the public/verification key, the signatures for a set of messages chosen - non-adaptively and indepedently of the public key, and an arbitrary message, + non-adaptively and indepedently of the public key, and an arbitrary message, the adversary is tasked with forging a signature for the given (latter) message - *) abstract theory UUFGCMA. (* (Proper) distribution over type of to-be-signed artifacts ('messages') *) op [lossless] dmsg : msg_t distr. - + (* Number of messages the adversary obtains signatures for in UUF-GCMA game *) const n_uufgcma : { int | 0 <= n_uufgcma } as ge0_nuufgcma. @@ -2514,7 +2514,7 @@ theory KeyUpdating. var sigl : sig_t list; var is_valid, is_fresh : bool; - (* Sample message for which the adversary must forge a signature *) + (* Sample message for which the adversary must forge a signature *) m' <$ dmsg; (* Ask adversary to choose a list of messages for which to receive signatures *) @@ -2523,7 +2523,7 @@ theory KeyUpdating. (* Generate a key pair using the considered signature scheme *) (pk, sk) <@ S.keygen(); - (* + (* Construct a list sigl of at most n_uufgcma signatures. Here, the i-th signature is a signature for the i-th message in the list ml previously provided by the adversary. Naturally, the signatures are created using the signing algorithm @@ -2541,26 +2541,26 @@ theory KeyUpdating. } (* - Ask the adversary to forge a signature for message m' given the public key pk + Ask the adversary to forge a signature for message m' given the public key pk and a list of signatures sigl for the messages previously chosen by the adversary - (i.e., the messages in list ml) + (i.e., the messages in list ml) *) sig' <@ A.forge(pk, sigl, m'); - (* - Verify (w.r.t. message m') the signature sig' provided by the adversary - using the verification algorithm of the considered signature scheme + (* + Verify (w.r.t. message m') the signature sig' provided by the adversary + using the verification algorithm of the considered signature scheme *) is_valid <@ S.verify(pk, m', sig'); - (* - Check whether message for which the adversary forged a signature is fresh - (i.e., check whether message is not included in the set of messages for which + (* + Check whether message for which the adversary forged a signature is fresh + (i.e., check whether message is not included in the set of messages for which the adversary received signatures) *) is_fresh <- ! m' \in (take (size sigl) ml); - (* + (* Success iff (1) "is_valid": the forged signature provided by the adversary is valid, and (2) "is_fresh": the message for which the adversary forged a signature is fresh. @@ -2570,12 +2570,12 @@ theory KeyUpdating. }. end UUFGCMA. - - (* - - + + (* + - Selective UnForgeability under Generic Chosen-Message Attack (SUF-GCMA). After picking a message, the adversary is given the public/verification key and - the signatures for a set of messages chosen non-adaptively and indepedently + the signatures for a set of messages chosen non-adaptively and indepedently of the public key, and is tasked with forging a signature for the picked message - *) @@ -2610,7 +2610,7 @@ theory KeyUpdating. (* Generate a key pair using the considered signature scheme *) (pk, sk) <@ S.keygen(); - (* + (* Construct a list sigl of at most n_sufgcma signatures. Here, the i-th signature is a signature for the i-th message in the list ml previously provided by the adversary. Naturally, the signatures are created using the signing algorithm @@ -2628,41 +2628,41 @@ theory KeyUpdating. } (* - Ask the adversary to forge a signature for the previously picked message m' - given the public key pk and a list of signatures sigl for the messages - previously chosen by the adversary (i.e., the messages in list ml) + Ask the adversary to forge a signature for the previously picked message m' + given the public key pk and a list of signatures sigl for the messages + previously chosen by the adversary (i.e., the messages in list ml) *) sig' <@ A.forge(pk, sigl); - (* - Verify (w.r.t. message m') the signature sig' provided by the adversary - using the verification algorithm of the considered signature scheme + (* + Verify (w.r.t. message m') the signature sig' provided by the adversary + using the verification algorithm of the considered signature scheme *) is_valid <@ S.verify(pk, m', sig'); - (* - Check whether message for which the adversary forged a signature is fresh - (i.e., check whether message is not included in the set of messages for which + (* + Check whether message for which the adversary forged a signature is fresh + (i.e., check whether message is not included in the set of messages for which the adversary received signatures) *) is_fresh <- ! m' \in (take (size sigl) ml); - (* + (* Success iff (1) "is_valid": the forged signature provided by the adversary is valid, and (2) "is_fresh": the message for which the adversary forged a signature is fresh. *) - return is_valid /\ is_fresh; + return is_valid /\ is_fresh; } }. end SUFGCMA. - - + + (* - Existential UnForgeability under Generic Chosen-Message Attack (EUF-GCMA) - Given the public/verification key and the signatures for a set of messages - chosen non-adaptively and indepedently of the public key, the adversary is tasked + Given the public/verification key and the signatures for a set of messages + chosen non-adaptively and indepedently of the public key, the adversary is tasked with forging a signature for any fresh message - *) @@ -2677,7 +2677,7 @@ theory KeyUpdating. }. (* EUF-GCMA game *) - module EUF_GCMA(S : Scheme, A : Adv_EUFGCMA) = { + module EUF_GCMA(S : Scheme, A : Adv_EUFGCMA) = { proc main() : bool = { var pk : pk_t; var sk : sk_t; @@ -2685,7 +2685,7 @@ theory KeyUpdating. var ml : msg_t list; var sigl : sig_t list; var sig, sig': sig_t; - var is_valid, is_fresh : bool; + var is_valid, is_fresh : bool; (* Ask adversary to choose a list of messages for which to receive signatures *) ml <@ A.choose(); @@ -2693,7 +2693,7 @@ theory KeyUpdating. (* Generate a key pair using the considered signature scheme *) (pk, sk) <@ S.keygen(); - (* + (* Construct a list sigl of at most n_eufgcma signatures. Here, the i-th signature is a signature for the i-th message in the list ml previously provided by the adversary. Naturally, the signatures are created using the signing algorithm @@ -2712,38 +2712,38 @@ theory KeyUpdating. (* Ask the adversary to forge a signature for the any message (and provide both - the message and the signature) given the public key pk and a list of - signatures sigl for the messages previously chosen by the adversary - (i.e., the messages in list ml) + the message and the signature) given the public key pk and a list of + signatures sigl for the messages previously chosen by the adversary + (i.e., the messages in list ml) *) (m', sig') <@ A.forge(pk, sigl); - (* - Verify (w.r.t. message m') the signature sig' provided by the adversary - using the verification algorithm of the considered signature scheme + (* + Verify (w.r.t. message m') the signature sig' provided by the adversary + using the verification algorithm of the considered signature scheme *) is_valid <@ S.verify(pk, m', sig'); - (* - Check whether message for which the adversary forged a signature is fresh - (i.e., check whether message is not included in the set of messages for which + (* + Check whether message for which the adversary forged a signature is fresh + (i.e., check whether message is not included in the set of messages for which the adversary received signatures) *) is_fresh <- ! m' \in (take (size sigl) ml); - (* + (* Success iff (1) "is_valid": the forged signature provided by the adversary is valid, and (2) "is_fresh": the message for which the adversary forged a signature is fresh. *) - return is_valid /\ is_fresh; - } + return is_valid /\ is_fresh; + } }. end EUFGCMA. - - + + (* - -- + -- Non-Adaptive Chosen-Message Attack (NACMA)/Directed Chosen-Message Attack (DCMA). Attacks in which the adversary is given the public/verification key as well as the signatures for a set of *chosen* messages. Here, all messages are chosen @@ -2751,12 +2751,12 @@ theory KeyUpdating. messages may depend on the public key; i.e., the adversary is given the public key when asked to provide the messages -- - *) - (* - - - UnBreakability under Non-Adaptive Chosen-Message Attack (UB-NACMA). + *) + (* + - + UnBreakability under Non-Adaptive Chosen-Message Attack (UB-NACMA). Given the public/verification key and the signatures for a set of non-adaptively - chosen messages, the adversary is tasked with computing the secret key + chosen messages, the adversary is tasked with computing the secret key corresponding to the public/verification key - *) @@ -2767,7 +2767,7 @@ theory KeyUpdating. (* Class of adversaries against UB-NACMA *) module type Adv_UBNACMA = { proc choose(pk : pk_t) : msg_t list - proc break(sigl : sig_t list) : sk_t + proc break(sigl : sig_t list) : sk_t }. (* UB-NACMA game *) @@ -2783,13 +2783,13 @@ theory KeyUpdating. (* Generate a key pair using the considered signature scheme *) (pk, sk) <@ S.keygen(); - (* + (* Ask adversary to choose a list of messages for which to receive signatures - given the public key pk + given the public key pk *) ml <@ A.choose(pk); - (* + (* Construct a list sigl of at most n_ubnacma signatures. Here, the i-th signature is a signature for the i-th message in the list ml previously provided by the adversary. Naturally, the signatures are created using the signing algorithm @@ -2806,11 +2806,11 @@ theory KeyUpdating. sigl <- rcons sigl sig; } - (* + (* Ask adversary to compute the secret key sk given the public key pk (in the - call to A.choose(pk)) and a list of signatures sigl for the messages previously - chosen by the adversary (i.e., the messages in list ml) - *) + call to A.choose(pk)) and a list of signatures sigl for the messages previously + chosen by the adversary (i.e., the messages in list ml) + *) sk' <@ A.break(sigl); (* Success iff the adversary correctly computed the secret key sk *) @@ -2818,20 +2818,20 @@ theory KeyUpdating. } }. end UBNACMA. - - + + (* - - + - Universal UnForgeability under Non-Adaptive Chosen-Message Attack (UUF-NACMA). Given the public/verification key, the signatures for a set of non-adaptively - chosen messages, and an arbitrary message, the adversary is tasked with forging + chosen messages, and an arbitrary message, the adversary is tasked with forging a signature for the given (latter) message - *) abstract theory UUFNACMA. (* (Proper) distribution over type of to-be-signed artifacts ('messages') *) op [lossless] dmsg : msg_t distr. - + (* Number of messages the adversary obtains signatures for in UUF-RMA game *) const n_uufnacma : { int | 0 <= n_uufnacma } as ge0_nuufnacma. @@ -2852,19 +2852,19 @@ theory KeyUpdating. var sigl : sig_t list; var is_valid, is_fresh : bool; - (* Sample message for which the adversary must forge a signature *) + (* Sample message for which the adversary must forge a signature *) m' <$ dmsg; (* Generate a key pair using the considered signature scheme *) (pk, sk) <@ S.keygen(); - (* + (* Ask adversary to choose a list of messages for which to receive signatures - given the public key pk + given the public key pk *) ml <@ A.choose(pk); - (* + (* Construct a list sigl of at most n_uufnacma signatures. Here, the i-th signature is a signature for the i-th message in the list ml previously provided by the adversary. Naturally, the signatures are created using the signing algorithm @@ -2883,25 +2883,25 @@ theory KeyUpdating. (* Ask the adversary to forge a signature for message m' given the public key pk - (in the call to A.choose(pk)) and a list of signatures sigl for the messages - previously chosen by the adversary (i.e., the messages in list ml) + (in the call to A.choose(pk)) and a list of signatures sigl for the messages + previously chosen by the adversary (i.e., the messages in list ml) *) sig' <@ A.forge(sigl, m'); - (* - Verify (w.r.t. message m') the signature sig' provided by the adversary - using the verification algorithm of the considered signature scheme + (* + Verify (w.r.t. message m') the signature sig' provided by the adversary + using the verification algorithm of the considered signature scheme *) is_valid <@ S.verify(pk, m', sig'); - (* - Check whether message for which the adversary forged a signature is fresh - (i.e., check whether message is not included in the set of messages for which + (* + Check whether message for which the adversary forged a signature is fresh + (i.e., check whether message is not included in the set of messages for which the adversary received signatures) *) is_fresh <- ! m' \in (take (size sigl) ml); - (* + (* Success iff (1) "is_valid": the forged signature provided by the adversary is valid, and (2) "is_fresh": the message for which the adversary forged a signature is fresh. @@ -2911,12 +2911,12 @@ theory KeyUpdating. }. end UUFNACMA. - - (* - - + + (* + - Selective UnForgeability under Non-Adaptive Chosen-Message Attack (SUF-NACMA). After picking a message, the adversary is given the public/verification key and - the signatures for a set of non-adaptively chosen messages, and is tasked with + the signatures for a set of non-adaptively chosen messages, and is tasked with forging a signature for the picked message - *) @@ -2951,13 +2951,13 @@ theory KeyUpdating. (* Generate a key pair using the considered signature scheme *) (pk, sk) <@ S.keygen(); - (* + (* Ask adversary to choose a list of messages for which to receive signatures - given the public key pk + given the public key pk *) ml <@ A.choose(pk); - (* + (* Construct a list sigl of at most n_sufnacma signatures. Here, the i-th signature is a signature for the i-th message in the list ml previously provided by the adversary. Naturally, the signatures are created using the signing algorithm @@ -2976,25 +2976,25 @@ theory KeyUpdating. (* Ask the adversary to forge a signature for message m' given the public key pk - (in the call to A.choose(pk)) and a list of signatures sigl for the messages - previously chosen by the adversary (i.e., the messages in list ml) + (in the call to A.choose(pk)) and a list of signatures sigl for the messages + previously chosen by the adversary (i.e., the messages in list ml) *) sig' <@ A.forge(sigl); - (* - Verify (w.r.t. message m') the signature sig' provided by the adversary - using the verification algorithm of the considered signature scheme + (* + Verify (w.r.t. message m') the signature sig' provided by the adversary + using the verification algorithm of the considered signature scheme *) is_valid <@ S.verify(pk, m', sig'); - (* - Check whether message for which the adversary forged a signature is fresh - (i.e., check whether message is not included in the set of messages for which + (* + Check whether message for which the adversary forged a signature is fresh + (i.e., check whether message is not included in the set of messages for which the adversary received signatures) *) is_fresh <- ! m' \in (take (size sigl) ml); - (* + (* Success iff (1) "is_valid": the forged signature provided by the adversary is valid, and (2) "is_fresh": the message for which the adversary forged a signature is fresh. @@ -3003,8 +3003,8 @@ theory KeyUpdating. } }. end SUFNACMA. - - + + (* - Existential UnForgeability under Non-Adaptive Chosen-Message Attack (EUF-NACMA). @@ -3023,7 +3023,7 @@ theory KeyUpdating. }. (* EUF-NACMA game *) - module EUF_NACMA(S : Scheme, A : Adv_EUFNACMA) = { + module EUF_NACMA(S : Scheme, A : Adv_EUFNACMA) = { proc main() : bool = { var pk : pk_t; var sk : sk_t; @@ -3031,18 +3031,18 @@ theory KeyUpdating. var ml : msg_t list; var sigl : sig_t list; var sig, sig': sig_t; - var is_valid, is_fresh : bool; + var is_valid, is_fresh : bool; (* Generate a key pair using the considered signature scheme *) (pk, sk) <@ S.keygen(); - (* + (* Ask adversary to choose a list of messages for which to receive signatures - given the public key pk + given the public key pk *) ml <@ A.choose(pk); - (* + (* Construct a list sigl of at most n_eufnacma signatures. Here, the i-th signature is a signature for the i-th message in the list ml previously provided by the adversary. Naturally, the signatures are created using the signing algorithm @@ -3062,50 +3062,50 @@ theory KeyUpdating. (* Ask the adversary to forge a signature for the any message (and provide both the message and the signature) given the public key pk (in the call to A.choose(pk)) - and a list of signatures sigl for the messages previously chosen by the adversary - (i.e., the messages in list ml) + and a list of signatures sigl for the messages previously chosen by the adversary + (i.e., the messages in list ml) *) (m', sig') <@ A.forge(sigl); - (* - Verify (w.r.t. message m') the signature sig' provided by the adversary - using the verification algorithm of the considered signature scheme + (* + Verify (w.r.t. message m') the signature sig' provided by the adversary + using the verification algorithm of the considered signature scheme *) is_valid <@ S.verify(pk, m', sig'); - (* - Check whether message for which the adversary forged a signature is fresh - (i.e., check whether message is not included in the set of messages for which + (* + Check whether message for which the adversary forged a signature is fresh + (i.e., check whether message is not included in the set of messages for which the adversary received signatures) *) is_fresh <- ! m' \in (take (size sigl) ml); - (* + (* Success iff (1) "is_valid": the forged signature provided by the adversary is valid, and (2) "is_fresh": the message for which the adversary forged a signature is fresh. *) - return is_valid /\ is_fresh; - } + return is_valid /\ is_fresh; + } }. end EUFNACMA. - + (* - -- + -- (Adaptive) Chosen-Message Attack (CMA). Attacks in which the adversary is given the public/verification key as well as the signatures for a set of *chosen* messages. Here, all messages are chosen - adaptively and may depend on the public key; that is, the adversary - (1) immediately receives a signature for a chosen message before choosing the + adaptively and may depend on the public key; that is, the adversary + (1) immediately receives a signature for a chosen message before choosing the subsequent message, and (2) is given the public key when asked to provide the messages. -- *) (* - General - *) - (* - Type for signing oracles used in (adaptive) CMA games, including procedures - for initialization and auxiliary tasks + (* + Type for signing oracles used in (adaptive) CMA games, including procedures + for initialization and auxiliary tasks *) module type Oracle_CMA(S : Scheme) = { proc init(sk_init : sk_t) : unit @@ -3114,49 +3114,49 @@ theory KeyUpdating. proc nr_queries() : int }. - (* - Type for signing oracles used in (adaptive) CMA games, only exposing the - procedure for signing + (* + Type for signing oracles used in (adaptive) CMA games, only exposing the + procedure for signing *) module type SOracle_CMA = { proc sign(m : msg_t) : sig_t }. - - (* - Default implementation of a signing oracle including procedures for - initialization and auxiliary tasks + + (* + Default implementation of a signing oracle including procedures for + initialization and auxiliary tasks *) module (O_CMA_Default : Oracle_CMA) (S : Scheme) = { include var O_Base_Default var sk : sk_t - + (* Initialize secret/signing key and oracle query list qs *) proc init(sk_init : sk_t) : unit = { sk <- sk_init; qs <- []; } - (* + (* Sign given message m using the considered signature scheme with the secret/signing key sk and append m to the list of oracle queries qs *) proc sign(m : msg_t) : sig_t = { var sig : sig_t; - + (sig, sk) <@ S.sign(sk, m); qs <- rcons qs m; - + return sig; } }. - - (* - - - UnBreakability under (Adaptive) Chosen-Message Attack (UB-CMA). + + (* + - + UnBreakability under (Adaptive) Chosen-Message Attack (UB-CMA). Given the public/verification key and the signatures for a set of adaptively - chosen messages, the adversary is tasked with computing the secret key + chosen messages, the adversary is tasked with computing the secret key corresponding to the public/verification key - *) @@ -3164,36 +3164,36 @@ theory KeyUpdating. module type Adv_UBCMA(O : SOracle_CMA) = { proc break(pk : pk_t) : sk_t }. - + (* UB-CMA game *) module UB_CMA(S : Scheme, A : Adv_UBCMA, O : Oracle_CMA) = { proc main() : bool = { var pk : pk_t; var sk, sk' : sk_t; - + (* Generate a key pair using the considered signature scheme *) (pk, sk) <@ S.keygen(); - + (* Initialize the signing oracle with the generated secret key *) O(S).init(sk); - (* + (* Ask adversary to compute the secret key sk given the public key pk and access to a signing oracle that it can query an unlimited number of times - *) + *) sk' <@ A(O(S)).break(pk); - + (* Success iff the adversary correctly computed the secret key sk. *) - return sk' = sk; + return sk' = sk; } }. - - + + (* - - + - Universal UnForgeability under (Adaptive) Chosen-Message Attack (UUF-CMA) Given the public/verification key, the signatures for a set of adaptively - chosen messages, and an arbitrary message, the adversary is tasked with forging + chosen messages, and an arbitrary message, the adversary is tasked with forging a signature for the given (latter) message - *) @@ -3218,7 +3218,7 @@ theory KeyUpdating. var sig : sig_t; var is_valid, is_fresh : bool; - (* Sample message for which the adversary must forge a signature *) + (* Sample message for which the adversary must forge a signature *) m <$ dmsg; (* Generate a key pair using the considered signature scheme *) @@ -3228,40 +3228,40 @@ theory KeyUpdating. O(S).init(sk); (* - Ask the adversary to forge a signature for message m given the public key pk + Ask the adversary to forge a signature for message m given the public key pk and and access to a signing oracle that it can query an unlimited number of times *) sig <@ A(O(S)).forge(pk, m); - (* - Verify (w.r.t. message m) the signature sig provided by the adversary - using the verification algorithm of the considered signature scheme + (* + Verify (w.r.t. message m) the signature sig provided by the adversary + using the verification algorithm of the considered signature scheme *) is_valid <@ S.verify(pk, m, sig); - (* - Check whether message for which the adversary forged a signature is fresh - (i.e., check whether message is not included in the list of messages for which + (* + Check whether message for which the adversary forged a signature is fresh + (i.e., check whether message is not included in the list of messages for which the adversary received signatures through an oracle query) *) is_fresh <@ O(S).fresh(m); - (* + (* Success iff (1) "is_valid": the forged signature provided by the adversary is valid, and (2) "is_fresh": the message for which the adversary forged a signature is fresh. *) - return is_valid /\ is_fresh; + return is_valid /\ is_fresh; } }. end UUFCMA. - - + + (* - Selective UnForgeability under Chosen-Message Attack (SUF-CMA). - After picking a message, the adversary is given the public/verification key - and the signatures for a set of adaptively chosen messages, and is tasked with + After picking a message, the adversary is given the public/verification key + and the signatures for a set of adaptively chosen messages, and is tasked with forging a signature for the picked message - *) @@ -3270,7 +3270,7 @@ theory KeyUpdating. proc pick() : msg_t proc forge(pk : pk_t) : sig_t }. - + (* SUF-CMA game *) module SUF_CMA(S : Scheme, A : Adv_SUFCMA, O : Oracle_CMA) = { proc main() : bool = { @@ -3279,41 +3279,41 @@ theory KeyUpdating. var m : msg_t; var sig : sig_t; var is_valid, is_fresh : bool; - - (* Ask the adversary to pick a message to forge a signature for *) + + (* Ask the adversary to pick a message to forge a signature for *) m <@ A(O(S)).pick(); - + (* Generate a key pair using the considered signature scheme *) (pk, sk) <@ S.keygen(); - + (* Initialize the signing oracle with the generated secret key *) O(S).init(sk); (* - Ask the adversary to forge a signature for message m given the public key pk + Ask the adversary to forge a signature for message m given the public key pk and and access to a signing oracle that it can query an unlimited number of times *) sig <@ A(O(S)).forge(pk); - (* - Verify (w.r.t. message m) the signature sig provided by the adversary - using the verification algorithm of the considered signature scheme + (* + Verify (w.r.t. message m) the signature sig provided by the adversary + using the verification algorithm of the considered signature scheme *) is_valid <@ S.verify(pk, m, sig); - - (* - Check whether message for which the adversary forged a signature is fresh - (i.e., check whether message is not included in the list of messages for which + + (* + Check whether message for which the adversary forged a signature is fresh + (i.e., check whether message is not included in the list of messages for which the adversary received signatures through an oracle query) *) is_fresh <@ O(S).fresh(m); - - (* + + (* Success iff (1) "is_valid": the forged signature provided by the adversary is valid, and (2) "is_fresh": the message for which the adversary forged a signature is fresh. *) - return is_valid /\ is_fresh; + return is_valid /\ is_fresh; } }. @@ -3321,7 +3321,7 @@ theory KeyUpdating. (* - Existential UnForgeability under Chosen-Message Attack (EUF-CMA) - Given the public/verification key and the signatures for a set of adaptively + Given the public/verification key and the signatures for a set of adaptively chosen messages, the adversary is tasked with forging a signature for any fresh message - *) @@ -3338,53 +3338,53 @@ theory KeyUpdating. var m : msg_t; var sig : sig_t; var is_valid, is_fresh : bool; - + (* Generate a key pair using the considered signature scheme *) (pk, sk) <@ S.keygen(); - + (* Initialize the signing oracle with the generated secret key *) O(S).init(sk); (* Ask the adversary to forge a signature for any message (and provide both the - message and the signature) given the public key pk and access to a signing oracle + message and the signature) given the public key pk and access to a signing oracle that it can query an unlimited number of times *) (m, sig) <@ A(O(S)).forge(pk); - (* - Verify (w.r.t. message m) the signature sig provided by the adversary - using the verification algorithm of the considered signature scheme + (* + Verify (w.r.t. message m) the signature sig provided by the adversary + using the verification algorithm of the considered signature scheme *) is_valid <@ S.verify(pk, m, sig); - - (* - Check whether message for which the adversary forged a signature is fresh - (i.e., check whether message is not included in the list of messages for which + + (* + Check whether message for which the adversary forged a signature is fresh + (i.e., check whether message is not included in the list of messages for which the adversary received signatures through an oracle query) *) is_fresh <@ O(S).fresh(m); - - (* + + (* Success iff (1) "is_valid": the forged signature provided by the adversary is valid, and (2) "is_fresh": the message for which the adversary forged a signature is fresh. *) - return is_valid /\ is_fresh; + return is_valid /\ is_fresh; } }. - - + + (* - - + - Strong Existential UnForgeability under Chosen-Message Attack (SEUF-CMA). - Given the public/verification key and the signatures for a set of adaptively + Given the public/verification key and the signatures for a set of adaptively chosen messages, the adversary is tasked with forging a fresh signature for any message - *) - (* - Type for signing oracles used in the SEUF-CMA game, including procedures - for initialization and auxiliary tasks + (* + Type for signing oracles used in the SEUF-CMA game, including procedures + for initialization and auxiliary tasks *) module type Oracle_SEUFCMA(S : Scheme) = { proc init(sk_init : sk_t) : unit @@ -3393,52 +3393,52 @@ theory KeyUpdating. proc nr_queries() : int }. - (* - Type for signing oracles used in the SEUF-CMA game, only exposing the - procedure for signing + (* + Type for signing oracles used in the SEUF-CMA game, only exposing the + procedure for signing *) module type SOracle_SEUFCMA = { proc sign(m : msg_t) : sig_t }. - - (* - Default implementation of a signing oracle including procedures for - initialization and auxiliary tasks + + (* + Default implementation of a signing oracle including procedures for + initialization and auxiliary tasks *) module (O_SEUFCMA_Default : Oracle_SEUFCMA) (S : Scheme) = { var sk : sk_t var qs : (msg_t * sig_t) list - + (* Initialize secret/signing key and oracle query list qs *) proc init(sk_init : sk_t) : unit = { sk <- sk_init; qs <- []; } - (* + (* Sign given message m using the considered signature scheme with the secret/signing key sk and append m to the list of oracle queries qs *) proc sign(m : msg_t) : sig_t = { var sig : sig_t; var msig : msg_t * sig_t; - + (sig, sk) <@ S.sign(sk, m); msig <- (m, sig); qs <- rcons qs msig; - + return sig; } - (* + (* Check whether given (message, signature) pair msig is fresh, i.e., whether this pair - is not contained in the list of oracle queries qs + is not contained in the list of oracle queries qs *) proc fresh(msig : msg_t * sig_t) : bool = { return ! msig \in qs; } - + (* Get the number of oracle queries, i.e., the size of the oracle query list qs *) proc nr_queries() : int = { return size qs; @@ -3458,39 +3458,39 @@ theory KeyUpdating. var m : msg_t; var sig : sig_t; var is_valid, is_fresh : bool; - + (* Generate a key pair using the considered signature scheme *) (pk, sk) <@ S.keygen(); - + (* Initialize the signing oracle with the generated secret key *) O(S).init(sk); (* Ask the adversary to forge a signature for any message (and provide both the - message and the signature) given the public key pk and access to a signing oracle + message and the signature) given the public key pk and access to a signing oracle that it can query an unlimited number of times *) (m, sig) <@ A(O(S)).forge(pk); - (* - Verify (w.r.t. message m) the signature sig provided by the adversary - using the verification algorithm of the considered signature scheme + (* + Verify (w.r.t. message m) the signature sig provided by the adversary + using the verification algorithm of the considered signature scheme *) is_valid <@ S.verify(pk, m, sig); - - (* + + (* Check whether (message, signature) pair (m, sig) returned by the adversary is fresh (i.e., check whether this pair is not included in the list of (message, signature) pairs of the signing oracle) *) is_fresh <@ O(S).fresh((m, sig)); - - (* + + (* Success iff (1) "is_valid": the forged signature provided by the adversary is valid, and (2) "is_fresh": the (message, signature) pair provided by the adversary is fresh. *) - return is_valid /\ is_fresh; + return is_valid /\ is_fresh; } }. end KeyUpdating. diff --git a/proof/security/DigitalSignaturesROM.eca b/proof/security/DigitalSignaturesROM.eca index 8034e8bc..89cd5461 100644 --- a/proof/security/DigitalSignaturesROM.eca +++ b/proof/security/DigitalSignaturesROM.eca @@ -1,6 +1,6 @@ (* --- Require/Import Theories --- *) (* -- Built-in (i.e, standard library) -- *) -require import AllCore List. +require import AllCore List Distr. require (*--*) ROM. diff --git a/proof/security/HashThenSignAux.eca b/proof/security/HashThenSignAux.eca deleted file mode 100644 index 83051495..00000000 --- a/proof/security/HashThenSignAux.eca +++ /dev/null @@ -1,2154 +0,0 @@ -(* -(* --- Require/Import --- *) -(* -- Built-In (Standard Library) -- *) -require import AllCore List Distr DList IntDiv RealExp StdOrder FMap BitEncoding FinType. -require (*--*) Word Subtype ROM. -(*---*) import RField IntOrder RealOrder BS2Int. - - -(* -- Local -- *) -require (*--*) DigitalSignatures DigitalSignaturesROM KeyedHashFunctions Reprogramming EUFRMA_Interactive_Equiv. - - - -(* --- Parameters --- *) -(* -- Proof-specific -- *) -(* TODO: Move to section *) -(* Number of message-signature pairs given to adversary *) -op n : { int | 0 <= n } as ge0_n. - -(* Number of allowed signature queries *) -op qS : { int | 0 <= qS <= n } as rng_qS. - -(* Number of allowed random oracle (hash) queries *) -op qH : { int | 0 <= qH } as ge0_qH. - -(* --- Types --- *) -(* -- General -- *) -(* Randomness (i.e., indexing keys) used for message compression (assumed to be finite) *) -type rco_t. - -(* TODO: Why finite? Fix in Reprogramming *) -clone import FinType as RCO with - type t <= rco_t. - -(* Auxiliary (indexing) input used for message compression (assumed to be finite) *) -type aux_t. - -(* TODO: Why finite? Fix in Reprogramming *) -clone FinType as AUX with - type t <= aux_t. - -clone FinProdType as MCOIDX with - type t1 <- rco_t, - type t2 <- aux_t, - theory FT1 <- RCO, - theory FT2 <- AUX - - proof *. - - -(* -- Fixed-length digital signature scheme -- *) -(* Public keys *) -type pk_fl_t. - -(* Secret keys *) -type sk_fl_t. - -(* Messages (assumed to be finite) *) -type msg_fl_t. - -(* Signatures *) -type sig_fl_t. - - - -(* -- Arbitrary-length digital signature scheme -- *) -(* Public keys; same as for fixed-length digital signature scheme *) -type pk_al_t = pk_fl_t. - -(* Messages (assumed to be finite) *) -type msg_al_t. - -(* TODO: Why finite? Fix in Reprogramming *) -clone FinType as MSG_AL with - type t <= msg_al_t. - -(* - Signatures; same as for fixed-length digital signature scheme but - extended with randomness/indexing key used for message compression -*) -type sig_al_t = rco_t * sig_fl_t. - - -(* -- Miscellaneous -- *) -(* Product type of indexing keys used for message compression and arbitrary-length messages *) -clone FinProdType as MCOINPNested with - type t1 <- rco_t * aux_t, - type t2 <- msg_al_t, - theory FT1 <- MCOIDX, - theory FT2 <- MSG_AL - - proof *. - -clone import FinType as MCOINP with - type t <= rco_t * aux_t * msg_al_t, - op enum <= map (fun (ram : (_ * _) * _) => (ram.`1.`1, ram.`1.`2, ram.`2)) MCOINPNested.enum - -proof *. -realize enum_spec. -move => ram; rewrite count_map /preim. -by rewrite -(MCOINPNested.enum_spec ((ram.`1, ram.`2), ram.`3)) /#. -qed. - -(* --- Operators --- *) -op extr_aux_verify : pk_al_t -> sig_al_t -> aux_t. - -(* --- Distributions --- *) -(* Proper, full, and uniform distribution over indexing keys used for message compression *) -op [lossless full uniform] drco : rco_t distr. - -(* Proper, full, and uniform distribution over fixed-length messages *) -op [lossless full uniform] dmsg_fl : msg_fl_t distr. - - - -(* --- Clones and imports --- *) -(* -- Proof-specific -- *) -(* Reprogramming technique and corresponding bound *) -(* TODO: Change ROM to PROM to fix finiteness, then move to section *) -clone import Reprogramming as Repro with - type from <- rco_t * aux_t * msg_al_t, - type hash <- msg_fl_t, - - op p_max_bound <- mu1 drco witness, - - op dhash <- dmsg_fl, - - theory FinFrom <- MCOINP - - rename [theory] "ROM_" as "MCORO" - rename [theory] "LE" as "MCOROLE" - - proof *. - realize dhash_ll by exact: dmsg_fl_ll. - -(** MCORO = ROM_ **) -import MCORO. -import MCOROLE. -module MCO = ERO. - -(* - (* TODO: Uncomment after moving below to section *) -clone import DigitalSignatures as DSS_FL with - type pk_t <= pk_fl_t, - type sk_t <= sk_fl_t, - type msg_t <= msg_fl_t, - type sig_t <= sig_fl_t -proof *. - -clone import DSS_FL.Stateless.EUFRMA as DSS_FL_EUFRMA with - op dmsg <= dmsg_fl, - op n_eufrma <= n -proof *. -realize dmsg_ll by exact: dmsg_fl_ll. -realize ge0_neufrma by exact: ge0_n. -*) - -(* Equivalence between the considered interactive EUF-RMA and regular EUF-RMA notions *) -(* TODO: Move to section, proving everything also works with above modules *) -clone import EUFRMA_Interactive_Equiv as EUFRMAEqv with - type msg_t <- msg_fl_t, - type sig_t <- sig_fl_t, - type pk_t <- pk_fl_t, - type sk_t <- sk_fl_t, - - op n_eufrma <- n, - op dmsg <- dmsg_fl, - - type ClassDS.pk_t <= pk_fl_t, - type ClassDS.sk_t <= sk_fl_t, - type ClassDS.msg_t <= msg_fl_t, - type ClassDS.sig_t <= sig_fl_t - - rename [theory] "Class_EUFRMA" as "DSS_FL_EUFRMA" - rename [theory] "ClassDS" as "DSS_FL" - - proof *. - realize dmsg_ll by exact: dmsg_fl_ll. - realize ge0_neufrma by exact: ge0_n. - -import DSS_FL_EUFRMA. - -(* --- Auxiliary lemmas --- *) -(* - The maximum probility of sampling any randomness-message pair (rco, m) - where rco is sampled according to drco and m is a fixed constant, is - equal to the probability of sampling some value from drco - (because drco is full and uniform) -*) -lemma p_max_rcom (aux : aux_t) (m : msg_al_t) : - Repro.p_max (dmap drco (fun (rco : rco_t) => (rco, aux, m))) = mu1 drco witness. -proof. -apply ler_anti; split => [|_]. -+ move: (listmax_in Real.(<=) RealOrder.ler_trans RealOrder.ler_total). - move=> /(_ 0%r (map (fun (x : rco_t * aux_t * msg_al_t) => - mu (dmap drco (fun (rco : rco_t) => (rco, aux, m))) ((=) x)) - MCOINP.enum) _). - - rewrite size_map /MCOINP.enum; move: (enumP witness). - case MCOINPNested.enum => //=; smt(size_ge0). - move/mapP => @/p_max [rcom] [rcomin /= ->]. - by rewrite dmapE /(\o) /= (drco_uni witness rcom.`1) 1,2:drco_fu /pred1 mu_le. -apply (ler_trans (mu1 (dmap drco (fun (rco : rco_t) => (rco, aux, m))) (witness, aux, m))) => [| @/pred1]. -+ rewrite ler_eqVlt; left. - by rewrite dmap1E /pred1 /(\o). -by rewrite (mu_eq _ _ (fun (p : rco_t * aux_t * msg_al_t) => (witness, aux, m) = p)) 1:/# p_maxE. -qed. - - - -(* --- Properties --- *) -(* -- Random oracle -- *) -(* - CR (of a random oracle) - *) -(* Class of adversaries againt CR (of a random oracle) *) -module type Adv_CR_RO(RO : POracle) = { - proc find() : (rco_t * aux_t * msg_al_t) * (rco_t * aux_t * msg_al_t) -}. - -(* CR (of a random oracle) game *) -module CR_RO(A : Adv_CR_RO, RO : Oracle) = { - proc main() = { - var x, x' : rco_t * aux_t * msg_al_t; - var y, y' : msg_fl_t; - - RO.init(); - - (x, x') <@ A(RO).find(); - - y <@ RO.o(x); - y' <@ RO.o(x'); - - return x <> x' /\ y = y'; - } -}. - - -(* - M-eTCR (of a random oracle) - *) -(* Module type for "target" oracles used in the M-eTCR (of a random oracle) game *) -module type Oracle_METCR = { - proc init() : unit - proc query(a : aux_t, x : msg_al_t) : rco_t - proc get(i : int) : rco_t * aux_t * msg_al_t - proc nr_targets() : int -}. - -(* - Module type for "target" oracles given to the adversaries - in the M-eTCR (of a random oracle) game -*) -module type TOracle_METCR = { - proc query(a : aux_t, x : msg_al_t) : rco_t -}. - -(* Default implementation of a "target" oracle used in the M-eTCR (of a random oracle) game *) -module O_METCR : Oracle_METCR = { - var ts : (rco_t * aux_t * msg_al_t) list - - proc init() : unit = { - ts <- []; - } - - proc query(aux : aux_t, x : msg_al_t) : rco_t = { - var rco : rco_t; - - rco <$ drco; - - ts <- rcons ts (rco, aux, x); - - return rco; - } - - (* Gets i-th element in list of targets; returns witness if index is out of bounds *) - proc get(i : int) : rco_t * aux_t * msg_al_t = { - return nth witness ts i; - } - - (* Returns the number of elements in the list of targets *) - proc nr_targets() : int = { - return size ts; - } -}. - -(* Class of adversaries against M_ETCR *) -module type Adv_METCR_RO(RO : POracle, O : TOracle_METCR) = { - proc find() : int * (rco_t * aux_t * msg_al_t) -}. - -(* M-eTCR (of a random oracle) game *) -module M_ETCR_RO(A : Adv_METCR_RO, O : Oracle_METCR, RO : Oracle) = { - proc main() = { - var x, x' : rco_t * aux_t * msg_al_t; - var y, y' : msg_fl_t; - var i, nrts : int; - - O.init(); - RO.init(); - - (i, x') <@ A(RO, O).find(); - - x <@ O.get(i); - - y <@ RO.o(x); - y' <@ RO.o(x'); - - nrts <@ O.nr_targets(); - - return 0 <= i < nrts /\ x <> x' /\ y = y'; - } -}. - - - -(* - --- - Hash-then-sign paradigm where the the randomness/indexing keys used for - message compression are sampled - --- -*) -theory WithSampling. - (* -- Types -- *) - (* - Arbitrary-length digital signature scheme - *) - (* Secret key; same as for fixed-length digital signature scheme *) - type sk_al_t = sk_fl_t. - - (* -- Operators -- *) - op extr_aux_sign : sk_al_t -> aux_t. - - - (* -- Clones and imports -- *) - (* - Arbitrary-length digital signature scheme (where the message compression - function is considered to be an RO) - *) - clone import DigitalSignaturesROM as DSS_AL with - type pk_t <- pk_al_t, - type sk_t <- sk_al_t, - type msg_t <- msg_al_t, - type sig_t <- sig_al_t, - - type in_t <- rco_t * aux_t * msg_al_t, - type out_t <- msg_fl_t, - type d_in_t <- int, - type d_out_t <- bool, - - op doutm <- fun _ => dmsg_fl - - proof *. - - import KeyUpdatingROM. - import DSS. - import KeyUpdating. - - - (* -- Arbitrary-length digital signature scheme -- *) - module (AL_KU_DSS(FL_KU_DSS : DSS_FL.KeyUpdating.Scheme) : Scheme_RO) (RO : POracle) = { - proc keygen = FL_KU_DSS.keygen - - proc sign(sk : sk_al_t, m : msg_al_t) : sig_al_t * sk_al_t = { - var rco : rco_t; - var aux : aux_t; - var cm : msg_fl_t; - var sigfl : sig_fl_t; - var sig : sig_al_t; - - rco <$ drco; - aux <- extr_aux_sign sk; - - cm <@ RO.o((rco, aux, m)); - - (sigfl, sk) <@ FL_KU_DSS.sign(sk, cm); - - sig <- (rco, sigfl); - - return (sig, sk); - } - - proc verify(pk : pk_al_t, m : msg_al_t, sig : sig_al_t) : bool = { - var rco : rco_t; - var aux : aux_t; - var cm : msg_fl_t; - var sigfl : sig_fl_t; - var ver : bool; - - rco <- sig.`1; - aux <- extr_aux_verify pk sig; - - cm <@ RO.o((rco, aux, m)); - - sigfl <- sig.`2; - - ver <@ FL_KU_DSS.verify(pk, cm, sigfl); - - return ver; - } - }. - - (* -- Reduction Adversaries -- *) - module (R_EUFCMARO_CRRO (FL_KU_DSS : DSS_FL.KeyUpdating.Scheme, A : Adv_EUFCMA_RO) : Adv_CR_RO) (RO : POracle) = { - module O_CMA_R_EUFCMARO_CRRO : SOracle_CMA = { - var sk : sk_al_t - var comps : (msg_fl_t * (rco_t * aux_t * msg_al_t)) list - - proc init(sk_init : sk_al_t) = { - sk <- sk_init; - comps <- []; - } - - proc sign(m : msg_al_t) : sig_al_t = { - var rco : rco_t; - var aux : aux_t; - var cm : msg_fl_t; - var sigfl : sig_fl_t; - var sig : sig_al_t; - - rco <$ drco; - aux <- extr_aux_sign sk; - cm <@ RO.o((rco, aux, m)); - - (sigfl, sk) <@ FL_KU_DSS.sign(sk, cm); - - sig <- (rco, sigfl); - - comps <- rcons comps (cm, (rco, aux, m)); - - return sig; - } - } - - proc find() : (rco_t * aux_t * msg_al_t) * (rco_t * aux_t * msg_al_t) = { - var pk : pk_al_t; - var sk : sk_al_t; - var ram : rco_t * aux_t * msg_al_t; - var rco' : rco_t; - var aux' : aux_t; - var mal' : msg_al_t; - var sig' : sig_al_t; - var mfl' : msg_fl_t; - - (pk, sk) <@ AL_KU_DSS(FL_KU_DSS, RO).keygen(); - - O_CMA_R_EUFCMARO_CRRO.init(sk); - - (mal', sig') <@ A(RO, O_CMA_R_EUFCMARO_CRRO).forge(pk); - - rco' <- sig'.`1; - aux' <- extr_aux_verify pk sig'; - - mfl' <@ RO.o((rco', aux', mal')); - - ram <- oget (assoc O_CMA_R_EUFCMARO_CRRO.comps mfl'); - - return (ram, (rco', aux', mal')); - } - }. - - module (R_EUFCMARO_METCRRO (FL_KU_DSS : DSS_FL.KeyUpdating.Scheme, A : Adv_EUFCMA_RO) : Adv_METCR_RO) (RO : POracle, O : TOracle_METCR) = { - module O_CMA_R_EUFCMARO_METCRRO : SOracle_CMA = { - var sk : sk_al_t - var comps : (msg_fl_t * (rco_t * aux_t * msg_al_t)) list - - proc init(sk_init : sk_al_t) = { - sk <- sk_init; - comps <- []; - } - - proc sign(m : msg_al_t) : sig_al_t = { - var aux : aux_t; - var rco : rco_t; - var cm : msg_fl_t; - var sigfl : sig_fl_t; - var sig : sig_al_t; - - aux <- extr_aux_sign sk; - - rco <@ O.query(aux, m); - - cm <@ RO.o((rco, aux, m)); - - (sigfl, sk) <@ FL_KU_DSS.sign(sk, cm); - - sig <- (rco, sigfl); - - comps <- rcons comps (cm, (rco, aux, m)); - - return sig; - } - } - - proc find() : int * (rco_t * aux_t * msg_al_t) = { - var pk : pk_al_t; - var sk : sk_al_t; - var rco' : rco_t; - var aux' : aux_t; - var mal' : msg_al_t; - var sig' : sig_al_t; - var mfl' : msg_fl_t; - var i : int; - - (pk, sk) <@ AL_KU_DSS(FL_KU_DSS, RO).keygen(); - - O_CMA_R_EUFCMARO_METCRRO.init(sk); - - (mal', sig') <@ A(RO, O_CMA_R_EUFCMARO_METCRRO).forge(pk); - - aux' <- extr_aux_verify pk sig'; - rco' <- sig'.`1; - - mfl' <@ RO.o((rco', aux', mal')); - - i <- index mfl' (unzip1 O_CMA_R_EUFCMARO_METCRRO.comps); - - return (i, (rco', aux', mal')); - } - }. - - module (R_EUFCMARO_IEUFRMA(A : Adv_EUFCMA_RO) : Adv_I_EUFRMA) (O : SOracle_RMA) = { - module O_CMA_R_EUFCMARO_IEUFRMA : SOracle_CMA = { - var qs : msg_al_t list - var comps : (msg_fl_t * (rco_t * aux_t * msg_al_t)) list - var pk : pk_fl_t - - proc init(pk_init : pk_fl_t) = { - pk <- pk_init; - qs <- []; - comps <- []; - } - - proc sign(m : msg_al_t) : sig_al_t = { - var rco : rco_t; - var aux : aux_t; - var cm : msg_fl_t; - var sigfl : sig_fl_t; - var sig : sig_al_t; - - rco <$ drco; - - (cm, sigfl) <@ O.sign(); - - aux <- extr_aux_verify pk (rco, sigfl); - - Wrapped_Oracle(MCO).set((rco, aux, m), cm); - - cm <@ Wrapped_Oracle(MCO).o((rco, aux, m)); - - sig <- (rco, sigfl); - - comps <- rcons comps (cm, (rco, aux, m)); - qs <- rcons qs m; - - return sig; - } - } - - proc forge(pk : pk_fl_t) : msg_fl_t * sig_fl_t = { - var m : msg_al_t; - var sig : sig_al_t; - var rco : rco_t; - var aux : aux_t; - var cm : msg_fl_t; - var sigfl : sig_fl_t; - - MCO.init(); - Wrapped_Oracle(MCO).init(); - O_CMA_R_EUFCMARO_IEUFRMA.init(pk); - - (m, sig) <@ A(Wrapped_Oracle(MCO), O_CMA_R_EUFCMARO_IEUFRMA).forge(pk); - - rco <- sig.`1; - sigfl <- sig.`2; - aux <- extr_aux_verify pk sig; - - cm <@ Wrapped_Oracle(MCO).o((rco, aux, m)); - - return (cm, sigfl); - } - }. - - - (* -- Auxiliary modules -- *) - (* Module used for counting queries of an EUF-CMA adversary (in the ROM) *) - module (QC_A(A : Adv_EUFCMA_RO) : Adv_EUFCMA_RO) (RO : POracle, O : DSS.KeyUpdating.SOracle_CMA) = { - var cS : int - var cH : int - - module QC_SO = { - proc sign(m : msg_al_t) : sig_al_t = { - var sig : sig_al_t; - - cS <- cS + 1; - - sig <@ O.sign(m); - - return sig; - } - } - - module QC_RO = { - proc o(x : rco_t * aux_t * msg_al_t) : msg_fl_t = { - var cm : msg_fl_t; - - cH <- cH + 1; - - cm <@ RO.o(x); - - return cm; - } - } - - proc forge(pk : pk_al_t) : msg_al_t * sig_al_t = { - var m : msg_al_t; - var sig : sig_al_t; - - cS <- 0; - cH <- 0; - - (m, sig) <@ A(QC_RO, QC_SO).forge(pk); - - return (m, sig); - } - }. - - - (* - -- - Proofs of EUF-CMA property for the arbitrary-length signature - scheme constructed as specifcied above (assuming message compression is a RO) - -- - *) - section Proofs_EUFCMA_RO_ALKUDSS. - (* - Declarations - *) - (* Fixed-length signature scheme *) - declare module FL_KU_DSS <: DSS_FL.KeyUpdating.Scheme{-ERO, -O_CMA_Default, -O_METCR, -R_EUFCMARO_CRRO, -R_EUFCMARO_METCRRO, -Wrapped_Oracle, -RepO, -O_RMA_Default, -R_EUFCMARO_IEUFRMA, -QC_A, -Lazy.LRO, -ReproGame, -R_EUFRMA_IEUFRMA}. - - (* Signing and verification procedure of fixed-length signature scheme always terminate *) - declare axiom FL_KU_DSS_sign_ll : islossless FL_KU_DSS.sign. - declare axiom FL_KU_DSS_verify_ll : islossless FL_KU_DSS.verify. - - (* Adversary aganst EUF-CMA in the ROM *) - declare module A <: Adv_EUFCMA_RO{-FL_KU_DSS, -ERO, -O_CMA_Default, -O_METCR, -R_EUFCMARO_CRRO, -R_EUFCMARO_METCRRO, -Wrapped_Oracle, -RepO, -O_RMA_Default, -R_EUFCMARO_IEUFRMA, -QC_A, -Lazy.LRO, -ReproGame, -R_EUFRMA_IEUFRMA}. - - (* The adversary always terminates if the oracle procedures it can call terminate *) - declare axiom A_forge_ll (RO <: POracle{-A}) (SO <: DSS.KeyUpdating.SOracle_CMA{-A}) : - islossless RO.o => islossless SO.sign => islossless A(RO, SO).forge. - - (* The adversary makes a limited number of queries to the given random (hash) oracle and signing oracle *) - declare axiom A_forge_queries (RO <: POracle{-A, -QC_A}) (SO <: SOracle_CMA{-A, -QC_A}) : - hoare[A(QC_A(A, RO, SO).QC_RO, QC_A(A, RO, SO).QC_SO).forge : - QC_A.cH = 0 /\ QC_A.cS = 0 ==> QC_A.cH <= qH /\ QC_A.cS <= qS]. - - (* Convenient form of the above assumption (direct consequence) *) - local lemma A_forge_queries_init (RO <: POracle{-A, -QC_A}) (SO <: SOracle_CMA{-A, -QC_A}): - hoare[QC_A(A, RO, SO).forge : true ==> QC_A.cH <= qH /\ QC_A.cS <= qS]. - proof. - proc; sp. - call (A_forge_queries RO SO). - by skip. - qed. - - - (* - Auxiliary oracles - *) - local module O_CMA_CC = { - var sk : sk_al_t - var qs : msg_al_t list - var comps : (msg_fl_t * (rco_t * aux_t * msg_al_t)) list - - proc init(sk_init : sk_al_t) : unit = { - sk <- sk_init; - qs <- []; - comps <- []; - } - - proc sign(m : msg_al_t) : sig_al_t = { - var rco : rco_t; - var aux : aux_t; - var cm : msg_fl_t; - var sigfl : sig_fl_t; - var sig : sig_al_t; - - rco <$ drco; - aux <- extr_aux_sign sk; - - cm <@ MCO.o((rco, aux, m)); - - (sigfl, sk) <@ FL_KU_DSS.sign(sk, cm); - - sig <- (rco, sigfl); - - comps <- rcons comps (cm, (rco, aux, m)); - qs <- rcons qs m; - - return sig; - } - - proc fresh(m : msg_al_t) : bool = { - return ! m \in qs; - } - - proc nr_queries() : int = { - return size qs; - } - - proc compressions() : (msg_fl_t * (rco_t * aux_t * msg_al_t)) list = { - return comps; - } - }. - - local module O_CMA_CC_NoRepro = { - include var O_CMA_CC [-sign] - - proc sign(m : msg_al_t) : sig_al_t = { - var rco : rco_t; - var aux : aux_t; - var cm : msg_fl_t; - var sigfl : sig_fl_t; - var sig : sig_al_t; - - rco <$ drco; - aux <- extr_aux_sign sk; - - cm <$ dmsg_fl; - - cm <@ Wrapped_Oracle(MCO).o((rco, aux, m)); - - (sigfl, sk) <@ FL_KU_DSS.sign(sk, cm); - - sig <- (rco, sigfl); - - comps <- rcons comps (cm, (rco, aux, m)); - qs <- rcons qs m; - - return sig; - } - }. - - local module O_CMA_CC_ReproSample = { - include var O_CMA_CC [-sign] - - proc sign(m : msg_al_t) : sig_al_t = { - var rco : rco_t; - var aux : aux_t; - var cm : msg_fl_t; - var sigfl : sig_fl_t; - var sig : sig_al_t; - - rco <$ drco; - aux <- extr_aux_sign sk; - cm <$ dmsg_fl; - - Wrapped_Oracle(MCO).set((rco, aux, m), cm); - cm <@ Wrapped_Oracle(MCO).o((rco, aux, m)); - - (sigfl, sk) <@ FL_KU_DSS.sign(sk, cm); - - sig <- (rco, sigfl); - - comps <- rcons comps (cm, (rco, aux, m)); - qs <- rcons qs m; - - return sig; - } - }. - - local module O_CMA_CC_ReproQuery = { - include var O_CMA_CC [-init, sign] - - proc init() = { - qs <- []; - comps <- []; - } - - proc sign(m : msg_al_t) : sig_al_t = { - var rco : rco_t; - var aux : aux_t; - var cm : msg_fl_t; - var sigfl : sig_fl_t; - var sig : sig_al_t; - - rco <$ drco; - aux <- extr_aux_sign sk; - - (cm, sigfl) <@ O_RMA_Default(FL_KU_DSS).sign(); - - Wrapped_Oracle(MCO).set((rco, aux, m), cm); - cm <@ Wrapped_Oracle(MCO).o((rco, aux, m)); - - sig <- (rco, sigfl); - - comps <- rcons comps (cm, (rco, aux, m)); - qs <- rcons qs m; - - return sig; - } - }. - - - (* - Auxiliary games - *) - local module EUF_CMA_RO_CC = { - var coll : bool - - proc main() = { - var pk : pk_al_t; - var sk : sk_al_t; - var m : msg_al_t; - var sig : sig_al_t; - var is_valid, is_fresh : bool; - var rco : rco_t; - var cm : msg_fl_t; - var comps : (msg_fl_t * (rco_t * msg_al_t)) list; - - MCO.init(); - - (pk, sk) <@ AL_KU_DSS(FL_KU_DSS, MCO).keygen(); - - O_CMA_CC.init(sk); - - (m, sig) <@ A(MCO, O_CMA_CC).forge(pk); - - is_valid <@ AL_KU_DSS(FL_KU_DSS, MCO).verify(pk, m, sig); - - is_fresh <@ O_CMA_CC.fresh(m); - - rco <- sig.`1; - cm <@ MCO.o(rco, m); - comps <@ O_CMA_CC.compressions(); - - coll <- assoc comps cm <> None; - - return is_valid /\ is_fresh; - } - }. - - local module EUF_CMA_RO_CC_NoRepro = { - var coll : bool - - proc main() = { - var pk : pk_al_t; - var sk : sk_al_t; - var m : msg_al_t; - var sig : sig_al_t; - var is_valid, is_fresh : bool; - var rco : rco_t; - var cm : msg_fl_t; - var sigfl : sig_fl_t; - var comps : (msg_fl_t * (rco_t * msg_al_t)) list; - - MCO.init(); - Wrapped_Oracle(MCO).init(); - - (pk, sk) <@ AL_KU_DSS(FL_KU_DSS, MCO).keygen(); - - O_CMA_CC_NoRepro.init(sk); - - (m, sig) <@ A(Wrapped_Oracle(MCO), O_CMA_CC_NoRepro).forge(pk); - - rco <- sig.`1; - sigfl <- sig.`2; - cm <@ Wrapped_Oracle(MCO).o(rco, m); - - is_valid <@ FL_KU_DSS.verify(pk, cm, sigfl); - - is_fresh <@ O_CMA_CC_NoRepro.fresh(m); - - comps <@ O_CMA_CC_NoRepro.compressions(); - - coll <- assoc comps cm <> None; - - return is_valid /\ is_fresh; - } - }. - - local module EUF_CMA_RO_CC_ReproSample = { - var coll : bool - - proc main() = { - var pk : pk_al_t; - var sk : sk_al_t; - var m : msg_al_t; - var sig : sig_al_t; - var is_valid, is_fresh : bool; - var rco : rco_t; - var cm : msg_fl_t; - var sigfl : sig_fl_t; - var comps : (msg_fl_t * (rco_t * msg_al_t)) list; - - MCO.init(); - Wrapped_Oracle(MCO).init(); - - (pk, sk) <@ AL_KU_DSS(FL_KU_DSS, MCO).keygen(); - - O_CMA_CC_ReproSample.init(sk); - - (m, sig) <@ A(Wrapped_Oracle(MCO), O_CMA_CC_ReproSample).forge(pk); - - rco <- sig.`1; - sigfl <- sig.`2; - cm <@ Wrapped_Oracle(MCO).o(rco, m); - - is_valid <@ FL_KU_DSS.verify(pk, cm, sigfl); - - is_fresh <@ O_CMA_CC_ReproSample.fresh(m); - - comps <@ O_CMA_CC_ReproSample.compressions(); - - coll <- assoc comps cm <> None; - - return is_valid /\ is_fresh; - } - }. - - local module EUF_CMA_RO_CC_ReproQuery = { - var coll : bool - - proc main() = { - var pk : pk_al_t; - var sk : sk_al_t; - var m : msg_al_t; - var sig : sig_al_t; - var is_valid, is_fresh : bool; - var rco : rco_t; - var cm : msg_fl_t; - var sigfl : sig_fl_t; - var comps : (msg_fl_t * (rco_t * msg_al_t)) list; - var nrqs : int; - - MCO.init(); - Wrapped_Oracle(MCO).init(); - - (pk, sk) <@ AL_KU_DSS(FL_KU_DSS, MCO).keygen(); - - O_RMA_Default(FL_KU_DSS).init(sk); - O_CMA_CC_ReproQuery.init(); - - (m, sig) <@ QC_A(A, Wrapped_Oracle(MCO), O_CMA_CC_ReproQuery).forge(pk); - - rco <- sig.`1; - sigfl <- sig.`2; - cm <@ Wrapped_Oracle(MCO).o(rco, m); - - is_valid <@ FL_KU_DSS.verify(pk, cm, sigfl); - - is_fresh <@ O_CMA_CC_ReproQuery.fresh(m); - - comps <@ O_CMA_CC_ReproSample.compressions(); - - coll <- assoc comps cm <> None; - - nrqs <@ O_CMA_CC_ReproQuery.nr_queries(); - - return nrqs <= qS /\ is_valid /\ is_fresh; - } - }. - - - (* - Auxiliary reduction adversaries - *) - local module (R_Repro_EUFCMARORepro : DistA) (WMCO : POracle, RepWMCO : RepO_t) = { - module O_R_Repro_EUFCMARORepro = { - include var O_CMA_CC [-sign] - - proc sign(m : msg_al_t) : sig_al_t = { - var rco : rco_t; - var cm : msg_fl_t; - var sigfl : sig_fl_t; - var sig : sig_al_t; - - (rco, m) <@ RepWMCO.repro(dmap drco (fun (rco : rco_t) => (rco, m))); - - cm <@ WMCO.o((rco, m)); - - (sigfl, sk) <@ FL_KU_DSS.sign(sk, cm); - - sig <- (rco, sigfl); - - comps <- rcons comps (cm, (rco, m)); - qs <- rcons qs m; - - return sig; - } - } - - proc distinguish() : bool = { - var pk : pk_al_t; - var sk : sk_al_t; - var m : msg_al_t; - var sig : sig_al_t; - var is_valid, is_fresh : bool; - var rco : rco_t; - var cm : msg_fl_t; - var sigfl : sig_fl_t; - var comps : (msg_fl_t * (rco_t * msg_al_t)) list; - var coll : bool; - - (pk, sk) <@ AL_KU_DSS(FL_KU_DSS, MCO).keygen(); - - O_R_Repro_EUFCMARORepro.init(sk); - - (m, sig) <@ QC_A(A, WMCO, O_R_Repro_EUFCMARORepro).forge(pk); - - rco <- sig.`1; - sigfl <- sig.`2; - cm <@ WMCO.o(rco, m); - - is_valid <@ FL_KU_DSS.verify(pk, cm, sigfl); - - is_fresh <@ O_R_Repro_EUFCMARORepro.fresh(m); - - comps <@ O_R_Repro_EUFCMARORepro.compressions(); - - coll <- assoc comps cm <> None; - - return is_valid /\ is_fresh /\ !coll; - } - }. - - - (* - Steps - *) - (* - Equivalence between original EUF-CMA game for the arbitrary-length digital - signature scheme and the auxiliary EUF_CMA_RO_CC game - *) - local equiv Equiv_EUFCMARO_EUFCMAROCC : - EUF_CMA_RO(AL_KU_DSS(FL_KU_DSS), A, O_CMA_Default, MCO).main ~ EUF_CMA_RO_CC.main : ={glob FL_KU_DSS, glob A} ==> ={res}. - proof. - proc; inline *. - seq 19 20 : (={is_valid, is_fresh}); last by wp. - seq 8 9 : (={glob FL_KU_DSS, pk, m, sig, ERO.m} /\ ={qs}(O_Base_Default, O_CMA_CC)); last by sim. - call (: ={glob FL_KU_DSS, ERO.m} - /\ ={qs}(O_Base_Default, O_CMA_CC) - /\ ={sk}(O_CMA_Default, O_CMA_CC)); 2: by proc. - + proc; inline{1} 1. - by wp; call (: true); call (: ={ERO.m}); auto. - by wp; call (: true); while (={w, ERO.m}); auto. - qed. - - (* - Given an adversary playing in the EUF_CAM_RO_CC game that wins and provides a forgery - that allows for the extraction of a collision for the message compression RO, we can - construct a reduction adversary against CR of the message compression RO - *) - local lemma EUFCMAROCC_CRRO &m: - Pr[EUF_CMA_RO_CC.main() @ &m : res /\ EUF_CMA_RO_CC.coll] - <= - Pr[CR_RO(R_EUFCMARO_CRRO(FL_KU_DSS, A), MCO).main() @ &m : res]. - proof. - byequiv => //. - proc; inline{1} 6; inline{2} 2. - conseq (: _ ==> is_fresh{1} /\ EUF_CMA_RO_CC.coll{1} => kx{2} <> kx'{2} /\ y{2} = y'{2}); 1: by smt(). - seq 4 4 : ( ={sk, comps}(O_CMA_CC, R_EUFCMARO_CRRO.O_CMA_R_EUFCMARO_CRRO) - /\ (glob MCO){1} = (glob ERO){2} - /\ m{1} = mal'{2} - /\ sig{1} = sig'{2} - /\ (forall (mfl : msg_fl_t) (rmal : rco_t * msg_al_t), (mfl, rmal) \in O_CMA_CC.comps{1} - => mfl = oget (MCO.m{1}.[rmal])) - /\ (forall (msg : msg_fl_t), assoc O_CMA_CC.comps{1} msg <> None - => (oget (assoc O_CMA_CC.comps{1} msg)).`2 \in O_CMA_CC.qs{1})). - + call (: ={glob FL_KU_DSS} - /\ ={sk, comps}(O_CMA_CC, R_EUFCMARO_CRRO.O_CMA_R_EUFCMARO_CRRO) - /\ (glob MCO){1} = (glob ERO){2} - /\ (forall (mfl : msg_fl_t) (rmal : rco_t * msg_al_t), (mfl, rmal) \in O_CMA_CC.comps{1} - => mfl = oget (MCO.m{1}.[rmal])) - /\ (forall (msg : msg_fl_t), assoc O_CMA_CC.comps{1} msg <> None - => (oget (assoc O_CMA_CC.comps{1} msg)).`2 \in O_CMA_CC.qs{1})). - - proc; inline *. - wp; call (: true); wp; rnd; skip => /> &1 &2 comps_def compsqs_rel rco _. - split => [mfl rmal | mfl]; rewrite mem_rcons /=. - * by move=> -[[-> <-] //|]; apply comps_def. - rewrite -cats1 assoc_cat. - case (mfl \in unzip1 R_EUFCMARO_CRRO.O_CMA_R_EUFCMARO_CRRO.comps{2}) => assin. - * by move/compsqs_rel => ->. - by move/assocTP => /= ->; rewrite assoc_cons. - - by proc; skip. - inline{1} 3; inline{2} 3. - wp; call (: true). - call (: true ==> (glob MCO){1} = (glob ERO){2}); last by skip. - proc. - by while (={w, ERO.m}); auto. - inline *; wp. - call{1} (: true ==> true); 1: by apply FL_KU_DSS_verify_ll. - wp; skip => /> &1 &2 comps_def compsqs_rel malnin assnnone. - split; 1: by rewrite negb_and; right => /#. - pose cm := oget ERO.m{2}.[sig'{2}.`1, mal'{2}]. - move: (comps_def cm (oget (assoc R_EUFCMARO_CRRO.O_CMA_R_EUFCMARO_CRRO.comps{2} cm)) _). - + by move/assocTP: assnnone; apply assoc_get_mem. - by move=> {3}-> /#. - qed. - - (* - Given an adversary playing in the EUF_CAM_RO_CC game that wins and provides a forgery - that allows for the extraction of a collision for the message compression RO, we can - construct a reduction adversary against M-eTCR of the message compression RO - *) - local lemma EUFCMAROCC_METCRRO &m: - Pr[EUF_CMA_RO_CC.main() @ &m : res /\ EUF_CMA_RO_CC.coll] - <= - Pr[M_ETCR_RO(R_EUFCMARO_METCRRO(FL_KU_DSS, A), O_METCR, MCO).main() @ &m : res]. - proof. - byequiv => //. - proc; inline{2} 3. - conseq (: _ ==> is_fresh{1} /\ EUF_CMA_RO_CC.coll{1} => 0 <= i{2} < nrts{2} /\ x{2} <> x'{2} /\ y{2} = y'{2}); 1: by smt(). - seq 4 5 : ( ={sk, comps}(O_CMA_CC, R_EUFCMARO_METCRRO.O_CMA_R_EUFCMARO_METCRRO) - /\ (glob MCO){1} = (glob ERO){2} - /\ m{1} = mal'{2} - /\ sig{1} = sig'{2} - /\ unzip2 R_EUFCMARO_METCRRO.O_CMA_R_EUFCMARO_METCRRO.comps{2} = O_METCR.ts{2} - /\ (forall (mfl : msg_fl_t) (rmal : rco_t * msg_al_t), (mfl, rmal) \in O_CMA_CC.comps{1} - => mfl = oget (MCO.m{1}.[rmal])) - /\ (forall (msg : msg_fl_t), assoc O_CMA_CC.comps{1} msg <> None - => (oget (assoc O_CMA_CC.comps{1} msg)).`2 \in O_CMA_CC.qs{1})). - + call (: ={glob FL_KU_DSS} - /\ ={sk, comps}(O_CMA_CC, R_EUFCMARO_METCRRO.O_CMA_R_EUFCMARO_METCRRO) - /\ (glob MCO){1} = (glob ERO){2} - /\ unzip2 R_EUFCMARO_METCRRO.O_CMA_R_EUFCMARO_METCRRO.comps{2} = O_METCR.ts{2} - /\ (forall (mfl : msg_fl_t) (rmal : rco_t * msg_al_t), (mfl, rmal) \in O_CMA_CC.comps{1} - => mfl = oget (MCO.m{1}.[rmal])) - /\ (forall (msg : msg_fl_t), assoc O_CMA_CC.comps{1} msg <> None - => (oget (assoc O_CMA_CC.comps{1} msg)).`2 \in O_CMA_CC.qs{1})). - - proc; inline *. - wp; call (: true); wp; rnd; wp; skip => /> &1 &2 comps_def compsqs_rel rco _. - split; last split => [ mfl rmal | mfl]. - * by rewrite map_rcons. - * by rewrite mem_rcons /= => -[[-> <-] // |]; apply comps_def. - rewrite mem_rcons -cats1 assoc_cat /=. - case (mfl \in unzip1 R_EUFCMARO_METCRRO.O_CMA_R_EUFCMARO_METCRRO.comps{2}) => assin. - * by move/compsqs_rel => ->. - by move/assocTP => /= ->; rewrite assoc_cons. - - by proc; skip. - inline *. - wp; call (: true). - by while (={w, ERO.m}); auto. - inline *; wp. - call{1} (: true ==> true); 1: by apply FL_KU_DSS_verify_ll. - wp; skip => /> &1 &2 comps_def compsqs_rel malnin assnnone. - split; 1: split => [| _]; 1: by rewrite index_ge0. - + have ->: - size (unzip2 R_EUFCMARO_METCRRO.O_CMA_R_EUFCMARO_METCRRO.comps{2}) - = - size (unzip1 R_EUFCMARO_METCRRO.O_CMA_R_EUFCMARO_METCRRO.comps{2}). - - by rewrite 2!size_map. - by rewrite index_mem -assocTP. - split; 1: by rewrite nth_onth -assoc_zip 1:2!size_map // zip_unzip /#. - pose cm := oget ERO.m{2}.[sig'{2}.`1, mal'{2}]. - move: (comps_def cm (oget (assoc R_EUFCMARO_METCRRO.O_CMA_R_EUFCMARO_METCRRO.comps{2} cm)) _). - + by move/assocTP: assnnone; apply assoc_get_mem. - move=> {3}->; congr; congr. - rewrite eq_sym -{1}(zip_unzip R_EUFCMARO_METCRRO.O_CMA_R_EUFCMARO_METCRRO.comps{2}). - by rewrite assoc_zip 1:2!size_map // nth_onth /oget /#. - qed. - - (* - The probability of an adversary winning the EUF_CMA_RO_CC game and providing a forgery - that does not allow for the extraction of a collision for the message compression RO - is equal to the probability of the analogous event in the EUF_CMA_RO_CC_NoRepro game - *) - local lemma EUFCMAROCC_EUFCMAROCCNoRepro &m : - Pr[EUF_CMA_RO_CC.main() @ &m : res /\ !EUF_CMA_RO_CC.coll] = - Pr[EUF_CMA_RO_CC_NoRepro.main() @ &m : res /\ !EUF_CMA_RO_CC_NoRepro.coll]. - proof. - byequiv => //. - proc; inline *. - wp; call (: true); wp => /=. - call (: ={glob O_CMA_CC, glob MCO} /\ Wrapped_Oracle.prog_list{2} = []). - + proc; inline *. - wp; call (: true); wp => /=. - rnd{2}; rnd. - by skip. - + proc; inline *. - by wp; skip. - wp; call (: true); wp => /=. - while (={w, ERO.m}); 1: by auto. - by wp; skip. - qed. - - (* - Distinguishing between reprogramming and not reprogramming the message compression - RO can be reduced to distinguishing between EUF_CMA_RO_CC_NoRepro (with no collision - extraction) and EUF_CMA_RO_CC_ReproSample (with no collision extraction). - *) - local lemma EUFCMARORepro_ReproGame &m: - `| Pr[EUF_CMA_RO_CC_NoRepro.main() @ &m : res /\ !EUF_CMA_RO_CC_NoRepro.coll] - - Pr[EUF_CMA_RO_CC_ReproSample.main() @ &m : res /\ !EUF_CMA_RO_CC_ReproSample.coll] | - = - `| Pr[ReproGame(MCO, R_Repro_EUFCMARORepro).main(false) @ &m : res] - - Pr[ReproGame(MCO, R_Repro_EUFCMARORepro).main(true) @ &m : res] |. - proof. - do 2! congr; last congr. - + byequiv => //. - proc; inline *. - wp; call (: true); wp => /=. - call (: ={glob FL_KU_DSS, glob O_CMA_CC, Wrapped_Oracle.prog_list} - /\ RepO.b{2} = false - /\ Wrapped_Oracle.prog_list{2} = []). - - proc; inline *. - rcondf{2} 7; 1: by auto. - wp; call (: true); wp => /=. - rnd{1}. - rnd (fun (rco : rco_t) => (rco, m{2})) - (fun (kx : rco_t * msg_al_t) => kx.`1). - wp; skip => /> &1. - split => [rcom | rcomeq]. - * by move/supp_dmap => [rco] [_ ->]. - split => [rcom rcomin | rcom_mu1 rco rcoin]. - * by rewrite (in_dmap1E_can _ _ (fun (x : _ * _) => x.`1)) //= /#. - by rewrite supp_dmap; exists rco; rewrite rcoin. - - proc; inline *. - by wp; skip. - wp; call (: true); wp; while (={w, ERO.m}). - - by wp; rnd; wp; skip. - by wp; skip. - byequiv => //. - proc; inline *. - wp; call (: true); wp => /=. - call (: ={glob FL_KU_DSS, glob O_CMA_CC, Wrapped_Oracle.prog_list} - /\ RepO.b{2} = true). - + proc; inline *. - rcondt{2} 7; 1: by auto. - wp; call (: true); wp => /=. - rnd. - rnd (fun (rco : rco_t) => (rco, m{2})) - (fun (kx : rco_t * msg_al_t) => kx.`1). - wp; skip => /> &1. - split => [rcom | rcomeq]. - * by move/supp_dmap => [rco] [_ ->]. - split => [rcom rcomin | rcom_mu1 rco rcoin]. - * by rewrite (in_dmap1E_can _ _ (fun (x : _ * _) => x.`1)) //= /#. - by rewrite supp_dmap; exists rco; rewrite rcoin. - + proc; inline *. - by wp; skip. - wp; call (: true); wp; while (={w, ERO.m}). - + by wp; rnd; wp; skip. - by wp; skip. - qed. - - (* Limit on the number of queries the reduction adversary against ReproGame makes *) - local hoare R_Repro_EUFCMARORepro_Queries : - R_Repro_EUFCMARORepro(Wrapped_Oracle(MCO), RepO(Wrapped_Oracle(MCO))).distinguish : - Wrapped_Oracle.ch = 0 /\ RepO.ctr = 0 /\ RepO.se - ==> - Wrapped_Oracle.ch <= qS + qH + 1 /\ RepO.ctr <= qS /\ RepO.se. - proof. - proc. - wp. - do 3! (call (: true) => //). - inline 6; inline 7. - wp => /=. - call (: Wrapped_Oracle.ch = 0 /\ RepO.ctr = 0 /\ RepO.se - ==> - QC_A.cH <= qH /\ QC_A.cS <= qS - /\ Wrapped_Oracle.ch = QC_A.cH + QC_A.cS /\ RepO.ctr = QC_A.cS /\ RepO.se). - + conseq (: Wrapped_Oracle.ch = 0 /\ RepO.ctr = 0 /\ RepO.se - ==> - Wrapped_Oracle.ch = QC_A.cH + QC_A.cS /\ RepO.ctr = QC_A.cS /\ RepO.se) - (: true ==> QC_A.cH <= qH /\ QC_A.cS <= qS) => //. - - by apply: (A_forge_queries_init (Wrapped_Oracle(ERO)) (<: R_Repro_EUFCMARORepro(Wrapped_Oracle(ERO), RepO(Wrapped_Oracle(ERO))).O_R_Repro_EUFCMARORepro)). - proc. - call (: Wrapped_Oracle.ch = QC_A.cH + QC_A.cS /\ RepO.ctr = QC_A.cS /\ RepO.se). - - proc; inline *. - wp; call (: true); wp => /=. - case RepO.b. - * rcondt 7; 1: by auto. - wp. - rnd; rnd. - wp; skip => /> &1 seT bT rcom _ cm _. - split => [/# |]. - by rewrite p_max_rcom. - rcondf 7; 1: by auto. - rnd. - wp; skip => /> &1 se b rcom _. - split => [/# |]. - by rewrite p_max_rcom. - - proc; inline *. - by wp; skip => /#. - by wp; skip. - do 2! (call(: true) => //). - by skip => /#. - qed. - - (* - The probability of an adversary winning the EUF_CMA_RO_CC_ReproSample game and providing - a forgery that does not allow for the extraction of a collision for the message - compression RO is equal to the probability of the analogous event in the - EUF_CMA_RO_CC_ReproQuery game - *) - local lemma EUFRMAROCCReproSample_Query &m: - Pr[EUF_CMA_RO_CC_ReproSample.main() @ &m : res /\ !EUF_CMA_RO_CC_ReproSample.coll] - = - Pr[EUF_CMA_RO_CC_ReproQuery.main() @ &m : res /\ !EUF_CMA_RO_CC_ReproQuery.coll]. - proof. - byequiv => //. - proc. - seq 5 6 : ( ={glob FL_KU_DSS, O_CMA_CC.comps, O_CMA_CC.qs, MCO.m, Wrapped_Oracle.prog_list, pk, m, sig} - /\ QC_A.cS{2} = size O_CMA_CC.qs{2} - /\ QC_A.cS{2} <= qS). - + call (: ={glob FL_KU_DSS, glob A, O_CMA_CC.comps, O_CMA_CC.qs, MCO.m, Wrapped_Oracle.prog_list, pk} - /\ ={sk}(O_CMA_CC, O_RMA_Default) - /\ O_CMA_CC.qs{2} = [] - ==> - ={res, glob FL_KU_DSS, O_CMA_CC.comps, O_CMA_CC.qs, MCO.m, Wrapped_Oracle.prog_list} - /\ ={sk}(O_CMA_CC, O_RMA_Default) - /\ QC_A.cS{2} = size O_CMA_CC.qs{2} - /\ QC_A.cS{2} <= qS). - - conseq (: ={arg, glob FL_KU_DSS, glob A, O_CMA_CC.comps, O_CMA_CC.qs, MCO.m, Wrapped_Oracle.prog_list} - /\ ={sk}(O_CMA_CC, O_RMA_Default) - /\ O_CMA_CC.qs{2} = [] - ==> - ={res, glob FL_KU_DSS, O_CMA_CC.comps, O_CMA_CC.qs, MCO.m, Wrapped_Oracle.prog_list} - /\ ={sk}(O_CMA_CC, O_RMA_Default) - /\ QC_A.cS{2} = size O_CMA_CC.qs{2}) - _ - (: true ==> QC_A.cH <= qH /\ QC_A.cS <= qS) => //. - * by apply (A_forge_queries_init (Wrapped_Oracle(MCO)) O_CMA_CC_ReproQuery). - proc *; inline *. - wp. - call (: ={glob FL_KU_DSS, O_CMA_CC.comps, O_CMA_CC.qs, MCO.m, Wrapped_Oracle.prog_list} - /\ ={sk}(O_CMA_CC, O_RMA_Default) - /\ QC_A.cS{2} = size O_CMA_CC.qs{2}). - * proc; inline *. - wp; call (: true); wp => /=. - rnd; rnd. - by wp; skip => />; smt(size_rcons). - * proc; inline *. - by wp; skip. - by wp; skip => /> /#. - inline *. - wp; call (: true); wp => /=. - while (={w, ERO.m}); 1: by auto. - by wp; skip. - inline *. - wp; call(: true); wp => /=. - by skip => />. - qed. - - (* - Given an adversary playing in the EUF_CMA_RO_CC_ReproQuery game that wins and provides - a forgery that does not allow for the extraction of a collision for the - message compression RO, we can construct a reduction adversary against - the interactive variant of EUF-RMA for the considered fixed-length digital - signature scheme - *) - local lemma EUFRMAROCCReproQuery_IEUFRMA &m : - Pr[EUF_CMA_RO_CC_ReproQuery.main() @ &m : res /\ !EUF_CMA_RO_CC_ReproQuery.coll] - <= - Pr[I_EUF_RMA(FL_KU_DSS, R_EUFCMARO_IEUFRMA(A), O_RMA_Default).main() @ &m : res]. - proof. - byequiv => //. - proc; inline *. - wp => /=. call (: true); wp => /=. - call (: ={glob FL_KU_DSS, MCO.m, Wrapped_Oracle.prog_list, O_RMA_Default.sk} - /\ ={qs, comps}(O_CMA_CC, R_EUFCMARO_IEUFRMA.O_CMA_R_EUFCMARO_IEUFRMA) - /\ size R_EUFCMARO_IEUFRMA.O_CMA_R_EUFCMARO_IEUFRMA.qs{2} = size DSS_FL.O_Base_Default.qs{2} - /\ (forall (cm : msg_fl_t) - (! exists (m : msg_al_t) (rco : rco_t), (cm, (rco, m)) \in R_EUFCMARO_IEUFRMA.O_CMA_R_EUFCMARO_IEUFRMA.comps{2}) - => - ! cm \in DSS_FL.O_Base_Default.qs{2})). - + proc; inline *. - wp; call (: true) => /=. - rnd; rnd. - wp; skip => /> &2 eqsz ninqs rco rcoin cm cmin. - rewrite 2!size_rcons eqsz assoc_cons /= => cm'. - rewrite mem_rcons /= negb_or => nex; split. - - move: nex; apply contra => ->. - by exists m{2} rco; rewrite mem_rcons. - apply ninqs; rewrite negb_exists => m /=; rewrite negb_exists => rco' /=. - move: nex; rewrite negb_exists => /(_ m) /=; rewrite negb_exists => /(_ rco') /=. - by rewrite mem_rcons /= negb_or => [#]. - + proc; inline *. - by wp; skip. - swap{1} 6 -5. - wp. - while (={w, ERO.m}); 1: by auto. - wp; call(: true); wp => /=. - skip => /> cmap msig comps' qs qs' plist eqsz ninqsp ver ltqS_szqs verT ninqs. - pose ifte := if _ then _ else _; move=> eqnone. - split; 1: by rewrite -eqsz; smt(rng_qS). - by apply: ninqsp; rewrite negb_exists /= => m; rewrite negb_exists /= => rco; smt(assoc_none). - qed. - - - (* - Security theorems (1/2) - *) - (* Security theorem with CR and interactive EUF-RMA *) - lemma ALKUDSS_EUFCMARO_CRRO_IEUFRMA &m : - Pr[EUF_CMA_RO(AL_KU_DSS(FL_KU_DSS), A, O_CMA_Default, MCO).main() @ &m : res] - <= - Pr[CR_RO(R_EUFCMARO_CRRO(FL_KU_DSS, A), MCO).main() @ &m : res] - + - Pr[I_EUF_RMA(FL_KU_DSS, R_EUFCMARO_IEUFRMA(A), O_RMA_Default).main() @ &m : res] - + - qS%r * (qS + qH + 1)%r * mu1 drco witness. - proof. - have ->: - Pr[EUF_CMA_RO(AL_KU_DSS(FL_KU_DSS), A, O_CMA_Default, MCO).main() @ &m : res] - = - Pr[EUF_CMA_RO_CC.main() @ &m : res]. - + by byequiv Equiv_EUFCMARO_EUFCMAROCC. - rewrite Pr[mu_split EUF_CMA_RO_CC.coll] -addrA ler_add 1:EUFCMAROCC_CRRO. - rewrite EUFCMAROCC_EUFCMAROCCNoRepro -ger0_norm 1:Pr[mu_ge0] // -subr0. - rewrite -(subrr Pr[EUF_CMA_RO_CC_ReproSample.main() @ &m : res /\ !EUF_CMA_RO_CC_ReproSample.coll]). - rewrite opprB (addrC Pr[EUF_CMA_RO_CC_ReproSample.main() @ &m : res /\ !EUF_CMA_RO_CC_ReproSample.coll]) addrA. - apply (ler_trans (`| Pr[EUF_CMA_RO_CC_NoRepro.main() @ &m : res /\ !EUF_CMA_RO_CC_NoRepro.coll] - - Pr[EUF_CMA_RO_CC_ReproSample.main() @ &m : res /\ !EUF_CMA_RO_CC_ReproSample.coll] | - + Pr[EUF_CMA_RO_CC_ReproSample.main() @ &m : res /\ !EUF_CMA_RO_CC_ReproSample.coll])). - + by rewrite -{4}(ger0_norm Pr[EUF_CMA_RO_CC_ReproSample.main() @ &m : res /\ !EUF_CMA_RO_CC_ReproSample.coll]) 1:Pr[mu_ge0]; smt(ler_norm_add). - rewrite addrC ler_add. - + by rewrite EUFRMAROCCReproSample_Query EUFRMAROCCReproQuery_IEUFRMA. - apply (ler_trans `| Pr[ReproGame(ERO, R_Repro_EUFCMARORepro).main(false) @ &m : res] - - Pr[ReproGame(ERO, R_Repro_EUFCMARORepro).main(true) @ &m : res] |). - + by rewrite EUFCMARORepro_ReproGame. - apply (rom_reprogramming R_Repro_EUFCMARORepro _ _ _ _ &m R_Repro_EUFCMARORepro_Queries). - + by move: rng_qS => [->]. - by smt(rng_qS ge0_qH). - qed. - - (* Security theorem with M-eTCR and interactive EUF-RMA *) - lemma ALKUDSS_EUFCMARO_METCRRO_IEUFRMA &m : - Pr[EUF_CMA_RO(AL_KU_DSS(FL_KU_DSS), A, O_CMA_Default, MCO).main() @ &m : res] - <= - Pr[M_ETCR_RO(R_EUFCMARO_METCRRO(FL_KU_DSS, A), O_METCR, MCO).main() @ &m : res] - + - Pr[I_EUF_RMA(FL_KU_DSS, R_EUFCMARO_IEUFRMA(A), O_RMA_Default).main() @ &m : res] - + - qS%r * (qS + qH + 1)%r * mu1 drco witness. - proof. - have ->: - Pr[EUF_CMA_RO(AL_KU_DSS(FL_KU_DSS), A, O_CMA_Default, MCO).main() @ &m : res] - = - Pr[EUF_CMA_RO_CC.main() @ &m : res]. - + by byequiv Equiv_EUFCMARO_EUFCMAROCC. - rewrite Pr[mu_split EUF_CMA_RO_CC.coll] -addrA ler_add 1:EUFCMAROCC_METCRRO. - rewrite EUFCMAROCC_EUFCMAROCCNoRepro -ger0_norm 1:Pr[mu_ge0] // -subr0. - rewrite -(subrr Pr[EUF_CMA_RO_CC_ReproSample.main() @ &m : res /\ !EUF_CMA_RO_CC_ReproSample.coll]). - rewrite opprB (addrC Pr[EUF_CMA_RO_CC_ReproSample.main() @ &m : res /\ !EUF_CMA_RO_CC_ReproSample.coll]) addrA. - apply (ler_trans (`| Pr[EUF_CMA_RO_CC_NoRepro.main() @ &m : res /\ !EUF_CMA_RO_CC_NoRepro.coll] - - Pr[EUF_CMA_RO_CC_ReproSample.main() @ &m : res /\ !EUF_CMA_RO_CC_ReproSample.coll] | - + Pr[EUF_CMA_RO_CC_ReproSample.main() @ &m : res /\ !EUF_CMA_RO_CC_ReproSample.coll])). - + by rewrite -{4}(ger0_norm Pr[EUF_CMA_RO_CC_ReproSample.main() @ &m : res /\ !EUF_CMA_RO_CC_ReproSample.coll]) 1:Pr[mu_ge0]; smt(ler_norm_add). - rewrite addrC; apply ler_add. - + by rewrite EUFRMAROCCReproSample_Query EUFRMAROCCReproQuery_IEUFRMA. - apply (ler_trans `| Pr[ReproGame(ERO, R_Repro_EUFCMARORepro).main(false) @ &m : res] - - Pr[ReproGame(ERO, R_Repro_EUFCMARORepro).main(true) @ &m : res] |). - + by rewrite EUFCMARORepro_ReproGame. - apply (rom_reprogramming R_Repro_EUFCMARORepro _ _ _ _ &m R_Repro_EUFCMARORepro_Queries). - + by move: rng_qS => [->]. - by smt(rng_qS ge0_qH). - qed. - - - (* - Additional declarations (for regular EUF-RMA) - *) - (* Models the signing procedure of FL-XMSS-TW *) - declare op opsign : sk_fl_t -> msg_fl_t -> sig_fl_t * sk_fl_t. - - (* - opsign precisely captures the semantics of the signing procedure of the - fixed-length digital signature scheme - *) - declare axiom FL_KU_DSS_sign_fun (sk : sk_fl_t) (cm : msg_fl_t) : - hoare[FL_KU_DSS.sign: arg = (sk, cm) ==> res = opsign sk cm]. - - (* - The signing procedure of the fixed-length digital signature scheme always - terminates (and is captured by opsign) - *) - local lemma FL_KU_DSS_sign_pfun (sk : sk_fl_t) (cm : msg_fl_t) : - phoare[FL_KU_DSS.sign: arg = (sk, cm) ==> res = opsign sk cm] = 1%r. - proof. by conseq FL_KU_DSS_sign_ll (FL_KU_DSS_sign_fun sk cm). qed. - - (* - The key generation procedure of the fixed-length digital signature - scheme is stateless (i.e., it produces the same output distribution for - all initial memories) - *) - declare axiom FL_KU_DSS_keygen_stateless: - equiv[FL_KU_DSS.keygen ~ FL_KU_DSS.keygen: true ==> ={res}]. - - (* - The verification procedure of the fixed-length digital signature - scheme is stateless (i.e., for a certain input, it produces the same output - distribution for all inital memories) - *) - declare axiom FL_KU_DSS_verify_stateless: - equiv[FL_KU_DSS.verify ~ FL_KU_DSS.verify: ={arg} ==> ={res}]. - - - (* - Security theorems (2/2) - *) - (* Security theorem with CR and EUF-RMA *) - lemma ALKUDSS_EUFCMARO_CRRO_EUFRMA &m : - Pr[EUF_CMA_RO(AL_KU_DSS(FL_KU_DSS), A, O_CMA_Default, MCO).main() @ &m : res] - <= - Pr[CR_RO(R_EUFCMARO_CRRO(FL_KU_DSS, A), MCO).main() @ &m : res] - + - Pr[EUF_RMA(FL_KU_DSS, R_EUFRMA_IEUFRMA(R_EUFCMARO_IEUFRMA(A))).main() @ &m : res] - + - qS%r * (qS + qH + 1)%r * mu1 drco witness - + - n%r * mu1 dmsg_fl witness. - proof. - move: (I_EUFRMA_le_EUF_RMA (R_EUFCMARO_IEUFRMA(A)) _). - + move=> SO SOs_ll. - proc; inline *. - wp. - call (A_forge_ll (Wrapped_Oracle(MCO)) (<: R_EUFCMARO_IEUFRMA(A, SO).O_CMA_R_EUFCMARO_IEUFRMA)). - - proc; inline *. - by wp; skip. - - proc; inline *. - wp; call (SOs_ll); rnd; skip => />. - by apply drco_ll. - wp. - while (true) (size w). - - move=> z. - wp; rnd; wp; skip => /> &1 neqw. - split; 2: apply dmsg_fl_ll. - by move: neqw; case (w{1}) => // rcom rcoml _ /= /#. - by wp; skip => />; smt(size_ge0 size_eq0). - move=> /(_ FL_KU_DSS FL_KU_DSS_sign_ll FL_KU_DSS_verify_ll). - move=> /(_ opsign FL_KU_DSS_sign_fun FL_KU_DSS_keygen_stateless FL_KU_DSS_verify_stateless). - move=> /(_ (mu1 dmsg_fl witness) &m _). - + by move=> cm; rewrite ler_eqVlt; left; rewrite &(dmsg_fl_uni) dmsg_fl_fu. - by move: (ALKUDSS_EUFCMARO_CRRO_IEUFRMA &m) => /#. - qed. - - (* Security theorem with M-eTCR and EUF-RMA *) - lemma ALKUDSS_EUFCMARO_METCRRO_EUFRMA &m : - Pr[EUF_CMA_RO(AL_KU_DSS(FL_KU_DSS), A, O_CMA_Default, MCO).main() @ &m : res] - <= - Pr[M_ETCR_RO(R_EUFCMARO_METCRRO(FL_KU_DSS, A), O_METCR, MCO).main() @ &m : res] - + - Pr[EUF_RMA(FL_KU_DSS, R_EUFRMA_IEUFRMA(R_EUFCMARO_IEUFRMA(A))).main() @ &m : res] - + - qS%r * (qS + qH + 1)%r * mu1 drco witness - + - n%r * mu1 dmsg_fl witness. - proof. - move: (I_EUFRMA_le_EUF_RMA (R_EUFCMARO_IEUFRMA(A)) _). - + move=> SO SOs_ll. - proc; inline *. - wp. - call (A_forge_ll (Wrapped_Oracle(MCO)) (<: R_EUFCMARO_IEUFRMA(A, SO).O_CMA_R_EUFCMARO_IEUFRMA)). - - proc; inline *. - by wp; skip. - - proc; inline *. - wp; call (SOs_ll); rnd; skip => />. - by apply drco_ll. - wp. - while (true) (size w). - - move=> z. - wp; rnd; wp; skip => /> &1 neqw. - split; 2: apply dmsg_fl_ll. - by move: neqw; case (w{1}) => // rcom rcoml _ /= /#. - by wp; skip => />; smt(size_ge0 size_eq0). - move=> /(_ FL_KU_DSS FL_KU_DSS_sign_ll FL_KU_DSS_verify_ll). - move=> /(_ opsign FL_KU_DSS_sign_fun FL_KU_DSS_keygen_stateless FL_KU_DSS_verify_stateless). - move=> /(_ (mu1 dmsg_fl witness) &m _). - + by move=> cm; rewrite ler_eqVlt; left; rewrite &(dmsg_fl_uni) dmsg_fl_fu. - by move: (ALKUDSS_EUFCMARO_METCRRO_IEUFRMA &m) => /#. - qed. - - end section Proofs_EUFCMA_RO_ALKUDSS. - -end WithSampling. - - - -(* - --- - Hash-then-sign paradigm where the the randomness/indexing keys used for - message compression are generated (via a PRF) - --- -*) -theory WithPRF. - (* -- Clones and imports (1/2) -- *) - (* Hash-then-sign paradigm with sampling; used as basis *) - clone import WithSampling as WS - - proof *. - - - (* -- Types -- *) - (* - Seeds (i.e., indexing keys) for PRF that produces (pseudo)randomness - (i.e., indexing keys) for message compression - *) - type ms_t. - - (* - Identifiers (e.g., indices) contained in secret keys; used as input to PRF - *) - type id_t. - - (* - Secret keys; same as for fixed-length digital signature scheme but - extended with seed used for PRF - *) - type sk_al_t = ms_t * sk_fl_t. - - - (* -- Distributions -- *) - (* Proper distribution over seeds used for PRF *) - op [lossless] dms : ms_t distr. - - - (* -- Operators -- *) - (* Produces (pseudo)randomness/indexing keys given a seed and an identifier *) - op mkg : ms_t -> id_t -> rco_t. - - clone import KeyedHashFunctions as MKG with - type key_t <- ms_t - type in_t <- id_t - type out_t <- rco_t - - op f <- mkg - - proof *. - - clone import PRF as MKG_PRF with - op dkey <- dms - op doutm <- fun _ => drco - - proof *. - realize dkey_ll by exact: dms_ll. - realize doutm_ll by smt(drco_ll). - - (* Extracts identifier from a secret key of the fixed-length digital signature scheme *) - op extr_id : sk_fl_t -> id_t. - - - (* -- Clones and imports (2/2) -- *) - (* - Scheme specification and security notions - *) - (* - Arbitrary-length signature scheme (using a PRF and assuming message - compression function is a RO) - *) - clone import DigitalSignaturesROM as DSS_AL_PRF with - type pk_t <- pk_al_t - type sk_t <- sk_al_t - type msg_t <- msg_al_t - type sig_t <- sig_al_t - - type in_t <- rco_t * msg_al_t - type out_t <- msg_fl_t - type d_in_t <- int - type d_out_t <- bool - - op doutm <- fun _ => dmsg_fl - - proof *. - - import KeyUpdatingROM. - import DSS. - import KeyUpdating. - - - (* -- Arbitrary-length signature scheme -- *) - (* - Specification of arbitrary-length digital signature scheme based on the fixed-length - digital signature scheme (using a PRF and assuming the message compression function - is a RO) - *) - module (AL_KU_DSS(FL_KU_DSS : DSS_FL.KeyUpdating.Scheme) : Scheme_RO) (RO : POracle) = { - proc keygen() : pk_al_t * sk_al_t = { - var ms : ms_t; - var pk : pk_al_t; - var skfl : sk_fl_t; - var sk : sk_al_t; - - ms <$ dms; - - (pk, skfl) <@ FL_KU_DSS.keygen(); - - sk <- (ms, skfl); - - return (pk, sk); - } - - proc sign(sk : sk_al_t, m : msg_al_t) : sig_al_t * sk_al_t = { - var ms : ms_t; - var id : id_t; - var skfl : sk_fl_t; - var rco : rco_t; - var cm : msg_fl_t; - var sigfl : sig_fl_t; - var sig : sig_al_t; - - ms <- sk.`1; - skfl <- sk.`2; - - id <- extr_id skfl; - - rco <- mkg ms id; - - cm <@ RO.o((rco, m)); - - (sigfl, skfl) <@ FL_KU_DSS.sign(skfl, cm); - - sig <- (rco, sigfl); - sk <- (ms, skfl); - - return (sig, sk); - } - - proc verify(pk : pk_al_t, m : msg_al_t, sig : sig_al_t) : bool = { - var rco : rco_t; - var cm : msg_fl_t; - var sigfl : sig_fl_t; - var ver : bool; - - rco <- sig.`1; - - cm <@ RO.o((rco, m)); - - sigfl <- sig.`2; - - ver <@ FL_KU_DSS.verify(pk, cm, sigfl); - - return ver; - } - }. - - - (* -- Reduction Adversaries -- *) - module (R_PRF_EUFCMARO (FL_KU_DSS : DSS_FL.KeyUpdating.Scheme, A : Adv_EUFCMA_RO) : Adv_PRF) (O : Oracle_PRF) = { - module O_CMA_R_PRF_EUFCMARO = { - var skfl : sk_fl_t - var qs : msg_al_t list - - proc init(skfl_init : sk_fl_t) : unit = { - skfl <- skfl_init; - qs <- []; - } - - proc sign(m : msg_al_t) : sig_al_t = { - var id : id_t; - var rco : rco_t; - var sigfl : sig_fl_t; - var sig : sig_al_t; - var cm : msg_fl_t; - - id <- extr_id skfl; - - rco <@ O.query(id); - - cm <@ MCO.o((rco, m)); - - (sigfl, skfl) <@ FL_KU_DSS.sign(skfl, cm); - - sig <- (rco, sigfl); - - qs <- rcons qs m; - - return sig; - } - - proc fresh(m : msg_al_t) : bool = { - return ! m \in qs; - } - } - - proc distinguish() : bool = { - var pk : pk_al_t; - var sk : sk_al_t; - var skfl : sk_fl_t; - var m : msg_al_t; - var sig : sig_al_t; - var is_valid, is_fresh : bool; - - MCO.init(); - - (pk, skfl) <@ FL_KU_DSS.keygen(); - - O_CMA_R_PRF_EUFCMARO.init(skfl); - - (m, sig) <@ A(MCO, O_CMA_R_PRF_EUFCMARO).forge(pk); - - is_valid <@ AL_KU_DSS(FL_KU_DSS, MCO).verify(pk, m, sig); - - is_fresh <@ O_CMA_R_PRF_EUFCMARO.fresh(m); - - return is_valid /\ is_fresh; - } - }. - - - (* - -- - Proofs of EUF-CMA property for the arbitrary-length signature - scheme constructed as specifcied above (assuming message compression is a RO) - -- - *) - section Proofs_EUFCMA_RO_ALKUDSS. - (* Fixed-length signature scheme *) - declare module FL_KU_DSS <: DSS_FL.KeyUpdating.Scheme{-ERO, -O_CMA_Default, -O_METCR, -R_EUFCMARO_CRRO, -R_EUFCMARO_METCRRO, -Wrapped_Oracle, -RepO, -O_RMA_Default, -R_EUFCMARO_IEUFRMA, -QC_A, -Lazy.LRO, -ReproGame, -R_EUFRMA_IEUFRMA, -R_PRF_EUFCMARO, -O_PRF_Default, -DSS_AL.DSS.KeyUpdating.O_CMA_Default}. - - (* Signing and verification procedure of fixed-length signature scheme always terminate *) - declare axiom FL_KU_DSS_sign_ll : islossless FL_KU_DSS.sign. - declare axiom FL_KU_DSS_verify_ll : islossless FL_KU_DSS.verify. - - (* - Checks whether a secret key of the fixed-length digital signature scheme is one that - could (directly) originate from the key generation - *) - declare op init_sk : sk_fl_t -> bool. - - (* - Captures the updating of a secret key performed by the signing procedure - of the fixed-length digital signature scheme. - *) - declare op skupd : sk_fl_t -> sk_fl_t. - - (* - Captures the updating of a secret key performed by the signing procedure - of the fixed-length digital signature scheme. - *) - declare op opsign : sk_fl_t -> msg_fl_t -> sig_fl_t * sk_fl_t. - - (* - Secret keys produced by the key generation procedure of the fixed-length digital - signature scheme satisfy init_sk - *) - declare axiom FL_KU_DSS_keygen_initsk : - hoare[FL_KU_DSS.keygen: true ==> init_sk res.`2]. - - (* - opsign precisely captures the semantics of the signing procedure of the - fixed-length digital signature scheme - *) - declare axiom FL_KU_DSS_sign_fun (sk : sk_fl_t) (cm : msg_fl_t) : - hoare[FL_KU_DSS.sign: arg = (sk, cm) ==> res = opsign sk cm]. - - (* - The signing procedure of the fixed-length digital signature scheme always - terminates (and is captured by opsign) - *) - local lemma FL_KU_DSS_sign_pfun (sk : sk_fl_t) (cm : msg_fl_t) : - phoare[FL_KU_DSS.sign: arg = (sk, cm) ==> res = opsign sk cm] = 1%r. - proof. by conseq FL_KU_DSS_sign_ll (FL_KU_DSS_sign_fun sk cm). qed. - - (* - The signing procedure of the fixed-length digital signature scheme - outputs a secret key that is the updated version (in accordance with skupd) of the - secret key provided as input - *) - declare axiom FL_KU_DSS_sign_skupd (skf : sk_fl_t) : - hoare[FL_KU_DSS.sign: arg.`1 = skf ==> res.`2 = skupd skf]. - - (* - Starting from a secret key produced by the key generation procedure of the - fixed-length digital signature scheme, updating in accordance with skupd results - (at least the first qS times) in a secret key with a unique identifier. - *) - declare axiom skupd_fold_id (i j : int) (sk : sk_fl_t) : - init_sk sk - => 0 <= i < qS - => 0 <= j < qS - => i <> j - => extr_id (fold skupd sk i) <> extr_id (fold skupd sk j). - - (* - The key generation procedure of the fixed-length digital signature - scheme is stateless (i.e., it produces the same output distribution for - all initial memories) - *) - declare axiom FL_KU_DSS_keygen_stateless: - equiv[FL_KU_DSS.keygen ~ FL_KU_DSS.keygen: true ==> ={res}]. - - (* - The verification procedure of the fixed-length digital signature - scheme is stateless (i.e., for a certain input, it produces the same output - distribution for all inital memories) - *) - declare axiom FL_KU_DSS_verify_stateless: - equiv[FL_KU_DSS.verify ~ FL_KU_DSS.verify: ={arg} ==> ={res}]. - - (* Adversary aganst EUF-CMA in the ROM *) - declare module A <: Adv_EUFCMA_RO{-FL_KU_DSS, -ERO, -O_CMA_Default, -O_METCR, -R_EUFCMARO_CRRO, -R_EUFCMARO_METCRRO, -Wrapped_Oracle, -RepO, -DSS_FL_EUFRMA.O_RMA_Default, -R_EUFCMARO_IEUFRMA, -QC_A, -Lazy.LRO, -ReproGame, -R_EUFRMA_IEUFRMA, -R_PRF_EUFCMARO, -O_PRF_Default, -DSS_AL.DSS.KeyUpdating.O_CMA_Default}. - - (* The adversary always terminates if the oracle procedures it can call terminate *) - declare axiom A_forge_ll (RO <: POracle{-A}) (SO <: SOracle_CMA{-A}) : - islossless RO.o => islossless SO.sign => islossless A(RO, SO).forge. - - (* The adversary makes a limited number of queries to the given random (hash) oracle and signing oracle *) - declare axiom A_forge_queries (RO <: POracle{-A, -QC_A}) (SO <: SOracle_CMA{-A, -QC_A}) : - hoare[A(QC_A(A, RO, SO).QC_RO, QC_A(A, RO, SO).QC_SO).forge : - QC_A.cH = 0 /\ QC_A.cS = 0 ==> QC_A.cH <= qH /\ QC_A.cS <= qS]. - - (* Convenient form of the above assumption (direct consequence) *) - local lemma A_forge_queries_init (RO <: POracle{-A, -QC_A}) (SO <: SOracle_CMA{-A, -QC_A}): - hoare[QC_A(A, RO, SO).forge : true ==> QC_A.cH <= qH /\ QC_A.cS <= qS]. - proof. - proc; sp. - call (A_forge_queries RO SO). - by skip. - qed. - - - (* - Steps - *) - (* - An adversary distinguishing between the EUF-CMA games for the different arbitrary-length - digital signature schemes (i.e., the one that samples the indexing keys used for - message compression and the one that generates these keys via mkg) can be used to - distinguish between the two different cases of the PRF game for mkg. - *) - local lemma ALKUDSS_EUFCMARO_PRF &m : - `| Pr[EUF_CMA_RO(AL_KU_DSS(FL_KU_DSS), A, O_CMA_Default, MCO).main() @ &m : res] - - Pr[WS.DSS_AL.KeyUpdatingROM.EUF_CMA_RO(WS.AL_KU_DSS(FL_KU_DSS), A, WS.DSS_AL.DSS.KeyUpdating.O_CMA_Default, MCO).main() @ &m : res] | - = - `| Pr[PRF(R_PRF_EUFCMARO(FL_KU_DSS, A), O_PRF_Default).main(false) @ &m : res] - - Pr[PRF(R_PRF_EUFCMARO(FL_KU_DSS, A), O_PRF_Default).main(true) @ &m : res] |. - proof. - do 2! congr; last congr. - + byequiv => //. - proc; inline{1} 2; inline{2} 2. - wp => /=. - call (: ={qs}(O_Base_Default, R_PRF_EUFCMARO.O_CMA_R_PRF_EUFCMARO)). - - by skip. - call (: ={glob FL_KU_DSS, ERO.m}). - - by inline *; call (: true); wp; skip. - call (: ={glob FL_KU_DSS, ERO.m} - /\ ={qs}(O_Base_Default, R_PRF_EUFCMARO.O_CMA_R_PRF_EUFCMARO) - /\ O_CMA_Default.sk{1}.`1 = O_PRF_Default.k{2} - /\ O_CMA_Default.sk{1}.`2 = R_PRF_EUFCMARO.O_CMA_R_PRF_EUFCMARO.skfl{2} - /\ ! O_PRF_Default.b{2}). - - proc; inline *. - wp. - rcondf{2} 3; 1: by auto. - call (: true). - by wp; skip. - - by proc; skip. - inline *. - wp; call (: true) => /=. - swap{1} 4 -1. - while (={ERO.m, w}); 1: by auto. - wp; rnd. - by wp; skip. - have ->: - Pr[WS.DSS_AL.KeyUpdatingROM.EUF_CMA_RO(WS.AL_KU_DSS(FL_KU_DSS), A, WS.DSS_AL.DSS.KeyUpdating.O_CMA_Default, MCO).main() @ &m : res] - = - Pr[WS.DSS_AL.KeyUpdatingROM.EUF_CMA_RO(WS.AL_KU_DSS(FL_KU_DSS), WS.QC_A(A), WS.DSS_AL.DSS.KeyUpdating.O_CMA_Default, MCO).main() @ &m : res]. - + byequiv => //. - proc; inline{1} 2; inline{2} 2. - seq 4 4 : (={glob FL_KU_DSS, WS.DSS_AL.DSS.O_Base_Default.qs, ERO.m, sig, pk, m}); 2: by sim. - inline{2} 4. - wp => /=. - call (: ={glob FL_KU_DSS, ERO.m, WS.DSS_AL.DSS.KeyUpdating.O_CMA_Default.sk, WS.DSS_AL.DSS.O_Base_Default.qs}). - - by proc; inline *; sim. - - by proc; inline *; wp; skip. - inline *. - wp; call (: true); wp. - while (={w, ERO.m}). - - by wp; rnd; wp; skip. - by wp; skip. - have ->: - Pr[PRF(R_PRF_EUFCMARO(FL_KU_DSS, A), O_PRF_Default).main(true) @ &m : res] - = - Pr[PRF(R_PRF_EUFCMARO(FL_KU_DSS, WS.QC_A(A)), O_PRF_Default).main(true) @ &m : res]. - + byequiv => //. - proc. - inline{1} 2; inline{2} 2. - seq 5 5 : (={glob FL_KU_DSS, R_PRF_EUFCMARO.O_CMA_R_PRF_EUFCMARO.qs, ERO.m, sig, pk, m}); 2: by sim. - inline{2} 5. - wp => /=. - call (: ={glob FL_KU_DSS, glob O_PRF_Default, ERO.m, R_PRF_EUFCMARO.O_CMA_R_PRF_EUFCMARO.qs, R_PRF_EUFCMARO.O_CMA_R_PRF_EUFCMARO.skfl}). - - by proc; inline *; sim. - - by proc; inline *; wp; skip. - inline *. - wp; call (: true); wp. - while (={w, ERO.m}). - - by wp; rnd; wp; skip. - by wp; rnd; wp; skip. - do 2! rewrite Pr[mu_split QC_A.cS <= qS] eq_sym. - congr; last first. - + byphoare => //. - hoare. - - move=> _ _; byphoare => //. - hoare. - proc; inline *. - wp; call (: true); wp => /=. - call (A_forge_queries ERO (<: R_PRF_EUFCMARO(FL_KU_DSS, QC_A(A), O_PRF_Default).O_CMA_R_PRF_EUFCMARO)). - wp 12; conseq (: _ ==> true); 1: smt(). - wp; call (: true). - by while (true); wp; rnd; wp; skip. - proc; inline *. - wp; call (: true); wp => /=. - call (A_forge_queries ERO (<: DSS_AL.DSS.KeyUpdating.O_CMA_Default(WS.AL_KU_DSS(FL_KU_DSS, ERO)))). - wp 8; conseq (: _ ==> true); 1: smt(). - wp; call (: true); while (true). - + by wp; rnd; wp; skip. - by wp; skip. - byequiv (: ={glob A, glob FL_KU_DSS} /\ arg{2} - ==> - res{1} /\ QC_A.cS{1} <= qS <=> res{2} /\ QC_A.cS{2} <= qS) => //. - proc. - inline{1} 2; inline{2} 2. - inline{1} 4; inline{2} 5. - seq 6 7 : ( ={glob FL_KU_DSS, glob A, pk, pk0, ERO.m, QC_A.cH, QC_A.cS} - /\ QC_A.cH{1} = 0 - /\ QC_A.cS{1} = 0 - /\ O_PRF_Default.b{2} - /\ O_PRF_Default.m{2} = empty - /\ DSS_AL.DSS.KeyUpdating.O_CMA_Default.sk{1} = R_PRF_EUFCMARO.O_CMA_R_PRF_EUFCMARO.skfl{2} - /\ DSS_AL.DSS.O_Base_Default.qs{1} = R_PRF_EUFCMARO.O_CMA_R_PRF_EUFCMARO.qs{2} - /\ init_sk R_PRF_EUFCMARO.O_CMA_R_PRF_EUFCMARO.skfl{2}) => /=. - + inline *. - wp. - call (: ={glob FL_KU_DSS} ==> ={glob FL_KU_DSS, res} /\ init_sk res{2}.`2). - conseq (: ={glob FL_KU_DSS} ==> ={glob FL_KU_DSS, res}) - _ - FL_KU_DSS_keygen_initsk. - by proc true. - while (={w, ERO.m}). - - wp; rnd. - by wp; skip. - by wp; rnd{2}; wp; skip. - inline{1} 4; inline{2} 4. - inline{1} 3; inline{2} 3. - wp => /=. - call (: qS < QC_A.cS, true) => />; [ by apply FL_KU_DSS_verify_ll | smt() | ]. - inline{1} 7; inline{2} 7. - wp => />. - exists* R_PRF_EUFCMARO.O_CMA_R_PRF_EUFCMARO.skfl{2}; elim* => skbc. - call (: qS < QC_A.cS - ={glob FL_KU_DSS, ERO.m, QC_A.cH, QC_A.cS} - /\ init_sk skbc - /\ O_PRF_Default.b{2} - /\ 0 <= QC_A.cS{2} <= qS - /\ DSS_AL.DSS.KeyUpdating.O_CMA_Default.sk{1} = R_PRF_EUFCMARO.O_CMA_R_PRF_EUFCMARO.skfl{2} - /\ R_PRF_EUFCMARO.O_CMA_R_PRF_EUFCMARO.skfl{2} = (fold skupd skbc QC_A.cS{2}) - /\ DSS_AL.DSS.O_Base_Default.qs{1} = R_PRF_EUFCMARO.O_CMA_R_PRF_EUFCMARO.qs{2} - /\ (forall (id : id_t), - id \in O_PRF_Default.m{2} <=> - (exists (i : int), 0 <= i < QC_A.cS{2} /\ id = extr_id (fold skupd skbc i))) - qS < QC_A.cS{1} /\ qS < QC_A.cS{2}). - + by move=> RO SO SOll ROll; apply (A_forge_ll RO SO ROll SOll). - + proc; inline *. - rcondt{2} 5; 1: by auto. - wp; sp 1 1. - case (qS < QC_A.cS{2}). - conseq (: _ ==> qS < QC_A.cS{1} /\ qS < QC_A.cS{2}) => //. - wp; sp. - call{1} FL_KU_DSS_sign_ll; call{2} FL_KU_DSS_sign_ll. - wp => /=. - by if{2}; auto. - + wp => />; 1: smt(). - rcondt{2} 4. - - move=> &1. - wp; skip => /> &2 cSr _ inskbc bT ge0_cSr _ m_def /lezNgt leqS_cSr1. - move/iffLR /contra: (m_def (extr_id (fold skupd skbc cSr))). - rewrite negb_exists /= => /(_ _) // i; rewrite negb_and -implybE => rng_i. - by apply skupd_fold_id => // /#. - + wp. - call (: ={glob FL_KU_DSS, arg} - /\ 1 <= QC_A.cS{2} - /\ arg{2}.`1 = fold skupd skbc (QC_A.cS{2} - 1) - ==> - ={glob FL_KU_DSS, res} - /\ res{2}.`2 = fold skupd skbc QC_A.cS{2}). - exists* QC_A.cS{2}; elim* => i. - conseq (: ={glob FL_KU_DSS, arg} ==> ={glob FL_KU_DSS, res}) - _ - (: arg.`1 = fold skupd skbc (i - 1) ==> res.`2 = skupd (fold skupd skbc (i - 1))) => //. - - move=> /> &2 ge1_i _ r ->; smt(foldS). - - by apply (FL_KU_DSS_sign_skupd (fold skupd skbc (i - 1))). - - by proc true. - wp; rnd. - wp; skip => /> &2 cSr _ inskbc bT ge0_cSr _ m_def /lezNgt leqS_cSr1 rco rcoin. - rewrite get_set_sameE oget_some //=; split => [/# | ge1_cSr sigsk sk_def]. - split => [/# | id]. - split => [idin | i ge0_i ltcSr1_i]. - - by move/mem_set: idin => [/m_def /# | ->]; last exists cSr => /#. - rewrite mem_set; case (i = cSr) => [-> | neqcS_i] //. - by left; apply m_def; exists i => /#. - + move=> &2 ltcS_qS. - proc; inline *. - wp; call FL_KU_DSS_sign_ll; wp. - rnd. - by wp; skip => />; smt(drco_ll). - + move=> &1. - proc; inline *. - wp; call FL_KU_DSS_sign_ll; wp; sp => /=. - if; last by wp; skip => /> /#. - wp. - if; last by wp; skip => /> /#. - wp; rnd. - by skip => />; smt(drco_ll). - + proc; inline *. - by wp; skip => />. - + move=> &2 ltcS_qS. - proc; inline *. - by wp; skip. - + move=> &1. - proc; inline *. - by wp; skip. - by skip => /> &2 bT inskbc; smt(fold0 mem_empty). - qed. - - (* - Security theorems - *) - (* Security theorem with PRF, CR and EUF-RMA *) - lemma ALKUDSS_EUFCMARO_PRF_CRRO_EUFRMA &m : - Pr[EUF_CMA_RO(AL_KU_DSS(FL_KU_DSS), A, O_CMA_Default, MCO).main() @ &m : res] - <= - `| Pr[PRF(R_PRF_EUFCMARO(FL_KU_DSS, A), O_PRF_Default).main(false) @ &m : res] - - Pr[PRF(R_PRF_EUFCMARO(FL_KU_DSS, A), O_PRF_Default).main(true) @ &m : res] | - + - Pr[CR_RO(R_EUFCMARO_CRRO(FL_KU_DSS, A), MCO).main() @ &m : res] - + - Pr[EUF_RMA(FL_KU_DSS, R_EUFRMA_IEUFRMA(R_EUFCMARO_IEUFRMA(A))).main() @ &m : res] - + - qS%r * (qS + qH + 1)%r * mu1 drco witness - + - n%r * mu1 dmsg_fl witness. - proof. - rewrite -ger0_norm 1:Pr[mu_ge0] // -subr0. - rewrite -(subrr Pr[WS.DSS_AL.KeyUpdatingROM.EUF_CMA_RO(WS.AL_KU_DSS(FL_KU_DSS), A, WS.DSS_AL.DSS.KeyUpdating.O_CMA_Default, MCO).main() @ &m : res]). - rewrite opprB (addrC Pr[WS.DSS_AL.KeyUpdatingROM.EUF_CMA_RO(WS.AL_KU_DSS(FL_KU_DSS), A, WS.DSS_AL.DSS.KeyUpdating.O_CMA_Default, MCO).main() @ &m : res]) addrA. - apply (ler_trans (`| Pr[EUF_CMA_RO(AL_KU_DSS(FL_KU_DSS), A, O_CMA_Default, MCO).main() @ &m : res] - - Pr[DSS_AL.KeyUpdatingROM.EUF_CMA_RO(WS.AL_KU_DSS(FL_KU_DSS), A, DSS_AL.DSS.KeyUpdating.O_CMA_Default, MCO).main() @ &m : res] | + - `| Pr[DSS_AL.KeyUpdatingROM.EUF_CMA_RO(WS.AL_KU_DSS(FL_KU_DSS), A, DSS_AL.DSS.KeyUpdating.O_CMA_Default, MCO).main() @ &m : res] |)); 1: smt(ler_norm_add). - rewrite -3!addrA &(ler_add) 1:ALKUDSS_EUFCMARO_PRF //. - rewrite ger0_norm 1:Pr[mu_ge0] //. - move: (ALKUDSS_EUFCMARO_CRRO_EUFRMA FL_KU_DSS FL_KU_DSS_sign_ll FL_KU_DSS_verify_ll A - _ _ opsign FL_KU_DSS_sign_fun FL_KU_DSS_keygen_stateless FL_KU_DSS_verify_stateless &m). - + by move => RO SO ROll SOll; apply (A_forge_ll RO SO ROll SOll). - + by move => RO SO; apply (A_forge_queries RO SO). - by rewrite !addrA. - qed. - - (* Security theorem with PRF, M-eTCR and EUF-RMA *) - lemma ALKUDSS_EUFCMARO_PRF_METCRRO_EUFRMA &m : - Pr[EUF_CMA_RO(AL_KU_DSS(FL_KU_DSS), A, O_CMA_Default, MCO).main() @ &m : res] - <= - `| Pr[PRF(R_PRF_EUFCMARO(FL_KU_DSS, A), O_PRF_Default).main(false) @ &m : res] - - Pr[PRF(R_PRF_EUFCMARO(FL_KU_DSS, A), O_PRF_Default).main(true) @ &m : res] | - + - Pr[M_ETCR_RO(R_EUFCMARO_METCRRO(FL_KU_DSS, A), O_METCR, MCO).main() @ &m : res] - + - Pr[EUF_RMA(FL_KU_DSS, R_EUFRMA_IEUFRMA(R_EUFCMARO_IEUFRMA(A))).main() @ &m : res] - + - qS%r * (qS + qH + 1)%r * mu1 drco witness - + - n%r * mu1 dmsg_fl witness. - proof. - rewrite -ger0_norm 1:Pr[mu_ge0] // -subr0. - rewrite -(subrr Pr[WS.DSS_AL.KeyUpdatingROM.EUF_CMA_RO(WS.AL_KU_DSS(FL_KU_DSS), A, WS.DSS_AL.DSS.KeyUpdating.O_CMA_Default, MCO).main() @ &m : res]). - rewrite opprB (addrC Pr[WS.DSS_AL.KeyUpdatingROM.EUF_CMA_RO(WS.AL_KU_DSS(FL_KU_DSS), A, WS.DSS_AL.DSS.KeyUpdating.O_CMA_Default, MCO).main() @ &m : res]) addrA. - apply (ler_trans (`| Pr[EUF_CMA_RO(AL_KU_DSS(FL_KU_DSS), A, O_CMA_Default, MCO).main() @ &m : res] - - Pr[DSS_AL.KeyUpdatingROM.EUF_CMA_RO(WS.AL_KU_DSS(FL_KU_DSS), A, DSS_AL.DSS.KeyUpdating.O_CMA_Default, MCO).main() @ &m : res] | + - `| Pr[DSS_AL.KeyUpdatingROM.EUF_CMA_RO(WS.AL_KU_DSS(FL_KU_DSS), A, DSS_AL.DSS.KeyUpdating.O_CMA_Default, MCO).main() @ &m : res] |)); 1: smt(ler_norm_add). - rewrite -3!addrA &(ler_add) 1:ALKUDSS_EUFCMARO_PRF //. - rewrite ger0_norm 1:Pr[mu_ge0] //. - move: (ALKUDSS_EUFCMARO_METCRRO_EUFRMA FL_KU_DSS FL_KU_DSS_sign_ll FL_KU_DSS_verify_ll A - _ _ opsign FL_KU_DSS_sign_fun FL_KU_DSS_keygen_stateless FL_KU_DSS_verify_stateless &m). - + by move => RO SO ROll SOll; apply (A_forge_ll RO SO ROll SOll). - + by move => RO SO; apply (A_forge_queries RO SO). - by rewrite !addrA. - qed. - - end section Proofs_EUFCMA_RO_ALKUDSS. - -end WithPRF. -*)