The Coq Café

The Coq Café is a meeting held in AIST-RCIS by members of the Research Team for Software Security. Due to changes in the affiliation of attendees, the meeting management went offline. Past meetings are still displayed below to give an idea of issues that motivate us. People who share similar interests in the Coq proof assistant are welcome to contact us.

Rules

Participants can:

1. Come with a problem they want to formalize in Coq and ask for help. Any problem is ok: research problems, exercises, etc. No expert-knowledge in Coq is required.
2. Come with a Coq formalization and ask for feedback or help. It is ok to enter into details of the formalization.
3. Come with an research output to share recent results.

Presentation material (slides, handouts, etc.) should not be necessary. White-board explanations are preferred. Live proofs are ok (a display device is always available).

Past meetings

• 15/08/07: 38th Coq Café: Survey of [MRST2006].
• 08/08/07: 37th Coq Café: Related work about mechanization of game-playing.
• 01/08/07: 36th Coq Café: Presentation by Toshihiro Yoshino from the University of Tokyo.
• 25/07/07: 35th Coq Café: Random chat.
• 18/07/07: The Coq Café goes cryptography: Lectures by Alfred Menezes at NTT laboratories.
• 11/07/07 (Exceptionally at 11:00): 34th Coq Café: Presentation by Gyesik Lee from INRIA on binders in Coq.
• 04/07/07: 33rd Coq Café: FMapList. Formal statement of FDH security.
• 27/06/07: 32nd Coq Café: Formal verification of heterogeneous code.
• 20/06/07: 31st Coq Café: A formalization of the "no race condition" property for a small concurrent language. Survey of [FF2000]. Hashed ElGamal in Coq.
• 13/06/07: 30th Coq Café: Survey of [FA1999].
• 06/06/07: 29th Coq Café: Introduction to bit commitment and oblivious transfer. Presentation by Anderson Nascimento from University of Brasilia. Recommended reference: [CCKLLPS2005].
• 30/05/07: 28th Coq Café: Introduction to pairing. Presentation by Lihua Wang from NICT [DBS2004,GGS2005].
• 23/05/07: The Coq Café goes Task PIOA: Special lectures by Roberto Segala at NTT Laboratories.
• 17/05/07: 27th Coq Café: 2nd Coq Café challenge.
• 09/05/07: 26th Coq Café: Draft proof-reading [N2007].
• 30/04-4/05/07: The Coq Café goes Golden Week.
• 25/04/07 (Exceptionally on Friday): 25th Coq Café: Tentative formalization of the Switching lemma (result in [ATM2007]).
• 20/04/07 (Exceptionally on Friday): 24th Coq Café: Semantic security of ElGamal in Coq.
• 13/04/07 (Exceptionally on Friday): 23rd Coq Café: Formalization of the fundamental lemmas of [BR2004].
• 04/04/07: 22nd Coq Café: Extension of [SU2005] with procedures.
• 30/03/07 (Exceptionally on Friday): 21st Coq Café: Tentative formalization of FDH.
• 23/03/07 (Exceptionally on Friday): 20th Coq Café: Semantics of call/return's, with the participation of Keiko Nakata.
• 14/03/07: 19th Coq Café: Exact security of FDH [C2000].
• 07/03/07: 18th Coq Café: Survey of the last JSIAM-FAIS meeting.
• 28/02/07: 17th Coq Café: Random chat about formal verification and provable security.
• 21/02/07: 16th Coq Café: CryptoVerif demo [B2006].
• 14/02/07: 15th Coq Café: Survey on formalization of the CDH assumption [HM2007].
• 07/02/07: 14th Coq Café: Matching binders with Ltac.
• 31/01/07: 13rd Coq Café: Security proof for FDH [P2005]. Presentation by Rui Zhang, Research Team for Physical Analysis.
• 24/01/07: 12th Coq Café: Formalization of Monads and probabilities.
• 17/01/07: 11th Coq Café: Formalization of El-Gamal security proofs [S2004,CdH2006].
• 10/01/07: 10th Coq Café: Formal verification of TLS using Paulson's Method.
• 27/12/06: 9th Coq Café: Formalization of Fail-safe C properties (part II).
• 20/12/06: The Coq Café goes Sendai: Presentation by Nicolas about a decision procedure for a fragment of separation logic.
• 13/12/06: 8th Coq Café: 1st Coq Café challenge. The Scheme tactic.
• 06/12/06: The Coq Café goes ASIAN 2006: Presentation by Reynald [AM2006].
• 29/11/06: 7th Coq Café: Formalization of Fail-safe C properties.
• 22/11/06: 6th Coq Café: Formalization of MinAML type system.
• 15/11/06: 5th Coq Café: Formalization of MinAML syntax and operational semantics [WZL2003].
• 08/11/06: 4th Coq Café: Random chat.
• 01/11/06: The Coq Café goes ICFEM 2006: Presentation by Nicolas [MAY2006].
• 25/10/06: 3rd Coq Café: Operational semantics and correctness definitions for a minimal AspectJ.
• 18/10/06: The Coq Café goes Isabelle: Special lecture by Christoph Sprenger on formal proofs in the BPW model.
• 11/10/06: 2nd Coq Café: Informal semantics of AspectJ.
• 04/10/06: 1st Coq Café: Random chat.

References:

• [ATM2007] Reynald Affeldt, Miki Tanaka and Nicolas Marti, "Formal Proof of Provable Security by Game-playing in a Proof Assistant", Provsec 2007.
• [N2007] David Nowak, "A Framework for Game-based Security Proofs", Cryptology ePrint Archive: Report 2007/199.
• [HM2007] Yoshikazu Hanatani and Hirofumi Muratani, "Description of CDH Assumption for CryptoVerif", SCIS 2007.
• [B2006] Bruno Blanchet, "Analyse de protocoles cryptographiques dans le modèle computationel", homepage.
• [B2006b] Bruno Blanchet and David Pointcheval, "Automated Security Proofs with Sequences of Games", CRYPTO 2006.
• [AM2006] Reynald Affeldt and Nicolas Marti, "An Approach to Formal Verification of Arithmetic Functions in Assembly", ASIAN 2006.
• [MAY2006] Nicolas Marti, Reynald Affeldt, and Akinori Yonezawa, "Formal Verification of the Heap Manager of an Operating System using Separation Logic", ICFEM 2006.
• [CdH2006] Ricardo Corin and Jerry den Hartog, "A Probabilistic Hoare-style logic for Game-based Cryptographic Proofs", ICALP-C 2006.
• [MRST2006] John C. Mitchell, Ajith Ramanathan, Andre Scedrov, and Vanessa Teague, "A probabilistic polynomial-time process calculus for the analysis of cryptographic protocols", TCS 2006.
• [GGS2005] M. Choudary Gorantla, Raju Gangishetti, and Ashutosh Saxena. A Survey on ID-Based Cryptographic Primitives. Cryptology ePrint Archive: Report 2005/094.
• [P2005] David Pointcheval, "Contemporary Cryptology Provable Security for Public Key Schemes", Advanced Course on Contemporary Cryptology, 2005.
• [CCKLLPS2005] R. Canetti, L. Cheung, D. Kaynar, M. Liskov, N. Lynch, O. Pereira, and R. Segala, "Using Probabilistic I/O Automata to Analyze an Oblivious Transfer Protocol", Cryptology ePrint Archive: Report 2005/452.
• [SU2005] Ando Saabas and Tarmo Uustalu, "A Compositional Natural Semantics and Hoare Logic for Low-Level Languages", SOS 2005.
• [DBS2004] Ratna Dutta, Rana Barua, and Palash Sarkar. Pairing-Based Cryptographic Protocols : A Survey. Cryptology ePrint Archive: Report 2004/064.
• [S2004] Victor Shoup, "Sequences of Games: A Tool for Taming Complexity in Security Proofs", available from www.shoup.net.
• [BR2004] M. Bellare and P. Rogaway, "The Game-Playing Technique", Draft, 2004.
• [WZL2003] David Walker, Steve Zdancewic, and Jay Ligatti, "A Theory of Aspects", ICFP 2003.
• [FF2000] Cormac Flanagan and Stephen N. Freund, "Type-Based Race Detection for Java", PLDI 2000.
• [C2000] Jean-Sébastien Coron, "On the Exact Security of Full Domain Hash", CRYPTO 2000.
• [FA1999] Cormac Flanagan and Martín Abadi, "Types for Safe Locking", ESOP 1999.