Books

Short works

Books : reviews

Steve Schneider.
Concurrent and Real-time Systems: the CSP approach.
Wiley. 2000

(read but not reviewed)

Steve Schneider.
The B-Method: an introduction.
Palgrave. 2001

(read but not reviewed)

This book provides a textbook introduction to the B-Method, a rigorous methodology for the development of correct software. The text covers all stages of the B software development process – from specification, through refinement and design, down to implementation and automatic code generation. The method uses a single uniform notation throughout development, designed to enable verification at each stage whilst placing particular emphasis on correctness.

• Suitable for undergraduate and postgraduate courses on formal methods and software development.
• Written in a clear tutorial style of explanation.
• Contains numerous illustrative examples, exercises and self-testing questions with solutions throughout.
• Relevant to users of any B-Method CASE tool.

[disclaimer: this is an inspection copy sent to me by the publisher]

Peter Y. A. Ryan, Steve Schneider, Michael Goldsmith, Gavin Lowe, A. W. Roscoe.
The Modelling and Analysis of Security Protocols: the CSP approach.
Addison Wesley. 2001

Security protocols are one of the most critical elements in enabling the secure communication and processing of information, ensuring its confidentiality, integrity, authenticity and availability. These protocols are vulnerable to a host of subtle attacks, so designing protocols to be impervious to such attacks has proved to be extremely challenging and error prone.

This book provides a thorough and detailed understanding of one of the most effective approaches to the design and evaluation of security critical systems, describing the role of security protocols in distributed secure systems and the vulnerabilities to which they are prey.

The authors introduce security protocols, the role they play and the cryptographic mechanisms they employ, and progress to detail their role in security architectures, e-commerce, e-cash and so on. Precise characterizations of key concepts in information security, such as confidentiality, authentication and integrity are discussed and a range of tools and techniques are described which will ensure that a protocol guarantees certain security services under appropriate assumptions.

Ali E. Abdallah, Peter Y. A. Ryan, Steve Schneider, eds.
Formal Aspects of Security: FASec 2002 revised papers.
Springer. 2003

(read but not reviewed)

Contents

Fred B. Schneider. Lifting reference models from the kernel. 2003
(keynote talk: extended abstract)
Andy Gordon. Authenticity types for cryptographic protocols. 2003
(invited talk: extended abstract)
Lawrence C. Paulson. Verifying the SET protocol: overview. 2003
(invited talk)
David von Oheimb. Interacting State Machines: a stateful approach to proving security. 2003
Frederic Oehl, Gerard Cece, Olga Kouchnarenko, David Sinclair. Automatic approximation for the verification of cryptographic protocols. 2003
Colin Boyd, Kapali Viswanathan. Towards a formal specification of the Bellare-Rogaway model for protocol analysis. 2003
Susan Stepney. Critical critical systems. 2003
(invited talk) full paper
Dieter Gollmann. Analysing security protocols. 2003
(invited talk)
Gethin Norman, Vitaly Shmatikov. Analysis of probabilistic contract signing. 2003
Sigrid Gurgens, Carsten Rudolph. Security analysis of (un-)fair non-repudiation protocols. 2003
Joseph Y. Halpern, Riccardo Pucella. Modeling adversaries in a logic for security protocol analysis. 2003
M. Debbabi, J. Desharnais, M. Fourati, E. Menif, F. Painchaud, N. Tawbi. Secure self-certified code for Java. 2003
J. Anthony Hall. Z styles for security properties and modern user interfaces. 2003
B. Preneel. Cryptographic challenges: the past and the future. 2003
(invited talk)
Ernie Cohen. TAPS: the last few slides. 2003
(invited talk)
Antonio Durante, Roberto Di Pietro, Luigi V. Mancini. Formal specification for fast automatic IDS training. 2003
Gordon Thomas Rohrmair, Gavin Lowe. Using CSP to detect insertion and evasion possibilities within the intrusion detection area. 2003
Felix C. Gartner. Revisiting liveness properties in the context of secure systems. 2003

Helen Treharne, Steve King, Martin C. Henson, Steve Schneider, eds.
ZB 2005: Formal Specification and Development in Z and B: Fourth International Conference of B and Z Users, Guildford, UK.
Springer. 2005

(read but not reviewed)

Contents

Cliff B. Jones. Specification before Satisfaction: the case for research into obtaining the right specification. 2005
(invited talk, extended abstract)
Michael Leuschel, Edd Turner. Visualising larger state spaces in ProB. 2005
John Derrick, Heike Wehrheim. Non-atomic refinement in Z and CSP. 2005
Steve Dunne, Stacey Conroy. Process refinement in B. 2005
Petra Malik, Mark Utting. CZT: a framework for Z tools. 2005
Graeme Smith, Luke Wildman. Model checking Z specifications using SAL. 2005
Ian Toyn, Andy Galloway. Proving properties of Stateflow models using ISO Standard Z and CADiZ. 2005
J. Christian Attiogbe. A stepwise development of the Peterson's mutual exclusion algorithm using B Abstract Systems. 2005
Pontus Bostrom, Marina Walden. An extension of Event B for developing Grid systems. 2005
Carroll Morgan, Thai Son Hoang, Jean-Raymond Abrial. The challenge of probabilistic Event B. 2005
(invited talk, extended abstract)
Jemima Rossmorris, Susan Stepney. Requirements as conjectures: intuitive DVD menu navigation. 2005
Frank Zeyda, Bill Stoddart, Steve Dunne. A Prospective-Value semantics for the GSL. 2005
Richard Banach, Simon Fraser. Retrenchment and the B-toolkit. 2005
Jean-Raymond Abrial, Dominique Cansell, Dominique Mery. Refinement and reachability in Event B. 2005
Soon-Kyeong Kim, David Carrington. A rigorous foundation for pattern-based design models. 2005
Nuno Amalio, Fiona Polack, Susan Stepney. An object-oriented structuring for Z based on Views. 2005
Yann Zimmermann, Diana Toma. Component reuse in B using ACL2. 2005
Didier Bert, Marie-Laure Potet, Nicolas Stouls. GeneSyst: a tool to reason about behavioral aspects of B Event specifications: aplication to security properties. 2005
Benjamin W. Long. Formal verification of a type flaw attack on a security protocol using Object-Z. 2005
Frederic Badeau, Arnaud Amelot. Using B as a high level programming language in an industrial project: Roissy VAL. 2005
(invited talk)
Thai Son Hoang, Zhendong Jin, Ken Robinson, Annabelle McIver, Carroll Morgan. Development via refinement in Probabilistic B -- foundation and case study. 2005
Eerke A. Boiten, John Derrick. Formal program development with approximations. 2005
Lindsay Groves. Practical data refinement for the Z schema calculus. 2005
Ingo Bruckner, Heike Wehrheim. Slicing Object-Z specifications for verification. 2005
Fabrice Bouquet, Frederic Dadeau, Julien Groslambert. Checking JML specifications with B Machines. 2005
Judy Bowen, Steve Reeves. Including design guidelines in the formal specification of interfaces in Z. 2005
Abdolbaghi Rezazadeh, Michael J. Butler. Some guidelines for formal development of web-based applications in the B-Method. 2005

Alistair A. McEwan, Steve Schneider, Wilson Ifill, Peter H. Welch.
Communicating Process Architectures 2007: WOTUG-30.
IOS Press. 2007

(read but not reviewed)