[Opendnssec-commits] [keihatsu.kirei.se/svn/dnssec] r5278 - home/yuri/enforcer_model2

Yuri Schaeffer yuri at keihatsu.kirei.se
Fri Jul 1 17:37:12 CEST 2011


Author: yuri
Date: 2011-07-01 17:37:12 +0200 (Fri, 01 Jul 2011)
New Revision: 5278

Modified:
   home/yuri/enforcer_model2/enforcer_rules.tex
Log:
Rules update.


Modified: home/yuri/enforcer_model2/enforcer_rules.tex
===================================================================
--- home/yuri/enforcer_model2/enforcer_rules.tex	2011-07-01 12:53:59 UTC (rev 5277)
+++ home/yuri/enforcer_model2/enforcer_rules.tex	2011-07-01 15:37:12 UTC (rev 5278)
@@ -3,21 +3,20 @@
 \usepackage{amssymb,amsmath}
 \usepackage[english]{babel}
 \usepackage{multirow}
-
 \usepackage{algorithmic}
 \usepackage{algorithm}
-
+%~ \usepackage{subequations}
 \usepackage{threeparttable} %footnotes in tables
-
 \usepackage{color}
-\definecolor{MinSig}{RGB}{255,163,53}
-\definecolor{Stdby}{RGB}{224,41,62}
-%~ \definecolor{MinSig}{RGB}{199,154,0}
-\newcommand{\highlightMinSig}[1]{\textcolor{MinSig}{\bf{#1}}}
-\newcommand{\highlightStandby}[1]{\textcolor{Stdby}{\bf{#1}}}
 
-%~ \newcommand{\mathbox}[1]{\fbox{\begin{minipage}{\linewidth}#1\end{minipage}}}
-\newcommand{\mathbox}[1]{#1}
+\definecolor{quotemarkcolor}{rgb}{0.8,0.8,0.8}
+\newenvironment{fancyquotation}{
+   \begin{quotation}
+	\noindent\llap{\raisebox{-2em}[2em][0pt]{\scalebox{5}{\color{quotemarkcolor}``}}}
+}{
+	\hfill\raisebox{-3em}[0em][0pt]{\scalebox{5}{\color{quotemarkcolor}''}}
+   \end{quotation}
+}
 
 \title{\textsc{Dnssec} Key State Transitions}
 \author{Yuri Schaeffer, Yuri at NLnetLabs.nl}
@@ -26,6 +25,22 @@
 \begin{document}
 \maketitle
 
+\section{Three Laws of DNSSEC}
+\begin{description}
+\item[First Law] An Enforcer may not injure a zone by revoking its DS record.
+\item[Second Law] An Enforcer must keep a secure KSK or an insecure KSK if that does not conflict with he first rule.
+\item[Third Law] An Enforcer must protect its ZSK security unless revoking does not conflict with the first or second rule.
+\item[Zeroth Law] An enforcer may not harm a zone, or, by inaction, allow zones to come to harm.
+\end{description}
+
+\begin{fancyquotation}
+Trevize frowned. ``How do you decide what is injurious, or not injurious, to humanity as a whole?''
+
+``Precisely, sir,'' said Daneel. ``In theory, the Zeroth Law was the answer to our problems. In practice, we could never decide. A human being is a concrete object. Injury to a person can be estimated and judged. Humanity is an abstraction.''
+\end{fancyquotation}
+\hfill--Foundation and Earth
+
+
 \section{Warning}
 This document is a rough explanation of an idea. It is based on earlier
 work and may use but not introduce terminology of an other document. 
@@ -33,15 +48,8 @@
 warning (well, you are warned now) and be plain wrong. This document is considered unsuitable
 for young children and Liberal-Arts majors. Read at OWN RISK.
 
-\subsection{Incompleteness / TODO}
-\begin{description}
-\item[Minimize Flags] define how the (in this document yet undefined) 
-minimize flags should exactly modify the rules.
-\item[Notation] Brush up notation of rules.
-\end{description}
+\pagebreak\tableofcontents
 
-\tableofcontents
-
 \section{Introduction}
 
 A key roll-over is a process that runs over time, at any time each 
@@ -260,8 +268,8 @@
 
 \subsection{Notation}
 
-For readability let $A$ denote a DS record, $B$ the DNSKEY, $C$ the 
-RRSIG DNSKEY, and $D$ the RRSIG. The state of a record is indicated 
+For readability let $D$ denote a DS record, $K$ the DNSKEY, $k$ the 
+RRSIG DNSKEY, and $S$ the RRSIG. The state of a record is indicated 
 with superscript and can be found in Table~\ref{tab:states}. These 
 states correspondent directly with the states from Figure~\ref 
 {fig:statemachine}. I.e. $hidden \equiv -$, $rumoured \equiv 
@@ -269,7 +277,7 @@
 The subscript of a record denotes the key it 
 belongs to. The
 current evaluated key has subscript $i$. E.g: the statement ``the DS of key $z$ is in 
-the Omnipresent state'' can be written as $A^{+}_{z}$. 
+the Omnipresent state'' can be written as $D^{+}_{z}$. 
 
 
 \begin{table}[h]
@@ -285,17 +293,14 @@
 \label{tab:states}
 \end{table}
 
-%~ notation
-%~ rules
-%~ algorithm
+%~ %%%% Depricated
+%~ Furthermore, the certain states are a subset of the uncertain states. So 
+%~ a Hidden record is also said to be Unretentive. 
+%~ $A_{x}^{-} \rightarrow A_{x}^{\downarrow}$.
 
-Furthermore, the certain states are a subset of the uncertain states. So 
-a Hidden record is also said to be Unretentive. 
-$A_{x}^{-} \rightarrow A_{x}^{\downarrow}$.
-
 \subsection{Rules}
 
-The system uses four rules, Equation~\eqref{eqn:rule1}\eqref{eqn:rule2}\eqref{eqn:rule3}\eqref{eqn:rule4}.
+The system uses three rules, Equation~\eqref{eqn:rule1}\eqref{eqn:rule2}\eqref{eqn:rule3}.
 To see if we can transition a record to the next state we first 
 test the three rules. They \emph{should} all be True, if not we apparently
 have an invalid zone on our hands. This isn't our fault (presumably\footnote{
@@ -313,22 +318,38 @@
 some extend repair invalid situations in a graceful manner. Also, it 
 allows unsigned zones to exist without special tricks.
 
-The four rules \emph{should} be true for each record of all keys. The 
+The three rules \emph{should} be true for each record of all keys. The 
 rules will be explained in a later section.
 
+\newcommand{\record}[3]{#1_{#2}^{#3}}
+
+\newcommand{\A}[2]{\record{D}{#1}{#2}}
+\newcommand{\B}[2]{\record{K}{#1}{#2}}
+\newcommand{\C}[2]{\record{k}{#1}{#2}}
+\newcommand{\D}[2]{\record{S}{#1}{#2}}
+
 \begin{eqnarray}
 \label{eqn:rule1}
-rule1:	&& A_{x}^{\uparrow} \\
+rule1(i)
+&:& 	\exists x\cdot\A{x}{\uparrow} \vee \A{x}{+}\\
+\nonumber
+\\
 \label{eqn:rule2}
-rule2:	&& \neg A_{x}^{\uparrow} (A_{i}^{-} \vee B_{i}^{+} C_{i}^{+}) \vee A_{x}^{\uparrow}
-	B_{x}^{+} C_{x}^{+} \vee A_{x}^{+} B_{x}^{\uparrow} C_{x}^{\uparrow}
-	A_{y}^{+} B_{y}^{\downarrow} C_{y}^{\downarrow}\\
+rule2(i)
+&:&		\forall x \cdot (\A{x}{-} \vee \exists y \cdot \B{y}{+}\C{y}{+} (\A{x}{}=\A{y}{}) ) \nonumber \\
+&\vee& 	\exists x\cdot\A{x}{+} \B{x}{+} \C{x}{+} \nonumber \\
+&\vee& 	\exists x,y\cdot\A{x}{\uparrow} \B{x}{+} \C{x}{+} \A{y}{\downarrow} \B{y}{+} \C{y}{+} \\
+&\vee&	\exists x,y\cdot \A{x}{+} \B{x}{\uparrow} \C{x}{\uparrow}	\A{y}{+} \B{y}{\downarrow} \nonumber \\
+&;&		alg(i)=alg(x)=alg(y) \nonumber \\
+\nonumber 
+\\
 \label{eqn:rule3}
-rule3:	&& \neg B_{x}^{\uparrow} (B_{i}^{-} \vee D_{i}^{+}) \vee B_{x}^{\uparrow}
-	D_{x}^{+} \vee B_{x}^{+} D_{x}^{\uparrow} B_{y}^{+}
-	D_{y}^{\downarrow} \\
-\label{eqn:rule4}
-rule4: && B_{i} \geq C_{i}
+rule3(i)
+&:&		\forall x \cdot (\B{x}{-} \vee \exists y \cdot \D{y}{+} (\B{x}{}=\B{y}{}) ) \nonumber\\
+&\vee&	\exists x\cdot \B{x}{+} \D{x}{+} \nonumber\\
+&\vee&	\exists x,y\cdot \B{x}{\uparrow} \D{x}{+} \B{y}{\downarrow} \D{y}{+} \\
+&\vee&	\exists x,y\cdot \B{x}{+} \D{x}{\uparrow} \B{y}{+} \D{y}{\downarrow} \nonumber \\
+&;&		alg(i)=alg(x)=alg(y) \nonumber 
 \end{eqnarray}
 
 \subsection{Algorithm}
@@ -385,52 +406,58 @@
 
 \section{Rules explained}
 
-\begin{equation}
-A_{x}^{\uparrow} 
-\end{equation}
+In a nutshell, the first rule makes sure the zone is kept signed at all times, the second keeps the KSK in a valid state and the third the ZSK. The three rules do influence each other. For example rule 3 does allow having no ZSK, but only if there is no KSK. Rule 2 does allow having no KSK but only if there is no DS published. Rule 1 seems simple but it is the only thing that keeps the zone from going unsigned.
 
-The notation is not sufficient here. What I mean to say is there must
-be a DS Rumoured or Omnipresent at all times. Does not matter which key
-or what algorithm.
+Disabling rule 1 will allow both other rules to go to unsigned (in a gracefull manner).
 
-\begin{equation}
-\neg A_{x}^{\uparrow} (A_{i}^{-} \vee B_{i}^{+} C_{i}^{+}) \vee A_{x}^{\uparrow}
-	B_{x}^{+} C_{x}^{+} \vee A_{x}^{+} B_{x}^{\uparrow} C_{x}^{\uparrow}
-	A_{y}^{+} B_{y}^{\downarrow} C_{y}^{\downarrow}
-\end{equation}
+\begin{eqnarray}
+\label{eqn:rule1Expl}
+rule1(i)
+&:& 	\exists x\cdot\A{x}{\uparrow} \vee \A{x}{+}
+\end{eqnarray}
 
-The second rule basically describes the dependency of the DS record
-on the DNSKEY record and the signature thereof. Either there is no DS
-published and the DNSKEY is well known, another DS is published with the
-DNSKEY well known, or two DS's are well known and their DNSKEYS are being 
-swapped.
+At all times there must be a DS published \eqref{eqn:rule1Expl}. The only exception is when the user wants his zone unsigned, this must be explicitly stated. If so, this rule must skipped. Skipping in other situations is possible, but ill advised. The enforcer may do a rollover via an unsigned zone.
 
-Although not stated explicitly, all records in the statement must have
-the same algorithm.
+In words: there must always exist a DS record introducing or omnipresent. It does not matter what algorithm or which key this DS belongs to. This seems incomplete but really forms a fundament for rule number 2.
 
-\begin{equation}
-\neg B_{x}^{\uparrow} (B_{i}^{-} \vee D_{i}^{+}) \vee B_{x}^{\uparrow}
-	D_{x}^{+} \vee B_{x}^{+} D_{x}^{\uparrow} B_{y}^{+}
-	D_{y}^{\downarrow}
-\end{equation}
+\begin{subequations}
+\label{eqn:rule2Expl}
+\begin{align}
+rule2(i)
+&:&		\forall x \cdot (\A{x}{-} \vee \exists y \cdot \B{y}{+}\C{y}{+} (\A{x}{}=\A{y}{}) ) \label{r2eUnsigned}\\
+&\vee& 	\exists x\cdot\A{x}{+} \B{x}{+} \C{x}{+} \label{r2eTrivial}\\
+&\vee& 	\exists x,y\cdot\A{x}{\uparrow} \B{x}{+} \C{x}{+} \A{y}{\downarrow} \B{y}{+} \C{y}{+} \label{r2eMinds}\\
+&\vee&	\exists x,y\cdot \A{x}{+} \B{x}{\uparrow} \C{x}{\uparrow}	\A{y}{+} \B{y}{\downarrow} \label{r2eMinkey}\\
+&;&		alg(i)=alg(x)=alg(y) \label{r2eAlg}
+\end{align}
+\end{subequations}
 
-The third rule expresses the dependency of the DNSKEY on the RRSIG. 
-Either there is no DNSKEY at all, the DNSKEY is being introduced with
-the RRSIG well known, or two DNSKEYs exist and their RRSIGS's are being
-swapped.
+Rule 2 describes the dependency of the DS record on the DNSKEY and its RRSIG. The subequations represent the different scenarios that are valid, at least one of these scenarios must be true at all times. The only keys that need to be considered are the keys with the same algorithm as the input key $i$ \eqref{r2eAlg}.
 
-Again, all record must have the same algorithm.
+Subequation~\eqref{r2eTrivial} is the trivial case: If there is a key with the DS, DNSKEY and RRSIG DNSKEY fully propagated all other keys of this algorithm can be in any state. No further requirements.
 
-\begin{equation}
-B_{i} \geq C_{i}
-\end{equation}
+Similar subequation~\eqref{r2eMinds} requires two keys swapping DS records. Again, if this is the case, the zone is valid for the KSK and other keys can be in any state without consequences.
 
-The state of the RRSIG DNSKEY may not be greater than the state of the
-DNSKEY. In the normal case both records are published together. In case
-of 5011 we need to introduce a new DNSKEY for some time \emph{without}
-signing the DNSKEY RRset. We must however prevent the signature to be 
-introduced or outroduced before the actual DNSKEY.
+Subequation~\eqref{r2eMinkey} also requires two keys, but now they are swapping DNSKEYs. Notice the outroduction of the signature is omitted in this subequation ($\C{y}{\downarrow}$), this is not an error. Including it would block the DNSKEY $\C{y}{}$.
 
+Finally the unsigned case, subequation~\eqref{r2eUnsigned}. It applies to zones unsigned \emph{for this algorithm}, which includes unsigned for \emph{any} algorithm. In the unsigned/partially signed case no DS may be published. If however a DS of key $x$ is published anyway there must be a key $y$ with the DNSKEY set propagated and the DS in the same state as key $x$. Like everywhere else $x$ and $y$ may be the same key.
+
+Let us review an example (ignoring rule 1 and 2). Say we have two keys: $\A{x}{+}\B{x}{+}\C{x}{+}$ and $\A{y}{+}\B{y}{-}\C{y}{-}$. We want the zone to become unsigned. At time 0 the zone is valid because of \eqref{r2eTrivial} and we can therefore outroduce the DS of $y$. Now, because of \eqref{r2eUnsigned} me may do the same with the DS of $x$ at the same time. When both are hidden the last mentioned rule allows the remaining DNSKEY and RRSIG DNSKEY to do whatever they want.
+
+\begin{subequations}
+\label{eqn:rule3Expl}
+\begin{align}
+rule3(i)
+&:&		\forall x \cdot (\B{x}{-} \vee \exists y \cdot \D{y}{+} (\B{x}{}=\B{y}{}) ) \\
+&\vee&	\exists x\cdot \B{x}{+} \D{x}{+} \\
+&\vee&	\exists x,y\cdot \B{x}{\uparrow} \D{x}{+} \B{y}{\downarrow} \D{y}{+} \\
+&\vee&	\exists x,y\cdot \B{x}{+} \D{x}{\uparrow} \B{y}{+} \D{y}{\downarrow} \\
+&;&		alg(i)=alg(x)=alg(y)
+\end{align}
+\end{subequations}
+
+The third rule works exactly the same as rule 2 but reasons about the ZSK part. 
+
 \section{Examples}
 
 Names for rollovers are taken from ``DNSSEC Key Timing 




More information about the Opendnssec-commits mailing list