\interactions^{j}_{2}  ~ \cdot ~ \interactions'^j_2
& ~\Big|~ & \keystore \drawnFrom \Gen(1^n); ~ (pk^i, sk^i) \in rng(\keystore); ~ b^i_2 \drawnFrom \Enc(pk^i, m^i_2); ~ 1 \leq i \leq k; ~ \\
&& t, v_{\{0,1\}}, \strategy \drawnFrom \adversary(1^n); ~
\interactions'^{s}_2 \drawnFrom \strategy(\interactions^{s}_2 \cdot ... \cdot \interactions^{j}_2 \cdot \interactions'^{j}_2); ~ 1 < s < j; ~ \interactions'^{j}_2 \drawnFrom \strategy(\skipcmd)
~ \big\}_n \\
\end{array}
\]

For all families of distributions $\interactionsdist_1$ and  $\interactionsdist_2$, if $\interactionsdist_1 \asymp \interactionsdist_2$ and $\cryptosys$ is CPA secure, then $\interactionsdist_1 \approx \interactionsdist_2$.

Similar to the previous rounds, we will reduce this problem to the Round 2 Secret and Low Equivalent Interactions indistinguishability problem. If there exists a Round 3 adversary $\adversary_{R3}$ then there also exists a Round 2 adversary, which will provide a contradiction.

We construct our adversary as follows. Given a sequence of low equivalent interactions (from Round 2) $\interactions_1$ and $\interactions_2$, we subdivide the interactions into sequences of interactions $\interactions^1_{\{1,2\}} ... \interactions^j_{\{1,2\}}$. We also add the categories in storing category keys arbitrarily in a static way and also add the category key signatures (as it was not in the previous round) by just performing the signing process according to the function.

For the strategy interactions, we just perform the draws from the strategy starting from the end of the sequences of interactions, working backwards and place them in their corresponding positions, i.e., $\interactions'^{s} \drawnFrom \strategy(\interactions^{s} \cdot ... \cdot \interactions'^{j} \cdot \interactions^{j}$ for $1 < s < j$. We note that, although the interactions may differ they are indistinguishable. That is because the first sequence of interactions $\interactions^j_{\{1,2\}}$ is a sub-problem of the Round 2 sequences of interactions. As a result, since the two sequences of interactions are computationally indistinguishable, then their corresponding draws from the strategy are also computationally indistinguishable.

As a result, we can then pass the final sequence of interactions to $\adversary_{R2}$ to distinguish the distributions.
Since we have shown how to construct a Round 2 adversary from a Round 3 adversary, we have a contradiction of the Round 2 lemma, so we conclude our proof.

§.§ Preservation of Low Equivalence

We will prove this lemma in two steps: first by showing that the invariant is preserved across steps $\rto{p}^*$ and then using that fact, we can show that the invariant is also preserved across low steps $\Lowstep{p}$.

Proof on Step relation $\rto{p}$: We will perform induction on the derivation of the steps (which will be finite when used with the low-step rules, i.e., it is well-founded) with the number of steps being $k$ being 1 less than the total number of (possibly high) steps in the context of a single low step.

Our inductive hypothesis will be if $\rconf{c_1}{\emptyset}{\skipcmd}{\versions_1} \lowEquivC \rconf{c_2'}{\emptyset}{\skipcmd}{\versions_2}$ and $\cryptosys$ is CPA Secure, then,

\hspace*{1cm} \textbf{Pr}\Big[
\rconf{c_1'}{\istoredist_1}{\interactionsdist_1}{\versions_1}
\not\lowEquivC
\rconf{c_2'}{\istoredist_2}{\interactionsdist_2}{\versions_2}
\textor
\versions_1 \neq \versions_2
~~\Big| ~\newline \hspace*{2cm}
~\keystore \drawnFrom \Gen(\principals, 1^n); ~
\keystore_1 = \keystore_0 \uplus \keystore; ~
\rconf{c_1}{\emptyset}{\skipcmd}{\zeroes} \rto{p_1} ... \rto{p_k}
\rconf{c_1'}{\istoredist_1}{\interactionsdist_1}{\versions_1};  \newline
\hspace*{2cm}
\keystore' \drawnFrom \Gen(\principals, 1^n); ~
\keystore_2 = \keystore_0 \uplus \keystore'; ~
\rconf{c_2}{\emptyset}{\skipcmd}{\zeroes} \rto{p_1'} ... \rto{p_{k'}'}
\rconf{c_2'}{\istoredist_2}{\interactionsdist_2}{\versions_2}
\Big]$

is negligible in $n$, and    $\hspace*{0cm} \Big\{  ~~ \interactions_1 ~~ \Big| ~~
\keystore' \drawnFrom \Gen(\principals, 1^n); ~
\keystore = \keystore_0 \uplus \keystore'; ~
\rconf{c_1}{\emptyset}{\skipcmd}{\zeroes} \rto{p_1} ... \rto{p_k}
\rconf{c_1'}{\istoredist_1}{\interactionsdist_1}{\versions_1}; ~ \interactions_1 \drawnFrom \interactionsdist_1 ~ ~ \Big\}_n \newline
\hspace*{7cm} \asymp \newline
\hspace*{0.5cm} \Big\{  ~~ \interactions_2 ~~ \Big| ~~
\keystore' \drawnFrom \Gen(\principals, 1^n);~
\keystore = \keystore_0 \uplus \keystore';~
\rconf{c_2}{\emptyset}{\skipcmd}{\zeroes} \rto{p_1'} ... \rto{p_{k'}'}
\rconf{c_2'}{\istoredist_2}{\interactionsdist_2}{\versions_2}; ~ \interactions_2 \drawnFrom \interactionsdist_2 ~ \Big\}_n $

. We must show as our inductive step that if our inductive hypothesis is true,
that the following is true:

\hspace*{0.5cm} \textbf{Pr}\Big[
\rconf{c_1''}{\istoredist_1'}{\interactionsdist_1'}{\versions_1'}
\not\lowEquivC
\rconf{c_2''}{\istoredist_2'}{\interactionsdist_2'}{\versions_2'}
~~\Big| \newline \hspace*{2cm}
~\keystore \drawnFrom \Gen(\principals, 1^n); ~
\keystore_1 = \keystore_0 \uplus \keystore; ~
\rconf{c_1}{\emptyset}{\skipcmd}{\zeroes} \rto{p_1} ... \rto{p_k}
\rconf{c_1'}{\istoredist_1}{\interactionsdist_1}{\versions_1}  \rto{p_{k+1}}
\rconf{c_1''}{\istoredist_1'}{\interactionsdist_1'}{\versions_1'};  \newline
\hspace*{2cm}
\keystore' \drawnFrom \Gen(\principals, 1^n); ~
\keystore_2 = \keystore_0 \uplus \keystore'; ~
\rconf{c_2}{\emptyset}{\skipcmd}{\zeroes} \rto{p_1'} ... \rto{p_{k'}'}
\rconf{c_2'}{\istoredist_2}{\interactionsdist_2}{\versions_2}
\rto{p'_{k'+1}}
\rconf{c_2''}{\istoredist_2'}{\interactionsdist_2'}{\versions_2'}
\Big]$
is negligible in $n$, and
$\hspace*{0cm} \Big\{  ~~ \interactions_1' ~~ \Big| ~~
\keystore' \drawnFrom \Gen(\principals, 1^n); ~
\keystore = \keystore_0 \uplus \keystore'; ~
\rconf{c_1}{\emptyset}{\skipcmd}{\zeroes} \rto{p_1} ... \rto{p_k}
\rconf{c_1'}{\istoredist_1}{\interactionsdist_1}{\versions_1}  \rto{p_{k+1}}
\rconf{c_1''}{\istoredist_1'}{\interactionsdist_1'}{\versions_1'}; ~ \interactions'_1 \drawnFrom \interactionsdist'_1 ~ \Big\}_n \newline~
\hspace*{8cm} \asymp \newline~
\hspace*{0.5cm} \Big\{  ~~ \interactions'_2 ~~ \Big| ~~
\keystore' \drawnFrom \Gen(\principals, 1^n);~
\keystore = \keystore_0 \uplus \keystore';~
\rconf{c_2}{\emptyset}{\skipcmd}{\zeroes} \rto{p_1'} ... \rto{p_{k'}'}
\rconf{c_2'}{\istoredist_2}{\interactionsdist_2}{\versions_2}
\rto{p'_{k'+1}}
\rconf{c_2''}{\istoredist_2'}{\interactionsdist_2'}{\versions_2'}; ~ \interactions'_2 \drawnFrom \interactionsdist'_2  ~ \Big\}_n $

The base case $k=0$ is direct as the initial interactions are a special case of interactions (i.e., $\skipcmd = \skipcmd$) and $\zeroes = \zeroes$ and we already know by supposition that $c_1 \lowEquivC c_2$.

For the inductive case, we now consider the derivation rule used for the $k+1$'th step and show that it preserves the inductive hypothesis, assuming it for the $k$'th step.

We note that the single steps may take differing numbers of steps (i.e., $k$ and $k'$). Due to the Low-to-High-to-Low step rule, though, these differences only occur when $\lcur$ is high. As a result, the only invariant we need to preserve is confidentiality-only low equivalence between configurations as the high steps do not change the versions, stores, or interactions. We can appeal to the preservation of low equivalence of LIO proved by Stefan et al. <cit.> to conclude the preservation confidentiality-only low equivalence of the standard (i.e., non-store and non-fetch) LIO internal steps. We now consider the low steps that affect the non-standard parts of LIO (i.e., the store and fetch commands).

We also note that since there are only a polynomial number of steps that the resulting sequences of configurations from single steps that do not preserve low equivalent in each step will still together be negligible. As a result, we only need to show that the probability of each step not preserving low equivalence is negligible in $n$. To that end, we will ignore the traces of steps with negligible probabilities that are not low equivalent.

* Case Fetch (Fetch-Exists, Fetch-Missing, or Fetch-Replay):

In this case, both configurations have a term with an evaluation context hole that is at a fetch command. That is, they are both attempting to fetch an entry from the store with key $\gv_k$ and $\gv_k'$. Due to low equivalence they are both fetching the same key, $\gv_k = \gv_k'$. As a result, they must each be using one of the following rules: Fetch-Exists, Fetch-Missing, or Fetch-Replay.

We know by our inductive hypothesis that the distributions of interactions are equivalent. Because the distributions are equal, we can consider steps where the draws are equivalent for values in the erased distributions.
We now consider now each case that $c_1'$  transitions with.

* Case  Fetch-Exists and $\canFlowToC{\projC{l_1}}{\projC{\lowlabel}}$: In this case the labeled value will be deserialized the same way and the same labeled value will be fetched. Since the labeled value is readable by the adversary it must be syntactically equivalent with all but negligible probability, otherwise the interactions would be distinguishable which would be a counter-example to Lemma <ref>. As a result, low equivalence will be preserved and both configurations will transition in the same way with all but negligible probability.

* Case  Fetch-Exists and $\cantFlowToC{\projC{l_1}}{\projC{\lowlabel}}$:
In general the value fetched from the store will vary, or it may be the case that only some of the time a value can even be deserialized.
In these cases, the configurations may transition using this rule and other interactions from the distribution may result in it using another rule.
However, if $c_2'$ transitions using another fetch rule (Fetch-Missing or Fetch-Replay),
the default value will be used. Since secret values can differ and still be low equivalent,
the resulting two configurations will still be low equivalent.  In each of these cases,
no new interactions are produced so the resulting distributions of interactions are still valid interactions by our inductive hypothesis (as they did not change).
As a result, low equivalence and the valid interactions invariant is preserved.

* Case  Fetch-Missing or Fetch-Replay: In these cases, the default labeled value will be used, which by our inductive hypothesis is already low equivalent (due to the configurations being low equivalent).
The other configurations will transition in a symmetric way described for the Fetch-Exists rule.

* Case Store:

In this case the distribution of stores and interactions will change
so we must show that they remain equivalent. That is, we must show that $\{ ~ \interactions'_1 ~|~ \interactions'_ \drawnFrom \interactionsdist'_1 \}_n \asymp \{ ~ \interactions'_2 ~|~ \interactions'_2 \drawnFrom \interactionsdist'_2 \}$ where

\begin{array}{l<{\hspace{-2mm}}c<{\hspace{-2mm}}l<{\hspace{-2mm}}l}
\interactionsdist_1' &=& \big\{ ~ & \concat{\concat{\storecmd{\gv_k}{\Labeled{l_1}{\bitstream_1}}}{\interactionsprime_1}}{\interactions_1} ~ ~ \Big|~ ~
\interactions_1 \drawnFrom \interactionsdist_1;  \arcr
%\probabilityOf{(\interactionsprime, \Labeled{l_1}{\bitstream}) =
(\interactionsprime_1, \Labeled{l_1}{\bitstream_1}) \drawnFrom \serialize{\istore_1}{\Labeled{l_1}{(\gv, \gv_k, \version_1)}}
~ \big\} \arcr
% \istoredist'_1 &=& \big\{~ & \interactions_1(\sigma_1) ~\Big|~ \istore_1 \drawnFrom \istoredist_1;~ \interactions_1 \drawnFrom \interactionsdist_1 ~ \big\}
\\
\interactionsdist_2' &=& \big\{ ~ & \concat{\concat{\storecmd{\gv_k}{\Labeled{l_1}{\bitstream_2}}}{\interactionsprime_2}}{\interactions_2} ~ ~ \Big|~ ~
\interactions_2 \drawnFrom \interactionsdist_2;  \arcr
%\probabilityOf{(\interactionsprime, \Labeled{l_1}{\bitstream}) =
(\interactionsprime_2, \Labeled{l_1}{\bitstream_2}) \drawnFrom \serialize{\istore_2}{\Labeled{l_1}{(\gv, \gv_k, \version_2)}}
~ \big\} \arcr
% \istoredist'_2 &=& \big\{~ & \interactions_2(\sigma_2) ~\Big|~ \istore_2 \drawnFrom \istoredist_2;~ \interactions_2 \drawnFrom \interactionsdist_2 ~ \big\}
\end{array}

We first note that the entry keys are the same from low equivalence. The versions are equal from low equivalence, i.e., $\version_1 = \version_2$. We also note that the distributions of interactions are valid interactions from our inductive hypothesis. For readable labeled values, we can conclude that they are  syntactically equivalent values from low equivalence. For non-readable values, the types of the secret values will be the same due to low equivalence (and so the serialized plaintext message will have the same length). As a result the $\storecmd{\gv_k}{\Labeled{l_1}{b_{\{0,1\}}}}$ will be a valid extension of valid interactions.

We next consider the creation of category keys (i.e.,
$\interactionsprime_1$ and $\interactionsprime_2$). The initialization of category keys will behave the same way as described for fetching a labeled value: it will either create new keys (if they were corrupted or not there), or $\skipcmd$. It will do this in the same way as the resulting interactions are indistinguishable. For the contents of the category keys, we can divide the parts of the category into deterministic parts (i.e., from Lemma <ref>) and secret encryptions.

With these considerations, we conclude that with all but negligible probability the resulting interactions will be valid interactions.

Finally, for the versions mappings, we note that they are both updated equivalently (i.e., incremented by the version in the mapping) and the versions mappings originally were equal, so the resulting versions are equal.

With all cases of the reduction shown to satisfy the proof obligation, we can conclude the inductive hypothesis is true for all steps used in the context of a single low step. We next show the low equivalence invariant on the low step relation.

Proof on Low-step relation $\Lowstep{p}$: by induction on the number of low steps $j$. Our inductive hypothesis will match our lemma.

* Base Case: $j = 1$: That is, we will prove the following:

We must show $\rconf{c_1'}{\istoredist_1}{\interactionsdist_1}{\versions_1}
\lowEquivC
\rconf{c_2'}{\istoredist_2}{\interactionsdist_2}{\versions_2} \textor \versions_1 \neq \versions_2$.
There are two cases we must consider in the low step relation, the Low-Step rule and the Low-to-High-to-Low-Step rule. In the Low-Step, we must show that the inductive hypothesis holds after a single step $\rto{p}$, and for the Low-to-High-to-Low-Step rule must hold for many (finite) steps $\rto{p}^*$. Note that the Low-Step rule is a special case of the Low-to-High-to-Low-Step rule so we only consider the more general case of preserving the invariant across many steps. To show this, we appeal to the previous proof made to show that the invariant is preserved across steps.

Unlike the single step relation, this includes a strategy interaction on the distribution of stores. Since both interactions receive the indistinguishable  distributions of interactions (from Lemma <ref> and the inductive hypothesis) so the resulting distributions from the strategy will also be computationally indistinguishable. That is because if they were not, then the strategy itself could be used as a counter-example for Lemma <ref>. In sum, the resulting strategy invocation results in a valid sequence of interactions.

From the previous proof on the single-step relation, we can conclude that
As a result, we satisfy the inductive hypothesis.

* Inductive Case $j=k+1$: That is, we will prove the following:

We now must show that, for any low equivalent configurations that the resulting single step will remain low equivalent.
We can use the same reasoning from the base case to show that the adversary interaction preserves equivalence on distributions of stores.

After this adversary interaction, we can invoke the single-step lemma result here to conclude that $c_1'' \lowEquiv c_2''$.

With the single low step relation handled we now must consider the distribution of distributions of interactions from the $\multistepnm$ function. For example, it may be the case that a particular distribution of interactions generated from one trace of low steps may be much more likely than another distribution of interactions. However, we can use the preservation of low equivalence to reason about the probabilities of corresponding low equivalent distributions of interactions.
We consider the distribution formed from the step function after 1 low step as a running example to make our arguments concrete, shown graphically in the main matter in <Ref>.

From our inductive hypothesis we know that corresponding low equivalent configurations have indistinguishable distributions of interactions. We now must consider the relationship between the probabilities that led to the corresponding low equivalent configurations (e.g., from the diagram $p_1$ and $p_2$, and also $p_1'$ and $p_2'$). If they are similar, then the resulting draws from the distributions will be similar (from low equivalence).

Consider the pairs of low equivalent configurations and the probabilities that led to those configurations (e.g., from the diagram $\rconf{c_1'}{\istoredist_1}{\interactionsdist_1}{\versions_1}$ with probability $p_1$ and $\rconf{c_2'}{\istoredist_2}{\interactionsdist_2}{\versions_2}$ with probability $p_2$).
Consider the ways the configurations can differ probabilistically (e.g., from the diagram, how $c_1$ steps to both $c_1'$ and $c_1''$ and how $c_2$ steps to both $c_2'$ and $c_2''$).
The low step relation is just the probability of the trace of single steps leading to the next low configuration. The Store and Internal-Step rules take steps with probability $1$ so they will not cause the low step to differ probabilistically.

Indeed, only the fetching rules Fetch-Exists, Fetch-Missing, and Fetch-Replay rules will cause the configurations to differ probabilistically. In particular they will differ based on the interactions drawn,  and as a result differ on how those interactions affect the fetch: if the entry is missing or not deserializeable (Fetch-Missing), if the value can be deserialized but the version is old (Fetch-Replay), or if it was successfully deserialized and the version is not old (Fetch-Valid).

Due to our inductive hypothesis we know that the distributions of interactions are valid interactions and as a result are indistinguishable from Lemma <ref>. For readable labeled values, the configurations will step with the same probability in lock-step with all but negligible probability, as the readable labeled values will be syntactically equivalent (as the distributions of erased stores are equivalent).

In the case where the label of the labeled value is not readable, the rules used to step may not be the same as they are the results of encrypted values.
For example, in one configuration a labeled value may be successfully fetched (using Fetch-Valid) but not in the corresponding configuration (e.g., Fetch-Missing was used). However, as noted above and by our inductive hypothesis, the different rules used will all step to a low equivalent configuration.
In addition, though, to the configurations being low equivalent, it is also the case that the sums of the probabilities of all steps taken will be equivalent with all but negligible probability. For example, if $c_1$ steps using Fetch-Missing with probability $p_1$, and Fetch-Valid with probability $p_2$, it is also the case that $c_2$ will use the same rules Fetch-Missing with probability $p_1$ and Fetch-Valid with probability $p_2$ due to indistinguishability of the interactions. That is because if it did not, then an adversary could be constructed to distinguish the interactions based on the proportions of rules used by the semantics. Intuitively, the draws of indistinguishable interactions will produce distributions of indistinguishable steps.

With this reasoning, we conclude that the probabilities of each corresponding single step taking place will be equal (e.g., in the diagram above, $p_1 = p_2$ and $p_2 = p_2'$). So, the resulting distribution of distributions over interactions will be still be valid interactions and so the $\asymp$ relation holds (and, by Lemma <ref>, they are also indistinguishable as a result).

§.§ Indistinguishability Proof

Let the random variable $\IND{b}{\keystore}{\adversary}{\principals}{j}{n}$ denote
the output of the following experiment, where
$\cryptosys = (\Gen, \Enc, \Dec, \Sign, \Verify)$,
$\adversary$ is a non-uniform ppt, $n \in \nat$, $b \in \{0,1\}$:

\figCTAGame

We say that using is CTA (Chosen-Term Attack) Secure if for all
non-uniform ppt $\adversary$, $j \in \nat$, keystores , and principals $\principals$:

\distfam{\IND{0}{\keystore}{\adversary}{\principals}{j}{n}} \cequiv
\distfam{\IND{1}{\keystore}{\adversary}{\principals}{j}{n}}

If if CPA Secure, then using is CTA Secure.

Direct result of low equivalence (interactions are valid interactions, i.e., they satisfy the $\asymp$ relation) and Lemma <ref> (indistinguishability of valid interactions).

§.§ Leveraged Forgery Lemmas

For all keystores $\keystore_0$ and terms $t$ and strategies $\strategy$ and principals $\principals$ and $j$,

\begin{array}{l}
\textbf{Pr}\Big[
~~\Big| \\
\hspace*{0.5cm} \keystore' \drawnFrom \Gen(\principals, 1^n); \\
\hspace*{0.5cm} \keystore = \keystore_0 \uplus \keystore'; \\
\hspace*{0.5cm} \rconf{c}{\istoredist}{\interactionsdist}{\versions} \drawnFrom \multistep{\keystore}{\conf{\Start{\keystore_0}}{\Clr{\keystore_0}}{t}}{\strategy}{j}
\Big] = 0
\end{array}

We will prove this lemma in two steps: first by showing that the invariant is preserved across steps $\rto{p}^*$ and then using that fact, we can show that the invariant is also preserved across low steps $\Lowstep{p}*$. Our invariant will serve as our inductive hypothesis in both cases.

Proof on Step relation $\rto{p}$: We will perform induction on the derivation of the steps (which will be finite when used with the low-step rules, i.e., it is well-founded) with the number of steps being $k$ being 1 less than the total number of (possibly high) steps in the context of a single low step, and our inductive hypothesis will be if  $\canFlowToStrictI{\projI{\pcOf{c}}}{\projI{\Start{\keystore_0}}}$ and,

\hspace*{4cm} \textbf{Pr}\Big[
~~\Big| \newline
\hspace*{5cm} \keystore' \drawnFrom \Gen(\principals, 1^n); \newline~
\hspace*{5cm} \keystore = \keystore_0 \uplus \keystore'; \newline~
\hspace*{5cm}
\rconf{c}{\emptyset}{\skipcmd}{\zeroes} \rto{p_1} ... \rto{p_k}
\rconf{c'}{\istoredist'}{\interactionsdist'}{\versions'}
\Big] = 0

\hspace*{4cm} \textbf{Pr}\Big[
~~\Big| \newline~
\hspace*{5cm} \keystore' \drawnFrom \Gen(\principals, 1^n); \newline~
\hspace*{5cm} \keystore = \keystore_0 \uplus \keystore'; \newline~
\hspace*{5cm}
\rconf{c}{\emptyset}{\skipcmd}{\zeroes} \rto{p_1} ... \rto{p_k}
\rconf{c'}{\istoredist}{\interactionsdist}{\versions} \rto{p_{k+1}}
\rconf{c''}{\istoredist'}{\interactionsdist'}{\versions'}
\Big] = 0

The base case $k=0$ is trivial as it is true by supposition.

For the inductive case, we now consider the derivation rule used for the $k+1$'th step and show that it preserves the inductive hypothesis, assuming it for the $k$'th step. We now perform a case analysis on the step used.

* Case Internal-Step:

In this derivation we have that:

[internal step]
c' c”

c' 1 c”''_1

By inspection of each of the LIO rules, the label is manipulated in the following ways:

* In Unlabel, the current label is joined with the level of the labeled value, so the flows relation between the current label and the starting label is preserved.

* In Reset the label is returned to its original label. However, from the ToLabeled rule, the label is based on the current label. As a result, since the label is based on a previous step's current label, and the inductive hypothesis assumes it was true for that point, then the label it is reset to is also satisfies the flow relation to the starting label.

* In all other rules, the current label is not changed, which by supposition satisfies the flow relation.

Proof on Low-Step relation p
By induction on $j$.

* Base Case: $j = 1$: That is, we will prove the following:

\begin{array}{l}
\textbf{Pr}\Big[
~~\Big| \\~
\hspace*{0.5cm} \keystore' \drawnFrom \Gen(\principals, 1^n); \\~
\hspace*{0.5cm} \keystore = \keystore_0 \uplus \keystore'; \newline~
\hspace*{0.5cm} \rconf{c}{\istoredist}{\interactionsdist}{\versions} \drawnFrom \multistep{\keystore}{\conf{\Start{\keystore}}{\Clr{\keystore}}{t}}{\strategy}{1}
\Big] = 0
\end{array}

There are two cases we must consider in the low step relation, the Low-Step rule and the Low-to-High-to-Low-Step rule. In the Low-Step, we must show that the inductive hypothesis holds after a single step $\rto{p}$, and for the Low-to-High-to-Low-Step rule must hold for many (finite) steps $\rto{p}^*$. Note that the Low-Step rule is a special case of the Low-to-High-to-Low-Step rule so we only consider the more general case of preserving the invariant across many steps. To show this, we appeal to the previous proof made to show that the invariant is preserved across steps. As a result, we have that:

\hspace*{4cm} \textbf{Pr}\Big[
~~\Big| \newline~
\hspace*{5cm} \keystore' \drawnFrom \Gen(\principals, 1^n); \newline~
\hspace*{5cm} \keystore = \keystore_0 \uplus \keystore'; \newline~
\hspace*{5cm}
\rconf{c}{\emptyset}{\skipcmd}{\zeroes} \rto{p_1} ... \rto{p_k}
\rconf{c'}{\istoredist}{\interactionsdist}{\versions}
\Big] = 0$

From the previous proof on the single-step relation, we can conclude that $\canFlowToStrictI{\projI{\pcOf{c}}}{\projI{\Start{\keystore_0}}}$. As a result, we satisfy the inductive hypothesis.

* Inductive Case: j = k+1: That is, we will prove the following:

\begin{array}{l}
\textbf{Pr}\Big[
~~\Big| \newline~
\hspace*{0.5cm} \keystore' \drawnFrom \Gen(\principals, 1^n); \\~
\hspace*{0.5cm} \keystore = \keystore_0 \uplus \keystore'; \newline~
\hspace*{0.5cm} \rconf{c}{\istoredist}{\interactionsdist}{\versions} \drawnFrom \multistep{\keystore}{\conf{\Start{\keystore}}{\Clr{\keystore}}{t}}{\strategy}{k+1}
\Big] = 0
\end{array}

We can expand the $\multistepnm$ metafunction to be

$ \hspace*{4cm}
\big(\rconf{c''}{\istoredist''}{\interactionsdist''}{\versions'}, p \cdot p'\big)
\newline~ \hspace*{4.5cm} \mathrm{where} \newline~ \hspace*{5cm}
\big(\rconf{c'}{\istoredist'}{\interactionsdist}{\versions}, p\big) \in \multistep{\keystore}{c}{\strategy}{k}; \newline~ \hspace*{5cm}
\interactionsdist' = \strategy(\interactionsdist); \newline~ \hspace*{5cm}
\Lowstep{p'}
\rconf{c''}{\istoredist''}{\interactionsdist''}{\versions'}

The strategy on the stores does not affect the current label.

After this adversary interaction, we can invoke the single-step lemma result here to conclude that $\canFlowToStrictI{\projI{\pcOf{c''}}}{\projI{\Start{\keystore_0}}}
$. As a result, the inductive hypothesis is true.

With all cases accounted for in the low step relation, and the single-step relation, we can conclude the proof.

§.§ Leveraged Forgery Security Proof

Define the Values function as follows:

\[
\begin{array}{lcll}
\mathrm{Values}_{\keystore}(\concat{\storecmd{\gv_k}{\Labeled{l_1}{b}}}{\interactions}) &=&   \concat{\storecmd{\gv_k}{\Labeled{l_1}{b}}}{\mathrm{Values}(\interactions)} & \textif \Labeled{l_1}{(\gv, \gv_k, n)} = \deserialize{\interactions}{\Labeled{l_1}{b}} \\
\mathrm{Values}_{\keystore}(\concat{\interaction}{\interactions}) &=&   \mathrm{Values}(\interactions) & \mathrm{otherwise}
\end{array}
\]

For all keystores $\keystore_0$, principals $p$ in principal sets $\principals$, and $j$ if $\cryptosys$ is secure against existential forgery under chosen message attacks, then
for all $~\canFlowToI{\projI{l_2}}{\canFlowToI{\projI{l_1}}{\projI{\authorityOf{\keystore_0}} \wedge p}}$,

\figForgeryProb

is negligible in $n$.

We consider the level required to produce a valid signature during a store operation. The signature must be valid for a $p \in \principals$. By inspection of the semantics, the only way to a valid signature would occur in the interaction is during the store operation, which uses the labeled value's label, or by the strategy.

According to the store operation, current label must be bounded above by the label
of the labeled value (i.e., $\canFlowTo{\lcur}{l_1}$). For integrity, this means
the current label's integrity component $I$ must be at least as trustworthy as the principal $p$.

By the previous lemma, we can conclude that the current integrity label will never be at a level $I'$ such that

\canFlowToStrictI{I'}{\projI{\Start{\keystore_0}}}$$

This means that the level of the computation would need to be at least

I = \projI{\authorityOf{\keystore_0 \uplus \{ p \mapsto \Gen(1^n) \} }}$$

By unpacking the definition of $\Start{\keystore \uplus \{ p \mapsto \Gen(1^n) \}}$, this integrity label satisfies the following relation

\canFlowToStrictI{ I }{ \projI{\Start{\keystore_0} }}

Which we have shown is impossible to reach. As a result, the current label's integrity level will never be at a level where it can sign the value using $p$'s private signing key.

As a result, the only way a high integrity value could be in the challenge store $\istore'$ and not in the original store $\istore$ would require the strategy to forge a signature itself without 's assistance. Since this occurs with
only negiglible probability, we have satisfied the proof obligation.

§.§ Soundness

Define $c_i \relatedclio c_r$ to be:

\begin{array}{llll}
\iconf{\conf{\lcur}{\lclr}{t}}{\istore_i} & \relatedclio & \rconf{\conf{\lcur}{\lclr}{t}}{\istore_r}{\interactions}{\versions} &
\mathrm{if~} \istore_i \relatedclio \istore_r \newline~
\istore_i[\gv_k \mapsto \Labeled{l_1}{\gv}] & \relatedclio & \istore_r[\gv_k \mapsto \Labeled{l_1}{b}] &
\mathrm{if~} \istore_i \relatedclio \istore_r \textand
\Labeled{l_1}{\gv} = \deserializevar{\istore_r}{\Labeled{l_1}{b}}{\typeOf{\gv}}
\end{array}

For all ideal configurations $c_i$, real configurations $c_r$, and strategies drawn from a non-uniform ppt adversary, if $c_i \relatedclio c_r$ then,

\begin{array}{l}
\textbf{Pr}\big[ (c_i', c_r') \not\in \relatedclio ~ \big| ~
\interactions \drawnFrom \strategy(\textsf{store}(c_r)); ~
\iinteractions = \mathcal{T}(c_r, \interactions); \newline~
\hspace*{22mm} (c_i, \iinteractions) \Lowstep{} c_i'; ~
(c_r, \interactions) \Lowstep{p} c_r'
\big]
\end{array}

is negligible in $n$.

§ IMPLEMENTATION DETAILS

In this section we discuss additional implementation details of our

§.§ Storing and Fetching

For each category used in the
program we generate a symmetric key and two RSA key pairs: an
encryption/decryption key pair and a signing/verification key
pair. This information is stored in the database after being
asymmetrically encrypted and then signed as described in
Section <ref>. Category key generation relies on the
RSA key pairs for each principal involved, which should be supplied by
the user in the form of an initial keystore when the computation

After the relevant IFC effects have been performed, storing a labeled
value involves fetching the symmetric key for each
category in its confidentiality clause as well as the signature keys
that correspond to each category in its integrity clause, potentially
generating these on the fly. The labeled value is serialized to a
bitstring, then RSA-PSS signed by at least one principal per integrity
category, and finally AES256-CTR onion-encrypted using the symmetric
key for each confidentiality category. Fetching involves the dual
operations, i.e., symmetric decryption and RSA-PSS signature

In order to avoid problems with improperly
escaped strings, we encode every bitstring in

§.§ User API

Our library provides all the  operations described in the
paper, plus a few extra functions that are necessary to glue code
with the rest of the program. Here are some of the most important ones.

code can be run using the  function. This
function takes two arguments: a record $\text{initialState}$ of type
and a computation $m$. The record
$\text{initialState}$ provides initial values for the current label,
the current clearance, the keystore, the version map and the store
label. The function simply establishes a connection with a Redis
and executes $m$ using
that database as the store and $\text{initialState}$ as the local

In order to generate keystores, we provide the utility function
. This function takes a list of principals
as argument, and produces a keystore with fresh asymmetric key pairs
for all of them. Our prototype does not provide means to store these
keystores beyond the execution of the program, but it would be
straightforward for users to implement this functionality in their own
programs, or with their own PKI.


# Bulging Triangles: Generalization of Reuleaux Triangles

Norihiro Someyama∗

(∗Shin-yo-ji Buddhist Temple, Tokyo, Japan
<EMAIL_ADDRESS>
ORCID iD: https://orcid.org/0000-0001-7579-5352)

###### Abstract

We introduce a bulging triangle like the generalization of the Reuleaux
triangle. We may be able to propose various ways to bulge a triangle, but this
paper presents the way so that its vertices are the same as them of the
original triangle. We find some properties and theorems of our bulging
triangles. In particular, we investigate, via calculus, whether basic facts
such as triangle inequalities and Pythagorean theorem hold for bulging
triangles.

Keywords: Reuleaux triangle, Covexity, Triangle inequality, Pythagorean
theorem.

2010 Mathematics Subject Classification: 51M04, 51M05, 51N20.

##  1 Introduction

There is the Reuleaux triangle (also called the spherical triangle) as one of
famous and notable figures in geometry. It is named after F. Reuleaux
(1829-1905), a German mechanical engineer. He considered a figure in which an
equilateral triangle is bulged in a natural way so that it has a constant
width. To be more precise, it is defined as follows:

Let $\triangle{\rm ABC}$ be an equilateral triangle consisting of vertices
${\rm A}$, ${\rm B}$ and ${\rm C}$. It namely holds that

$\displaystyle|\overline{{\rm AB}}|=|\overline{{\rm BC}}|=|\overline{{\rm
CA}}|$

where $\overline{{\rm AB}}$ denotes the side whose end points are ${\rm A}$
and ${\rm B}$, $|\overline{{\rm AB}}|$ denotes its length, and the other edges
are similar. We have a bulging equilateral triangle like Figure 1 by drawing
arcs with center ${\rm C}$ and radius $\overline{{\rm BC}}$, with center ${\rm
A}$ and radius $\overline{{\rm CA}}$ and with center ${\rm B}$ and radius
$\overline{{\rm AB}}$.

Figure 1: Reuleaux Triangle

The most notable property of the Reuleaux triangle is that it can rotate
completely while being within the square and touching all four sides of the
square. This property has been applied to architectural and engineering
technologies.

Any Reuleaux triangle has some trivial mathematical properties, e.g.,

  * •

it is (strictly) convex,

  * •

the “triangle inequality” holds, i.e., the sum of the lengths of any two
“round sides” is greater than the length of the remaining one “round side”,

  * •

the three “round sides” are equal and the common length is $\pi
a/3\fallingdotseq 1.047a$ if the length of one side of $\triangle{\rm ABC}$ is
$a$,

  * •

its area is $(\pi-\sqrt{3})a^{2}/2\fallingdotseq 1.628\times(\sqrt{3}a^{2}/4)$
(i.e., about 1.628 times the original area) if the length of one side of
$\triangle{\rm ABC}$ is $a$.

Moreover, Reuleaux triangles are widely applied in various fields and there is
no end to the list. See, e.g., [2] for the benefits and applications of
Reuleaux triangles. It is also well known that the Reuleaux triangle is one of
solutions for the Kakeya problem (see, e.g., [1] for more information).

Our aim in this paper is to introduce the “generalized” Reuleaux triangle with
different lengths on the three “round sides” and study the properties.

##  2 Main Topics

###  2.1 Definition of Bulging Triangles

Let $\triangle{\rm ABC}$ be a triangle. For convenience, think of this as an
acute triangle. We would like to make a figure that $\triangle{\rm ABC}$ is
bulged by the following way. Such a figure is called the bulging triangle
(stemmed) from $\triangle{\rm ABC}$ in this paper.

Figure 2: ${\rm AB}$-center ${\rm P}$

Consider the perpendicular bisector $\ell$ of side $\overline{{\rm AB}}$, and
find out the intersection point ${\rm P}$ of another side and $\ell$. Then,
remark that ${\rm P}$ lies on the longer ($\overline{{\rm BC}}$ in the case of
Figure 2) of the remaining two sides $\overline{{\rm BC}}$ and $\overline{{\rm
CA}}$. This fact is almost clear, but we will prove it later (Proposition
2.1). Determine intersection points ${\rm Q}$ and ${\rm R}$ in the same way
for sides $\overline{{\rm BC}}$ and $\overline{{\rm CA}}$. Here each ${\rm
P}$, ${\rm Q}$, ${\rm R}$ is, of course, uniquely determined. Note that

$\displaystyle|\overline{{\rm AP}}|$ $\displaystyle=|\overline{{\rm BP}}|,$
$\displaystyle|\overline{{\rm BQ}}|$ $\displaystyle=|\overline{{\rm CQ}}|,$
$\displaystyle|\overline{{\rm CR}}|$ $\displaystyle=|\overline{{\rm AR}}|.$

We obtain the “round side” of $\triangle{{\rm ABC}}$ by drawing the circular
arc whose center and radius are ${\rm P}$ and $|\overline{{\rm AP}}|\
(=|\overline{{\rm BP}}|)$, respectively. The other “round sides” are similarly
obtained. From the above, we have been able to define the “bulging triangle”
(Figure 3) that is naturally extended the Reuleaux triangle to the general
case. We can treat vertices of the original triangle as vertices of the
bulging triangle.

Figure 3: Bulging Triangle

In what follows, we set the following promises:

  * •

We write
$\stackrel{{\scriptstyle\rotatebox{-90.0}{{\tiny{\bf(}}}}}{{\triangle}}{\rm
ABC}$ for the bulging triangle whose vertices are ${\rm A}$, ${\rm B}$ and
${\rm C}$.

  * •

Its “round sides” are called edges of
$\stackrel{{\scriptstyle\rotatebox{-90.0}{{\tiny{\bf(}}}}}{{\triangle}}{\rm
ABC}$ and are denoted by $\widetilde{{\rm AB}}$, $\widetilde{{\rm BC}}$ and
$\widetilde{{\rm CA}}$. Their lengths are denoted by $|\widetilde{{\rm AB}}|$,
$|\widetilde{{\rm BC}}|$ and $|\widetilde{{\rm CA}}|$, respectively.

  * •

Three points ${\rm P}$, ${\rm Q}$ and ${\rm R}$ defined above are called
centers associated with edges of
$\stackrel{{\scriptstyle\rotatebox{-90.0}{{\tiny{\bf(}}}}}{{\triangle}}{\rm
ABC}$. We often abbreviate such ${\rm P}$ as the ${\rm AB}$-center and the
others are similar.

  * •

The radius (i.e., $\overline{{\rm AP}}$, $\overline{{\rm BP}}$, and so on) of
the sector consisting of ${\rm A}$, ${\rm B}$ and ${\rm P}$ is called the
${\rm AB}$-radius. The others are similar.

  * •

The “length of the radius” is simply abbreviated as “the radius” throughout
this paper.

######  Remark 2.1.

If $\triangle{\rm ABC}$ is an equilateral triangle, the ${\rm AB}$-center is
${\rm C}$, the ${\rm BC}$-center is ${\rm A}$ and the ${\rm CA}$-center is
${\rm B}$. Hence, the bulging triangle defined above is certainly an extension
of the Reuleaux triangle. $\blacklozenge$

###  2.2 Basic Properties of Bulging Triangles

######  Proposition 2.1.

The ${\rm AB}$-center ${\rm P}$ of the bulging triangle
$\stackrel{{\scriptstyle\rotatebox{-90.0}{{\tiny{\bf(}}}}}{{\triangle}}{\rm
ABC}$ is on the longer of the remaining two sides $\overline{{\rm
BC}},\overline{{\rm CA}}$. In other words, ${\rm P}$ is the internally
dividing point of either $\overline{{\rm BC}}$ or $\overline{{\rm CA}}$. The
${\rm BC}$-center and ${\rm CA}$-center are similar.

###### Proof.

Assume $\angle{\rm ABC}<\angle{\rm BAC}$ and denote by ${\rm P}$ the point
such that $|\overline{{\rm AP}}|=|\overline{{\rm BP}}|$. Then,

$\displaystyle\angle{\rm BAP}=\angle{\rm ABC}<\angle{\rm BAC}$

and so ${\rm P}$ is on $\overline{{\rm BC}}$. Since ${\rm P}$ is the ${\rm
AB}$-center of
$\stackrel{{\scriptstyle\rotatebox{-90.0}{{\tiny{\bf(}}}}}{{\triangle}}{\rm
ABC}$, this completes the proof. ∎

The bulging triangle that dents at a vertex is not ideal. We need to check the
following fact.

######  Proposition 2.2.

Let
$\stackrel{{\scriptstyle\rotatebox{-90.0}{{\tiny{\bf(}}}}}{{\triangle}}{\rm
ABC}$ be any bulging triangle from $\triangle{\rm ABC}$.

  * 1)

If $\triangle{\rm ABC}$ is acute, then
$\stackrel{{\scriptstyle\rotatebox{-90.0}{{\tiny{\bf(}}}}}{{\triangle}}{\rm
ABC}$ is convex;

  * 2)

If $\triangle{\rm ABC}$ is right, then
$\stackrel{{\scriptstyle\rotatebox{-90.0}{{\tiny{\bf(}}}}}{{\triangle}}{\rm
ABC}$ is convex;

  * 3)

If $\triangle{\rm ABC}$ is obtuse, then
$\stackrel{{\scriptstyle\rotatebox{-90.0}{{\tiny{\bf(}}}}}{{\triangle}}{\rm
ABC}$ is concave.

###### Proof.

Without loss of generality, we can visualize
$\stackrel{{\scriptstyle\rotatebox{-90.0}{{\tiny{\bf(}}}}}{{\triangle}}{\rm
ABC}$ from $\triangle{\rm ABC}$ with $\angle{\rm BCA}=\angle R$. Note that the
${\rm BC}$-center and the ${\rm CA}$-center match and the common point is the
middle point of $\overline{{\rm AB}}$. In other words, $\widetilde{{\rm
BC}}+\widetilde{{\rm CA}}$ (i.e., the arc formed by connecting
$\widetilde{{\rm BC}}$ and $\widetilde{{\rm CA}}$) coincides with semi-
circular arc $\stackrel{{\scriptstyle\rotatebox{-90.0}{(}}}{{{\rm BA}}}$
containing point ${\rm C}$. By virtue of the above, the proof is easily
obtained. ∎

In response to the result of Proposition 2.2, we exclusively consider bulging
triangles from acute or right-angled triangles in this paper.

For convenience, we put the following term.

######  Definition 2.1.

Let $\triangle{\rm ABC}$ be a right-angled triangle with $\angle{\rm
BCA}=\angle R$. The bulging triangle from this $\triangle{\rm ABC}$ is denoted
by
$\stackrel{{\scriptstyle\rotatebox{-90.0}{{\tiny{\bf(}}}}}{{\triangle}}_{R}{\rm
BCA}$. The others are similar. Such a bulging triangle is called the right-
angled bulging triangle in this paper. In particular, we call
$\stackrel{{\scriptstyle\rotatebox{-90.0}{{\tiny{\bf(}}}}}{{\triangle}}_{R}{\rm
BCA}$ the isosceles right-angled bulging triangle if $|\overline{{\rm
BC}}|=|\overline{{\rm CA}}|$.

We study the edges of a bulging triangle from the famous right triangle. In
particular, the result for an isosceles right-angled bulging triangle can be
shown to be exactly the same as the conventional one.

######  Proposition 2.3.

For
$\stackrel{{\scriptstyle\rotatebox{-90.0}{{\tiny{\bf(}}}}}{{\triangle}}_{R}{\rm
BCA}$ with $|\overline{{\rm BC}}|=a$, it follows that

  * 1)

one has

$\displaystyle|\widetilde{{\rm AB}}|:|\widetilde{{\rm BC}}|:|\widetilde{{\rm
CA}}|=\sqrt{2}:1:1$

if $\angle{\rm ABC}=\pi/4$,

  * 2)

one has

$\displaystyle|\widetilde{{\rm AB}}|:|\widetilde{{\rm BC}}|:|\widetilde{{\rm
CA}}|=4:\sqrt{3}:2\sqrt{3}$

if $\angle{\rm ABC}=\pi/3$.

###### Proof.

We leave the proof of 1) to the reader and prove only 2).

Figure 4: Right-Angled Bulging Triangle

Since $|\overline{{\rm BC}}|=a$ and $\angle{\rm ABC}=\pi/3$, we have

$|\overline{{\rm AB}}|=2a,\quad|\overline{{\rm CA}}|=\sqrt{3}a,\quad\angle{\rm
BAC}=\frac{\pi}{6}.$

Denoting by ${\rm P}$ the ${\rm AB}$-center, ${\rm P}$ lies on $\overline{{\rm
CA}}$, the ${\rm AB}$-radius is $2a/\sqrt{3}$ and $\angle{\rm APB}=2\pi/3$.
Hence we have

$\displaystyle|\widetilde{{\rm AB}}|=\frac{4\sqrt{3}}{9}\pi a.$ (2.1)

(See Figure 4.) Denoting by ${\rm Q}$ the ${\rm BC}$-center, ${\rm Q}$ lies on
$\overline{{\rm AB}}$, the ${\rm BC}$-radius is $a$ and $\angle{\rm
BPC}=\pi/3$. Hence we have

$\displaystyle|\widetilde{{\rm BC}}|=\frac{1}{3}\pi a.$ (2.2)

Denoting by ${\rm R}$ the ${\rm CA}$-center, ${\rm R}={\rm Q}$, the ${\rm
CA}$-radius is $a$ and $\angle{\rm CPA}=2\pi/3$. Hence we have

$\displaystyle|\widetilde{{\rm CA}}|=\frac{2}{3}\pi a.$ (2.3)

(2.1)-(2.3) imply the claim, so the proof is complete. ∎

We investigate the relationship between the edge of the bulging triangle and
the angle of the original triangle. Take note that we can meet exactly the
same results for a usual triangle.

######  Proposition 2.4.

Let
$\stackrel{{\scriptstyle\rotatebox{-90.0}{{\tiny{\bf(}}}}}{{\triangle}}{\rm
ABC}$ be an isosceles (but not necessarily right-angled) bulging triangle.
That is, suppose

$\angle{\rm ABC}=\angle{\rm BCA},\quad i.e.,\quad|\overline{{\rm
AB}}|=|\overline{{\rm CA}}|.$

Then, one has

$|\widetilde{{\rm AB}}|=|\widetilde{{\rm CA}}|.$

Figure 5: Isosceles Right-Angled Bulging Triangle

###### Proof.

Denote by ${\rm P}$ and ${\rm Q}$ the ${\rm AB}$-center and ${\rm CA}$-center
of $\stackrel{{\scriptstyle\rotatebox{-90.0}{{\tiny{\bf(}}}}}{{\triangle}}{\rm
ABC}$, respectively (see Figure 5). It is obviously that $\overline{{\rm
QP}}\parallel\overline{{\rm BC}}$. Considering the perpendicular bisector $L$,
passing through point ${\rm A}$, of $\overline{{\rm BC}}$, it follows that
${\rm Q}$ is the point of symmetry of ${\rm P}$ with respect to $L$. ${\rm B}$
is also, of course, the point of symmetry of ${\rm C}$ with respect to $L$.
Hence, the claim clearly holds. This completes the proof. ∎

######  Proposition 2.5.

Suppose that $\triangle{\rm ABC}$ obeys

$\displaystyle 0<\angle{\rm ABC}<\angle{\rm BCA}\leq\frac{\pi}{2}.$ (2.4)

Then,
$\stackrel{{\scriptstyle\rotatebox{-90.0}{{\tiny{\bf(}}}}}{{\triangle}}{\rm
ABC}$ from such $\triangle{\rm ABC}$ satisfies that

$\displaystyle|\widetilde{{\rm CA}}|<|\widetilde{{\rm AB}}|.$ (2.5)

###### Proof.

Put

$\displaystyle a:=|\overline{{\rm BC}}|,\quad b:=|\overline{{\rm CA}}|,\quad
c:=|\overline{{\rm AB}}|$ (2.6)

and

$\displaystyle\alpha:=\angle{\rm BAC},\quad\beta:=\angle{\rm
ABC},\quad\gamma:=\angle{\rm BCA}.$ (2.7)

We prove tha claim by dividing into two patterns.

  * i)

The case of $\alpha\leq\beta$:

By noting that $\beta<\gamma$, we have

$\displaystyle|\widetilde{{\rm CA}}|=\frac{b}{2\cos\alpha}(\pi-2\alpha)$

and

$\displaystyle|\widetilde{{\rm AB}}|=\frac{c}{2\cos\alpha}(\pi-2\alpha).$

From $\beta<\gamma$ again, we obtain $b<c$. This implies (2.5).

  * ii)

The case of $\beta\leq\alpha$:

By noting that $\beta<\gamma$, we have

$\displaystyle|\widetilde{{\rm CA}}|=\frac{b}{2\cos\alpha}(\pi-2\alpha)$

and

$\displaystyle|\widetilde{{\rm AB}}|=\frac{c}{2\cos\beta}(\pi-2\beta).$

From $\beta<\gamma$ again, we obtain $b<c$. In order to gain (2.5), we should
prove

$\displaystyle\frac{\pi-2\alpha}{\cos\alpha}<\frac{\pi-2\beta}{\cos\beta}.$
(2.8)

Consider the function with respect to $\alpha\in(0,\pi/2)$,

$\displaystyle F(\alpha):=(\pi-2\beta)\cos\alpha-(\pi-2\alpha)\cos\beta,$

by fixing $\beta$. Since $0<\beta\leq\alpha<\pi/2$ and

$\displaystyle F^{\prime}(\alpha)=-(\pi-2\beta)\sin\alpha+2\cos\beta,$

we have

$\displaystyle F^{\prime\prime}(\alpha)=-(\pi-2\beta)\cos\alpha<0.$

We can thus concludes that $F$ is monotone decreasing.

$\lim_{\alpha\uparrow\pi/2}F(\alpha)=0$

regardless of the value of $\beta$, and so $F(\alpha)>0$ on $(0,\pi/2)$.
Therefore, we have shown (2.8) and can obtain (2.5).

Hence this completes the proof. ∎

Regarding the converse of Proposition 2.5, it seems that yet another
sufficient condition is necessary. This point is different from the property
of a usual triangle.

######  Proposition 2.6.

Let
$\stackrel{{\scriptstyle\rotatebox{-90.0}{{\tiny{\bf(}}}}}{{\triangle}}{\rm
ABC}$ be a bulging triangle that $\angle{\rm BAC}$ is the minimum internal
angle of $\triangle{\rm ABC}$. Then, $|\widetilde{{\rm AB}}|>|\widetilde{{\rm
CA}}|$ implies $\angle{\rm BCA}>\angle{\rm ABC}$.

###### Proof.

We adopt the notations, (2.6) and (2.7), again. We should prove that
$\beta<\gamma$ if $\alpha<\min\\{\beta,\gamma\\}$ and $|\widetilde{{\rm
CA}}|<|\widetilde{{\rm AB}}|$. Since $\alpha<\beta$ and $\alpha<\gamma$ by the
assumption, we have

$\displaystyle|\widetilde{{\rm AB}}|$
$\displaystyle=\frac{c}{2\cos\alpha}(\pi-2\alpha),$
$\displaystyle|\widetilde{{\rm CA}}|$
$\displaystyle=\frac{b}{2\cos\alpha}(\pi-2\alpha).$

Another assumption, $|\widetilde{{\rm AB}}|>|\widetilde{{\rm CA}}|$, then
implies $c>b$, and so we concludes $\gamma>\beta$. Hence this completes the
proof. ∎

###  2.3 Theorems and the Proofs

Recall that the triangle inequality always holds for any general triangle (see
[7] for the proofs). Let us first show that a property like the triangle
inequality holds for a bulging triangle.

######  Theorem 2.1.

For any
$\stackrel{{\scriptstyle\rotatebox{-90.0}{{\tiny{\bf(}}}}}{{\triangle}}{\rm
ABC}$, one has

$\displaystyle|\widetilde{{\rm AB}}|<|\widetilde{{\rm BC}}|+|\widetilde{{\rm
CA}}|.$ (2.9)

###### Proof.

The policy of this proof is similar to Proposition 2.5. Put (2.6) and (2.7)
again.

  * i)

The case of $\alpha\leq\beta$:

By noting that $\beta<\gamma$, we have

$\displaystyle|\widetilde{{\rm BC}}|=\frac{a}{2\cos\beta}(\pi-2\beta),$
$\displaystyle|\widetilde{{\rm CA}}|=\frac{b}{2\cos\alpha}(\pi-2\alpha)$

and

$\displaystyle|\widetilde{{\rm AB}}|=\frac{c}{2\cos\alpha}(\pi-2\alpha).$

The triangle inequality derives $b+c>a$, and so

$\displaystyle|\widetilde{{\rm CA}}|+|\widetilde{{\rm AB}}|$
$\displaystyle=\frac{b+c}{2\cos\alpha}(\pi-2\alpha)$
$\displaystyle>\frac{a(\pi-2\alpha)}{2\cos\alpha}.$

In order to gain (2.9), we should prove

$\displaystyle\frac{\pi-2\alpha}{\cos\alpha}>\frac{\pi-2\beta}{\cos\beta}.$
(2.10)

Consider the function with respect to $\alpha\in(0,\pi/2)$,

$\displaystyle F(\alpha):=-(\pi-2\beta)\cos\alpha+(\pi-2\alpha)\cos\beta,$

by fixing $\beta$. Since $0<\alpha\leq\beta<\pi/2$ and

$\displaystyle F^{\prime}(\alpha)=(\pi-2\beta)\sin\alpha-2\cos\beta,$

we have

$\displaystyle F^{\prime\prime}(\alpha)=(\pi-2\beta)\cos\alpha>0.$

We can thus concludes that $F$ is monotone increasing. We now put

$\displaystyle G(\beta):=\lim_{\alpha\downarrow
0}F(\alpha)=\pi\cos\beta+2\beta-\pi.$

Then it is easy to see that $G(\beta)>0$ on $(0,\pi/2)$, so we leave this
confirmation to the reader. It namely follows that $F(\alpha)>0$ on
$(0,\pi/2)$. Therefore, we have shown (2.10) and can obtain (2.9).

  * ii)

The case of $\beta\leq\alpha$:

The same discussion is repeated, so we leave it to the reader.

Hence this completes the proof. ∎

Let us next verify that “Pythagorean Theorem” holds only for a right-angled
bulging triangle whose two edges are equal.

######  Theorem 2.2.

For
$\stackrel{{\scriptstyle\rotatebox{-90.0}{{\tiny{\bf(}}}}}{{\triangle}}_{R}{\rm
BCA}$, it follows that

$\displaystyle\begin{cases}|\widetilde{{\rm AB}}|^{2}\geq|\widetilde{{\rm
BC}}|^{2}+|\widetilde{{\rm CA}}|^{2}&{\rm if}\ \angle{\rm
ABC}\in[\pi/4,\theta_{0}],\vspace{1mm}\\\ |\widetilde{{\rm
AB}}|^{2}<|\widetilde{{\rm BC}}|^{2}+|\widetilde{{\rm CA}}|^{2}&{\rm if}\
\angle{\rm ABC}\in(\theta_{0},\pi/2),\end{cases}$

where

$\displaystyle\theta_{0}:=\frac{\pi|\overline{{\rm CA}}|}{2(|\overline{{\rm
BC}}|+|\overline{{\rm CA}}|)}.$

The equality holds if $\angle{\rm ABC}=\theta_{0}$ or $|\overline{{\rm
BC}}|=|\overline{{\rm CA}}|$, i.e., $\angle{\rm ABC}=\angle{\rm BAC}=\pi/4$.

###### Proof.

Put $a:=|\overline{{\rm BC}}|$, $b:=|\overline{{\rm CA}}|$,
$c:=|\overline{{\rm AB}}|$. Without loss of generality, we can set that $a\leq
b$.

Figure 6: Coordinate Representation of Isosceles Right-Angled Bulging Triangle

We prove the claim by algebraic geometry. Set ${\rm A}(a,b)$, ${\rm B}(0,0)$
and ${\rm C}(a,0)$. Consider the ${\rm AB}$-perpendicular bisector $\ell_{{\rm
AB}}$. This is given by

$\displaystyle y=-\frac{a}{b}\left(x-\frac{a}{2}\right)+\frac{b}{2}.$

By finding the intersection point of $\ell_{{\rm AB}}$ and line $x=a$, we have
the ${\rm AB}$-center ${\rm P}(a,-a^{2}/2b+b/2)$. Thus, the ${\rm AB}$-radius
$r_{{\rm AB}}$ is given by

$\displaystyle r_{{\rm AB}}=|\overline{{\rm
AP}}|=b-\left(-\frac{a^{2}}{2b}+\frac{b}{2}\right)=\frac{a^{2}+b^{2}}{2b}.$

Denote by ${\rm M}$ the midpoint of segment $\overline{{\rm AB}}$ and put
$\theta:=\angle{\rm APM}=\angle{\rm BPM}$ (see Figure 6). It follows
$\tan\theta=b/a$, since obviously $\angle{\rm ABC}=\theta$. Hence,

$\displaystyle|\widetilde{{\rm AB}}|=\frac{a^{2}+b^{2}}{b}{\rm
Arctan}\,\frac{b}{a}.$ (2.11)

Similarly, we obtain

$\displaystyle|\widetilde{{\rm
BC}}|=\sqrt{a^{2}+b^{2}}\left(\frac{\pi}{2}-{\rm Arctan}\,\frac{b}{a}\right)$
(2.12)

and

$\displaystyle|\widetilde{{\rm CA}}|=\sqrt{a^{2}+b^{2}}{\rm
Arctan}\,\frac{b}{a}.$ (2.13)

By virtue of (2.11)-(2.13), we have

$\displaystyle|\widetilde{{\rm
AB}}|^{2}=\left(\frac{a^{2}+b^{2}}{b}\right)^{2}{\rm Arctan}^{2}\,\frac{b}{a}$
(2.14)

and

$\displaystyle\begin{aligned} &|\widetilde{{\rm BC}}|^{2}+|\widetilde{{\rm
CA}}|^{2}\\\ =&(a^{2}+b^{2})\left(\frac{\pi^{2}}{4}-\pi{\rm
Arctan}\,\frac{b}{a}+2{\rm Arctan}^{2}\,\frac{b}{a}\right).\end{aligned}$
(2.15)

We here put $t:={\rm Arctan}(b/a)$ and

$\displaystyle F(t)$ $\displaystyle:=\frac{(|\widetilde{{\rm
BC}}|^{2}+|\widetilde{{\rm CA}}|^{2})-|\widetilde{{\rm
AB}}|^{2}}{a^{2}+b^{2}}$ $\displaystyle\ =\frac{b^{2}-a^{2}}{b^{2}}t^{2}-\pi
t+\frac{\pi^{2}}{4}.$

Note that its domain is the interval $[\pi/4,\pi/2)$ from the assumption
“$a\leq b$”. The axis of the parabola $F$ which is convex downward is

$\displaystyle t=\alpha:=\frac{\pi b^{2}}{2(b^{2}-a^{2})}$

and

$\displaystyle\frac{b^{2}}{b^{2}-a^{2}}-1=\frac{a^{2}}{b^{2}-a^{2}}>0,\quad{\rm
i.e.,}\quad\frac{\pi}{2}<\alpha.$

Moreover, we have

$\displaystyle F(\pi/4)=\frac{\pi^{2}(b^{2}-a^{2})}{16b^{2}}\geq 0$

and

$\displaystyle\lim_{t\uparrow\pi/2}F(t)=-\frac{\pi^{2}a^{2}}{4b^{2}}<0.$

We find, by the intermediate value theorem, that $F$ has a unique zero point

$\displaystyle\theta_{0}=\frac{\pi b}{2(a+b)},$

and we concludes that $F\geq 0$ on $[\pi/4,\theta_{0}]$ and $F<0$ on
$(\theta_{0},\pi/2)$. Therefore, the claim has been proved and we have found
that “Pythagorean theorem” does not generally hold.

We find the condition for the equal sign to hold. It is obvious that the
equality holds if $\theta=\theta_{0}$ by virtue of the above discussion. If
$a=b$, we have $\theta=\pi/4$ and ${\rm Arctan}(b/a)=1$. Hence, from (2.14)
and (2.15), “Pythagorean theorem” holds:

$\displaystyle|\widetilde{{\rm AB}}|^{2}=|\widetilde{{\rm
BC}}|^{2}+|\widetilde{{\rm CA}}|^{2}\left(=\frac{\pi^{2}a^{2}}{4}\right).$

This completes the proof. ∎

######  Remark 2.2.

We check that the “triangle inequality” holds for right-angled bulging
triangle via the proof of Theorem 2.2. Since

$\displaystyle|\widetilde{{\rm AB}}|=\frac{a^{2}+b^{2}}{b}{\rm
Arctan}\,\frac{b}{a}$

and

$\displaystyle|\widetilde{{\rm BC}}|+|\widetilde{{\rm
CA}}|=\frac{\pi}{2}\sqrt{a^{2}+b^{2}},$

we need to prove

$\displaystyle\frac{\sqrt{a^{2}+b^{2}}}{b}{\rm
Arctan}\,\frac{b}{a}<\frac{\pi}{2}$ (2.16)

so as to see

$\displaystyle|\widetilde{{\rm AB}}|<|\widetilde{{\rm BC}}|+|\widetilde{{\rm
CA}}|.$

We obtain $\pi/4\leq{\rm Arctan}(b/a)<\pi/2$ because of the assumption “$a\leq
b$”. The left-hand side of (2.16) can be rewritten as

$\displaystyle\frac{\sqrt{a^{2}+b^{2}}}{b}{\rm Arctan}\,\frac{b}{a}=\frac{{\rm
Arctan}(b/a)}{\sin({\rm Arctan}(b/a))},$

so it is sufficient to verify that

$\displaystyle f(x)=\frac{x}{\sin x},\quad x\in[\pi/4,\pi/2),$

is strictly monotone increasing and $f(x)<\pi/2$. It is easy to see that fact,
so we leave it to the reader. We have (2.16) as a result. $\blacklozenge$

We finally investigate the relationship between the bulging triangle and the
circle. It is well known that any triangle is inscribed in a circle. We here
try a similar argument for right-angled bulging triangles. The method of the
proof of Theorem 2.2 is useful for this.

######  Theorem 2.3.

Any
$\stackrel{{\scriptstyle\rotatebox{-90.0}{{\tiny{\bf(}}}}}{{\triangle}}_{R}{\rm
BCA}$ is inscribed in a circle whose center is the midpoint ${\rm M}$ of ${\rm
A}$ and ${\rm B}$ and whose radius is $|\overline{{\rm AM}}|$.

Figure 7: Circumscribed Circle of Right-Angled Bulging Triangle

###### Proof.

We saw that $\widetilde{{\rm BC}}+\widetilde{{\rm CA}}$ is semi-circular arc
$\stackrel{{\scriptstyle\rotatebox{-90.0}{(}}}{{{\rm BA}}}$ containing ${\rm
C}$ in the proof of Proposition 2.2. Moreover, the center and radius of that
semi-circular arc are ${\rm M}$ and $|\overline{{\rm AM}}|$, respectively.
Denote by $C$ the circle whose center is ${\rm M}$ and whose radius is
$|\overline{{\rm AM}}|$. Consider the line ${\rm PM}$ (i.e., perpendicular
bisector $\ell$ of $\overline{{\rm AB}}$) and the intersection point ${\rm X}$
of $\ell$ and $C$ (see Figure 7). Recall

$\displaystyle{\rm M}(a/2,b/2),\quad{\rm P}(a,(-a^{2}+b^{2})/2b).$ (2.17)

Then, it is sufficient to prove that the ${\rm CA}$-radius is shorter than the
radius of the circumscribed circle, i.e.,

$\displaystyle|\overline{{\rm AP}}|<|\overline{{\rm XP}}|.$ (2.18)

It has already been obtained that

$\displaystyle|\overline{{\rm AP}}|=\frac{a^{2}+b^{2}}{2b}$ (2.19)

in the proof of Theorem 2.2. Since

$|\overline{{\rm XM}}|=|\overline{{\rm
AM}}|=\frac{c}{2}=\frac{\sqrt{a^{2}+b^{2}}}{2}$

and

$|\overline{{\rm MP}}|=\frac{a\sqrt{a^{2}+b^{2}}}{2b}$

from (2.17), we have

$\displaystyle|\overline{{\rm XP}}|=|\overline{{\rm XM}}|+|\overline{{\rm
MP}}|=\frac{(a+b)\sqrt{a^{2}+b^{2}}}{2b}.$ (2.20)

We should thus check

$\displaystyle\frac{(a+b)\sqrt{a^{2}+b^{2}}}{2b}>\frac{a^{2}+b^{2}}{2b}$
(2.21)

to prove (2.18), according to (2.19) and (2.20). We gain that

$\displaystyle\frac{(a+b)\sqrt{a^{2}+b^{2}}}{2b}-\frac{a^{2}+b^{2}}{2b}$
$\displaystyle=\frac{\sqrt{a^{2}+b^{2}}}{2b}\\{(a+b)-\sqrt{a^{2}+b^{2}}\\},$

but the triangle inequality for $\triangle{{\rm ABC}}$ implies that

$(a+b)-\sqrt{a^{2}+b^{2}}=(a+b)-c>0.$

So (2.21), i.e., (2.18) has obtained. This completes the proof. ∎

######  Remark 2.3.

The best feature of the above proof is to show (2.21), i.e.,

$a+b>\sqrt{a^{2}+b^{2}}.$

This was a paraphrase of the triangle inequality. The triangle inequality
seems to have already been considered trivial in ancient Greek times, but it
is quite interesting that such a trivial property is the essence of Theorem
2.3. $\blacklozenge$

##  3 Conclusion

We have defined the generalized Reuleaux triangles by one of many ways. Beside
this way, there is for instance a way to construct a generalization of the
Reuleaux triangle $\triangle{\rm ABC}$ as the closed and convex curve
consisting of three arcs centered on each ${\rm A}$, ${\rm B}$, ${\rm C}$.
That can be seen a little in [6]. As we can see from this, “generalization”
has many implications.

We have proved that “triangle inequalities” always hold but “Pythagorean
theorems” do not generally hold for bulging triangles defined in this paper.
Also, right-angled bulging triangles have good qualities (the latter claim of
Theorem 2.2 and Remark 2.2). In that sense, our definition of the
generalization of Reuleaux triangles would be moderately appropriate.

We may however be able to define new bulging triangles satisfying the above
two properties. In addition, there are a number of topics left by this paper:

  * •

We can easily obtain the area of a Reuleaux triangle (see Introduction of this
paper), but it seems difficult to find that of a general bulging triangle.

  * •

It is unclear if any (not necessarily right-angled) bulging triangle is
inscribed in a circle.

  * •

The application of bulging triangles is our concern. etc.

We would like to make research on them a future subject.

## References

  * [1] Besicovitch, A.S.: The Kakeya Problem, The American Mathematical Monthly, Vol. 70, No. 7 (1963), pp. 697-706.
  * [2] Barrallo, J., González-Quintial, F. and Sánchez-Beitia, S.: An Introduction to the Vesica Piscis, the Reuleaux Triangle and Related Geometric Constructions in Modern Architecture, Nexus Network Journal (2015) 17, pp. 671-684.
  * [3] Dillon, M.I.: Geometry Through History, Springer (2018).
  * [4] Fitzpatrick, R. (Edited): Euclid’s Elements of Geometry (from Euclidis Elementa, edidit et Latine interpretatus est I.L. Heiberg, in aedibus B.G. Teubneri), ISBN 978-0-6151-7984-1 (Revised and corrected - 2008).
  * [5] Kodaira, K.: Invitation to Geometry, Iwanami Shoten (in Japanese, 2019).
  * [6] Ridley, J.N.: A Generalization of Reuleaux Triangle, http://frink.machighway.com/ dynamicm/constant-diameter-curves.pdf, 2 pages.
  * [7] Someyama, N. and Borongan, M.L.A.: New Proofs of Triangle Inequalities, Journal of Ramanujan Society of Mathematics and Mathematical Sciences, Vol. 7, No. 1 (Dedicated to Prof. A.K. Agarwal’s 70th Birth Anniversary, 2019), pp. 85-92.