Joint Workshop on

Foundations of Computer Security,
Automated Reasoning for Security Protocol Analysis
Issues in the Theory of Security

Affiliated with LICS 2008 and CSF 21

Pittsburgh, PA, USA, June 21 (Saturday) and 22 (Sunday), 2008

Home. Invited Talks. Accepted Papers. Program. Location and additional information.

Background, aim and scope. Submission. Important dates. Publication. Audience. PC.

Pictures by Catalin Hritcu

Invited Talks

Accepted Papers


09:15 - 09:30 Welcome
Invited talk I Chair: Luca Viganò
09:30 - 10:30 What is Cryptographic Protocol Analysis?
Joshua Guttman
10:30 - 11:00 Coffee break
Session I Chair: Iliano Cervesato
11:00 - 11:30 A Note on First-order Logic and Security Protocols
Reynald Affeldt and Hubert Comon-Lundh
11:30 - 12:00 Active Intruders with Caps
Siva Anantharaman, Hai Lin, Christopher Lynch, Paliath Narendran and Michael Rusinowitch
12:00 - 12:30 Statically Detecting Message Confusions in a Multi-Protocol Setting
Chiara Bodei, Linda Brodo, Pierpaolo Degano and Han Gao
12:30 - 14:00 Lunch
Session II Chair: Veronique Cortier
14:00 - 14:30 Separating two roles of hashing in one-way message authentication
Long Nguyen and Bill Roscoe
14:30 - 15:00 Using Elyjah to Analyse Java Implementations of Cryptographic Protocols
Nicholas O'Shea
15:00 - 15:30 MultiTrust: An Authorization Framework with Customizable Distributed Proof Construction
Charles Zhang and Marianne Winslett
15:30 - 16:00 Coffee break
Session III Chair: David Basin
16:00 - 16:30 Testing Decision Procedures for Security-by-Contract
Nataliia Bielova, Fabio Massacci and Ida Sri Rejeki Siahaan
16:30 - 17:00 On Secure Distributed Implementations of Dynamic Access Control
Avik Chaudhuri
17:00 - 17:30 Analysing Object-Capability Security
Toby Murray
Invited talk II Chair: Sandro Etalle
09:30 - 10:30 On the Evolution of Adversary Models in Cryptographic Protocols (Part II: the Fragility of Adversary Definitions)
Invited Talk by Virgil Gligor
10:30 - 11:00 Coffee break
Session IV Chair: Cedric Fournet
11:00 - 11:30 Type-checking Zero-knowledge
Michael Backes, Catalin Hritcu and Matteo Maffei
11:30 - 12:00 Computationally Sound Symbolic Anonymity of a Ring Signature
Yusuke Kawamoto, Hideki Sakurada and Masami Hagiya
12:00 - 12:30 Automated Proofs for Asymmetric Encryption
Pascal Lafourcade, Cristian Ene, Yassine Lakhnech, Judicaël Courant and Marion Daubignard
12:30 - 14:00 Lunch
Session V Chair: Cathy Meadows
14:00 - 14:30 Chaining Secure Channels
Christopher Dilloway
14:30 - 15:00 Certificates for Tree Automata Completion
Roberto Zunino
15:00 - 15:30 A Logic for Reasoning about Networked Secure Systems
Deepak Garg, Jason Franklin, Dilsun Kaynar and Anupam Datta
15:30 - 16:00 Coffee break
16:00 - 18:00 WG 1.7 business meeting
18:30 - Workshop dinner

The workshop dinner on Sunday (June 22) will be at the Monterey Bay Fish Grotto, one of Pittsburgh's nicer restaurants with a great view of downtown Pittsburgh and the three rivers. Since the restaurant is several miles from campus, we have arranged for buses to take us from the workshop location to the restaurant and back. The buses will be departing campus at 6:30pm and returning around 9:30pm. There is no extra fee for the dinner or transportation (i.e., the costs are covered by the workshop).

We hope everyone will be able to attend the dinner. If you know that you won't be able to make it, however, we'd appreciate it if you could tell us.

Location and additional information

The workshop will take place at Newell Simon Hall 1305. A campus map is available at the local information page of LICS 2008.
Further information about registration, travel, and venue can be found at the websites of LICS 2008 and CSF 21.

Background, aim and scope

Computer security is an established field of computer science of both theoretical and practical significance. In recent years, there has been increasing interest in logic-based foundations for various methods in computer security, including the formal specification, analysis and design of security protocols and their applications, the formal definition of various aspects of security such as access control mechanisms, mobile code security and denial-of-service attacks, and the modeling of information flow and its application to confidentiality policies, system composition, and covert channel analysis.

WITS is the official annual workshop organised by the IFIP WG 1.7 on "Theoretical Foundations of Security Analysis and Design", established to promote the investigation on the theoretical foundations of security, discovering and promoting new areas of application of theoretical techniques in computer security and supporting the systematic use of formal techniques in the development of security related applications. This is the eighth meeting in the series.
The workshop FCS continues a tradition, initiated with the Workshops on Formal Methods and Security Protocols (FMSP) in 1998 and 1999, then with the Workshop on Formal Methods and Computer Security (FMCS) in 2000, and finally with the LICS satellite Workshop on Foundations of Computer Security (FCS) in 2002 through 2005, of bringing together the formal methods and the security communities.
ARSPA is a series of workshops on Automated Reasoning for Security Protocol Analysis, bringing together researchers and practitioners from both the security and the formal methods communities, from academia and industry, who are working on developing and applying automated reasoning techniques and tools for the formal specification and analysis of security protocols. The first two ARSPA workshops were held as satellite events of the 2nd International Joint Conference on Automated Reasoning (IJCAR'04) and of the 32nd International Colloquium on Automata, Languages and Programming (ICALP'05), respectively.
FCS and ARSPA have been joining forces since 2006: FCS-ARSPA'06 was affiliated with LICS'06, in the context of FLoC'06, and FCS-ARSPA'07 was affiliated with LICS'07 and ICALP'07.

The aim of the joint workshop FCS-ARSPA-WITS'08 is to provide a forum for continued activity in different areas of computer security, bringing computer security researchers in closer contact with the LICS community and giving LICS attendees an opportunity to talk to experts in computer security, on the one hand, and contribute to bridging the gap between logical methods and computer security foundations, on the other.

We are interested both in new results in theories of computer security and also in more exploratory presentations that examine open questions and raise fundamental concerns about existing theories, as well as in new results on developing and applying automated reasoning techniques and tools for the formal specification and analysis of security protocols. We thus solicit submissions of papers both on mature work and on work in progress.
Possible topics include, but are not limited to:
Automated reasoning techniques
Composition issues
Formal specification
Foundations of verification
Information flow analysis
Language-based security
Logic-based design
Program transformation
Security models
Static analysis
Statistical methods
Trust management
for Access control and resource usage control
Availability and denial of service
Covert channels
Integrity and privacy
Intrusion detection
Malicious code
Mobile code
Mutual distrust
Security policies
Security protocols
All submissions will be peer-reviewed. Authors of accepted papers must guarantee that their paper will be presented at the workshop.


Submissions should be at most 15 pages (a4paper, 11pt), including references. The cover page should include title, names of authors, co-ordinates of the corresponding author, an abstract, and a list of keywords. Submissions that are clearly too long may be rejected immediately. Additional material intended for the referees but not for publication in the final version - for example details of proofs - may be placed in a clearly marked appendix that is not included in the page limit.
Authors are invited to submit their papers electronically, as portable document format (pdf) or postscript (ps); please, do not send files formatted for work processing packages (e.g., Microsoft Word or Wordperfect files).

The only mechanism for paper submissions is via the

electronic submission web-site
powered by easychair. Please, follow the instructions given there.

Important dates

Papers due: April 10, 2008 (extended)
Notification of acceptance: May 16, 2008
Final papers: June 01, 2008


Informal proceedings will be made available in electronic format and they will be distributed to all participants of the workshop.

Moreover, workshop participants will be invited to submit full versions of their papers to a special issue of the Journal of Automated Reasoning, which will be open also to non-participants, in all cases with fresh reviewing.


Participation to the workshop will be open to anybody willing to register.

Program Committee

Last modified: Mon May 8 10:27:24 CEST 2006