home > book reviews > Steve Schneider
Google > Steve Schneider


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)