From 0ca687fe1ea88d7b3c19c81a562e38278af9647b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= Date: Fri, 28 Apr 2023 11:37:22 -0300 Subject: [PATCH 01/24] Add title and purpose of the document --- praos-design-decisions.md | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 praos-design-decisions.md diff --git a/praos-design-decisions.md b/praos-design-decisions.md new file mode 100644 index 0000000..56bf79d --- /dev/null +++ b/praos-design-decisions.md @@ -0,0 +1,7 @@ +# Design decisions of the Praos specification + +The purpose of this document is to record the design decisions that +were made during the development of the current version of the +[**Ouroboros Praos**](https://eprint.iacr.org/2017/573.pdf) protocol +specification formalized in Isabelle/HOL. In particular, it is reported +what aspects were modeled (and how) and what aspects were left out. From 55a993ca4894830406cb36010e5a0eef73be3330 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= Date: Fri, 28 Apr 2023 11:47:06 -0300 Subject: [PATCH 02/24] Add the original goal of the formalization --- praos-design-decisions.md | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/praos-design-decisions.md b/praos-design-decisions.md index 56bf79d..3742e0d 100644 --- a/praos-design-decisions.md +++ b/praos-design-decisions.md @@ -5,3 +5,11 @@ were made during the development of the current version of the [**Ouroboros Praos**](https://eprint.iacr.org/2017/573.pdf) protocol specification formalized in Isabelle/HOL. In particular, it is reported what aspects were modeled (and how) and what aspects were left out. + +## Original goal + +The original goal for implementing a version of Ouroboros Praos in +Isabelle/HOL was to have a formalized version of the protocol that +would serve as a reference specification based directly on the +Ouroboros Praos paper and that would allow us to formally prove +properties of it. From c31ee14fa53005e8c3f4d519e1440e3e4132a08e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= Date: Fri, 28 Apr 2023 11:56:50 -0300 Subject: [PATCH 03/24] Add a section on the security analysis --- praos-design-decisions.md | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/praos-design-decisions.md b/praos-design-decisions.md index 3742e0d..f6caf40 100644 --- a/praos-design-decisions.md +++ b/praos-design-decisions.md @@ -13,3 +13,22 @@ Isabelle/HOL was to have a formalized version of the protocol that would serve as a reference specification based directly on the Ouroboros Praos paper and that would allow us to formally prove properties of it. + +## Security analysis + +In principle, such properties would be functional properties only, thus +a security analysis of the protocol was out of scope and, consequently, +we do not model concepts such as the environment $\mathcal{Z}$, the +adversary $\mathcal{A}$, etc. Moreover, we do not need to deal with +probabilities or computational complexity measures. + +However, we retain the use of the Universal Composability (UC) +framework for the sake of design modularity. It is important to mention +that in the Praos paper the protocol is described in the so-called +*hybrid model*, in which the protocol assumes the availability of +idealized versions of some cryptographic primitives, called +*ideal functionalities*, that can be invoked by the protocol +participants, much like sub-routines. These ideal functionalities can be +replaced later with concrete implementations without affecting the +security properties of the protocol. Thus, we model these ideal +functionalities as Isabelle `locale`s. From 44b17fd3ad88849fb06f7219cad28bbd396ed370 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= Date: Fri, 28 Apr 2023 14:11:49 -0300 Subject: [PATCH 04/24] Add a section on cryptographic primitives --- praos-design-decisions.md | 86 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 86 insertions(+) diff --git a/praos-design-decisions.md b/praos-design-decisions.md index f6caf40..d8ced50 100644 --- a/praos-design-decisions.md +++ b/praos-design-decisions.md @@ -32,3 +32,89 @@ participants, much like sub-routines. These ideal functionalities can be replaced later with concrete implementations without affecting the security properties of the protocol. Thus, we model these ideal functionalities as Isabelle `locale`s. + +## Cryptographic primitives + +### Public-key cryptography + +The Ouroboros Praos protocol is based on a public-key cryptographic +system. We state a correctness property that establishes a relationship +between the generated verification and secret keys: if we generate the +keys using the key generation function then it is possible to retrieve +the verification key from the secret key. Although not explicitly +stated, the paper assumes this property holds. Another property that is +normally assumed is that it is infeasible (i.e., having a negligible +probability) to derive the secret key from the public key. However, +since this is a probabilistic security property, we leave it out. + +Further, in cryptography, key generation is usually modeled as an +efficient probabilistic algorithm. However, we adopt a more realistic +approach and model the key generator as an ordinary, deterministic +algorithm. + +### Digital signatures + +The paper describes two digital signature schemes: A regular digital +signature scheme, denoted by $\mathcal{F}_{\mathsf{DSIG}}$, which is +used to sign transactions, and a special digital signature scheme, +denoted by $\mathcal{F}_{\mathsf{KES}}$, which is used to sign blocks +and has the capability of allowing the signing key to evolve, in such a +way that the adversary cannot forge past signatures. For our purposes, +though, we model a single, ordinary digital signature scheme for signing +both transactions and blocks. + +In traditional cryptography, signing and verification procedures are +efficient algorithms. Moreover, the former is usually probabilistic (as +is the case in the paper). However, again, we model both procedures as +ordinary, deterministic algorithms. Regarding properties, and as stated +in the paper, we only require a correctness property stating that the +signature produced by signing a message can be checked to be valid, +provided that the verification key used to check the validity of the +signature is derived from the secret key used to sign the message. This +correctness property, though, changes a bit for the case of +$\mathcal{F}_{\mathsf{KES}}$, a fact that we naturally ignore. + +Finally, the paper states that the scheme $\mathcal{F}_{\mathsf{DSIG}}$ +is EUF-CMA-secure, and that the scheme $\mathcal{F}_{\mathsf{KES}}$ is +secure with respect to a special definition of forward security. As +usual, we do not enforce this security properties but simply assume +them. + +### Verifiable random functions (VRF) + +In the Praos protocol, the stakeholders use a VRF for executing the +private lottery to check whether they're slot leaders for a particular +slot. Also, stakeholders use a VRF to include a pseudorandom value in +each block they produce. The paper uses a special VRF which is more +secure than standard VRFs, since it guarantees that VRF values cannot be +predicted even if the adversary is allowed to generate the secret and +verification keys. Naturally, for this work, we stick to the regular +definition of a VRF. + +In traditional cryptography, evaluation of VRFs (and pseudorandom +functions in general) is an efficient algorithm; however we only assume +that. Regarding properties, and as stated in the paper, VRFs satisfy the +properties of uniqueness, provability, and pseudorandomness (i.e., it is +difficult for an efficient adversary to distinguish a VRF value from a +truly random value). Since this last property is probabilistic in nature, +we only require the first two properties. + +Finally, in the paper, pseudorandom values produced by VRFs are +bit-strings, which can be regarded as values of any type and thus we +model them by using a type parameter. However, the paper loosely uses +such values in the comparison to a *real-valued* threshold to check for +slot leadership. Therefore, we require the existence of a function +`value_to_real` in the interface of VRFs that casts VRF values to real +numbers. + +### Hash functions + +The paper uses the *Random Oracle Model* (ROM). In the ROM, a hash +function is modeled as a random oracle, which is basically a magical +black box that implements a truly random function. As the ROM is used +just for the purposes of the security proof, we model a collision-free +cryptographic hash functions instead. Theoretically, cryptographic hash +functions have certain properties, e.g., they are one-way functions, +meaning that they are difficult to invert by an efficient adversary. +But, this property is probabilistic in nature, so we cannot enforce it +in the code. From 8b7c46d8e7a4fa771741a133f59bbee247de8e02 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= Date: Fri, 28 Apr 2023 14:29:13 -0300 Subject: [PATCH 05/24] Add a section on the protocol parameters --- praos-design-decisions.md | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/praos-design-decisions.md b/praos-design-decisions.md index d8ced50..e93a870 100644 --- a/praos-design-decisions.md +++ b/praos-design-decisions.md @@ -118,3 +118,33 @@ functions have certain properties, e.g., they are one-way functions, meaning that they are difficult to invert by an efficient adversary. But, this property is probabilistic in nature, so we cannot enforce it in the code. + +## Protocol parameters + +### Parameter $k$ + +As the paper states, the parameter $k$ establishes how deep in the chain +(in terms of number of blocks) a transaction needs to be in order to be +declared as stable. Although the paper does not explicitly say whether +$k$ must be positive (it does say that $k \in \N$), Theorem 7 (Chain +quality) defines $\mu = 1/k$, therefore $k$ must be positive. + +### Parameter $f$ + +The parameter $f$, called *active slot coefficient*, establishes the +probability that at least one stakeholder is elected as a slot leader in +each slot, that is, the probability that a slot is not empty. Although +the paper does not explicitly say so, we assume $f$ to be a strictly +positive probability; otherwise all slots would be empty. Moreover, for +example, Theorem 4 in the paper assumes $f \in (0, 1]$. + +### Parameter $\epsilon$ + +The parameter $\epsilon$ represents the advantage in terms of stake of +the honest stakeholders against the adversarial ones. Although the paper +does not explicitly say so, we assume $\epsilon \in (0,1)$, as is the +case for example in Theorem 5 (Common prefix) in the paper. Finally, +although the parameter $\epsilon$ is used almost exclusively in the +security analysis of the protocol, we need to include it nevertheless, +since it is also used in the computation of the new epoch randomness +performed by the sub-protocol $\pi_{RLB}$. From 4915b61039fff25710d0973a680ff7871f3550b1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= Date: Fri, 28 Apr 2023 14:33:32 -0300 Subject: [PATCH 06/24] Add a section on slots and epochs --- praos-design-decisions.md | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/praos-design-decisions.md b/praos-design-decisions.md index e93a870..6b982e1 100644 --- a/praos-design-decisions.md +++ b/praos-design-decisions.md @@ -148,3 +148,11 @@ although the parameter $\epsilon$ is used almost exclusively in the security analysis of the protocol, we need to include it nevertheless, since it is also used in the computation of the new epoch randomness performed by the sub-protocol $\pi_{RLB}$. + +## Slots and epochs + +For numbering slots and epochs, the paper uses the mathematician's +convention of starting from 1, and so we do in our formalization. +However, it is probably better to use the computer science's convention +of zero-based indexing in order to facilitate computations involving +indexes. From e8cc681e71c9a3ad5ef742126386ec3a28f528ed Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= Date: Fri, 28 Apr 2023 14:40:48 -0300 Subject: [PATCH 07/24] Add a section on the initialization phase --- praos-design-decisions.md | 40 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 40 insertions(+) diff --git a/praos-design-decisions.md b/praos-design-decisions.md index 6b982e1..5e22ed4 100644 --- a/praos-design-decisions.md +++ b/praos-design-decisions.md @@ -156,3 +156,43 @@ convention of starting from 1, and so we do in our formalization. However, it is probably better to use the computer science's convention of zero-based indexing in order to facilitate computations involving indexes. + +## Initialization phase and the functionality +$\mathcal{F}_\mathsf{INIT}$ + +The paper includes an ideal functionality $\mathcal{F}_\mathsf{INIT}$, +which is passed the initial stakes of all stakeholders as parameters +and does the following: + + 1. Receives the verification keys from each stakeholder during the + first round of the protocol and stores them locally. + 2. When all stakeholders have sent their verification keys, it + constructs a genesis block including these keys, the initial stakes, + and an initial random value $\eta$. + 3. When asked by a stakeholder in later rounds, it sends the genesis + block to the stakeholder. + +On the other hand, the stakeholder's initialization phase comprises the +following steps: + + 1. In the first round, the stakeholder sends requests to + $\mathcal{F}_\mathsf{VRF}$, $\mathcal{F}_\mathsf{KES}$, and + $\mathcal{F}_\mathsf{DSIG}$ to generate their verification keys, and + then sends them to $\mathcal{F}_\mathsf{INIT}$. + 2. In the next round, the stakeholder obtains the genesis block from + $\mathcal{F}_\mathsf{INIT}$. + +In our formalization, we have simplified this initialization protocol +in several ways: + +1. We do not model $\mathcal{F}_\mathsf{INIT}$. +2. Each stakeholder is parametrized with its secret keys. **NOTE**: +This may be an over-simplification, since the `generate` function of the +VRF and digital signature modules should be used instead. +3. The verification keys of each stakeholder reside only in the genesis +block, which is given to each stakeholder as a parameter. **NOTE**: This +may be an over-simplification, since the `generate` function of the VRF +and digital signature modules should be used instead. But then again, +some protocol similar to the one used with $\mathcal{F}_\mathsf{INIT}$ +in the paper should be used in order for stakeholders to be able to +publish their verification keys. From 90c84817f65c3058ec93b97afc96c6567398007c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= Date: Fri, 28 Apr 2023 14:44:42 -0300 Subject: [PATCH 08/24] Drop a spurious line break in the title of a section --- praos-design-decisions.md | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/praos-design-decisions.md b/praos-design-decisions.md index 5e22ed4..806b34f 100644 --- a/praos-design-decisions.md +++ b/praos-design-decisions.md @@ -157,8 +157,7 @@ However, it is probably better to use the computer science's convention of zero-based indexing in order to facilitate computations involving indexes. -## Initialization phase and the functionality -$\mathcal{F}_\mathsf{INIT}$ +## Initialization phase and the functionality $\mathcal{F}_\mathsf{INIT}$ The paper includes an ideal functionality $\mathcal{F}_\mathsf{INIT}$, which is passed the initial stakes of all stakeholders as parameters From c00f571f2cf1dd76614575e94685c57850c43854 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= Date: Fri, 28 Apr 2023 15:17:15 -0300 Subject: [PATCH 09/24] Fix rendering of the LaTeX symbol for natural numbers --- praos-design-decisions.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/praos-design-decisions.md b/praos-design-decisions.md index 806b34f..a47f360 100644 --- a/praos-design-decisions.md +++ b/praos-design-decisions.md @@ -126,8 +126,8 @@ in the code. As the paper states, the parameter $k$ establishes how deep in the chain (in terms of number of blocks) a transaction needs to be in order to be declared as stable. Although the paper does not explicitly say whether -$k$ must be positive (it does say that $k \in \N$), Theorem 7 (Chain -quality) defines $\mu = 1/k$, therefore $k$ must be positive. +$k$ must be positive (it does say that $k \in \mathbb{N}$), Theorem 7 +(Chain quality) defines $\mu = 1/k$, therefore $k$ must be positive. ### Parameter $f$ From 09aa5b1578b20c75c343b2f63af4210ff2e880e1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= Date: Fri, 28 Apr 2023 17:14:59 -0300 Subject: [PATCH 10/24] Work around a known issue with LaTeX underscores The issue is explained in https://github.com/orgs/community/discussions/16939 --- praos-design-decisions.md | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/praos-design-decisions.md b/praos-design-decisions.md index a47f360..46b0993 100644 --- a/praos-design-decisions.md +++ b/praos-design-decisions.md @@ -55,9 +55,9 @@ algorithm. ### Digital signatures The paper describes two digital signature schemes: A regular digital -signature scheme, denoted by $\mathcal{F}_{\mathsf{DSIG}}$, which is +signature scheme, denoted by $\mathcal{F}\_{\mathsf{DSIG}}$, which is used to sign transactions, and a special digital signature scheme, -denoted by $\mathcal{F}_{\mathsf{KES}}$, which is used to sign blocks +denoted by $\mathcal{F}\_{\mathsf{KES}}$, which is used to sign blocks and has the capability of allowing the signing key to evolve, in such a way that the adversary cannot forge past signatures. For our purposes, though, we model a single, ordinary digital signature scheme for signing @@ -72,10 +72,10 @@ signature produced by signing a message can be checked to be valid, provided that the verification key used to check the validity of the signature is derived from the secret key used to sign the message. This correctness property, though, changes a bit for the case of -$\mathcal{F}_{\mathsf{KES}}$, a fact that we naturally ignore. +$\mathcal{F}\_{\mathsf{KES}}$, a fact that we naturally ignore. -Finally, the paper states that the scheme $\mathcal{F}_{\mathsf{DSIG}}$ -is EUF-CMA-secure, and that the scheme $\mathcal{F}_{\mathsf{KES}}$ is +Finally, the paper states that the scheme $\mathcal{F}\_{\mathsf{DSIG}}$ +is EUF-CMA-secure, and that the scheme $\mathcal{F}\_{\mathsf{KES}}$ is secure with respect to a special definition of forward security. As usual, we do not enforce this security properties but simply assume them. @@ -157,9 +157,9 @@ However, it is probably better to use the computer science's convention of zero-based indexing in order to facilitate computations involving indexes. -## Initialization phase and the functionality $\mathcal{F}_\mathsf{INIT}$ +## Initialization phase and the functionality $\mathcal{F}\_\mathsf{INIT}$ -The paper includes an ideal functionality $\mathcal{F}_\mathsf{INIT}$, +The paper includes an ideal functionality $\mathcal{F}\_\mathsf{INIT}$, which is passed the initial stakes of all stakeholders as parameters and does the following: @@ -175,16 +175,16 @@ On the other hand, the stakeholder's initialization phase comprises the following steps: 1. In the first round, the stakeholder sends requests to - $\mathcal{F}_\mathsf{VRF}$, $\mathcal{F}_\mathsf{KES}$, and - $\mathcal{F}_\mathsf{DSIG}$ to generate their verification keys, and - then sends them to $\mathcal{F}_\mathsf{INIT}$. + $\mathcal{F}\_\mathsf{VRF}$, $\mathcal{F}\_\mathsf{KES}$, and + $\mathcal{F}\_\mathsf{DSIG}$ to generate their verification keys, and + then sends them to $\mathcal{F}\_\mathsf{INIT}$. 2. In the next round, the stakeholder obtains the genesis block from - $\mathcal{F}_\mathsf{INIT}$. + $\mathcal{F}\_\mathsf{INIT}$. In our formalization, we have simplified this initialization protocol in several ways: -1. We do not model $\mathcal{F}_\mathsf{INIT}$. +1. We do not model $\mathcal{F}\_\mathsf{INIT}$. 2. Each stakeholder is parametrized with its secret keys. **NOTE**: This may be an over-simplification, since the `generate` function of the VRF and digital signature modules should be used instead. @@ -192,6 +192,6 @@ VRF and digital signature modules should be used instead. block, which is given to each stakeholder as a parameter. **NOTE**: This may be an over-simplification, since the `generate` function of the VRF and digital signature modules should be used instead. But then again, -some protocol similar to the one used with $\mathcal{F}_\mathsf{INIT}$ +some protocol similar to the one used with $\mathcal{F}\_\mathsf{INIT}$ in the paper should be used in order for stakeholders to be able to publish their verification keys. From 4299015ce4d63de42a58b433b57973f180285f3d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= Date: Fri, 5 May 2023 11:38:30 -0300 Subject: [PATCH 11/24] Add a section on the static and dynamic stake cases --- praos-design-decisions.md | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/praos-design-decisions.md b/praos-design-decisions.md index 46b0993..60dd353 100644 --- a/praos-design-decisions.md +++ b/praos-design-decisions.md @@ -149,6 +149,16 @@ security analysis of the protocol, we need to include it nevertheless, since it is also used in the computation of the new epoch randomness performed by the sub-protocol $\pi_{RLB}$. +## The static and dynamic stake cases + +The paper describes and analyzes the protocol in two settings: The +_static stake_ case and the _dynamic stake_ case. In the former, the +initial stake distribution is hardcoded into the genesis block and +remains fixed during the whole execution (i.e., one epoch); in the +latter, the stake distribution is allowed to change over time and the +protocol execution spans multiple epochs. Since we are not interested in +the security analysis, we model the full protocol. + ## Slots and epochs For numbering slots and epochs, the paper uses the mathematician's From c8703afef091b499403c42e69e8da9fcefb1a9ac Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= Date: Fri, 5 May 2023 11:41:33 -0300 Subject: [PATCH 12/24] Add a section on transactions and blocks --- praos-design-decisions.md | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/praos-design-decisions.md b/praos-design-decisions.md index 60dd353..a0c0690 100644 --- a/praos-design-decisions.md +++ b/praos-design-decisions.md @@ -205,3 +205,23 @@ and digital signature modules should be used instead. But then again, some protocol similar to the one used with $\mathcal{F}\_\mathsf{INIT}$ in the paper should be used in order for stakeholders to be able to publish their verification keys. +## Transactions and blocks + +In the paper, the environment $\mathcal{Z}$ issues transactions on +behalf of any stakeholder $U_i$ by requesting a signature on the +transaction and handing the transaction data $^*d \in \{0,1\}^*$ to +stakeholders to put them into blocks. We decide not to model transaction +processing this way but use a more realistic approach instead: +Transactions are assumed to be received by stakeholders through the +network. + +Regarding the application of a transaction to a stake distribution, the +paper does not define how this is done, so we use the intuitive +definition and assume that the source and target stakeholders exist in +the stake distribution and that the source stakeholder has enough stake +for the withdrawal. + +Regarding the application of a block to a stake distribution, the paper +does not define how this is done, so we assume that it simply means +applying all transactions in the block to the stake distribution. + From acf5a86216ab79b3a9d92297ac81afc5676498ce Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= Date: Fri, 5 May 2023 11:46:23 -0300 Subject: [PATCH 13/24] Escape asterisks to fix rendering issues --- praos-design-decisions.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/praos-design-decisions.md b/praos-design-decisions.md index a0c0690..426cf28 100644 --- a/praos-design-decisions.md +++ b/praos-design-decisions.md @@ -209,7 +209,7 @@ publish their verification keys. In the paper, the environment $\mathcal{Z}$ issues transactions on behalf of any stakeholder $U_i$ by requesting a signature on the -transaction and handing the transaction data $^*d \in \{0,1\}^*$ to +transaction and handing the transaction data $^\*d \in \{0,1\}^\*$ to stakeholders to put them into blocks. We decide not to model transaction processing this way but use a more realistic approach instead: Transactions are assumed to be received by stakeholders through the From 54f70019c5bec5bfdf83cdc25085d6e44db66c9b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= Date: Fri, 5 May 2023 12:02:08 -0300 Subject: [PATCH 14/24] Fix typo in LaTeX expression --- praos-design-decisions.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/praos-design-decisions.md b/praos-design-decisions.md index 426cf28..bda8bf3 100644 --- a/praos-design-decisions.md +++ b/praos-design-decisions.md @@ -209,7 +209,7 @@ publish their verification keys. In the paper, the environment $\mathcal{Z}$ issues transactions on behalf of any stakeholder $U_i$ by requesting a signature on the -transaction and handing the transaction data $^\*d \in \{0,1\}^\*$ to +transaction and handing the transaction data $d^\* \in \{0,1\}^\*$ to stakeholders to put them into blocks. We decide not to model transaction processing this way but use a more realistic approach instead: Transactions are assumed to be received by stakeholders through the From 24c9ae9def6da79e9b7bc3c3da46919f260efa00 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= Date: Fri, 5 May 2023 12:07:27 -0300 Subject: [PATCH 15/24] Work around a known issue with LaTeX curly braces The issue is explained in https://github.com/orsharir/github-mathjax/issues/10 --- praos-design-decisions.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/praos-design-decisions.md b/praos-design-decisions.md index bda8bf3..381615d 100644 --- a/praos-design-decisions.md +++ b/praos-design-decisions.md @@ -209,7 +209,7 @@ publish their verification keys. In the paper, the environment $\mathcal{Z}$ issues transactions on behalf of any stakeholder $U_i$ by requesting a signature on the -transaction and handing the transaction data $d^\* \in \{0,1\}^\*$ to +transaction and handing the transaction data $d^\* \in \\{0,1\\}^\*$ to stakeholders to put them into blocks. We decide not to model transaction processing this way but use a more realistic approach instead: Transactions are assumed to be received by stakeholders through the From 02fe84dff675c1fb92887b5a61c50b7980b82c3d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= Date: Fri, 5 May 2023 12:10:49 -0300 Subject: [PATCH 16/24] Add a section on the use of the randomness beacon --- praos-design-decisions.md | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/praos-design-decisions.md b/praos-design-decisions.md index 381615d..2551613 100644 --- a/praos-design-decisions.md +++ b/praos-design-decisions.md @@ -225,3 +225,14 @@ Regarding the application of a block to a stake distribution, the paper does not define how this is done, so we assume that it simply means applying all transactions in the block to the stake distribution. +## Functionality $\mathcal{F}^{\tau,r}\_{RLB}$ and subprotocol $\pi\_{RLB}$ + +In the paper, the functionality $\mathcal{F}^{\tau,r}\_{RLB}$ models a +randomness beacon that basically provides a fresh nonce for each epoch +to (re)seed the election process. Furthermore, this beacon is resettable +and leaky in order to strengthen the adversary, as the purpose of the +beacon is to enable the security analysis of the full protocol. The +paper also presents a subprotocol $\pi\_{RLB}$ that simulates the beacon +in the $\mathcal{F}\_\mathsf{INIT}$-hybrid model via a simple algorithm +that collects randomness from the blockchain. Therefore, we choose to +directly model $\pi\_{RLB}$, which is ultimately used by implementations. From a2a44b1024dd6d7126752f689378612133476180 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= Date: Tue, 9 May 2023 17:02:44 -0300 Subject: [PATCH 17/24] Add a section on the chain selection rule --- praos-design-decisions.md | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/praos-design-decisions.md b/praos-design-decisions.md index 2551613..ddfa13b 100644 --- a/praos-design-decisions.md +++ b/praos-design-decisions.md @@ -236,3 +236,12 @@ paper also presents a subprotocol $\pi\_{RLB}$ that simulates the beacon in the $\mathcal{F}\_\mathsf{INIT}$-hybrid model via a simple algorithm that collects randomness from the blockchain. Therefore, we choose to directly model $\pi\_{RLB}$, which is ultimately used by implementations. + +## Chain selection rule + +According to the paper, the function $\mathsf{maxvalid}$ should favor the +current chain if it is the longest, otherwise choose arbitrarily. In the +latter case, we make a specific decision, namely, we choose a chain that +was delivered first out of those with maximal length (which is one of +the possible choices suggested by the paper). However, if the need +arises, it is possible to leave this choice unspecified. From 9559ac6d7a1423f3b0fbe68f6ca65069f98bf3e3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= Date: Tue, 9 May 2023 17:04:13 -0300 Subject: [PATCH 18/24] Add a section on the semi-synchronous setting --- praos-design-decisions.md | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/praos-design-decisions.md b/praos-design-decisions.md index ddfa13b..11300e1 100644 --- a/praos-design-decisions.md +++ b/praos-design-decisions.md @@ -245,3 +245,21 @@ latter case, we make a specific decision, namely, we choose a chain that was delivered first out of those with maximal length (which is one of the possible choices suggested by the paper). However, if the need arises, it is possible to leave this choice unspecified. + +## The semi-synchronous setting + +In the paper, a semi-synchronous model with an upper bound $\Delta$ in +message delay is used, which is unknown to the stakeholders. Regarding +$\Delta$, we stress the fact that the protocol is oblivious of $\Delta$ +and this bound is only used in the security analysis. Hence, from the +protocol's point of view, the network is no better than an eventual +delivery network (without a concrete bound). This can be easily modeled +using our process calculus, for example, as a reliable broadcasting +server process. + +Regarding synchrony of processors, the paper assumes that stakeholders +are equipped with (roughly) synchronized clocks that indicate the +current slot, and that any clock drift is subsumed in the slot length. +In the same spirit, we assume the existence of an external +'clock process' that signals each stakeholder when a round (i.e., slot) +ends. From f232d617b5c8078188d679d02dfbacfe310b4e7b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= Date: Tue, 9 May 2023 17:06:22 -0300 Subject: [PATCH 19/24] Add a section on the delayed diffuse functionality --- praos-design-decisions.md | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/praos-design-decisions.md b/praos-design-decisions.md index 11300e1..545c671 100644 --- a/praos-design-decisions.md +++ b/praos-design-decisions.md @@ -263,3 +263,24 @@ current slot, and that any clock drift is subsumed in the slot length. In the same spirit, we assume the existence of an external 'clock process' that signals each stakeholder when a round (i.e., slot) ends. + +## The "Delayed Diffuse" functionality + +We do not model the network as a separate ideal functionality +$\textsf{DDiffuse}_\Delta$ but rely on our process calculus features for +communication. In particular, each stakeholder is parametrized with a +'network interface', comprised by a dedicated channel used to receive +messages from the network (stored in the stakeholder's 'incoming string' +or 'mailbox' in the paper's parlance) and another dedicated channel used +to broadcast (or 'diffuse', in the paper's parlance) a message to the +network. + +Also, the $\textsf{DDiffuse}_\Delta$ functionality guarantees that +messages sent in a round are received with a delay of at most $\Delta$ +rounds. As mentioned before, we instead assume that the protocol is +executed on a network featuring eventual delivery of messages. + +Finally, the paper states that a stakeholder is allowed to diffuse once +in a round. We enforce this restriction explicitly in the stakeholder +process implementation, which broadcasts a chain once at the end of the +current round should the stakeholder is elected as a slot leader. From 97c13912ea782ab11bbc249d8d3abbe33b6a8f15 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= Date: Tue, 9 May 2023 18:00:35 -0300 Subject: [PATCH 20/24] Clarify the version of the paper used in the specification --- praos-design-decisions.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/praos-design-decisions.md b/praos-design-decisions.md index 545c671..5db35cb 100644 --- a/praos-design-decisions.md +++ b/praos-design-decisions.md @@ -6,6 +6,11 @@ were made during the development of the current version of the specification formalized in Isabelle/HOL. In particular, it is reported what aspects were modeled (and how) and what aspects were left out. +It is important to note that our specification is based on +[**an earlier version of the paper**](https://link.springer.com/chapter/10.1007/978-3-319-78375-8_3), +therefore it may be necessary to revise the specification to adapt it to +the latest version. + ## Original goal The original goal for implementing a version of Ouroboros Praos in From 3595d29b168f8538265cd7d84379710076a58f91 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= Date: Tue, 9 May 2023 20:12:44 -0300 Subject: [PATCH 21/24] Add a comment on the validity of transactions --- praos-design-decisions.md | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/praos-design-decisions.md b/praos-design-decisions.md index 5db35cb..a2fc747 100644 --- a/praos-design-decisions.md +++ b/praos-design-decisions.md @@ -220,6 +220,21 @@ processing this way but use a more realistic approach instead: Transactions are assumed to be received by stakeholders through the network. +The paper does not impose any definition of validity of transactions, +therefore we assume a sensible definition based on implementations, +which happens to coincide with Definition 4 in the latest version of +the paper. However, since this definition is not precise enough in our +opinion, we assume that the references to $x$ are actually to $s$ and +that $x \in \mathbb{N}$ instead of $x \in \mathbb{Z}$. Also, it is +important to point out that there is a mismatch between the earlier +paper used for our specification and the latest version: In the former, +the transaction data received from the environment is not validated +prior to including it in a new block, whereas in the latter transaction +data is validated in order to extract the maximal sequence of +transactions that is consistent with the current local chain. As +already mentioned, we may have to adapt our specification to cope with +this change. + Regarding the application of a transaction to a stake distribution, the paper does not define how this is done, so we use the intuitive definition and assume that the source and target stakeholders exist in From 90239f0ee59a1cee4806c3111072c98352adcc60 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= Date: Tue, 9 May 2023 20:17:43 -0300 Subject: [PATCH 22/24] Add a section on chains --- praos-design-decisions.md | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/praos-design-decisions.md b/praos-design-decisions.md index a2fc747..e7cc915 100644 --- a/praos-design-decisions.md +++ b/praos-design-decisions.md @@ -245,6 +245,24 @@ Regarding the application of a block to a stake distribution, the paper does not define how this is done, so we assume that it simply means applying all transactions in the block to the stake distribution. +## Chains + +In regards to the validity of chains, it is important to point out that +there is a mismatch between the earlier paper used for our specification +and the latest version: In the former, chains that include blocks with +slots in the future are not rejected but pruned accordingly, whereas in +the later such chains should be rejected. + +On the other hand, regarding the chain extension procedure, there is an +improvement in the latest version of the paper: The hash value of the +tip of the current best chain, called 'state', is computed on the fly +only when constructing a new block; whereas in the earlier paper this +state is kept internally and updated whenever a new local chain is +adopted, as well as before a new block is difussed. + +Again, we may have to adapt our specification to cope with the +above-mentioned changes. + ## Functionality $\mathcal{F}^{\tau,r}\_{RLB}$ and subprotocol $\pi\_{RLB}$ In the paper, the functionality $\mathcal{F}^{\tau,r}\_{RLB}$ models a From 47d8eee80f725d44a8f2257106bd62d8d28391e4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= Date: Tue, 9 May 2023 20:21:34 -0300 Subject: [PATCH 23/24] Add a section on stakeholder states --- praos-design-decisions.md | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/praos-design-decisions.md b/praos-design-decisions.md index e7cc915..a89a6b8 100644 --- a/praos-design-decisions.md +++ b/praos-design-decisions.md @@ -322,3 +322,11 @@ Finally, the paper states that a stakeholder is allowed to diffuse once in a round. We enforce this restriction explicitly in the stakeholder process implementation, which broadcasts a chain once at the end of the current round should the stakeholder is elected as a slot leader. + +## Stakeholder state + +The paper assumes that a stakeholder internally stores certain type of +data, such as the set of chains and transactions received from the +network in the current slot. We define a specific structure to hold +all the data that is needed for a stakeholder to be able to run the +protocol, e.g., its transaction mempool. From 60369f45b1216af5fec6e80455f4d92b476a3039 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20D=C3=ADaz?= Date: Tue, 9 May 2023 20:25:01 -0300 Subject: [PATCH 24/24] Add a section on formal proofs of properties --- praos-design-decisions.md | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/praos-design-decisions.md b/praos-design-decisions.md index a89a6b8..47bc735 100644 --- a/praos-design-decisions.md +++ b/praos-design-decisions.md @@ -330,3 +330,14 @@ data, such as the set of chains and transactions received from the network in the current slot. We define a specific structure to hold all the data that is needed for a stakeholder to be able to run the protocol, e.g., its transaction mempool. + +## Formal proofs of properties + +Currently, our specification of the protocol is accompanied by a +battery of formal proofs, which comprise basically sanity checks +of the sequential parts of the code, as well as proofs of very +basic properties such as the "independent aggregation" property +stated in the paper. For checking functions operating on +transactions, blocks and chains, we define appropriate state +transition systems which constitute a sort of "mini-ledger", +very much in the spirit of the Cardano ledger specification.