ダヴィッド ノヴァック
Research scientist, Détaché du CNRS
Research Team for Software Security, RCIS, AIST, Japan
A verification toolbox for cryptographic primitives on top of the proof assistant Coq
(DBLP, BibTeX file)
See Section Others below for freely available full versions.
| [1] | Jean Goubault-Larrecq, Slawomir Lasota, and David Nowak. Logical relations for monadic types. Mathematical Structures in Computer Science, 18(6):1169-1217, December 2008. [ http ] |
| [2] | Stéphane Demri and David Nowak. Reasoning about transfinite sequences. International Journal of Foundations of Computer Science, 18(1):87-112, February 2007. [ http ] |
| [3] | Stéphane Demri, Ranko Lazić, and David Nowak. On the freeze quantifier in Constraint LTL: decidability and complexity. Information and Computation, 205(1):2-24, January 2007. [ http ] |
| [4] | David Nowak. Synchronous structures. Information and Computation, 204(8):1295-1324, August 2006. [ http ] |
See Section Others below for freely available full versions.
| [1] | Reynald Affeldt, David Nowak, and Kiyoshi Yamada. Certifying assembly with formal cryptographic proofs: the case of BBS. In Automated Verification of Critical Systems 2009, volume 23 of Electronic Communications of the EASST. EASST. [ http ] |
| [2] | David Nowak and Kiyoshi Yamada. Towards a certified implementation of a cryptographically secure pseudorandom bit generator. In The 11th JSSST Workshop on Programming and Programming Languages (PPL 2009), pages 16-20. [ http ] |
| [3] | David Nowak. On formal verification of arithmetic-based cryptographic primitives. In Information Security and Cryptology - ICISC 2008, 11th International Conference, Seoul, Korea, December 3-5, 2008, Proceedings, volume 5461 of Lecture Notes in Computer Science, pages 368-382. Springer. [ http ] |
| [4] | David Nowak. A framework for game-based security proofs. In Information and Communications Security, 9th International Conference, ICICS 2007, Zhengzhou, China, December 12-15, 2007, Proceedings, volume 4861 of Lecture Notes in Computer Science, pages 319-333. Springer. [ http ] |
| [5] | Slawomir Lasota, David Nowak, and Yu Zhang. On completeness of logical relations for monadic types. In Advances in Computer Science - ASIAN 2006, Secure Software, 11th Asian Computing Science Conference, Tokyo, Japan, December 6-8, 2006, Proceedings, volume 4435 of Lecture Notes in Computer Science, pages 223-230. Springer. [ http ] |
| [6] | Stéphane Demri and David Nowak. Reasoning about transfinite sequences (extended abstract). In Automated Technology for Verification and Analysis: Third International Symposium, ATVA 2005, Taipei, Taiwan, October 4-7, 2005. Proceedings, volume 3707 of Lecture Notes in Computer Science, pages 248-262. Springer. [ http ] |
| [7] | Stéphane Demri, Ranko Lazić, and David Nowak. On the freeze quantifier in Constraint LTL: decidability and complexity. In 12th International Symposium on Temporal Representation and Reasoning (TIME 2005), 23-25 June 2005, Burlington, Vermont, USA, pages 113-121. IEEE Computer Society. [ http ] |
| [8] | Jean Goubault-Larrecq, Slawomir Lasota, David Nowak, and Yu Zhang. Complete lax logical relations for cryptographic lambda-calculi. In Computer Science Logic, 18th International Workshop, CSL 2004, 13th Annual Conference of the EACSL, Karpacz, Poland, September 20-24, 2004, Proceedings, volume 3210 of Lecture Notes in Computer Science, pages 400-414. Springer. [ http ] |
| [9] | Sébastien Bardin, Alain Finkel, and David Nowak. Toward symbolic verification of programs handling pointers. In Proceedings of the 3rd International Workshop on Automated Verification of Infinite-State Systems (AVIS'04), Electronic Notes in Theoretical Computer Science, Barcelona, Spain, April 2004. Elsevier. To appear. |
| [10] | Yu Zhang and David Nowak. Logical relations for dynamic name creation. In Computer Science Logic, 17th International Workshop, CSL 2003, 12th Annual Conference of the EACSL, and 8th Kurt Güdel Colloquium, KGC 2003, Vienna, Austria, August 25-30, 2003, Proceedings, volume 2803 of Lecture Notes in Computer Science, pages 575-588. Springer. [ http ] |
| [11] | Mickaël Kerbœuf, David Nowak, and Jean-Pierre Talpin. Formal proof of a polychronous protocol for loosely time-triggered architectures. In Formal Methods and Software Engineering, 5th International Conference on Formal Engineering Methods, ICFEM 2003, Singapore, November 5-7, 2003, Proceedings, volume 2885 of Lecture Notes in Computer Science, pages 359-374. Springer. [ http ] |
| [12] | Ranko Lazić and David Nowak. On a semantic definition of data independence. In Typed Lambda Calculi and Applications, 6th International Conference, TLCA 2003, Valencia, Spain, June 10-12, 2003, Proceedings, volume 2701 of Lecture Notes in Computer Science, pages 226-240. Springer. [ http ] |
| [13] | Jean Goubault-Larrecq, Slawomir Lasota, and David Nowak. Logical relations for monadic types. In Computer Science Logic, 16th International Workshop, CSL 2002, 11th Annual Conference of the EACSL, Edinburgh, Scotland, UK, September 22-25, 2002, Proceedings, volume 2471 of Lecture Notes in Computer Science, pages 553-568. Springer. [ http ] |
| [14] | Ranko Lazić and David Nowak. A unifying approach to data-independence. In CONCUR 2000 - Concurrency Theory, 11th International Conference, University Park, PA, USA, August 22-25, 2000, Proceedings, volume 1877 of Lecture Notes in Computer Science, pages 581-595. Springer. [ http ] |
| [15] | Mickaël Kerbœuf, David Nowak, and Jean-Pierre Talpin. Specification and verification of a steam-boiler with Signal-Coq. In Theorem Proving in Higher Order Logics, 13th International Conference, TPHOLs 2000, Portland, Oregon, USA, August 14-18, 2000, Proceedings, volume 1869 of Lecture Notes in Computer Science, pages 356-371. Springer. [ http ] |
| [16] | David Nowak, Jean-Pierre Talpin, and Paul Le Guernic. Synchronous structures. In CONCUR '99: Concurrency Theory, 10th International Conference, Eindhoven, The Netherlands, August 24-27, 1999, Proceedings, volume 1664 of Lecture Notes in Computer Science, pages 494-509. Springer. [ http ] |
| [17] | Jean-Pierre Talpin and David Nowak. A synchronous semantics of higher-order processes for modeling reconfigurable reactive systems. In Foundations of Software Technology and Theoretical Computer Science, 18th Conference, Chennai, India, December 17-19, 1998, Proceedings, volume 1530 of Lecture Notes in Computer Science, pages 78-89. Springer. [ http ] |
| [18] | David Nowak, Jean-René Beauvais, and Jean-Pierre Talpin. Co-inductive axiomatization of a synchronous language. In Proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'98), volume 1479 of Lecture Notes in Computer Science, pages 387-399. Springer. [ http ] |
| [19] | David Nowak, Jean-Pierre Talpin, Thierry Gautier, and Paul Le Guernic. An ML-like module system for the synchronous language Signal. In Euro-Par '97 Parallel Processing, Third International Euro-Par Conference, Passau, Germany, August 26-29, 1997, Proceedings, volume 1300 of Lecture Notes in Computer Science, pages 1244-1253. Springer. [ http ] |
| [1] | Reynald Affeldt, David Nowak, and Kiyoshi Yamada. Certifying assembly with formal cryptographic proofs: the case of bbs. Research report 2009/322, Cryptology ePrint Archive, July 2009. 18 pages. [ http ] |
| [2] | David Nowak. On formal verification of arithmetic-based cryptographic primitives. Research report 0904.1110, arXiv, April 2009. 13 pages. [ http ] |
| [3] | David Nowak. A framework for game-based security proofs. Research report 2007/199, Cryptology ePrint Archive, May 2007. Revised in November 2007. 16 pages. [ http ] |
| [4] | Slawomir Lasota, David Nowak, and Yu Zhang. On completeness of logical relations for monadic types. Research report cs.LO/0612106, arXiv, December 2006. 20 pages. [ http ] |
| [5] | Stéphane Demri, Ranko Lazić, and David Nowak. On the freeze quantifier in Constraint LTL: decidability and complexity. Research report cs.LO/0609008, arXiv, September 2006. 29 pages. [ http ] |
| [6] | Jean Goubault-Larrecq, Slawomir Lasota, and David Nowak. Logical relations for monadic types. Research report cs.LO/0511006, arXiv, November 2005. Revised in March 2008. 83 pages. [ http ] |
| [7] | Stéphane Demri and David Nowak. Reasoning about transfinite sequences. Research report cs.LO/0505073, arXiv, May 2005. Revised in August 2006. 38 pages. [ http ] |
| [8] | Stéphane Demri, Ranko Lazić, and David Nowak. On the freeze quantifier in constraint LTL: Decidability and complexity. Research report LSV-05-03, Laboratoire Spécification et Vérification, ENS Cachan, April 2005. 13 pages. [ .pdf ] |
| [9] | Jean Goubault-Larrecq, Slawomir Lasota, David Nowak, and Yu Zhang. Complete lax logical relations for cryptographic lambda-calculi. Research report LSV-04-4, Laboratoire Spécification et Vérification, École Normale Supérieure de Cachan, February 2004. 16 pages. [ .ps ] |
| [10] | Sébastien Bardin, Alain Finkel, and David Nowak. Rapport final. Contract report, Contract P11L03/F01304/0 + 50.0241 between EDF and LSV, November 2003. 50 pages. |
| [11] | Sébastien Bardin, Alain Finkel, and David Nowak. Note de synthèse à 10 mois. Contract report, Contract P11L03/F01304/0 + 50.0241 between EDF and LSV, August 2003. 21 pages. |
| [12] | Sébastien Bardin, Alain Finkel, David Nowak, and Philippe Schnoebelen. Note de synthèse à 6 mois. Contract report, Contract P11L03/F01304/0 + 50.0241 between EDF and LSV, July 2003. 43 pages. |
| [13] | Ranko Lazić and David Nowak. On a semantic definition of data independence. Research report CS-RR-392, Department of Computer Science, University of Warwick, December 2002. 20 pages. [ .ps.gz ] |
| [14] | David Nowak, editor. Proceedings of the Workshop on Automated Verification of Critical Systems (AVoCS'01), number PRG-RR-01-07 in Programming Research Group research reports, Oxford, England, UK, April 2001. [ .ps.gz ] |
| [15] | Ranko Lazić and David Nowak. A unifying approach to data-independence. Technical Report PRG-TR-4-00, Oxford University Computing Laboratory (OUCL), June 2000. 30 pages. [ .ps.gz ] |
| [16] | Mickaël Kerbœuf, David Nowak, and Jean-Pierre Talpin. The steam boiler controller problem in Signal-Coq. Research report 3773, Institut National de Recherche en Informatique et Automatique (INRIA), October 1999. 59 pages. [ .html ] |
| [17] | Mickaël Kerbœuf, David Nowak, and Jean-Pierre Talpin. The steam boiler controller problem in Signal-Coq. Internal Publication 1266, Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), October 1999. 59 pages. [ http ] |
| [18] | David Nowak. Spécification et preuve de systèmes réactifs. PhD thesis, Université de Rennes 1, October 1999. 176 pages. [ .html ] |
| [19] | David Nowak. The semantics of Tuplink. Research report RT0292, IBM Japan Ltd., Tokyo Research Laboratory, September 1998. |
| [20] | David Nowak, Jean-Pierre Talpin, and Thierry Gautier. Un système de modules avancé pour Signal. Research report 3176, Institut National de Recherche en Informatique et Automatique (INRIA), June 1997. 34 pages. [ .html ] |
| [21] | David Nowak, Jean-Pierre Talpin, and Thierry Gautier. Un système de modules avancé pour Signal. Internal Publication 1109, Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), June 1997. 34 pages. [ http ] |
This web page has been partly generated by bibtex2html