2 Search Results for "Gilbert, Henri"


Document
Formal Proof and Analysis of an Incremental Cycle Detection Algorithm

Authors: Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud, and François Pottier

Published in: LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019)


Abstract
We study a state-of-the-art incremental cycle detection algorithm due to Bender, Fineman, Gilbert, and Tarjan. We propose a simple change that allows the algorithm to be regarded as genuinely online. Then, we exploit Separation Logic with Time Credits to simultaneously verify the correctness and the worst-case amortized asymptotic complexity of the modified algorithm.

Cite as

Armaël Guéneau, Jacques-Henri Jourdan, Arthur Charguéraud, and François Pottier. Formal Proof and Analysis of an Incremental Cycle Detection Algorithm. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 18:1-18:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{gueneau_et_al:LIPIcs.ITP.2019.18,
  author =	{Gu\'{e}neau, Arma\"{e}l and Jourdan, Jacques-Henri and Chargu\'{e}raud, Arthur and Pottier, Fran\c{c}ois},
  title =	{{Formal Proof and Analysis of an Incremental Cycle Detection Algorithm}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{18:1--18:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{Harrison, John and O'Leary, John and Tolmach, Andrew},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.18},
  URN =		{urn:nbn:de:0030-drops-110739},
  doi =		{10.4230/LIPIcs.ITP.2019.18},
  annote =	{Keywords: interactive deductive program verification, complexity analysis}
}
Document
QUAD: Overview and Recent Developments

Authors: David Arditti, Côme Berbain, Olivier Billet, Henri Gilbert, and Jacques Patarin

Published in: Dagstuhl Seminar Proceedings, Volume 7021, Symmetric Cryptography (2007)


Abstract
We give an outline of the specification and provable security features of the QUAD stream cipher proposed at Eurocrypt 2006. The cipher relies on the iteration of a multivariate system of quadratic equations over a finite field, typically GF(2) or a small extension. In the binary case, the security of the keystream generation can be related, in the concrete security model, to the conjectured intractability of the MQ problem of solving a random system of m equations in n unknowns. We show that this security reduction can be extended to incorporate the key and IV setup and provide a security argument related to the whole stream cipher.We also briefly address software and hardware performance issues and show that if one is willing to pseudorandomly generate the systems of quadratic polynomials underlying the cipher, this leads to suprisingly inexpensive hardware implementations of QUAD.

Cite as

David Arditti, Côme Berbain, Olivier Billet, Henri Gilbert, and Jacques Patarin. QUAD: Overview and Recent Developments. In Symmetric Cryptography. Dagstuhl Seminar Proceedings, Volume 7021, pp. 1-20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)


Copy BibTex To Clipboard

@InProceedings{arditti_et_al:DagSemProc.07021.9,
  author =	{Arditti, David and Berbain, C\^{o}me and Billet, Olivier and Gilbert, Henri and Patarin, Jacques},
  title =	{{QUAD: Overview and Recent Developments}},
  booktitle =	{Symmetric Cryptography},
  pages =	{1--20},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{7021},
  editor =	{Eli Biham and Helena Handschuh and Stefan Lucks and Vincent Rijmen},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.07021.9},
  URN =		{urn:nbn:de:0030-drops-10155},
  doi =		{10.4230/DagSemProc.07021.9},
  annote =	{Keywords: MQ problem, stream cipher, provable security, Gr\~{A}ƒ\^{A}¶bner basis}
}
  • Refine by Author
  • 1 Arditti, David
  • 1 Berbain, Côme
  • 1 Billet, Olivier
  • 1 Charguéraud, Arthur
  • 1 Gilbert, Henri
  • Show More...

  • Refine by Classification
  • 1 Software and its engineering → Correctness
  • 1 Software and its engineering → Software performance
  • 1 Theory of computation → Graph algorithms analysis
  • 1 Theory of computation → Program verification

  • Refine by Keyword
  • 1 Gröbner basis
  • 1 MQ problem
  • 1 complexity analysis
  • 1 interactive deductive program verification
  • 1 provable security
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2007
  • 1 2019

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail