1: \documentclass[11pt,twocolumn]{article}

2: \usepackage{myusenix}

3: 

4: \usepackage{graphics}

5: \usepackage{url}

6: \usepackage{algorithm}

7: \usepackage[]{myalgorithmic}	% used to fix bug with line

8: 				% number labeling in the original style

9: 				% file

10: \usepackage{latexsym}		%for the qed symbol

11: \usepackage{amsthm}		%to fix the problem with long theorem names

12: \usepackage{amssymb}		%for the \varnothing symbol

13: \newtheorem{theorem}{Theorem}

14: \newtheorem{lemma}{Lemma}

15: \newtheorem{definition}{Definition}

16: 

17: %\newcommand{\qed}[0]{\hfill\ensuremath{\Box}}

18: \newcommand{\algname}[1]{\edef\algcs{\csname#1::name\endcsname}\textsc{\small\algcs}}

19: 

20: \newcommand{\algsig}[2]{\edef\algcs{\csname#1::name\endcsname}\edef\algcmd{\gdef\algcs{#2}}\algcmd\label{#1}\algname{#1}}

21: 

22: %\newcommand{\algref}[1]{\algname{#1}[Algorithm~\ref{#1}]}

23: \newcommand{\algref}[1]{\algname{#1}}

24: 

25: \author{Petros Maniatis \hspace{4mm} Mary Baker\\ {\em Computer

26: Science Department, Stanford University}\\ {\em Stanford, CA 94305,

27: USA}\\

28: %\vspace{.3in}

29: {\tt \{maniatis,mgbaker\}@cs.stanford.edu}\\

30: \url{http://identiscape.stanford.edu/}} % end author

31: 

32: \date{}

33: \pagestyle{myheadings}

34: 

35: \begin{document}

36: 

37: \title{\bf Authenticated Append-only Skip Lists}

38: 

39: \maketitle

40: 

41: \thispagestyle{empty}

42: 

43: \begin{abstract}

44: \small In this work we describe, design and analyze the security of a

45: tamper-evident, append-only data structure for maintaining secure data

46: sequences in a loosely coupled distributed system where individual

47: system components may be mutually distrustful.  The resulting data

48: structure, called an Authenticated Append-Only Skip List (AASL), allows

49: its maintainers to produce one-way digests of the entire data sequence,

50: which they can publish to others as a commitment on the contents and

51: order of the sequence.  The maintainer can produce efficiently succinct

52: proofs that authenticate a particular datum in a particular position of

53: the data sequence against a published digest.  AASLs are secure against

54: tampering even by malicious data structure maintainers.  First, we show

55: that a maintainer cannot ``invent'' and authenticate data elements for

56: the AASL after he has committed to the structure.  Second, he cannot

57: equivocate by being able to prove conflicting facts about a particular

58: position of the data sequence.  This is the case even when the data

59: sequence grows with time and its maintainer publishes successive

60: commitments at times of his own choosing.

61: 

62: AASLs can be invaluable in reasoning about the integrity of system logs

63: maintained by untrusted components of a loosely-coupled distributed

64: system.

65: \end{abstract}

66: 

67: 

68: \section{\label{sec:introduction}Introduction}

69: 

70: Dependable systems rely heavily on logs of data, system events,

71: transactions, and security decisions.  Inspecting such logs while the

72: system is running (on-line) or after an exceptional event has caused the

73: system to cease operations (off-line) can help maintain accountability

74: through audit trails, repair failures through undo/redo logs, and

75: improve performance via profiling.

76: 

77: In distributed systems, especially those intended for loosely-coupled

78: communities of independent components (generally called

79: \emph{peer-to-peer systems}), it is frequently infeasible to maintain a

80: central system log; in fact, often there is no central authority that

81: can be trusted by all participating components to maintain a log

82: faithfully.  Instead, each component stores its own log of events

83: observed locally, or of interactions with other components.  The log for

84: the entire system does not exist physically; it is made up of log

85: fragments scattered around different system components.

86: 

87: These distributed log fragments must be perused for answers when a

88: failure occurs or a component is reported as misbehaving.  For example,

89: consider a distributed file system, where component $A$ requests that

90: component $B$ store datum $d$ and $B$ accepts.  Later $A$ attempts to

91: retrieve datum $d$ from $B$ and $B$ denies having this datum.  $A$ can

92: convincingly accuse $B$ of misbehavior only if it can show that, at

93: first, $B$ agreed to hold $d$ and, \emph{later}, $B$ denied having done

94: so.

95: 

96: In such a setting, logs can be a very sensitive and vulnerable system

97: resource.  A component, along with the entity that operates it, cannot

98: trust another component to retain the order of its locally logged events

99: or to refrain from changing events after it has logged them.  This

100: prevents $A$, in the example above, from using $B$'s log to justify its

101: accusation.  Similarly, an arbiter must be skeptical of an accusation

102: made by $A$ that relies on the integrity of $A$'s log.

103: 

104: The problem has been addressed in the literature via the use of

105: collision-resistant hash functions to link the contents of earlier log

106: entries to later

107: ones~\cite{Haber1991,Maniatis2002b,Schneier1998,Spreitzer1997}.  The

108: collision-resistance property of the hash functions used makes it very

109: difficult to ``rewrite history'' in a sensitive log, without causing

110: dramatic changes in the entire log.  However, with very few exceptions

111: (notably, work by Buldas et al.~\cite{Buldas1998}), no attention has

112: been paid to the scalability of such hash-based techniques when logs

113: grow very long and interesting sensitive log entries may have been

114: created years---and billions of log entries---ago.

115: 

116: In this paper, we analyze the security of the \emph{Authenticated

117: Append-only Skip List} (AASL).  The AASL is a novel data structure that

118: is designed for the efficient maintenance of and access to very large,

119: tamper-evident sequences of data.  AASLs provide a mechanism for

120: detecting structural corruption, such as modification, removal or

121: reordering of data, whenever those data are accessed.  We have used

122: AASLs in Timeweave~\cite{Maniatis2002b}, a mechanism that allows

123: components of a distributed system to maintain a local trustworthy view

124: of a global system log.

125: 

126: A distributed system component that maintains an AASL can compute

127: succinct one-way digests of the entire structure; these digests can

128: serve as a \emph{commitment} on the data structure contents and order,

129: and can be conveyed to other system components as such.  A remote

130: component wishing to establish whether a particular datum appears in

131: such a data sequence (membership) can request a \emph{proof} from the

132: maintainer of the AASL.  This proof can be verified against the digest

133: to which the maintainer has committed.

134: 

135: AASLs are guaranteed to prevent maintainers from proving conflicting

136: facts about a data sequence, even at different points in the evolution

137: of the sequence over time.  In this paper, we describe the construction

138: of AASLs and prove the security guarantees they offer.

139: 

140: 

141: 

142: \section{\label{sec:background}Background}

143: 

144: In this section, we describe related work that protects sensitive logs

145: from tampering, and related work on securing the contents of skip lists.

146: 

147: The integrity of public logs or commitment sequences has traditionally

148: been protected through the use of one-way hash functions.  Spreitzer et

149: al.~\cite{Spreitzer1997} describe how to protect the modification order

150: of a weakly consistent, replicated data system, by placing successive

151: write and read operations in a \emph{hash chain}; this is a linked list,

152: where every element is annotated with a label computed by hashing

153: together the value of the element and the label of the preceding

154: element.  Schneier and Kelsey~\cite{Schneier1998} propose a historic

155: integrity scheme for logs of untrusted or vulnerable machines.  Their

156: work protects access-controlled log entries against tampering or

157: unauthorized retroactive disclosure through hash chaining.  In secure

158: digital time stamping~\cite{Haber1991}, a digital notary places

159: documents in a hash chain, so as to be able to derive temporal

160: precedences between document commitments.

161: 

162: Unfortunately, reasoning about simple hash chains can be very expensive

163: when they grow long.  To check that a particular element occupies the

164: beginning of the chain, all the hashes between that element and the end

165: of the chain must be performed.  Buldas et al.~\cite{Buldas1998} improve

166: greatly on this linear cost; they describe optimally efficient hash

167: graphs that permit the extraction of such temporal precedences with

168: optimal proof sizes, on the order of the logarithm of the size of the

169: graph.

170: 

171: Goodrich et al.~\cite{Goodrich2001} retrofit skip lists for

172: tamper-evidence.  In that work, the authors propose an authenticated

173: skip list that relies on commutative hashing.  Anagnostopoulos et

174: al.~\cite{Anagnostopoulos2001} extend this construct to deal with

175: persistent data collections, where older versions of the skip list are

176: available, and they are each, by themselves, an authenticated skip list.

177: However, these structures are not designed to be append-only.  As a

178: result, they are not well-suited for tamper-evident logs: a malicious

179: maintainer can remove and then reinsert elements from the ``middle'' of

180: the structure across version changes.  A verifier must check vigilantly

181: that a log entry that interests him remains consistently in every new

182: version of the structure produced by the maintainer, which can be very

183: expensive when versions are produced frequently.

184: 

185: We have used the structure described in this paper in previous

186: work~\cite{Maniatis2002b} to preserve the historic integrity of a

187: loosely coupled distributed system.  Here we focus on a detailed design

188: and analysis of the security guarantees that the structure offers.

189: 

190: 

191: 

192: \section{\label{sec:skipLists:design}Design}

193: 

194: An Authenticated Append-only Skip List (AASL) is a data structure

195: conceptually based on skip lists~\cite{Pugh1990}.  Skip lists are sorted

196: linked lists with extra links, designed to allow fast lookup of the

197: stored data elements by taking ``shortcuts.''  The basic idea is to

198: enhance linked lists, which connect each element in the data sequence to

199: its successor, by also linking some elements to successors further down

200: the sequence.  Roughly half of the elements have links to their two-hop

201: successor, roughly a quarter of the elements have links to their

202: four-hop successor, and so on.  As a result, during traversal from

203: element $a$ to element $b$, the traversal path follows repeatedly the

204: longest available link from the current element that does not overshoot

205: the destination $b$, and thereby reaches $b$ in fewer steps than would

206: be possible by just traversing every intervening element between $a$ and

207: $b$.  Skip list traversals achieve logarithmic traversal path lengths in

208: the number of data elements in the structure, as opposed to the linear

209: paths offered by regular linked lists.

210: 

211: 

212: 

213: 

214: \subsection{\label{sec:skipLists:design:construction}AASL construction}

215: 

216: AASLs take advantage of the shortcut idea, described above, albeit in a

217: deterministic fashion as opposed to the randomized nature of the

218: original skip lists.  AASLs of $n$ elements consist of $\log_2 n$

219: coexisting linked lists, each designated by a different \emph{level}

220: number.  The linked list at level 0 is a regular linked list connecting

221: all elements in the data sequence.  The linked list at level 1 is a

222: linked list that only contains every other element from the original

223: data sequence.  The linked list at level $l$ contains every $2^l$-th

224: element of the original data sequence.  Element $i$ belongs to the

225: $l$-level linked list if and only if $i$ is divisible by $2^l$.

226: Figure~\ref{fig:skipLists:AbstractSkipList} illustrates this basic

227: structure.

228: 

229: \begin{figure}

230: \centerline{\includegraphics{AbstractSkipList}}

231: \caption[A deterministic skip list]{An example of a deterministic skip

232: list, containing 10 data elements.  Boxes denote element positions

233: (indices), and circles denote the actual element data.  We represent the

234: skip list as an overlapping set of linked lists, each at a different

235: level.  Pointers are marked with the level of the linked list to which

236: they belong.  The thick gray line outlines a traversal of the skip list,

237: from the 3rd to the 7th element.}

238: \label{fig:skipLists:AbstractSkipList}

239: \end{figure}

240: 

241: AASL elements, in addition to their datum and their index number, carry

242: an \emph{authenticator}.  The authenticator $T^i$ for the $i$-th element

243: is a value derived via a few applications of a one-way hash function

244: $h$, such as SHA-1~\cite{SHA1}, to the datum $d_i$ of the $i$-th element

245: and the authenticators of the immediate predecessors of that element on

246: each of the linked lists in which it appears.

247: 

248: \begin{figure}

249: \centerline{\includegraphics{SkipListDetail}}

250: \caption[A detail of the skip list construction.]{An illustration of the

251: construction of the skip list authenticators for elements 9 and 10.  The

252: construction of the 8-th authenticator is not shown.}

253: \label{fig:skipLists:SkipListDetail}

254: \end{figure}

255: 

256: More specifically, an authenticator is computed in two steps (see

257: Figure~\ref{fig:skipLists:SkipListDetail}).  First, the \emph{partial

258: authenticators} for an element are computed, one for each list in which

259: that element participates.  A partial authenticator is a value computed

260: by hashing together the current index number, the current datum, the

261: current list level, and the authenticator of the preceding element on

262: that list.  The partial authenticator $L_i^l$ for the element in

263: position $i$ on the list at level $l$ is computed by

264: \begin{equation}

265: \label{eqn:skipLists:L}

266: L_i^l = h(i \| l \| d_i \| T^{i-2^l})

267: \end{equation}

268: where $\|$ denotes bit-string concatenation.  Second, the partial

269: authenticators are combined, again using the hash function, to produce

270: the element authenticator.  The authenticator $T^i$ of the $i$-th

271: element is computed by

272: \begin{equation}

273: \label{eqn:skipLists:T}

274: T^i=h(L_i^0 \| L_i^1 \| \ldots \| L_i^{f_i})

275: \end{equation}

276: where $f_i$ is the highest level of linked list in which the $i$-th

277: element appears.  $f_i$ is defined by the relation

278: \begin{equation}

279: \label{eqn:skipLists:f}

280: f_i = \{n : i = 2^n r \wedge \gcd(2,r) = 1\}

281: \end{equation}

282: 

283: A very useful property of skip lists is that they can be traversed from

284: a source element $i$ to a destination element $n$ ($i \geq n$) in a

285: number of steps that is logarithmic in the elements of the structure.

286: At every step, a linked list at the highest level is picked, among those

287: in which the current element participates, so as to travel the farthest

288: distance towards the destination, without overtaking it.

289: Algorithm~\ref{alg:skipLists:singleHopTraversalLevel} specifies how a

290: single hop is chosen for such a traversal.  The thick gray line in

291: Figure~\ref{fig:skipLists:AbstractSkipList} illustrates a traversal of

292: the structure.

293: 

294: \begin{algorithm}

295: \caption[Next-hop traversal level in AASL traversal.]{\small

296: \algsig{alg:skipLists:singleHopTraversalLevel}{SingleHopTraversalLevel}

297: $(i,n) \Rightarrow l$.  Return the highest linked list level $l$ that

298: must be followed in the AASL from element $i$ to element $n$, where $i

299: \geq n$.}

300: \begin{algorithmic}[1]

301: \small

302: 

303: \STATE $l \leftarrow 0$

304: 

305: \WHILE{$2^l$ divides $i$}

306: 

307: \IF{$i + 2^l \leq n$}

308: 

309: \STATE $L \leftarrow l$ \COMMENT{$L$-hop does not overtake $n$.}

310: 

311: \ELSE

312: 

313: \STATE Return $L$ \COMMENT{Last safe hop level.}

314: 

315: \ENDIF

316: 

317: \STATE $l \leftarrow l + 1$

318: \ENDWHILE

319: 

320: \STATE Return $L$ \COMMENT{The highest level possible for $i$.}

321: 

322: \end{algorithmic}

323: \end{algorithm}

324: 

325: 

326: 

327: \subsection{\label{sec:skipLists:design:membership}AASL Membership

328: Proofs}

329: 

330: The primary use of AASLs is to support authenticated answers to

331: membership questions, such as ``what is the 7-th element in the AASL?'',

332: while maintaining the append-only property of the AASL.  To accomplish

333: this functionality, it is important, first, that the party asking the

334: question (the \emph{verifier}) know in which AASL she is asking that

335: question; and, second, that once the verifier receives a response, she

336: holds that response as unequivocal for the AASL in question.

337: 

338: An AASL is uniquely determined by a \emph{digest}.  This is the

339: authenticator of the last appended element into the structure.  The

340: maintainer of an AASL conveys this short value to potential verifiers as

341: \emph{commitment} to the exact contents of the AASL.  A verifier who

342: receives such a digest verifies all subsequent exchanges with the

343: maintainer against this digest.

344: 

345: A response to a membership question on the contents of an AASL consists

346: of a \emph{membership claim} and a \emph{membership proof}.  A

347: membership claim has the form ``Data element $d$ occupies the $i$-th

348: position of the AASL whose $n$-th authenticator is known to the

349: verifier,'' and is denoted by $\langle i, n, d \rangle$.  The

350: corresponding membership proof is denoted by $E^{i, n, d}$.  This proof

351: convinces the verifier that, first, the maintainer had decided what the

352: $i$-th value $d$ would be before issuing the $n$-th authenticator;

353: second, the maintainer cannot authenticate any other value $d' \neq d$

354: as the value of the $i$-th element of the AASL with the known $n$-th

355: authenticator $T$.

356: 

357: The AASL maintainer constructs the membership proof $E^{i, n, d}$ by

358: traversing the AASL from the $i$-th to the $n$-th element, hop by hop,

359: as described by \algref{alg:skipLists:singleHopTraversalLevel}.  For

360: every encountered skip list element $j$, the maintainer constructs a

361: \emph{proof component} $C^j$ that consists of the $j$-th data element

362: and the authenticators of its predecessors on all the linked lists in

363: which it appears: $C^j = \langle d_j; \langle T^{j-2^l} : 0 \leq l \leq

364: f_j \rangle \rangle$.  The sequence of all proof components makes up the

365: membership proof $E^{i,n,d} = \langle C^j: j \in S^{i, n}\rangle$, where

366: $S^{i, n}$ is the sequence of elements traversed from $i$ to $n$.  The

367: appendix contains Algorithm~\ref{alg:skipLists:singleElementComponent},

368: which describes the construction process for a single proof component,

369: and Algorithm~\ref{alg:skipLists:constructWholeMembershipProof}, which

370: outlines the overall proof construction process.

371: 

372: The verifier processes a membership proof against the AASL authenticator

373: that it holds to verify the validity of a membership claim.  The

374: verification process mimics the proof construction process.  The

375: verifier's job, however, is to make sure that the purported proof is

376: well-formed and yields the known authenticator starting with the element

377: datum and position in the maintainer's membership claim.  The

378: verification may succeed with a positive result, which means that the

379: claim is true; it may succeed with a negative result, which means that

380: the claim is false, i.e., it \emph{cannot} be true; and it may fail, in

381: which case nothing is known about the claim, except that the supplied

382: proof is inappropriate for the given claim.

383: 

384: For every element $j$ in the traversal from the $i$-th to the $n$-th

385: element, the verifier checks that the corresponding component $C$ in the

386: proof is formed as component $C^j$ should be formed; he then uses that

387: component to compute what the $j$-th authenticator should be based on

388: that component.  Furthermore, since, during traversal, the authenticator

389: of a traversed element is always used in the computation of the

390: authenticator of the next traversed element, the verifier must check

391: that the authenticators it computes in earlier steps of the verification

392: process are consistent with those used in later verification steps.

393: Finally, the proof must be checked for applicability, that is, it should

394: match the claim it purportedly proves: if a membership proof claims to

395: prove the membership claim $\langle i, n, d \rangle$, then the datum in

396: the first proof component should be $d$.

397: 

398: Algorithm~\ref{alg:skipLists:processProofComponent} details how a single

399: proof component is handled by the verification process.

400: Algorithm~\ref{alg:skipLists:processWholeMembershipProof} details the

401: overall proof verification process, making use of the single-component

402: proof verification from

403: Algorithm~\ref{alg:skipLists:processProofComponent}.

404: 

405: \begin{algorithm}

406: \caption[Process a proof component in an

407: AASL.]{\small\algsig{alg:skipLists:processProofComponent}{ProcessProofComponent}

408: $(j, C) \Rightarrow T$.  Process the proof component $C$ that

409: corresponds to the $j$-th element in an AASL, and return the resulting

410: $j$-th AASL authenticator.}

411: \begin{algorithmic}[1]

412: \small

413: 

414: \STATE $\langle d; \langle T_0, T_1, \ldots, T_F \rangle \rangle

415: \leftarrow C$ \COMMENT{Parse $C$.}

416: 

417: \IF{$F \neq f_j$

418: \label{alg:skipLists:processProofComponent:checkNoComponents}}

419: 

420: \STATE Proof component is invalid

421: 

422: \ENDIF

423: 

424: \STATE $P \leftarrow \varnothing$

425: 

426: \FOR{$l = 0$ to $F$}\label{alg:skipLists:processProofComponent:loopStart}

427: 

428: \STATE $L \leftarrow h(j \| l \| d \| T_l)$ \COMMENT{Calculates

429: $L_j^l$. If the proof is correct, then $T_l$ must be $T^{j - 2^l}$ in

430: the original AASL.}

431: \label{alg:skipLists:processProofComponent:L}

432: 

433: \STATE $P \leftarrow P \| L$

434: \label{alg:skipLists:processProofComponent:concatenate}

435: 

436: \ENDFOR \label{alg:skipLists:processProofComponent:loopEnd}

437: 

438: \STATE $T \leftarrow h(P)$ \COMMENT{Should calculate $T^j$.}

439: \label{alg:skipLists:processProofComponent:T}

440: 

441: \STATE Return $T$

442: 

443: \end{algorithmic}

444: \end{algorithm}

445: 

446: 

447: 

448: 

449: 

450: 

451: \begin{algorithm}

452: \caption[Process a membership proof within an

453: AASL.]{\small\algsig{alg:skipLists:processWholeMembershipProof}{ProcessMembershipProof}

454: $(i, n, d, T, E) \Rightarrow \mathit{TRUE}/\mathit{FALSE}$.  Process the

455: membership proof $E$ of the membership claim $\langle i, n, d \rangle$

456: against authenticator $T$.}

457: \begin{algorithmic}[1]

458: \small

459: 

460: \STATE $\langle C_1, C_2, \ldots, C_S \rangle \leftarrow E$

461: \COMMENT{Parse $E$.}

462: 

463: \STATE $T_\mathit{cur} \leftarrow$

464: \algref{alg:skipLists:processProofComponent} $(i, C_1)$

465: \label{alg:skipLists:processWholeMembershipProof:firstStart}

466: \COMMENT{Should calculate $T^i$.}

467: 

468: \STATE $T_\mathit{prev} \leftarrow T_\mathit{cur}$

469: 

470: \STATE $l \leftarrow$ \algref{alg:skipLists:singleHopTraversalLevel}

471: $(i, n)$

472: 

473: \STATE $j \leftarrow i + 2^l$

474: \label{alg:skipLists:processWholeMembershipProof:firstEnd}

475: \label{alg:skipLists:processWholeMembershipProof:firstIncrement}

476: 

477: \STATE $c \leftarrow 2$ \COMMENT{Component counter.}

478: 

479: \WHILE{$j \leq n$}

480: \label{alg:skipLists:processWholeMembershipProof:loopStart}

481: 

482: \STATE $T_\mathit{cur} \leftarrow$

483: \algref{alg:skipLists:processProofComponent} $(j, C_c)$ \COMMENT{Should

484: return $T^j$.}

485: \label{alg:skipLists:processWholeMembershipProof:T}

486: 

487: \STATE $\langle d'; \langle T_0, T_1, \ldots, T_F \rangle \rangle

488: \leftarrow C_c$

489: \label{alg:skipLists:processWholeMembershipProof:continuityStart}

490: \label{alg:skipLists:processWholeMembershipProof:parseC}

491: 

492: \IF{$T_l \neq T_\mathit{prev}$}

493: \label{alg:skipLists:processWholeMembershipProof:continuity}

494: 

495: \STATE Proof is invalid \COMMENT{The values for the same authenticator

496: computed in the previous step and included in the current component

497: differ.}

498: 

499: \ENDIF \label{alg:skipLists:processWholeMembershipProof:continuityEnd}

500: 

501: \STATE $T_\mathit{prev} \leftarrow T_\mathit{cur}$

502: \label{alg:skipLists:processWholeMembershipProof:previousCurrent}

503: 

504: \STATE $l \leftarrow$ \algref{alg:skipLists:singleHopTraversalLevel}

505: $(j, n)$

506: 

507: \STATE $j \leftarrow j + 2^l$

508: \label{alg:skipLists:processWholeMembershipProof:increment}

509: 

510: \STATE $c \leftarrow c + 1$

511: 

512: \ENDWHILE \label{alg:skipLists:processWholeMembershipProof:loopEnd}

513: 

514: \IF{$S \neq c$}

515: \label{alg:skipLists:processWholeMembershipProof:checkNoComponents}

516: 

517: \STATE Proof is invalid \COMMENT{Wrong number of proof components.}

518: 

519: \ENDIF

520: 

521: \IF{$T_\mathit{cur} \neq T$}

522: \label{alg:skipLists:processWholeMembershipProof:checkAuthenticator}

523: 

524: \STATE Proof is invalid \COMMENT{The $T^n$ just computed from the proof

525: is different from the $T^n$ known.}

526: 

527: \ENDIF

528: 

529: \STATE $\langle d'; \langle \ldots \rangle \rangle \leftarrow C_1$

530: \COMMENT{Parse the datum in the first

531: component.}\label{alg:skipLists:processWholeMembershipProof:responseStart}

532: 

533: \IF{$d = d'$}

534: \label{alg:skipLists:processWholeMembershipProof:compareDatum}

535: 

536: \STATE Return TRUE

537: 

538: \ELSE

539: 

540: \STATE Return FALSE

541: 

542: \ENDIF \label{alg:skipLists:processWholeMembershipProof:responseEnd}

543: 

544: \end{algorithmic}

545: \end{algorithm}

546: 

547: Section~\ref{sec:skipLists:security} proves the security properties of

548: AASLs, as described informally above.  Namely, given an AASL digest

549: known to verifiers who follow

550: \algref{alg:skipLists:processWholeMembershipProof}, the maintainer can

551: only authenticate a single, unique membership claim per element to any

552: of those verifiers, and he can determine that digest only after he has

553: decided which claims he wishes to authenticate.

554: 

555: 

556: 

557: 

558: 

559: 

560: \subsection{\label{sec:skipLists:design:evolution}AASL Evolution}

561: 

562: AASLs are useful in distributing the contents of fixed-forever data

563: sequences, but can be invaluable in distributing the contents of data

564: sequences that grow over time.  In this section we address how AASLs can

565: be used when the data sequences on which they are based evolve over

566: time, especially when the verifier needs to access the sequence as it

567: changes.

568: 

569: As new elements are appended to a data sequence that a maintainer keeps

570: in an AASL, the AASL grows with new authenticators for the new elements.

571: Whenever it is necessary to commit to newer versions of the AASL, the

572: maintainer updates verifiers with the new AASL digest, i.e., the

573: currently last AASL authenticator.  In addition to the security

574: guarantees described in the previous section, verifiers of a dynamic

575: AASL must also be convinced that membership claims they verified in

576: previous versions of the AASL remain true in the new version.  Simply,

577: the AASL maintainer must be unable to ``rewrite history'' to which he has

578: committed in the past when he advances to a new version of the

579: structure.

580: 

581: The preservation of AASL history is supported by an \emph{advancement

582: proof}, which accompanies the new digest in an AASL version update.  An

583: advancement proof is very similar to a membership proof.  Intuitively,

584: an advancement proof authenticates a membership claim about an

585: authenticator, instead of a data value.  We call this an

586: \emph{advancement claim}; it has the form ``$T_\mathit{prev}$ is the

587: $i$-th authenticator of the AASL whose $n$-th authenticator is

588: $T_\mathit{new}$.''

589: 

590: Because advancement proofs are basically membership proofs, their

591: construction is almost identical to membership proof construction, and

592: their components have the same form.  Advancement proof $A^{i, n}$ from

593: the $i$-th to the $n$-th AASL authenticator is the same as membership

594: proof $E^{i, n, d}$ without the first proof component.  The first proof

595: component of a membership proof computes the authenticator of the source

596: element from the element datum and earlier AASL authenticators; this

597: step is unnecessary when the source element authenticator is already

598: known, as is the case with advancement.  In the appendix, we outline the

599: advancement proof construction algorithm

600: (Algorithm~\ref{alg:skipLists:constructWholeAdvancementProof}).

601: Figure~\ref{fig:skipLists:SingleAdvancement} illustrates an example of

602: advancement.

603: 

604: \begin{figure}

605: \centerline{\includegraphics{SingleAdvancement}}

606: \caption[An example of advancement in a dynamic AASL]{An example of

607: advancement in a dynamic AASL. In version 1, the AASL has elements 1

608: through 9.  The corresponding advancement proof from the empty AASL to

609: version 1 is $A^{0,9}=\langle \langle d_8; \langle T^7, T^6, T^4, T^0

610: \rangle \rangle, \langle d_9; \langle T^8 \rangle \rangle \rangle$.

611: Then the maintainer adds element 10 and publishes version 2, with

612: advancement proof $A^{9,10}=\langle \langle d_{10}; \langle T^{9}, T^{8}

613: \rangle \rangle \rangle$.  The gray links delineate the traversal paths

614: that the two advancements take.}

615: \label{fig:skipLists:SingleAdvancement}

616: \end{figure}

617: 

618: A verifier need remember three pieces of information for a given remote

619: dynamic AASL: the latest AASL size $n$, the latest digest $T$, and a

620: vector of earlier authenticators called a \emph{basis}.

621: 

622: The basis vector is used to check consistency among the values of

623: ``reusable'' authenticators included in different advancement proofs for

624: the same AASL.  Reusable authenticators are those AASL authenticators

625: that may appear again in subsequent advancement proofs for the AASL.  In

626: the appendix, we illustrate an example of cheating that a malicious AASL

627: maintainer can perpetrate when he is free to use inconsistent values for

628: such reusable authenticators across advancements.  

629: 

630: The structure of a basis vector resembles the binary representation of

631: the AASL element index to which it corresponds.  Specifically, basis

632: $B^i$ for element $i$ is a vector of $l$ authenticators, where $l =

633: \lfloor \log_2 i \rfloor$ is the number of significant bits in the

634: binary representation of $i$. The vector contains a special ``empty''

635: value in those positions in which the binary representation of $i$

636: contains a 0; the rest of the basis vector's positions are occupied by

637: authenticator values.  These authenticator values correspond to the

638: authenticators of the elements encountered in the traversal of the AASL

639: from element 0 to element $i$.  A traversal from 0 to $i$ proceeds in

640: hops of decreasing length, starting with the largest power of 2 that is

641: less than or equal to the destination.  For example, for destination 9

642: (binary $1001$), the traversal from 0 first hops over $8 = 2^3$ elements

643: to element 8, and then over one last element ($2^0$) to element 9 (see

644: Figure~\ref{fig:skipLists:SingleAdvancement}).  In the associated basis

645: $B^9$, each non-zero ``bit'' position is annotated with the

646: authenticator of the element from which the corresponding traversal hop

647: launches, that is $B^9 = \langle T^0, \varnothing, \varnothing, T^8

648: \rangle$.  The basis $B^0$ for the $0$-th element (the initial value of

649: the AASL) contains no values.  Note that verifiers need not remember

650: bases for a static AASLs, since the concept of advancement is

651: meaningless in those.

652: 

653: Advancement proof verification occurs in two phases.  First, the

654: verifier checks whether the last digest he holds can appear in the AASL

655: of the new digest.  This check is almost identical to the verification

656: of membership proofs, as described in

657: Section~\ref{sec:skipLists:design:membership}, with the exception that

658: what is verified is the membership of an authenticator, not a datum, in

659: the AASL.

660: 

661: The second phase of checking an advancement proof deals with the basis.

662: For every component in the proof, the authenticators included therein

663: are checked against the values of any corresponding authenticators in

664: the basis.  If the component is consistent with remembered authenticator

665: values, the basis is updated with any reusable authenticators seen first

666: in the component.  In the end, the basis is updated to reflect the newly

667: acquired digest and advancement proof.

668: Algorithm~\ref{alg:skipLists:processAdvancementProofComponent} provides

669: the details, and is reminiscent of binary addition of positive integers.

670: 

671: \begin{algorithm}

672: \caption[Process an advancement component for a dynamic

673: AASL.]{\small\algsig{alg:skipLists:processAdvancementProofComponent}{ProcessAdvancementProofComponent}

674: $(j, T, B, C, l) \Rightarrow B'$.  Process an advancement component $C$

675: that takes a hop of level $l$ from the $j$-th digest $T$ with basis $B$.

676: Return the new basis.  }

677: \begin{algorithmic}[1]

678: \small

679: 

680: \STATE $\langle d; \langle T_0, T_1, \ldots, T_F \rangle \rangle

681: \leftarrow C$ \COMMENT{Parse $C$.}

682: 

683: \IF{$F \neq f_j$

684: \label{alg:skipLists:processAdvancementProofComponent:checkNoComponents}}

685: 

686: \STATE Proof component is invalid \COMMENT{The component contains the

687: wrong number of authenticators.}

688: 

689: \ENDIF

690: 

691: \STATE $\langle B_0, \ldots, B_b \rangle \leftarrow B$ \COMMENT{The

692: values in the basis vector.}

693: 

694: \IF{$B_l = \varnothing$}

695: 

696: \STATE $B_l \leftarrow T$

697: \label{alg:skipLists:processAdvancementProofComponent:or}

698: 

699: \STATE Return $\langle B_0, \ldots, B_b \rangle$

700: 

701: \ELSE

702: 

703: \STATE $c \leftarrow l$ \COMMENT{Current basis element.}

704: 

705: \WHILE{$B_c \neq \varnothing$}

706: 

707: \IF{$B_c \neq T_{c + 1}$}

708: \label{alg:skipLists:processAdvancementProofComponent:consistency}

709: 

710: \STATE Advancement is invalid. \COMMENT{The maintainer is now sending a

711: different value ($T_{c + 1}$) for an authenticator whose value he

712: reported as $B_c$ before.}

713: 

714: \ENDIF

715: 

716: \STATE $\mathit{carry} \leftarrow B_c$

717: 

718: \STATE $B_c \leftarrow \varnothing$

719: \label{alg:skipLists:processAdvancementProofComponent:zero}

720: 

721: \STATE $c \leftarrow c + 1$

722: 

723: \ENDWHILE

724: 

725: \STATE $B_c \leftarrow \mathit{carry}$

726: 

727: \STATE Return $\langle B_0, \ldots, B_{\max\{b,c\}} \rangle$

728: \COMMENT{The vector may have grown by one non-empty element.}

729: 

730: \ENDIF

731: 

732: \end{algorithmic}

733: \end{algorithm}

734: 

735: \algref{alg:skipLists:processAdvancementProofComponent} is invoked once

736: for every component in the advancement proof, after that component has

737: been processed as a membership proof component.

738: Algorithm~\ref{alg:skipLists:processWholeAdvancementProof} describes how

739: the whole advancement proof verification proceeds.

740: 

741: \begin{algorithm}

742: \caption[Process an advancement proof within an

743: AASL.]{\small\algsig{alg:skipLists:processWholeAdvancementProof}{ProcessAdvancementProof}

744: $(i, n, T_\mathit{prev}, B_\mathit{prev}, T_\mathit{new}, A) \Rightarrow

745: B_\mathit{new}$.  Process the advancement proof $A$ that establishes

746: $T_\mathit{new}$ as the $n$-th authenticator, starting with the $i$-th

747: authenticator $T_\mathit{prev}$ and basis $B_\mathit{prev}$.  The

748: process returns the new basis $B_\mathit{new}$, if successful.}

749: \begin{algorithmic}[1]

750: \small

751: 

752: \STATE $\langle C_2, \ldots, C_S \rangle \leftarrow A$ \COMMENT{Parse

753: $A$.  The numbering starts with 2, to be consistent with the numbering

754: in \algref{alg:skipLists:processWholeMembershipProof}.}

755: 

756: \STATE $c \leftarrow 2$ \COMMENT{Component counter.}

757: 

758: \STATE $j \leftarrow i$

759: \label{alg:skipLists:processWholeAdvancementProof:firstEnd}

760: 

761: \WHILE{$j < n$}

762: \label{alg:skipLists:processWholeAdvancementProof:loopStart}

763: 

764: \STATE $l \leftarrow$ \algref{alg:skipLists:singleHopTraversalLevel}

765: $(j, n)$ \label{alg:skipLists:processWholeAdvancementProof:l}

766: 

767: \STATE $B_\mathit{new} \leftarrow$

768: \algref{alg:skipLists:processAdvancementProofComponent} $(j,

769: T_\mathit{prev}, B_\mathit{prev}, C_c, l)$ \COMMENT{This returns $B^{j +

770: 2^l}$.}\label{alg:skipLists:processWholeAdvancementProof:B}

771: 

772: \STATE $j \leftarrow j + 2^l$ \COMMENT{Next element in traversal.}

773: \label{alg:skipLists:processWholeAdvancementProof:increment}

774: 

775: \STATE $T_\mathit{cur} \leftarrow$

776: \algref{alg:skipLists:processProofComponent} $(j, C_c)$ \COMMENT{Should

777: be $T^j$.}

778: \label{alg:skipLists:processWholeAdvancementProof:T}

779: 

780: \STATE $\langle d; \langle T_0, T_1, \ldots, T_F \rangle \rangle

781: \leftarrow C_c$ \COMMENT{Parse $C_c$.}

782: \label{alg:skipLists:processWholeAdvancementProof:continuityStart}

783: \label{alg:skipLists:processWholeAdvancementProof:parseC}

784: 

785: \IF[$T_\mathit{prev}$ should be $T^{j - 2^l}$.]{$T_l \neq

786: T_\mathit{prev}$}

787: \label{alg:skipLists:processWholeAdvancementProof:continuity}

788: 

789: \STATE Proof is invalid \COMMENT{The value of $T^{j - 2^l}$ computed in

790: the previous step is not the same as the value for $T^{j - 2^l}$ in the

791: current proof component.}

792: 

793: \ENDIF \label{alg:skipLists:processWholeAdvancementProof:continuityEnd}

794: 

795: \STATE $T_\mathit{prev} \leftarrow T_\mathit{cur}$

796: \label{alg:skipLists:processWholeAdvancementProof:previousCurrent}

797: 

798: \STATE $B_\mathit{prev} \leftarrow B_\mathit{new}$

799: 

800: \STATE $c \leftarrow c + 1$

801: 

802: \ENDWHILE \label{alg:skipLists:processWholeAdvancementProof:loopEnd}

803: 

804: \IF{$S \neq c$}

805: \label{alg:skipLists:processWholeAdvancementProof:checkNoComponents}

806: 

807: \STATE Proof is invalid \COMMENT{Wrong number of proof components.}

808: 

809: \ENDIF

810: 

811: \IF{$T_\mathit{cur} \neq T_\mathit{new}$}

812: \label{alg:skipLists:processWholeAdvancementProof:checkAuthenticator}

813: 

814: \STATE Proof is invalid \COMMENT{The $T^n$ claimed by the advancement is

815: different from the one computed by processing the advancement proof.}

816: 

817: \ENDIF

818: 

819: \STATE Return $B_\mathit{new}$

820: 

821: \end{algorithmic}

822: \end{algorithm}

823: 

824: A powerful use of AASLs is to determine the possible relative orders of

825: insertion of different data in the maintainer's tamper-evident data

826: sequence.  For example, let Molly by an AASL maintainer who claims that

827: she did not learn value $a$ until after she had committed to value $b$.

828: If verifier Van holds valid proofs of the membership claims $\langle i,

829: j, a \rangle$ and $\langle k, n, b \rangle$ in Molly's AASL, where $i <

830: j < k < n$, then he can convince anyone who agrees on Molly's $j$-th and

831: $n$-th AASL authenticators that she is lying; Molly must have known

832: value $a$ before her commitment to the $j$-th authenticator, and

833: therefore before her commitment to $b$.  Such temporal orderings can

834: apply also to the data themselves, when those data contain a ``freshness

835: marker'', as is the case, for example, with signed statements containing

836: a nonce.  We detail how temporal ordering in a distributed log can be

837: preserved in the Timeweave project~\cite{Maniatis2002b}.

838: 

839: In the next section, we prove the security properties of static AASLs,

840: described in Section~\ref{sec:skipLists:design:membership}, and of

841: dynamic AASLs, described in this section.

842: 

843: 

844: 

845: 

846: 

847: 

848: 

849: 

850: \section{\label{sec:skipLists:security}Security Analysis}

851: 

852: In this section, we substantiate the security guarantees that AASLs

853: offer to their users.  Our goal is to secure the ``commitment metaphor''

854: of AASLs for verifiers who follow the membership and advancement proof

855: verification procedures described in the previous section.  Informally,

856: this means that, first, diligent verifiers accept only a single, unique

857: membership claim for every position in the data sequence on which an

858: AASL is built; second, the data structure maintainer must decide which

859: membership claims he can prove before he commits to the AASL by giving a

860: digest to potential verifiers.

861: 

862: There are two distinct ``roles'' that a malicious adversary can take,

863: with regards to an AASL.  On one hand, the adversary may be an

864: eavesdropper, who wishes to prove to a verifier a false membership claim

865: of his choosing, for an AASL that he does not maintain.  On the other

866: hand, the adversary may be the AASL maintainer, who wishes either to

867: defer choosing to which membership claim to commit until after he has

868: apparently committed; or to prove conflicting membership claims to

869: different verifiers (a membership claim $\langle i, n, d \rangle$

870: conflicts with membership claim $\langle i, n', d' \rangle$ if $d \neq

871: d'$).  A malicious AASL maintainer is a more powerful adversary, because

872: he can use arbitrary means to produce a digest before he has to relay it

873: to potential verifiers.  In what follows, we prove that AASLs are

874: resistant to such attacks.

875: 

876: First, we show that an adversary is unable to construct convincing

877: membership proofs (that he has not already seen) from a random AASL

878: digest.  This prevents a malicious eavesdropper from proving false

879: membership claims.  This also prevents a malicious AASL maintainer from

880: committing to bogus digests and only deciding later what to prove to its

881: unsuspecting verifiers.  This property is similar to the pre-image

882: resistance property of one-way functions.

883: 

884: \begin{theorem}[AASL Membership Proof Pre-image Resistance]

885: \label{thm:skipLists:proofPreImageResistance}

886: Consider randomly chosen $T$ from the set of values of the hash function

887: $h$.  A computationally bound adversary cannot construct efficiently an

888: AASL membership proof $E^{i,n,d}$ of any datum $d$ in position $i$ of an

889: $n$-element AASL, for any $i$ and $n$ ($0 < i \leq n$).

890: \end{theorem}

891: 

892: This result follows directly from the pre-image resistance of the hash

893: function $h$.

894: 

895: Suppose the adversary can pick $d$, $i$ and $n$ and construct a

896: membership proof $E^{i,n,d}$ of $d$ in position $i$, where $T$ is the

897: given $n$-th authenticator, so that a verifier in possession of $T$ and

898: following Algorithms~\ref{alg:skipLists:processProofComponent} and

899: \ref{alg:skipLists:processWholeMembershipProof} accepts the proof.

900: 

901: Given $E^{i,n,d}$, $i$, $d$, $n$ and $T$,

902: Algorithm~\ref{alg:skipLists:processWholeMembershipProof} executed by

903: the verifier must fail to match the condition of

904: Line~\ref{alg:skipLists:processWholeMembershipProof:checkAuthenticator}.

905: This means that in the last iteration of

906: Line~\ref{alg:skipLists:processWholeMembershipProof:T}, $T_\mathit{cur}$

907: returned from Algorithm~\ref{alg:skipLists:processProofComponent} must

908: be the random $T$ given to the adversary in the challenge.  However,

909: this means that, in Line~\ref{alg:skipLists:processProofComponent:T} of

910: Algorithm~\ref{alg:skipLists:processProofComponent}, the adversary must

911: be able to find a pre-image of the pre-image resistant hash function $h$

912: for random image $T$.  As a result, the hypothesis is false, and the

913: adversary cannot produce a pre-image proof.\qed

914: 

915: Theorem~\ref{thm:skipLists:proofPreImageResistance} only deals with

916: cheap, unsophisticated malice.  We proceed by addressing more

917: sophisticated attacks that rely on the manipulation of corrupt AASLs by

918: their maintainer or on the manipulation of observed proofs by an

919: eavesdropper.  There are three types of such attacks.  First, the

920: adversary can modify correct proofs to make them prove a false

921: membership claim.  Second, the maintainer can produce an AASL digest

922: against which he can prove conflicting membership claims.  Third, the

923: maintainer can produce AASL digests and advancement proofs so as to

924: prove conflicting membership claims against different versions of the

925: AASL.  We call the first two attacks second pre-image and collision,

926: respectively.  We call the third attack \emph{evolutionary collision},

927: because it relies on subverting AASL evolution across versions.

928: 

929: In the next theorem, we prove that AASLs are resistant to the second

930: type of attack, collision attacks

931: (Theorem~\ref{thm:skipLists:proofCollisionResistance}).  AASLs are also

932: resistant to the first type of attack, second pre-image, but the proof

933: is a direct corollary of collision resistance, so we defer to the

934: Appendix for it

935: (Theorem~\ref{thm:skipLists:proofSecondPreImageResistance}).

936: 

937: \begin{theorem}[AASL Membership Proof Collision Resistance]

938: \label{thm:skipLists:proofCollisionResistance}

939: 

940: A computationally bound adversary cannot construct two membership proofs

941: $E$ and $E'$ verifiable against the same authenticator $T$ that

942: authenticate different data values in the same sequence position.

943: 

944: \end{theorem}

945: 

946: Suppose that an adversary can, in fact, construct an efficient proof

947: collision with proofs $E$ and $E'$ against common authenticator $T$.

948: Let the two membership claims be $t = \langle i, n, d \rangle$ and $t' =

949: \langle i, n', d' \rangle$, respectively ($t \neq t'$).  We trace

950: \algref{alg:skipLists:processWholeMembershipProof} backwards for both

951: proofs $E$ and $E'$ in parallel, and reach a violation of the one-way

952: properties of the hash function $h$.

953: 

954: Since both membership proofs can be verified against the same

955: authenticator $T$ (which corresponds to a purported AASL's $n$-th

956: element in the case of $E$ and a different purported AASL's $n'$-th

957: element in the case of $E'$), in the last iteration of

958: Line~\ref{alg:skipLists:processWholeMembershipProof:T} of

959: Algorithm~\ref{alg:skipLists:processWholeMembershipProof}, the

960: invocation of Algorithm~\ref{alg:skipLists:processProofComponent} must

961: yield the same result $T$.  In this last iteration, local variable $j$,

962: the current element of the purported AASL, is equal to $n$ and $n'$,

963: respectively.

964: 

965: However, this means that the adversary must be able to cause the

966: verifier to invoke \algref{alg:skipLists:processProofComponent} with

967: input $(n, C)$ and $(n', C')$ but receive the same result $T$ for both

968: invocations.  This is equivalent to passing to

969: Equations~\ref{eqn:skipLists:L} and \ref{eqn:skipLists:T} different

970: $i$'s and $T$'s but calculating the same $T^i$.  Intuitively, since the

971: two equations use a one-way hash function, this should be impossible,

972: i.e., \algref{alg:skipLists:processProofComponent} should only return

973: the same result when invoked with identical inputs (we prove this

974: rigorously in the Appendix, in

975: Lemma~\ref{lem:skipLists:differentProofComponentsSameT}).  Therefore, in

976: the last iteration \algref{alg:skipLists:processProofComponent} can only

977: be invoked with $(n, C)$ and $(n', C')$ if $n = n'$.  This restricts our

978: assumed proof collision to support membership claims that only differ in

979: the data values $d$ and $d'$.

980: 

981: Since both proofs authenticate position $i$ in an $n$-length AASL,

982: Line~\ref{alg:skipLists:processWholeMembershipProof:checkNoComponents}

983: of \algref{alg:skipLists:processWholeMembershipProof} imposes that the

984: proof lengths must be equal to the same $S$.  We prove inductively on

985: the number of components in the two proofs that the two proofs must be

986: identical.  Induction follows the iterations of the loop in

987: \algref{alg:skipLists:processWholeMembershipProof},

988: Lines~\ref{alg:skipLists:processWholeMembershipProof:loopStart} --

989: \ref{alg:skipLists:processWholeMembershipProof:loopEnd}, from last

990: iteration to first.

991: 

992: The base case for the last components $C_S$ and $C'_S$, respectively,

993: follows directly from the collision resistance claim of

994: \algref{alg:skipLists:processProofComponent}

995: (Lemma~\ref{lem:skipLists:differentProofComponentsSameT} in the

996: appendix) and from the supposition that both proofs are verifiable

997: against the same authenticator $T$.

998: 

999: To establish the inductive step, consider the $c$-th proof components

1000: $C_c$ and $C'_c$ of the two membership proofs and assume they are equal.

1001: In the associated loop iteration in

1002: \algref{alg:skipLists:processWholeMembershipProof},

1003: Line~\ref{alg:skipLists:processWholeMembershipProof:parseC} extracts the

1004: individual $F$ hash values of the $c$-th proof component; these are

1005: pairwise equal across the two respective proof components, since the

1006: components themselves are equal.  The $l$-th of these hash values must

1007: be equal to the value of the respective $T_\mathit{prev}$, in

1008: Line~\ref{alg:skipLists:processWholeMembershipProof:continuity}.  Since

1009: the $l$-th hash values are equal across proofs, the values of

1010: $T_\mathit{prev}$ are the same in the invocations of

1011: \algref{alg:skipLists:processWholeMembershipProof} for the two

1012: membership proofs.  But, in the previous loop iteration, in

1013: Line~\ref{alg:skipLists:processWholeMembershipProof:previousCurrent},

1014: $T_\mathit{prev}$ had been assigned the value of the respective

1015: $T_\mathit{cur}$, computed using

1016: \algref{alg:skipLists:processProofComponent} in

1017: Line~\ref{alg:skipLists:processWholeMembershipProof:T}.  Because of the

1018: collision resistance of \algref{alg:skipLists:processProofComponent},

1019: this means that the inputs to the two respective invocations of

1020: \algref{alg:skipLists:processProofComponent} must also be identical in

1021: that loop iteration, which means that the $(c-1)$-st element components

1022: $C_{c-1}$ and $C'_{c-1}$, respectively, are also identical.  This proves

1023: the inductive step.

1024: 

1025: The induction applies to all but the first proof components in the two

1026: proofs, which are processed outside the loop of

1027: \algref{alg:skipLists:processWholeMembershipProof}, in

1028: Lines~\ref{alg:skipLists:processWholeMembershipProof:firstStart} --

1029: \ref{alg:skipLists:processWholeMembershipProof:firstEnd}.  The same

1030: argument as the inductive step above can also be applied here: the

1031: $T_\mathit{cur}$ returned by the respective invocations of

1032: \algref{alg:skipLists:processProofComponent} on the respective first

1033: proof components is the same $T_\mathit{prev}$ that ends up matching the

1034: identical $l$-th hash values of the respective, equal second proof

1035: components in

1036: Line~\ref{alg:skipLists:processWholeMembershipProof:continuity} of the

1037: first loop iteration.  Consequently, the respective first proof

1038: components must also be equal.

1039: 

1040: We have shown that two proofs $E$ and $E'$ authenticating the same

1041: element position $i$ against the same authenticator $T$ must be

1042: identical.  But in \algref{alg:skipLists:processWholeMembershipProof},

1043: Line~\ref{alg:skipLists:processWholeMembershipProof:compareDatum}, the

1044: datum in the first component of a proof must match the one whose

1045: membership is verified.  This contradicts the collision hypothesis,

1046: because the condition in

1047: Line~\ref{alg:skipLists:processWholeMembershipProof:compareDatum} only

1048: succeeds if the algorithm is invoked with the data value that occupies

1049: the first proof component of the two proofs.  $d$ and $d'$ cannot be

1050: different.  \qed

1051: 

1052: Finally, we prove that AASLs are resistant to the third type of

1053: malicious manipulation attack, evolutionary collision, in

1054: Theorem~\ref{thm:skipLists:evolutionaryCollisionResistance}.  AASLs have

1055: the property of evolutionary collision-resistance if it is impossible

1056: for a computationally constrained adversary to produce advancements and

1057: membership proofs that authenticate two different data elements $d$ and

1058: $d' \neq d$ for the same position $i$, in \emph{any} version of the same

1059: AASL.

1060: 

1061: The definition is fairly broad in scope: it covers unrelated, mutually

1062: unknown verifiers $\mathcal{A}$ and $\mathcal{B}$, who, through

1063: different sequences of advancements, arrive at the same digest $T$ for

1064: position $n$ of an AASL at different times; a malicious prover must be

1065: unable to convince $\mathcal{A}$ that $d$ is at position $i$ \emph{and}

1066: convince $\mathcal{B}$ that $d' \neq d$ is at position $i$, even in

1067: different versions of the AASL in its separate evolution paths towards

1068: length $n$ and digest $T$.

1069: 

1070: Two advancements $A^{i,j}$ and $A^{k,l}$ are \emph{connected} if the

1071: source element of the latter advancement is the destination element of

1072: the former, that is $j = k$.  In what follows, we refer to a sequence of

1073: connected advancements as an \emph{advancement sequence}, and the

1074: sequence of element positions traversed by that advancement sequence as

1075: an \emph{advancement path}.  In a similar manner, we define the sequence

1076: of element positions traversed by a membership proof as a

1077: \emph{membership proof path}.

1078: 

1079: Our proof strategy for evolutionary collision resistance is to show that

1080: if two diligent verifiers have both accepted the same authenticator for

1081: the same AASL element, they must arrive at the same value for the

1082: authenticators of some other strategic AASL elements.  Namely, we show

1083: that the two verifiers must ``agree'' on the authenticators they compute

1084: during the processing of the membership proofs with which the adversary

1085: seeks to fool them.  From

1086: Theorem~\ref{thm:skipLists:proofCollisionResistance}, if two verifiers

1087: agree on the authenticators computed during membership proof

1088: verification, they cannot be verifying the truth of conflicting

1089: membership claims.

1090: 

1091: To reduce authenticator agreement during the verification of independent

1092: advancement paths to authenticator agreement during the verification of

1093: independent membership proofs, we use two ``authenticator agreement

1094: claims,'' which we describe here informally, but prove rigorously in the

1095: Appendix.

1096: 

1097: First, if a membership proof verification and an advancement proof

1098: verification agree on the value of a particular AASL authenticator, then

1099: they must also agree on the authenticator values of all earlier AASL

1100: elements that the two paths---the advancement and the membership proof

1101: paths---have in common (see

1102: Lemma~\ref{lem:skipLists:authenticatorAgreementProofAdvancement} in the

1103: appendix).

1104: 

1105: Second, if two runs of the advancement verification algorithm, applied

1106: to two different advancement sequences, agree on the value of a

1107: particular AASL authenticator, then they must also agree on the

1108: authenticator values of all earlier AASL elements that the two

1109: advancement paths have in common (see

1110: Lemma~\ref{lem:skipLists:commonAdvancementPoints} in the appendix).

1111: 

1112: Equipped with these two claims, we now tackle evolutionary collision

1113: resistance.

1114: 

1115: \begin{theorem}[Evolutionary collision resistance of AASL membership

1116: proofs.]

1117: \label{thm:skipLists:evolutionaryCollisionResistance}

1118: Consider two independent verifiers, $\mathcal{A}$ and $\mathcal{B}$ and

1119: a computationally constrained adversary who conveys to them

1120: independently two advancement sequences.  It is impossible for the

1121: adversary to produce advancement sequences and membership proofs in such

1122: a way that, first, the two verifiers, processing their respective

1123: advancement sequences, advance to element position $n$ with the same

1124: digest $T$; and, second, the two verifiers, processing separate

1125: membership proofs, authenticate, at any time, two conflicting membership

1126: claims.

1127: \end{theorem}

1128: 

1129: It is already known, from

1130: Theorem~\ref{thm:skipLists:proofCollisionResistance}, that conflicting

1131: membership claims cannot be authenticated against the \emph{same}

1132: authenticator.  Here we address the case where the two aspiring proofs

1133: authenticate different data values for the same AASL position against

1134: the authenticators of different versions of that AASL held by the two

1135: verifiers.

1136: 

1137: Let $i$ be the element position for whose data element the adversary

1138: wishes to fool two verifiers, $\mathcal{A}$ and $\mathcal{B}$, and let

1139: $j$ and $k$ be the element positions against whose authenticators he

1140: wishes to produce the offending proofs for the verifiers; specifically,

1141: the adversary wishes to authenticate the membership claims $\langle i,

1142: j, d \rangle$ to $\mathcal{A}$ and $\langle i, k, d' \rangle$ to

1143: $\mathcal{B}$.  Without loss of generality, we assume $j < k$, so $0 < i

1144: \leq j < k \leq n$.

1145: 

1146: Consider the abstract illustration of this setup in

1147: Figure~\ref{fig:skipLists:CommonElements}.  $\mathcal{A}$'s advancement

1148: path, the dark dashed line, does not necessarily go through element $i$,

1149: but it certainly touches element $j$ (since the adversary's membership

1150: proof is authenticated to $\mathcal{A}$ against the $j$-th

1151: authenticator) and element $n$ (since the two verifiers agree on the

1152: value of the $n$-th authenticator).  Similarly, $\mathcal{B}$'s

1153: advancement path, the lighter dashed line, does not necessarily go

1154: through element $i$, but certainly touches elements $k$ and $n$.

1155: $\mathcal{A}$'s membership proof path (the thick dark line) starts from

1156: $i$ and ends at $j$, and $\mathcal{B}$'s membership proof path (the

1157: lighter dark line) starts from $i$ and ends at $k$.

1158: 

1159: \begin{figure}

1160: \centerline{\includegraphics{CommonElements}}

1161: \caption[Common elements in independent verifiers' view of the same

1162: AASL.]{Illustration of the proof of

1163: Theorem~\ref{thm:skipLists:evolutionaryCollisionResistance}. Verifier

1164: $\mathcal{A}$ advances to the $n$-th digest of the AASL via element $j$.

1165: When $\mathcal{A}$ held the $j$-th digest for the AASL, he had

1166: successfully authenticated a datum for the $i$-th position.  Verifier

1167: $\mathcal{B}$ advances to the $n$-th digest of the AASL via element $k$.

1168: When $\mathcal{B}$ held the $k$-th digest for the AASL, he had

1169: successfully authenticated a datum for the same $i$-th position as

1170: $\mathcal{A}$ did.}

1171: \label{fig:skipLists:CommonElements}

1172: \end{figure}

1173: 

1174: There is an element in $[j, k]$, element $m$, that is common among

1175: $\mathcal{A}$'s advancement path, $\mathcal{B}$'s advancement path, and

1176: $\mathcal{B}$'s membership proof path. This results from the fact that

1177: $\mathcal{B}$'s membership proof and advancement paths both start before

1178: element $j$ and touch element $k$, and $\mathcal{A}$'s advancement path

1179: touches element $j$ and continues past element $k$.  An intuitive reason

1180: for this is that $\mathcal{A}$'s advancement path can skip element $k$

1181: only by ``jumping'' over it on a high-level linked list.  Then,

1182: $\mathcal{B}$'s membership proof and advancement paths must touch the

1183: jumping-off point of $\mathcal{A}$'s path, on their way to ``lower''

1184: $k$.  We prove this claim rigorously in

1185: Lemma~\ref{lem:skipLists:parallelPaths}, in the Appendix.

1186: 

1187: The two advancements agree on the value of $T^n$ after processing the

1188: respective advancement sequences in

1189: \algref{alg:skipLists:processWholeAdvancementProof}, as per the theorem

1190: assumption.  Because of the second authenticator agreement claim

1191: described above, this means that the two advancement algorithms also

1192: agree with each other on the value of $T^m$ after processing the

1193: corresponding part of their respective advancement sequences that brings

1194: them both to element $m$.

1195: 

1196: Because $\mathcal{B}$'s membership proof verification, to succeed, must

1197: agree on the value of $T^k$ with the advancement verification algorithm,

1198: and because of the first authenticator agreement claim above, the

1199: membership proof verification algorithm on $\mathcal{B}$ also agrees on

1200: the value of $T^m$ with $\mathcal{B}$'s advancement verification

1201: algorithm after they both reach element $m$.  Therefore, $\mathcal{B}$'s

1202: membership proof verification algorithm and both advancement

1203: verification algorithms agree on the value of $T^m$ after reaching

1204: element $m$.

1205: 

1206: As above, there is an element in $[i, j]$, element $r$, that is common

1207: among $\mathcal{A}$'s advancement path, and $\mathcal{A}$ and

1208: $\mathcal{B}$'s membership proof paths.  This is because both membership

1209: proof paths start at $i$ and go to or past $j$, and $\mathcal{A}$'s

1210: advancement path starts before $i$ and touches element $j$ (since

1211: $\mathcal{A}$'s membership proof must be verifiable against the digest

1212: for element $j$, as per the theorem assumptions).

1213: 

1214: Because $\mathcal{A}$'s membership and advancement proof verification

1215: algorithms must agree on the value of $T^j$ for the membership proof to

1216: be accepted, and from the first authenticator agreement claim once more,

1217: the membership proof verification algorithm on $\mathcal{A}$ also agrees

1218: on the value of $T^r$ with $\mathcal{A}$'s advancement algorithm after

1219: reaching element $r$.  From the same claim, since $\mathcal{B}$'s

1220: membership and $\mathcal{A}$'s advancement proof verification algorithms

1221: agree on the value of $T^m$ after reaching element $m$, they must also

1222: agree on the value of $T^r$ after they reach element $r$.  As a result,

1223: the two membership proof verification algorithms reach element $r$ with

1224: the same value for $T^r$.

1225: 

1226: However, this contradicts

1227: Theorem~\ref{thm:skipLists:proofCollisionResistance}.  If the adversary

1228: could manage to create two membership proofs starting with different

1229: data values on element $i$ and computing the same authenticator for

1230: element $r$, then he would be able to produce same-version collisions,

1231: as well, which Theorem~\ref{thm:skipLists:proofCollisionResistance}

1232: precludes.  Therefore, the two data elements $d$ and $d'$ cannot be

1233: different.\qed

1234: 

1235: \section{Conclusions}

1236: 

1237: In this work we describe, design and analyze the security of a

1238: tamper-evident, append-only data structure for maintaining secure data

1239: sequences in a loosely coupled distributed system, where individual

1240: system components may be mutually distrustful.  The resulting data

1241: structure, called Authenticated Append-Only Skip List, allows its

1242: maintainers to produce one-way digests of the entire data sequence,

1243: which they can publish to others as a commitment on the contents and

1244: order of the sequence.  The maintainer can produce efficiently succinct

1245: proofs that authenticate a particular datum in a particular position of

1246: the data sequence against a published digest.

1247: 

1248: AASLs are secure against tampering even by malicious structure

1249: maintainers.  First, we have shown that a maintainer cannot ``invent''

1250: and authenticate data elements for the AASL after he has committed to

1251: the structure.  Second, he cannot equivocate by being able to prove

1252: conflicting facts about a particular position of the data sequence.

1253: This is the case, even when the data sequence grows with time and its

1254: maintainer publishes successive commitments at times of his own

1255: choosing.

1256: 

1257: We have implemented and extensively measured the performance and storage

1258: requirements of AASLs (we present a discussion of practical

1259: implementation considerations in the Appendix).  We have used AASLs

1260: extensively in Timeweave~\cite{Maniatis2002b}, a system for preserving

1261: historic integrity in trust-free peer-to-peer systems.

1262: 

1263: 

1264: {\small

1265: \bibliographystyle{acm}

1266: \bibliography{IdentiScape}

1267: }

1268: 

1269: \clearpage

1270: 

1271: \appendix

1272: \section{The Need For Bases}

1273: 

1274: We give here a simple example of how ``forgetting'' the values of

1275: reusable authenticators can allow a malicious maintainer to authenticate

1276: conflicting membership claims across AASL versions.  Consider the

1277: authenticator for element 8, in

1278: Figure~\ref{fig:skipLists:SingleAdvancement2}; it is used in all

1279: membership proofs verifiable against the digest of version 1 ending with

1280: element 9, since the authenticator for element 9 depends on a single

1281: partial authenticator, that for element 8.  However, the authenticator

1282: for element 8 is also used in all membership proofs verifiable against

1283: the digest of version 2 ending with element 10, because the

1284: authenticator for element 10 also depends on the authenticator for

1285: element 8 for one of its partial authenticators.

1286: 

1287: A malicious maintainer can construct two authenticators $T^8$ and

1288: ${T^8}'$ for element 8 to accommodate two different elements $d_8$ and

1289: $d_8'$, respectively, using Equations~\ref{eqn:skipLists:L} and

1290: \ref{eqn:skipLists:T}, as follows:

1291: \begin{eqnarray}

1292: T^8	& =	&	h(h(8 \| 0 \| d_8 \| T^7) \ \| \ 

1293: 			h(8 \| 1 \| d_8 \| T^6) \ \| \nonumber \\

1294: 	&	&	h(8 \| 2 \| d_8 \| T^4) \ \| \ 

1295: 			h(8 \| 3 \| d_8 \| T^0)) \nonumber \\

1296: {T^8}'	& =	&	h(h(8 \| 0 \| d_8' \| T^7) \ \| \ 

1297: 			h(8 \| 1 \| d_8' \| T^6) \ \| \nonumber \\ 

1298: 	&	&	h(8 \| 2 \| d_8' \| T^4) \ \| \ 

1299: 			h(8 \| 1 \| d_8' \| T^0)) \nonumber

1300: \end{eqnarray}

1301: He can then construct a single authenticator $T^9$ for element 9 based

1302: on ${T^8}'$:

1303: \[ T^9 = h(h(9 \| 0 \| d_9 \| {T^8}')) \]

1304: and use it to commit to version 1, which ends at element 9, with this

1305: $T^9$ and the first advancement proof $A^{0,9}$:

1306: \[ A^{0,9} = \langle \langle d_8'; \langle T^7, T^6, T^4, T^0 \rangle \rangle, \langle

1307: d_9; \langle {T^8}' \rangle \rangle \rangle \] The digest $T^9$ for version 1

1308: authenticates $d_8'$ in position 8 with the following membership proof:

1309: \[ E^{8, 9, d_8'} = \langle \langle d_8'; \langle T^7, T^6, T^4, T^0 \rangle \rangle, \langle d_9;

1310: \langle {T^8}' \rangle \rangle \rangle \]

1311: 

1312: Now the malicious maintainer can construct a corrupt authenticator

1313: $T^{10}$ for the 10-th element, by mixing $T^8$ from the AASL that

1314: contains $d_8$ in position 8, and ${T^9}$, from the AASL that contains

1315: $d_8'$ in position 8:

1316: \[ T^{10} = h(h(10 \| 0 \| d_{10} \| T^9) \| h(10 \| 1 \| d_{10} \|

1317: T^8)) \] and publish it as the digest for version 2, with the

1318: corresponding advancement proof

1319: \[ A^{9, 10} = \langle \langle d_{10}; \langle

1320: T^9, T^8 \rangle \rangle \rangle \] In conflict to version 1, version 2

1321: authenticates element $d_8$ in position 8, with the following membership

1322: proof:

1323: \[ E^{8, 10, d_8} = \langle \langle d_8; \langle T^7, T^6, T^4, T^0 \rangle \rangle,

1324: \langle d_{10}; \langle T^9, T^8 \rangle \rangle \rangle \]

1325: 

1326: \begin{figure}

1327: \centerline{\includegraphics{SingleAdvancement}}

1328: \caption[An example of advancement in a dynamic AASL]{A repeat of

1329: Figure~\ref{fig:skipLists:SingleAdvancement}. An example of advancement

1330: in a dynamic AASL. In version 1, the AASL has elements 1 through 9.  The

1331: corresponding advancement is $A^{0,9}=\langle \langle d_8; \langle T^7,

1332: T^6, T^4, T^0 \rangle \rangle, \langle d_9; \langle T^8 \rangle \rangle

1333: \rangle$.  Then the maintainer adds element 10 and publishes version 2,

1334: with advancement $A^{9,10}=\langle \langle d_{10}; \langle T^{9}, T^{8}

1335: \rangle \rangle \rangle$.  The gray links delineate the traversal paths

1336: that the two advancements take.}

1337: \label{fig:skipLists:SingleAdvancement2}

1338: \end{figure}

1339: 

1340: The problem lies in the verifier's forgetting that the value for the

1341: purported authenticator of element 8 was ${T^8}'$ in the first

1342: advancement $A^{0,9}$ to version 1, whereas the same authenticator has

1343: the value $T^8 \neq {T^8}'$ in the second advancement $A^{9,10}$ from

1344: version 1 to version 2.  To avoid this problem, verifiers keep track of

1345: reusable authenticators, such as $T^8$ in the example above.  With every

1346: advancement received, a verifier checks that any reused authenticators

1347: in the advancement agree with those known so far in the basis for the

1348: same AASL; then, the verifier updates that basis with any new reusable

1349: authenticators included in the newly received advancement.

1350: 

1351: 

1352: 

1353: \section{Algorithms}

1354: 

1355: Here we describe the proof construction algorithms in detail.  They do

1356: not participate in any of the security proofs, since the security

1357: guarantees offered by AASLs have to do with what claims diligent

1358: verifiers accept.

1359: 

1360: First, Algorithm~\ref{alg:skipLists:singleElementComponent}, describes

1361: how individual proof components are constructed.  These proof components

1362: participate in both membership and advancement proofs.

1363: 

1364: \begin{algorithm}

1365: \caption[Construction of a proof component for an

1366: AASL.]{\small\algsig{alg:skipLists:singleElementComponent}{SingleProofComponent}

1367: $(j) \Rightarrow C$.  Return a proof component $C$ for the AASL element

1368: in position $j$.}

1369: \begin{algorithmic}[1]

1370: \small

1371: 

1372: \STATE $T_\mathit{vec} \leftarrow \varnothing$ \COMMENT{Authenticators.}

1373: 

1374: \FOR{$l = 0$ to $f_j$}

1375: 

1376: \STATE $T_\mathit{vec} \leftarrow T_\mathit{vec} \| T^{j - 2^l}$

1377: 

1378: \ENDFOR

1379: 

1380: \STATE $C \leftarrow \langle d_j; T_\mathit{vec} \rangle$

1381: 

1382: \STATE Return $C$

1383: 

1384: \end{algorithmic}

1385: \end{algorithm}

1386: 

1387: Then, we proceed by describing how a whole membership proof

1388: (Algorithm~\ref{alg:skipLists:constructWholeMembershipProof}) and a

1389: whole advancement proof

1390: (Algorithm~\ref{alg:skipLists:constructWholeAdvancementProof}) are

1391: constructed.

1392: 

1393: \begin{algorithm}

1394: \caption[Construction of a membership proof within an

1395: AASL.]{\small\algsig{alg:skipLists:constructWholeMembershipProof}{ConstructMembershipProof}

1396: $(i, n) \Rightarrow E$.  Return a membership proof $E$ for the $i$-th

1397: element of an AASL, verifiable against the $n$-th authenticator, where

1398: $n \geq i$.}

1399: \begin{algorithmic}[1]

1400: \small

1401: 

1402: \STATE $E \leftarrow \varnothing$ \COMMENT{The proof.}

1403: 

1404: \STATE $j \leftarrow i$ \COMMENT{Current element.}

1405: 

1406: \REPEAT

1407: 

1408: \STATE $C \leftarrow$ \algref{alg:skipLists:singleElementComponent}

1409: $(j)$

1410: 

1411: \STATE $E \leftarrow E \| C$

1412: 

1413: \STATE $l \leftarrow$ \algref{alg:skipLists:singleHopTraversalLevel}

1414: $(j, n)$

1415: 

1416: \STATE $j \leftarrow j + 2^l$

1417: 

1418: \UNTIL{$j > n$}

1419: 

1420: \STATE Return $E$

1421: 

1422: \end{algorithmic}

1423: \end{algorithm}

1424: 

1425: \begin{algorithm}

1426: \caption[Construction of an advancement proof within an

1427: AASL.]{\small\algsig{alg:skipLists:constructWholeAdvancementProof}{ConstructAdvancementProof}

1428: $(i, n) \Rightarrow A$.  Construct an advancement proof from the $i$-th

1429: authenticator of an AASL to the $n$-th authenticator, where $n > i$.}

1430: \begin{algorithmic}[1]

1431: \small

1432: 

1433: \STATE $A \leftarrow \varnothing$ \COMMENT{The proof.}

1434: 

1435: \STATE $j \leftarrow i$ \COMMENT{Current element.}

1436: 

1437: \WHILE{$j < n$}

1438: 

1439: \STATE $l \leftarrow$ \algref{alg:skipLists:singleHopTraversalLevel}

1440: $(j, n)$

1441: 

1442: \STATE $j \leftarrow j + 2^l$

1443: 

1444: \STATE $C \leftarrow$ \algref{alg:skipLists:singleElementComponent}

1445: $(j)$

1446: 

1447: \STATE $A \leftarrow A \| C$

1448: 

1449: \ENDWHILE

1450: 

1451: \STATE Return $A$

1452: 

1453: \end{algorithmic}

1454: \end{algorithm}

1455: 

1456: 

1457: 

1458: 

1459: \section{Proofs of Additional Claims}

1460: 

1461: In this appendix, we prove the intuitive claims we have used in the

1462: security analysis of the paper.

1463: 

1464: First, we prove a claim necessary for the collision-resistance theorem

1465: (Theorem~\ref{thm:skipLists:proofCollisionResistance}), showing that

1466: \algref{alg:skipLists:processProofComponent} is collision-resistant.

1467: 

1468: \begin{lemma}[Different proof components cannot yield the same

1469: authenticator]

1470: \label{lem:skipLists:differentProofComponentsSameT}

1471: 

1472: Consider two independent invocations of

1473: \algref{alg:skipLists:processProofComponent} with inputs $(j, C)$ and

1474: $(j', C')$ respectively.  If the two invocations yield the same result

1475: $T$, then the inputs must be identical ($j = j'$ and $C = C'$).

1476: 

1477: \end{lemma}

1478: 

1479: In both invocations, Line~\ref{alg:skipLists:processProofComponent:T}

1480: must yield the same result $T$.  Since $h$ is collision resistant, the

1481: input $P$ to the hash function must be the same across invocations.

1482: 

1483: Input $P$ is constructed in the loop of

1484: Lines~\ref{alg:skipLists:processProofComponent:loopStart} -

1485: \ref{alg:skipLists:processProofComponent:loopEnd}, by concatenating a

1486: hash result, produced in

1487: Line~\ref{alg:skipLists:processProofComponent:L}, to the running $P$ in

1488: every iteration.  To ensure that $P$ is the same in both invocations,

1489: the loop must be iterated the same number of times (so as to construct

1490: $P$'s of the same bit length), and all appended $L$-elements in the

1491: respective invocations must be identical.

1492: 

1493: At every iteration of the loop,

1494: Line~\ref{alg:skipLists:processProofComponent:L} computes the current

1495: $L$ by hashing together the index $j$ of the assumed AASL element to

1496: which the current proof component should correspond, the iteration

1497: number $l$ (which is, by default, the same across invocations), the

1498: purported data value of the $j$-th AASL element, and the $l$-th

1499: authenticator value contained in the proof component.  Again, due to the

1500: collision resistance of the hash function $h$, the $L$ values computed

1501: in the two invocations can be identical only if the input index $j$ is

1502: equal across invocations, and, similarly, if all parts of the input

1503: proof component $C$ are respectively identical.  This means that two

1504: invocations of \algref{alg:skipLists:processProofComponent} for inputs

1505: $(j, C)$ and $(j', C')$ can yield the same $T$ if and only if $j = j'$

1506: and $C = C'$. \qed

1507: 

1508: As mentioned in the paper, second pre-image resistance is a corollary of

1509: the collision resistance theorem.

1510: 

1511: 

1512: \begin{theorem}[AASL Membership Proof Second Pre-image Resistance]

1513: \label{thm:skipLists:proofSecondPreImageResistance}

1514: 

1515: Consider a membership proof $E^{i,n,d}$ that verifies against

1516: authenticator $T$ the membership claim $\langle i, n, d \rangle$, where

1517: $0 < i \leq n$, and $d$ is a data value.  A computationally bound

1518: adversary cannot construct efficiently a different membership proof $E'$

1519: verifiable against the same authenticator $T$ that authenticates a

1520: conflicting membership claim.

1521: 

1522: \end{theorem}

1523: 

1524: Suppose that an adversary can, in fact, construct efficiently such a

1525: second proof $E'$ for the membership claim $t' = \langle i, n', d'

1526: \rangle$, where $n \neq n'$ or $d \neq d'$.  This means that he has an

1527: efficient way to construct collisions as well: he creates a legitimate

1528: AASL, picks a random position and constructs a membership proof $E$ for

1529: it, then constructs another membership proof $E'$ for a different data

1530: element in the same position.  The two proofs would be a collision as

1531: defined in Theorem~\ref{thm:skipLists:proofCollisionResistance}.

1532: However, we have already shown that collisions are not possible, so the

1533: proof machinery must also be second pre-image resistant. \qed

1534: 

1535: Before we can prove the authenticator agreement claims, we must first

1536: establish that skip list traversal, as described by

1537: \algref{alg:skipLists:singleHopTraversalLevel}, follows the rules of the

1538: skip list, specifically that both source and destination of an $l$-level

1539: hop are divisible by $2^l$.

1540: 

1541: \begin{lemma}[Correctness of skip list traversal]

1542: \label{lem:skipLists:correctTraversal}

1543: In both advancement paths and membership proof paths, as accepted by the

1544: verification algorithms

1545: \algref{alg:skipLists:processWholeAdvancementProof} and

1546: \algref{alg:skipLists:processWholeMembershipProof}, respectively, every

1547: hop from element $i$ to element $j$ has length $2^l$, such that $2^l$

1548: divides both $i$ and $j$.

1549: \end{lemma}

1550: 

1551: We prove this claim informally, by inspection of the corresponding

1552: algorithms.

1553: 

1554: The path of an advancement is verified by

1555: \algref{alg:skipLists:processWholeAdvancementProof}.  The verified path

1556: starts with the source element $i$, given in the input parameters to the

1557: algorithm, and proceeds by increments of $2^l$ in

1558: Line~\ref{alg:skipLists:processWholeAdvancementProof:increment} inside

1559: the loop.  The exponent $l$ of the path length is determined by

1560: \algref{alg:skipLists:singleHopTraversalLevel}, given the current

1561: element $j$ and the ultimate destination $n$ of the advancement.

1562: 

1563: Similarly, a membership proof path is verified by

1564: \algref{alg:skipLists:processWholeMembershipProof}.  The path starts

1565: with the source element $i$ where the element to be authenticated is

1566: claimed to reside in the input parameters.  Then the path proceeds by

1567: increments of $2^l$ in

1568: Line~\ref{alg:skipLists:processWholeMembershipProof:firstIncrement} for

1569: the first hop and

1570: Line~\ref{alg:skipLists:processWholeMembershipProof:increment} for all

1571: subsequent hops.  Both lines receive their $l$ from the result of

1572: \algref{alg:skipLists:singleHopTraversalLevel}, given the current

1573: element $j$ ($i$ in the case of

1574: Line~\ref{alg:skipLists:processWholeMembershipProof:firstIncrement}) and

1575: the ultimate destination $n$ of the membership proof.

1576: 

1577: For both types of paths, it suffices to show that the $l$ computed by

1578: \algref{alg:skipLists:singleHopTraversalLevel} is such that $2^l$

1579: divides $j$.  Then it must also divide the destination $j + 2^l$.

1580: \algref{alg:skipLists:singleHopTraversalLevel} uses as a fall-through

1581: selection of $l$ the value $0$, which is consistent with the claim,

1582: since $2^0 = 1$ divides all elements.  When the loop in the algorithm is

1583: executed at least once, the variable $L$ returned is always one that has

1584: passed the conditional check of the loop, that is, $2^L$ divides the

1585: source element $j$ (called $i$ in

1586: \algref{alg:skipLists:singleHopTraversalLevel}).

1587: 

1588: We have shown that membership proof paths, and paths of single

1589: advancements satisfy the claim.  For advancement paths of multiple

1590: advancements the claim also holds, since connected advancements share an

1591: element: the earlier one ends where the later one begins.  This means

1592: there are no additional hops in the resulting advancement path to those

1593: included in the individual advancements, which already satisfy the claim

1594: as we showed above. \qed

1595: 

1596: We continue by analyzing the concept of the basis.  We use the two

1597: lemmata below in authenticator agreement.

1598: 

1599: \begin{lemma}[Correspondence of bases to binary representations]

1600: \label{lem:skipLists:binaryBasis}

1601: Given the $l$-th AASL element, if the binary representation $b_k b_{k-1}

1602: \ldots b_{0}$ of $l$ has a $0$ in bit position $i$, then the

1603: corresponding basis vector $B^l$ has an empty value in vector position

1604: $i$, and a non-empty value otherwise.

1605: \end{lemma}

1606: Bases are changed only via

1607: \algref{alg:skipLists:processAdvancementProofComponent}, so we

1608: concentrate on that to prove this lemma.  We prove the lemma by

1609: induction on all AASL elements, and for every element on all hop lengths

1610: leading to that element.

1611: 

1612: By definition, the base case holds, since $B^0$ has only empty values,

1613: just as the binary representation of $0$ has only $0$'s.

1614: 

1615: We assume that the lemma holds for all bases up to that of element

1616: $k-1$: that is, the basis vector for AASL element index $m \leq k - 1$

1617: has an empty value in position $l$ if and only if the binary

1618: representation of $m$ has a 0 in bit position $l$.  We show that this

1619: must also hold for the basis $B^k$ that corresponds to element index

1620: $k$.

1621: 

1622: \algref{alg:skipLists:processAdvancementProofComponent} yields the basis

1623: $B^k$ for element index $k$ whenever its input contains the source

1624: element index $j$ and the hop level $l$ and $j = k - 2^l$.

1625: \algref{alg:skipLists:processWholeAdvancementProof} expects the outcome

1626: of such an invocation to be $B^k = B^{j + 2^l}$ in

1627: Line~\ref{alg:skipLists:processWholeAdvancementProof:B}.

1628: 

1629: There are $f_k + 1$ ways in which

1630: \algref{alg:skipLists:processAdvancementProofComponent} can be invoked

1631: to return $B^k$, one for each different level $l$ at which an

1632: advancement path reaches element $k$.  This is because, as shown in

1633: Lemma~\ref{lem:skipLists:correctTraversal},

1634: Line~\ref{alg:skipLists:processWholeAdvancementProof:l} of

1635: \algref{alg:skipLists:processWholeAdvancementProof} can only return $l$s

1636: such that the source (and consequently the destination) of the level-$l$

1637: hop (computed in

1638: Line~\ref{alg:skipLists:processWholeAdvancementProof:increment}) is

1639: divisible by $2^l$.  Since $f_k$ is the exponent of the largest power of

1640: 2 that divides $k$, as per Equation~\ref{eqn:skipLists:f}, there are

1641: $f_k + 1$ invocations of

1642: Line~\ref{alg:skipLists:processWholeAdvancementProof:B} that make

1643: variable $j$ in

1644: Line~\ref{alg:skipLists:processWholeAdvancementProof:increment} to take

1645: the value $k$.

1646: 

1647: We consider invocations of

1648: \algref{alg:skipLists:processAdvancementProofComponent} for all $l$ such

1649: that $0 \leq l \leq f_k$, where $j = k - 2^l$ and $B = B^j$.  All of the

1650: possible input bases $B = B^j$ correspond to element indices $j$ that

1651: precede $k$, and as a result are covered by the inductive hypothesis,

1652: above.

1653: 

1654: In the ``then'' branch of the conditional

1655: (Line~\ref{alg:skipLists:processAdvancementProofComponent:or}), the

1656: previous AASL element index $j$ had a 0 in the $l$-th bit position of

1657: its binary representation.  By turning that 0 to a 1 via assigning a

1658: non-empty value to the $l$-th basis vector element, we add $2^l$ to the

1659: binary representation of $j = k - 2^l$, and we therefore reach the

1660: binary representation for $k$.

1661: 

1662: If, instead, the ``else'' branch of the conditional is executed, the

1663: previous basis vector must have had a non-empty value in its $l$-th

1664: position, and, as a result, the binary representation of $j$ must have

1665: had a 1 in the $l$-th bit position of its binary representation.  The

1666: algorithm places empty values in all vector positions from the $l$-th

1667: one upwards that contain non-empty values and sets to a non-empty value

1668: (the value of the $\mathit{carry}$ variable) the first vector position

1669: $m > l$ that it finds containing an empty value.  This translates into

1670: zeroing out all 1 bits in the binary representation of $j$ from the

1671: $l$-th to the $m-1$-st bit positions, and placing a 1 in the formerly 0

1672: $m$-th bit.  Zeroing out a 1 bit in position $p$ means subtraction by

1673: $2^p$, so the result of the operation is to add $(2^m - \sum_{p = l}^{m

1674: - 1}{2^p} = 2^l)$ to the binary representation of $j = k - 2^l$, which

1675: again yields the binary representation of $k$.

1676: 

1677: This proves the inductive step, and as a result the lemma holds for all

1678: bases computed by

1679: \algref{alg:skipLists:processAdvancementProofComponent}.\qed

1680: 

1681: 

1682: 

1683: 

1684: 

1685: \begin{lemma}[Survival of authenticators in a basis]

1686: \label{lem:skipLists:authenticatorSurvival}

1687: Consider a portion of an advancement path that goes through elements $e$

1688: and $e' = e + 2^l$, for non-negative integers $e$ and $l$.  If $T^{e}$

1689: is the authenticator for element $e$ computed by the advancement

1690: processing algorithm after reaching that element, then the value for

1691: $T^{e}$ is preserved by the algorithm in the basis, and still regarded

1692: as that of $T^{e}$ during processing of element $e'$.

1693: \end{lemma}

1694: 

1695: Informally, this lemma claims that while processing intermediate hops

1696: between two elements that are successive multiples of $2^l$, the

1697: advancement verification algorithm remembers the authenticator of the

1698: first multiple, and uses its value to check the correctness of the

1699: processed advancement component when it reaches the second multiple.

1700: 

1701: Since both $e$ and $e'$ are divisible by $2^l$, then in the binary

1702: representation of $e$, bits $0$ through at least $l - 1$ are all 0.

1703: Because of Lemma~\ref{lem:skipLists:binaryBasis}, all

1704: basis elements in positions $0$ through at least $l - 1$ must be the

1705: empty value.

1706: 

1707: \begin{subparagraph}{Case 1: $e$ and $e'$ are consecutive elements in

1708: the advancement path.}

1709: 

1710: The advancement path takes a single hop at level $l$ from $e$ to $e'$.

1711: To process this advancement hop, the verifier executes an iteration of

1712: the loop in \algref{alg:skipLists:processWholeAdvancementProof} where

1713: the local variable $j$ is equal to $e$ and the level returned in

1714: Line~\ref{alg:skipLists:processWholeAdvancementProof:l} is $l$.

1715: 

1716: The value for $T^e$ was either passed as input $T_\mathit{prev}$ to the

1717: algorithm, if this hop is the first in its advancement, or computed and

1718: stored in $T_\mathit{cur}$ in the previous iteration of the loop in

1719: Line~\ref{alg:skipLists:processWholeAdvancementProof:T}, and then copied

1720: to $T_\mathit{prev}$ in

1721: Line~\ref{alg:skipLists:processWholeAdvancementProof:previousCurrent}.

1722: 

1723: Trivially, therefore, the value of $T_\mathit{prev}$, which the

1724: algorithm regards as $T^e$ during the loop iteration that starts with $j

1725: = e$, is passed as input to

1726: \algref{alg:skipLists:processAdvancementProofComponent} in

1727: Line~\ref{alg:skipLists:processWholeAdvancementProof:B} and checked for

1728: consistency in

1729: Line~\ref{alg:skipLists:processWholeAdvancementProof:continuity}.  This

1730: proves the claim for this case.

1731: 

1732: \end{subparagraph}

1733: 

1734: 

1735: \begin{subparagraph}{Case 2: $e$ and $e'$ are not consecutive elements

1736: in the advancement path.}

1737: 

1738: Leaving element $e$, the advancement path takes a hop at level $p$,

1739: where $p < l$.  Therefore, during the invocation of

1740: \algref{alg:skipLists:processAdvancementProofComponent} that takes as

1741: input the basis of element $e$,

1742: Line~\ref{alg:skipLists:processAdvancementProofComponent:or} is

1743: executed.  What the algorithm regards at the time as $T^{e}$ (passed to

1744: it in its input parameters) is placed in the $p$-th position of the

1745: basis.  Since all vector positions up to position $l-1$ contained the

1746: empty value before this modification, $T^{e}$ is the last (indeed, the

1747: only) non-empty value in the newly created basis vector in positions 0

1748: through $l-1$.

1749: 

1750: In what remains of the advancement path to $e'$, the value for $T^{e}$

1751: is always the last non-empty element in vector positions 0 through

1752: $l-1$.  This is the case right after advancement element $e$ has been

1753: processed, as shown above.  We use this fact as the base case of an

1754: inductive argument.

1755: 

1756: Assume that $T^e$ is the last non-empty value in the first $l$ elements

1757: of the basis vector, and it occupies position $q < l$.  From

1758: Lemma~\ref{lem:skipLists:binaryBasis}, the current element index is only

1759: divisible, at most, by powers of 2 up to $2^{q}$.  This means that the

1760: next advancement hop, as determined by

1761: \algref{alg:skipLists:singleHopTraversalLevel} in

1762: Line~\ref{alg:skipLists:processWholeAdvancementProof:l} of

1763: \algref{alg:skipLists:processWholeAdvancementProof} can only proceed by

1764: a hop of length that is a power of 2 up to $2^{q}$.  This only changes

1765: the $q+1$ least significant bits of the element's binary representation.

1766: Therefore, even if the ``else'' branch of the conditional in

1767: \algref{alg:skipLists:processAdvancementProofComponent} is executed, the

1768: value of $T^{e}$ is the last non-empty value before the $l$-th element

1769: of the basis, and as a result is pushed to a higher element position of

1770: the basis.

1771: 

1772: The only advancement hop that can eliminate $T^{e}$ from the first $l$

1773: elements of the basis is the last one, leading to $e'$.  Then value

1774: $T^e$ occupies position $(l-1)$ of the basis: we showed above there

1775: cannot be any non-empty values between itself and position $l$, and the

1776: value must be eliminated from the first $l$ positions of the basis,

1777: since $e'$ is divisible by $2^l$ and has no 1's in its binary

1778: representation up to and including bit position $l-1$.

1779: 

1780: This means that when element $e'$ is reached by the advancement proof

1781: verification algorithm, the value for $T^e$ is in the basis, in position

1782: $l-1$.  This is the basis vector position in which the algorithm expects

1783: to find the value for $T^e$ during consistency checking in

1784: Line~\ref{alg:skipLists:processAdvancementProofComponent:consistency} of

1785: \algref{alg:skipLists:processAdvancementProofComponent}.  Indeed, the

1786: last advancement proof component that is processed is the one

1787: corresponding to element index $e'$, which has in the $l$-th position

1788: among its included authenticators what the prover sent as $T^{e' - 2^l}

1789: = T^{e}$.  Note that when

1790: Line~\ref{alg:skipLists:processAdvancementProofComponent:consistency} is

1791: executed and eliminates value $T^e$ from basis vector position $l-1$,

1792: the local loop variable $c$ is equal to $l-1$.

1793: \end{subparagraph}

1794: 

1795: Consequently, we have shown that the claim holds for both possible cases

1796: of advancement paths between $e$ and $e'$, which proves the lemma.  \qed

1797: 

1798: The proofs for evolutionary collision resistance and for the

1799: authenticator agreement lemmata rely heavily on common elements in

1800: membership or advancement proof paths.  We proceed with two lemmata that

1801: examine the arrangement of common elements of parallel paths.  First, we

1802: look at common elements of parallel paths, regardless of the path type

1803: (advancement or membership proof).  Then, we show that between two

1804: common elements in a membership proof and advancement path, the

1805: advancement path always takes shorter hops than the membership proof

1806: path.

1807: 

1808: \begin{lemma}[Common elements of parallel paths]

1809: \label{lem:skipLists:parallelPaths}

1810: Let $i$ and $j$ be positive integers, such that $i < j$.

1811: \begin{enumerate}

1812: \item Consider a path $A$ that includes element $i$ and continues to $j$

1813: or past it. There is at least one element in $[i, j]$ that is shared by

1814: $A$ and every path that starts at or before $i$ and includes element

1815: $j$.  The last element on path $A$ before $j$ (or $j$ if it is in path

1816: $A$) is such an element.

1817: \item (The mirror case) Consider a path $A$ that starts at or before

1818: element $i$ and includes element $j$. There is at least one element in

1819: $[i, j]$ that is shared by $A$ and every path that includes element $i$

1820: and continues to element $j$ or past it.  The first element on $A$ after

1821: $i$ (or $i$ if it is in path $A$) is such an element.

1822: \end{enumerate}

1823: \end{lemma}

1824: 

1825: We prove only the first part of the lemma.  The proof for the second

1826: part of the lemma is a trivial ``mirror image'' of the proof for the

1827: first part.

1828: 

1829: If path $A$ contains element $j$, then we are trivially done.

1830: 

1831: Now, assume that path $A$ does not contain element $j$, and consider

1832: Figure~\ref{fig:skipLists:ParallelPaths}.  Path $A$ must be able to

1833: overshoot element $j$ on its way from $i$ to beyond $j$.  For this to

1834: happen, path $A$ must advance from its last element $m$ before $j$

1835: (i.e., $i \leq m < j$) past $j$, by a hop of level $l$ and length $2^l$,

1836: where $2^l$ divides $m$, and $j$ must not participate in any linked list

1837: at level $l$ or higher (i.e., $2^l$ does not divide $j$).  The end point

1838: of this hop is $m + 2^l > j$.

1839: 

1840: \begin{figure}

1841: \centerline{\includegraphics{ParallelPaths}}

1842: \caption[Two parallel, interleaved paths.]{Two parallel, interleaved

1843: paths $A$ and $B$.  $A$ contains $i$, but not necessarily $j$.  $B$

1844: contains $j$ but not necessarily $i$.  The thick gray lines represent

1845: single hops, as picked by

1846: \algref{alg:skipLists:singleHopTraversalLevel}.}

1847: \label{fig:skipLists:ParallelPaths}

1848: \end{figure}

1849: 

1850: Suppose $m$ is not the single common element among path $A$ and every

1851: path that starts at or before $i$ and includes element $j$.  Then there

1852: must be a path $B'$ that manages to overshoot element $m$ on its way to

1853: $j$.  For this to happen, path $B'$ must advance to its first element

1854: $n$ after $m$ (i.e., $m < n \leq j$) past $m$, by a hop of level $l'$

1855: and length $2^{l'}$, and element $m$ must not participate in any linked

1856: list at level $l'$ or higher (i.e., $2^{l'}$ does not divide $m$).  This

1857: means that $l' > l$, since $m$ is divisible by $2^l$.  If $n$

1858: participates in the linked list at level $l'$, it must be divisible by

1859: $2^{l'}$ and, as a result, also by $2^l$.  However, that is impossible,

1860: since $m < n \leq j < m + 2^l$.

1861: 

1862: Therefore, every path $B$ that starts at or before $i$ and includes $j$

1863: must include element $m$, which also belongs to path $A$.\qed

1864: 

1865: 

1866: \begin{lemma}[Common elements of proof and advancement paths]

1867: \label{lem:skipLists:commonProofAdvancementPoints}

1868: If a membership proof path has two common elements $e$ and $e'$ with an

1869: advancement path, then every element in the proof path between $e$ and

1870: $e'$ is also shared by that advancement path.

1871: \end{lemma}

1872: 

1873: Consider a membership proof path and an advancement path that share

1874: elements $e$ and $e > e'$, but share no other elements between them.

1875: 

1876: To prove the lemma, we suppose that none of the proof elements between

1877: $e$ and $e'$ belong to the advancement path (see

1878: Figure~\ref{fig:skipLists:ProofAndAdvancement}).  We show below that

1879: this hypothesis leads to a contradiction.

1880: 

1881: \begin{figure}

1882: \centerline{\includegraphics{ProofAndAdvancement}}

1883: \caption[Proof and advancement paths.]{Proof and advancement paths

1884: between their common elements $e$ and $e'$.  The thick gray line

1885: indicates a single hop, as calculated by

1886: \algref{alg:skipLists:singleHopTraversalLevel}.}

1887: \label{fig:skipLists:ProofAndAdvancement}

1888: \end{figure}

1889: 

1890: After common element $e$, the two paths diverge.  The membership proof

1891: takes a hop at level $l$, whereas the advancement takes a hop at a lower

1892: level $l' < l$.  The advancement cannot take a hop at a level higher

1893: than that of the proof; if such a hop were available that did not

1894: overshoot $e'$, then the proof would have also taken it (see

1895: \algref{alg:skipLists:singleHopTraversalLevel}).  Furthermore, the

1896: advancement cannot take a hop at the same level $l$ as the proof,

1897: because that would make the two paths identical between $e$ and $e'$,

1898: which contradicts the hypothesis that intermediate membership proof

1899: elements do not belong to the advancement path.  We call the next

1900: element on the advancement path $p = e + 2^{l'}$, and the next element

1901: on the membership proof path $q = e + 2^l$.

1902: 

1903: Because of Lemma~\ref{lem:skipLists:parallelPaths}, there must be a

1904: common element between the two paths in $[p, q]$.  However, this

1905: contradicts the hypothesis that the two paths share no elements between

1906: $e$ and $e'$.  As a result, all membership proof elements between $e$

1907: and $e'$ must also belong to the advancement path. \qed

1908: 

1909: 

1910: Finally, we prove the two authenticator agreement lemmata.

1911: 

1912: \begin{lemma}[Authenticator agreement between a membership proof and an advancement

1913: proof verification]

1914: \label{lem:skipLists:authenticatorAgreementProofAdvancement}

1915: If the membership proof verification

1916: Algorithm~\ref{alg:skipLists:processWholeMembershipProof} and the

1917: advancement verification Algorithm

1918: \ref{alg:skipLists:processWholeAdvancementProof}, given an advancement

1919: sequence and a membership proof, respectively, agree on the value of

1920: authenticator $T^n$ for element $n$ during their independent executions,

1921: then they also agree on the authenticator value $T^e$ of every other

1922: earlier element $e$ ($e < n$) that the advancement path and membership

1923: proof path have in common.

1924: \end{lemma}

1925: 

1926: Let $k$ be the number of common elements in the two paths up to element

1927: $n$, and $n = e_1 > e_2 > \ldots > e_k$ the common elements, from last

1928: to first.  We prove the lemma using induction on the common elements

1929: $e_i$, by following backwards

1930: Algorithms~\ref{alg:skipLists:processWholeMembershipProof} and

1931: \ref{alg:skipLists:processWholeAdvancementProof}.

1932: 

1933: The base case for $e_1$ holds from the lemma assumption, since $e_1 =

1934: n$.

1935: 

1936: For the inductive step, we assume that the two algorithms agree on the

1937: value of $T^{e_i}$.  We must show that the two algorithms also agree on

1938: the value of $T^{e_{i+1}}$ when they process the corresponding proof

1939: component to reach element $e_{i+1}$.

1940: 

1941: When the two algorithms process their respective proof component to

1942: compute the common $T^{e_i}$ they use Equations~\ref{eqn:skipLists:L}

1943: and \ref{eqn:skipLists:T}.  Specifically, they both compute

1944: \begin{eqnarray}

1945: T^{e_i} & = & h(\ldots \| L^{l}_{e_i} \| \ldots) \nonumber\\

1946:         & = & h(\ldots \| \overbrace{h(e_i \| l \| d_i \| T^{e_i -

1947:               2^l})}^{L^{l}_{e_i}} \| \ldots) \nonumber

1948: \end{eqnarray}

1949: by invoking \algref{alg:skipLists:processProofComponent} in

1950: Line~\ref{alg:skipLists:processWholeMembershipProof:T} of

1951: \algref{alg:skipLists:processWholeMembershipProof} and

1952: Line~\ref{alg:skipLists:processWholeAdvancementProof:T} of

1953: \algref{alg:skipLists:processWholeAdvancementProof}. Since $h$ is

1954: collision resistant, when the two algorithms process element $e_i$ they

1955: must agree on the values of all $T^{e_i - 2^l}$, for every level $l$ of

1956: linked lists in which element $e_i$ participates.

1957: 

1958: Consider what happens in the two paths between elements $e_{i+1}$ and

1959: $e_i$.  Common element $e_{i+1}$ must be the membership proof element

1960: immediately preceding $e_i$, because of

1961: Lemma~\ref{lem:skipLists:commonProofAdvancementPoints}.  Therefore,

1962: because of Lemma~\ref{lem:skipLists:correctTraversal}, $e_{i} = e_{i+1}

1963: + 2^{l'}$ for some non-negative $l'$.  The advancement hop that arrives

1964: at $e_i$ must be at the same level $l'$ or lower level.  This is because

1965: a higher-level $l'' > l'$ hop would have taken the advancement path from

1966: $e_{i+1}$ to element $e_{i+1} + 2^{l''}$, which must lie beyond $e_i =

1967: e_{i+1} + 2^{l'}$.  Therefore, the advancement path between $e_{i+1}$

1968: and $e_i$ follows either a single hop of level $l'$ and length $2^{l'}$,

1969: which is identical to that followed by the membership proof path, or a

1970: sequence of shorter hops at levels lower then $l'$.

1971: 

1972: \begin{subparagraph}{Case 1: The advancement path is identical to the

1973: membership proof path.} The value for $T^{e_{i+1}}$ used to compute

1974: $T^{e_i}$ in the two algorithms while processing element $e_i$ is the

1975: same as that known by the algorithms while processing the previous

1976: element $e_{i+1}$, from

1977: Line~\ref{alg:skipLists:processWholeMembershipProof:continuity} of

1978: \algref{alg:skipLists:processWholeMembershipProof} and

1979: Line~\ref{alg:skipLists:processWholeAdvancementProof:continuity} of

1980: \algref{alg:skipLists:processWholeAdvancementProof}, which proves the

1981: inductive step.

1982: 

1983: \end{subparagraph}

1984: 

1985: \begin{subparagraph}{Case 2: The advancement path is not identical to

1986: the membership proof path.} We must establish that the value of

1987: $T^{e_{i+1}}$ that \algref{alg:skipLists:processWholeAdvancementProof}

1988: computes while processing element $e_{i+1}$ is the same as that known

1989: while processing the next common element $e_i$.  This follows from

1990: Lemma~\ref{lem:skipLists:authenticatorSurvival}, since elements

1991: $e_{i+1}$ and $e_i$ are successive multiples of $2^{l'}$.

1992: 

1993: As a result, the value for $T^{e_{i+1}}$ produced by the advancement

1994: verification algorithm while processing element $e_{i+1}$ is the same as

1995: the value for $T^{e_{i+1}}$ used by the membership proof verification

1996: algorithm while processing element $e_i$.  This is the same value as

1997: that for $T^{e_{i+1}}$ produced by the proof verification algorithm

1998: while processing element $e_{i+1}$, as seen in

1999: Line~\ref{alg:skipLists:processWholeMembershipProof:continuity} of

2000: \algref{alg:skipLists:processWholeMembershipProof}.  This proves the

2001: inductive step.

2002: \end{subparagraph}

2003: 

2004: The inductive step holds for both possible cases of advancement paths,

2005: and as a result, the inductive argument holds, proving the lemma.  \qed

2006: 

2007: 

2008: 

2009: 

2010: \begin{lemma}[Authenticator agreement between two independent

2011: advancement paths]

2012: \label{lem:skipLists:commonAdvancementPoints}

2013: If two invocations of the advancement verification

2014: Algorithm~\ref{alg:skipLists:processWholeAdvancementProof}, given two

2015: advancement sequences, respectively, agree on the value of authenticator

2016: $T^n$ computed after reaching element $n$ during their independent

2017: executions, then they also agree on the authenticator value $T^e$

2018: computed after reaching every other earlier element $e$ ($e < n$) that

2019: the advancement paths have in common.

2020: \end{lemma}

2021: 

2022: This proof is similar in structure to that of the preceding lemma.

2023: 

2024: Let $k$ be the number of common elements in the two paths up to element

2025: $n$, and $n = e_1 > e_2 > \ldots > e_k$ the actual elements, from last

2026: to first.  We prove the lemma using induction on the common elements

2027: $e_i$, by following backwards two invocations of

2028: Algorithm~\ref{alg:skipLists:processWholeAdvancementProof}.

2029: 

2030: The base case for $e_1$ holds from the lemma assumption, since $e_1 =

2031: n$.

2032: 

2033: For the inductive step, we assume that the two algorithms agree on the

2034: value of $T^{e_i}$, after reaching element $e_i$.  We must show that the

2035: two algorithms also agree on the value of $T^{e_{i+1}}$ after they reach

2036: element $e_{i+1}$.

2037: 

2038: When the two algorithms process their respective proof component to

2039: compute the common $T^{e_i}$ they use Equations~\ref{eqn:skipLists:L}

2040: and \ref{eqn:skipLists:T}.  Specifically, they both compute

2041: \begin{eqnarray}

2042: T^{e_i} & = & h(\ldots \| L^{l}_{e_i} \| \ldots) \nonumber\\

2043:         & = & h(\ldots \| \overbrace{h(e_i \| l \| d_i \| T^{e_i -

2044:               2^l})}^{L^{l}_{e_i}} \| \ldots) \nonumber

2045: \end{eqnarray}

2046: by invoking \algref{alg:skipLists:processProofComponent} in

2047: Line~\ref{alg:skipLists:processWholeAdvancementProof:T} of

2048: \algref{alg:skipLists:processWholeAdvancementProof}.  Since $h$ is

2049: collision resistant, when the two algorithm runs process element $e_i$

2050: they must agree on the values of all $T^{e_i - 2^l}$, for every level

2051: $l$ of linked lists in which element $e_i$ participates.

2052: 

2053: Consider what happens in the two paths between elements $e_{i+1}$ and

2054: $e_i$.

2055: 

2056: \begin{subparagraph}{Case 1: Element $e_{i+1}$ immediately precedes

2057: element $e_i$ in both paths.}  Both paths advance from $e_{i+1}$ to

2058: $e_{i}$ in a single hop at level $l$, of length $2^l$.

2059: 

2060: As shown above, the two runs agree on the value of $T^{e_i - 2^l}$.

2061: Since $e_i - 2^l = e_{i+1}$, and from

2062: Line~\ref{alg:skipLists:processWholeAdvancementProof:continuity} of

2063: \algref{alg:skipLists:processWholeAdvancementProof}, the value for

2064: $T^{e_{i + 1}}$ while processing element $e_i$ must be identical to the

2065: value that the two runs compute for $T^{e_{i+1}}$ after processing the

2066: advancement at the previous element $e_{i + 1}$.

2067: \end{subparagraph}

2068: 

2069: \begin{subparagraph}{Case 2: Element $e_{i+1}$ does not immediately

2070: precede element $e_i$ in at least one of the paths.}  The two paths

2071: merge from two different immediate sources to element $e_i$ on their way

2072: from element $e_{i+1}$.  Because of

2073: Lemma~\ref{lem:skipLists:correctTraversal}, for some

2074: non-negative integers $0 \leq l < l'$ without loss of generality, the

2075: element immediately preceding $e_i$ on the first path is $p = e_i -

2076: 2^l$, and on the second it is $q = e_i - 2^{l'}$.  Note that $q < p$.

2077: 

2078: Lemma~\ref{lem:skipLists:parallelPaths} guarantees

2079: that there must be a common element between the two paths in $[q, p]$,

2080: since the first path starts at or before $q$ and reaches $p$ on its way

2081: to $e_i$, whereas the second path starts at $q$ and goes past $p$ on its

2082: way to $e_i$.  Since $q$ is the element immediately preceding $e_i$ on

2083: the second path, it must be the common element that

2084: Lemma~\ref{lem:skipLists:parallelPaths} anticipates.

2085: Therefore, $e_{i+1} = q$.

2086: 

2087: Because of Lemma~\ref{lem:skipLists:authenticatorSurvival},

2088: both runs of the advancement verification algorithm agree on the value

2089: of $T^{e_{i+1}}$ after processing element $e_{i+1}$ and after reaching

2090: element $e_i$.

2091: 

2092: \end{subparagraph}

2093: 

2094: The inductive step holds for both possible cases of advancement path

2095: commonalities and, as a result, the inductive argument holds, proving

2096: the lemma.  \qed

2097: 

2098: 

2099: \section{\label{sec:skipLists:implementation}Implementation}

2100: 

2101: We implement authenticated append-only skip lists using Java.  We focus

2102: here on a disk-based implementation, since it allows much larger data

2103: sequences than any memory-only implementation can, as well as

2104: persistence in the face of machine reboots.

2105: 

2106: An AASL is stored on disk as a linear file that consists of a

2107: \emph{preamble} and a sequence of \emph{element entries}, one for each

2108: element currently contained in the AASL.  An element entry consists of

2109: a data section and an authenticator section.

2110: 

2111: The data section primarily holds the datum stored in the associated AASL

2112: element.  This is the datum that participates in the computation of

2113: authenticators, as per Equations~\ref{eqn:skipLists:L} and

2114: \ref{eqn:skipLists:T}.  We call this the \emph{sensitive datum}.  Every

2115: element in a single AASL has sensitive data of a constant length, which

2116: is set when the AASL is initially created.

2117: 

2118: The data section of element entries may also contain an

2119: \emph{insensitive datum}.  This is also a fixed-length bit string.

2120: However, it does not participate in authenticator computations.

2121: Insensitive data may be useful information to the maintainer, collocated

2122: with the sensitive data for access efficiency, that need not be

2123: authenticated to remote verifiers of the AASL.  Since insensitive data

2124: do not participate in authenticator computations, they can be changed at

2125: will by the AASL maintainer unobtrusively to AASL verifiers.

2126: 

2127: The authenticator section of an element entry contains the authenticator

2128: computed for that element.

2129: 

2130: The preamble of the AASL file contains the lengths in bytes of the

2131: sensitive and insensitive data in element entries, and the element

2132: position of the last incorporated element into the AASL.

2133: 

2134: An empty AASL contains exactly one element entry: the entry for element

2135: $0$, which is a special entry.  Element entry $0$ has inconsequential

2136: sensitive and insensitive data.  Only its authenticator is meaningful.

2137: This authenticator is a value from the result domain of the hash

2138: function used, and it is agreed upon among all users of the AASL in

2139: advance.

2140: 

2141: Our implementation has a deviation from the abstract design of AASLs

2142: described in Section~\ref{sec:skipLists:design}.  We slightly modify how

2143: authenticators are computed for elements of odd indices, which only

2144: participate in a single linked list.  For such elements we skip the

2145: outer hash operation described in Equation~\ref{eqn:skipLists:T}, from

2146: concatenated partial authenticators to the actual authenticator of the

2147: element.  Since odd elements have only a single partial authenticator,

2148: that single partial authenticator is sufficient to ensure the collision

2149: resistance of AASL digests, and can serve as the actual authenticator of

2150: the element.  Furthermore, since half of the element indices are odd,

2151: this savings in computation can be significant compared to the overall

2152: computation required by AASL operations.

2153: 

2154: Another implementation optimization in the implemented AASLs deals with

2155: authenticator redundancy in membership and advancement proofs.  In the

2156: idealized algorithms \algref{alg:skipLists:processWholeMembershipProof}

2157: and \algref{alg:skipLists:processWholeAdvancementProof}, authenticators

2158: computed for the previous proof component are compared against the

2159: corresponding authenticator included in the next proof component (see

2160: Lines~\ref{alg:skipLists:processWholeMembershipProof:continuity} and

2161: \ref{alg:skipLists:processWholeAdvancementProof:continuity},

2162: respectively).  Since we compute these authenticators in the process of

2163: verifying membership and advancement proofs anyway, there is no need

2164: also to include them in the proofs themselves.  Consequently, we skip

2165: such authenticators in the AASL implementation.

2166: 

2167: 

2168: 

2169: 

2170: 

2171: 

2172: 

2173: 

2174: 

2175: 

2176: 

2177: 

2178: 

2179: {

2180: \tiny

2181: \begin{verbatim}

2182: $Id: PODC2003.tex,v 1.23 2003/02/07 01:11:25 maniatis Exp $

2183: \end{verbatim}

2184: }

2185: 

2186: \end{document}

2187: % LocalWords:  AASL AASLs

2188: