author : Steve Schneider

(disclaimer: this is an inspection copy sent to me by the publisher)

Contents

• Fred B. Schneider.

Lifting reference models from the kernel

(keynote talk: extended abstract)

• Andy Gordon.

Authenticity types for cryptographic protocols

(invited talk: extended abstract)

• Lawrence C. Paulson.

Verifying the SET protocol: overview

(invited talk)

• David von Oheimb.

Interacting State Machines: a stateful approach to proving security

• Frederic Oehl, Gerard Cece, Olga Kouchnarenko, David Sinclair.

Automatic approximation for the verification of cryptographic protocols

• Colin Boyd, Kapali Viswanathan.

Towards a formal specification of the Bellare-Rogaway model for protocol analysis

• Susan Stepney.

Critical critical systems

(invited talk) full paper

• Dieter Gollmann.

Analysing security protocols

(invited talk)

• Gethin Norman, Vitaly Shmatikov.

Analysis of probabilistic contract signing

• Sigrid Gurgens, Carsten Rudolph.

Security analysis of (un-)fair non-repudiation protocols

• Joseph Y. Halpern, Riccardo Pucella.

Modeling adversaries in a logic for security protocol analysis

• M. Debbabi, J. Desharnais, M. Fourati, E. Menif, F. Painchaud, N. Tawbi.

Secure self-certified code for Java

• J. Anthony Hall.

Z styles for security properties and modern user interfaces

• B. Preneel.

Cryptographic challenges: the past and the future

(invited talk)

• Ernie Cohen.

TAPS: the last few slides

(invited talk)

• Antonio Durante, Roberto Di Pietro, Luigi V. Mancini.

Formal specification for fast automatic IDS training

• Gordon Thomas Rohrmair, Gavin Lowe.

Using CSP to detect insertion and evasion possibilities within the intrusion detection area

• Felix C. Gartner.

Revisiting liveness properties in the context of secure systems

Contents

• Cliff B. Jones.

Specification before Satisfaction: the case for research into obtaining the right specification

(invited talk, extended abstract)

• Michael Leuschel, Edd Turner.

Visualising larger state spaces in ProB

• John Derrick, Heike Wehrheim.

Non-atomic refinement in Z and CSP

• Steve Dunne, Stacey Conroy.

Process refinement in B

• Petra Malik, Mark Utting.

CZT: a framework for Z tools

• Graeme Smith, Luke Wildman.

Model checking Z specifications using SAL

• Ian Toyn, Andy Galloway.

Proving properties of Stateflow models using ISO Standard Z and CADiZ

• J. Christian Attiogbe.

A stepwise development of the Peterson's mutual exclusion algorithm using B Abstract Systems

• Pontus Bostrom, Marina Walden.

An extension of Event B for developing Grid systems

• Carroll Morgan, Thai Son Hoang, Jean-Raymond Abrial.

The challenge of probabilistic Event B

(invited talk, extended abstract)

• Jemima Rossmorris, Susan Stepney.

Requirements as conjectures: intuitive DVD menu navigation

• Frank Zeyda, Bill Stoddart, Steve Dunne.

A Prospective-Value semantics for the GSL

• Richard Banach, Simon Fraser.

Retrenchment and the B-toolkit

• Jean-Raymond Abrial, Dominique Cansell, Dominique Mery.

Refinement and reachability in Event B

• Soon-Kyeong Kim, David Carrington.

A rigorous foundation for pattern-based design models

• Nuno Amalio, Fiona Polack, Susan Stepney.

An object-oriented structuring for Z based on Views

• Yann Zimmermann, Diana Toma.

Component reuse in B using ACL2

• Didier Bert, Marie-Laure Potet, Nicolas Stouls.

GeneSyst: a tool to reason about behavioral aspects of B Event specifications: aplication to security properties

• Benjamin W. Long.

Formal verification of a type flaw attack on a security protocol using Object-Z

• Frederic Badeau, Arnaud Amelot.

Using B as a high level programming language in an industrial project: Roissy VAL

(invited talk)

• Thai Son Hoang, Zhendong Jin, Ken Robinson, Annabelle McIver, Carroll Morgan.

Development via refinement in Probabilistic B -- foundation and case study

• Eerke A. Boiten, John Derrick.

Formal program development with approximations

• Lindsay Groves.

Practical data refinement for the Z schema calculus

• Ingo Bruckner, Heike Wehrheim.

Slicing Object-Z specifications for verification

• Fabrice Bouquet, Frederic Dadeau, Julien Groslambert.

Checking JML specifications with B Machines

• Judy Bowen, Steve Reeves.

Including design guidelines in the formal specification of interfaces in Z

• Abdolbaghi Rezazadeh, Michael J. Butler.

Some guidelines for formal development of web-based applications in the B-Method