| December 6th, 2006 | |
| 10:00-10:30 | Registration and Opening |
| 10:30-11:30 | Secure Protection |
|
Security Evaluation of a Type of Table-network Block Cipher Implementation Akira Matsunaga and Tsutomu Matsumoto (Yokohama National University, Japan) |
|
|
A Symbolic Intruder Model for Hash-Collision Attacks Yannick Chevalier and Mounira Kourjieh (Universit Paul Sabatier Toulouse 3/IRIT, France) |
|
| 11:30-12:30 | Short Papers Session I: Security |
|
A Denotational Approach to Scope-based Compensable Flow Language for Web Services Huibiao Zhu, Geguang Pu and Jifeng He (East China Normal University, China) |
|
|
Certificateless Authenticated Two-Party Key Agreement Protocols Tarjei Mandt and Chik How Tan (Gj¿vik University College, Norway) |
|
| 12:00-2:00 | Lunch Break (120 minutes) |
| 2:00-3:00 | Invited Talk |
|
Security Considerations in the Online World -- a Windows Live/MSN Perspective Li Gong (Windows Live China, Microsoft Corporation, China) |
|
| 3:00-3:30 | Short Break (30 minutes) |
| 3:30-4:30 | Secure Execution Support |
|
FORM : A Federated Rights Expression Model for Open DRM Frameworks Thierry Sans, Frederic Cuppens and Nora Cuppens-Boulahia (GET/ENST-Bretagne, France) |
|
|
A Method of Safety Analysis for Runtime Code Update Masatomo Hashimoto (National Institute of Advanced Industrial Science and Technology, Japan) |
|
| 4:30-4:50 | Short Break (20 minutes) |
| 4:50-5:50 | Automated Support for Security |
|
Automaton-based Confidentiality Monitoring Gurvan Le Guernic (IRISA, France), Anindya Banerjee (Kansas State University, USA), Thomas Jensen (IRISA, France) and David Schmidt (Kansas State University, USA) |
|
|
Efficient and Practical Control Flow Monitoring for Program Security Nai Xia, Bing Mao and Li Xie (Nanjing University, China) |
|
| 6:00- | Reception |
| December 7th, 2006 | |
| 10:00-11:30 | Reactive Systems |
|
Modular Formalization of Reactive Modules in Coq Ming-Hsien Tsai and Bow-Yaw Wang (Academia Sinica, Taiwan) |
|
|
Closing Internal Timing Channels by Transformation Alejandro Russo, John Hughes (Chalmers University of Technology, Sweden), David Naumann (Stevens Institute of Technology, USA) and Andrei Sabelfeld ((Chalmers University of Technology, Sweden) |
|
|
Responsiveness in process calculi Lucia Acciai and Michele Boreale (Dipartimento di Sistemie Informatica, Italy) |
|
| 11:30-11:45 | Short Break (15 minutes) |
| 11:45-12:15 | Theories for Security |
|
Normal Proofs in Intruder Theories Vincent Bernat and Hubert Comon-Lundh (LSV, CNRS, INRIA, Ecole Normale Superieure de Cachan, France) |
|
| 12:15-2:00 | Lunch Break (105 minutes) | 2:00-2:10 | Greeting from NII and Conference Officers Yoshichi Tohkura |
| 2:10-3:10 | Invited Talk |
|
Symbolic and Computational Analysis of Network Protocol Security John Mitchell (Stanford University, USA) |
|
| 3:10-3:30 | Short Break (20 minutes) |
| 3:30-5:00 | Theories for Security |
|
Breaking and Fixing Public-Key Kerberos Iliano Cervesato (Deductive Solutions, USA), Aaron D.Jaggard (Tulane University, USA), Andre Scedrov, Joe-Kai Tsay and Christopher Walstad (University of Pennsylvania, USA) | |
|
The Computational Soundness of Formal Indistinguishability and Static Equivalence Gergei Bana, Payman Mohassel and Till Stegers (University of California at Davis, USA) |
|
|
Secrecy Analysis in Protocol Composition Logic Arnab Roy, Anupam Datta, Ante Derek, John Mitchell (Stanford University, USA) and Jean-Pierre Seifert (Intel, USA) |
|
| 5:00-5:20 | Memorial Session for Gilles Kahn |
| 7:00- | Conference Dinner |
| December 8th, 2006 | |
| 10:00-11:00 | Short Papers Session II: Theory |
|
A Type-theoretic Framework for Formal Reasoning with Different Logical Foundations Zhaohui Luo (University of London, UK) |
|
|
On Completeness of Logical Relations for Monadic Types Slawomir Lasota (Warsaw University, Poland), David Nowak (National Institute of Advanced Industrial Science and Technology, Japan) and Yu Zhang (CEA, France) |
|
|
A Spatial Logical Characterisation of Context Bisimulation Zining Cao (Nanjing University of Aero. & Astro, China) |
|
|
Information Hiding in the Join Calculus Qin Ma (OFFIS, Germany) and Luc Maranget (INRIA-Rocquencourt, France) |
|
| 11:00-11:20 | Short Break (20 minutes) |
| 11:20-12:20 | Short Papers Session III: Verification |
|
Modeling Urgency in Component Based Real-time Systems Tang Nguyen, Dang Van Hung and Mizuhito Ogawa (Japan Advanced Institute of Science and Technolog, Japan) |
|
|
Translating Graphical Conceptual Model From STATEMATE to FNLOG Yousra Ben Daly Hlaoui and Leila Jemni Ben Ayed (Campus Universitaire, Tunis) |
|
|
Maintaining Data Consistency of XML Databases Using Verification Techniques Khandoker Asadul Islam and Yoshimichi Watanabe (University of Yamanashi, Japan) |
|
|
An Operational Semantics of Program Dependence Graphs for Unstructured Programs Souhei Ito, Shigeki Hagihara and Naoki Yonezaki (Tokyo Institute of Technology, Japan) |
|
| 12:20-2:00 | Lunch Break (100 minutes) |
| 2:00-3:00 | Invited Talk |
|
Verification of Large Complex Software by Abstract Interpretation Patrick Cousot (Ecole Normale Superieure-Paris, France) |
|
| 3:00-3:20 | Short Break (20 minutes) |
| 3:20-4:20 | Verification and Theories I |
|
Proving Noninterference by Fully Complete Translation to the Simply Typed Lambda Calculus Naokata Shikuma and Atsushi Igarashi (Kyoto University, Japan) |
|
|
Formalization of CTL* in Calculus of Inductive Constructions Ming-Hsien Tsai and Bow-Yaw Wang (Academia Sinica, Taiwan) |
|
| 4:20-4:40 | Short Beark (20 minutes) |
| 4:40-5:40 | Verification and Theories II |
|
Inferring Disjunctive Postconditions Corneliu Popeea and Wei-Ngan Chin (National University of Singapore, Singapore) | |
|
An Approach to Formal Verification of Arithmetic Functions in Assembly Reynald Affeldt and Nicolas Marti (National Institute of Advanced Industrial Science and Technology, Japan) | |
| 5:40-5:50 | Closing |