Formal Aspects of Security: First International Conference, FASec 2002, London, UK, December 16-18, 2002, Revised Papers (Lecture Notes in Computer Science (2629))

This book constitutes the thoroughly refereed post-proceedings of the First International Conference on Formal Aspects of Security, FASec 2002, held in London, UK, in December 2002. The 11 revised full papers presented together with 7 invited contributions were carefully reviewed, selected, and improved for inclusion in the book. The papers are organized in topical sections on protocol verification, analysis of protocols, security modelling and reasoning, and intrusion detection systems and liveness. Preface Formal Aspects Of Security (fasec) Was Held At Royal Holloway, University Of London, 18–20 December 2002. The Occasion Celebrated A Jubilee, Namely The 25thanniversaryoftheestablishmentofbcs-facs,theformalaspectsofc- Puting Science Specialist Group Of The British Computer Society. Fasec Is One Of A Series Of Events Organized By Bcs-facs To Highlight The Use Of Formal Me- Ods, Emphasize Their Relevance To Modern Computing, And Promote Their Wider Application. As The Architecture Model Of Information Systems Evolves From - Connected Pcs,throughintranet (lan) And Internet (wan), To Mobile Internet And Grids, Security Becomes Increasingly Critical To All Walks Of Society: C- Merce, ?nance, Health, Transport, Defence And Science. It Is No Surprise Therefore That Security Is One Of The Fastest-growing Research Areas In Computer Science. Theaudience Offasec Includes Thosein The Formalmethods Community Who Have(orwouldliketodevelop)adeeper Interestinsecurity,andthoseinsecurity Who Would Like To Understand How Formal Methods Can Make Important Cont- Butions To Some Aspects Of Security. The Scope Of Fasec Is Deliberately Broad Andcoverstopics That Rangefrommodelling Securityrequirementsthroughsp- I?cation, Analysis, And Veri?cations Of Cryptographic Protocols To Certi?ed Code. The Discussions At Fasec 2002 Encompassed Many Aspects Of Security: From Theoretical Foundations Through Support Tools And On To Applications. Formal Methods Has Made A Substantial Contribution To This Exciting ?eld In The Past. Lifting Reference Monitors From The Kernel / F.b. Schneider -- Authenticity Types For Cryptographic Protocols / A. Gordon -- Verifying The Set Protocol: Overview / L.c. Paulson -- Interacting State Machines: A Stateful Approach To Proving Security / D. Von Oheimb. Ali E. Abdallah, Peter Ryan, Steve Schneider (eds.). Includes Bibliographical References And Index. Front Matter....Pages - Lifting Reference Monitors from the Kernel....Pages 1-2 Authenticity Types for Cryptographic Protocols....Pages 3-3 Verifying the SET Protocol: Overview....Pages 4-14 Interacting State Machines: A Stateful Approach to Proving Security....Pages 15-32 Automatic Approximation for the Verification of Cryptographic Protocols....Pages 33-48 Towards a Formal Specification of the Bellare-Rogaway Model for Protocol Analysis....Pages 49-61 Critical Critical Systems....Pages 62-70 Analysing Security Protocols....Pages 71-80 Analysis of Probabilistic Contract Signing....Pages 81-96 Security Analysis of (Un-) Fair Non-repudiation Protocols....Pages 97-114 Modeling Adversaries in a Logic for Security Protocol Analysis....Pages 115-132 Secure Self-certified Code for Java....Pages 133-151 Z Styles for Security Properties and Modern User Interfaces....Pages 152-166 Cryptographic Challenges: The Past and the Future....Pages 167-182 TAPS: The Last Few Slides....Pages 183-190 Formal Specification for Fast Automatic IDS Training....Pages 191-204 Using CSP to Detect Insertion and Evasion Possibilities within the Intrusion Detection Area....Pages 205-220 Revisiting Liveness Properties in the Context of Secure Systems....Pages 221-238 Back Matter....Pages -