============================================================================
WORKSHOP ON FOUNDATIONS FOR SECURE/SURVIVABLE SYSTEMS AND NETWORKS
January 25 and 26, 2001
Conference Hall in West 8 Building, Tokyo Institute of Technology
Tokyo, JAPAN
supported by
Secure Information Foundation Project
(安全な情報基盤)
A Grant-In-Aid for Scientific Research
(Ministry of Education, Culture, Sports, Science and Technology, Japan)
============================================================================
PROGRAM
============================================================================
January 25 (Thursday)
=====================
10:00-10:15 Opening
10:15-11:45
Security Protocol Analysis for Unicast and Multicast Using the
CAPSL Integrated Protocol Environment
Grit Denker (SRI International)
(Joint work with Jon Millen)
11:45-13:30 Lunch
13:30-14:30
Nonce Analysis and Strand Space Model:
Yet Another Reconsideration on Protocol Verification
Masami Hagiya (U. Tokyo),
Takamichi Saito (Sci. U. Tokyo),
Koichi Takahashi (ETL),
Yozo Toda (Chiba U.)
14:30-14:45 Break
14:45-16:15
How to Build an Insecure System
Drew Dean (Xerox PARC)
16:15-16:30 Break
16:30-17:30 Discussion
End of the first Day.
============================================================================
January 26 (Friday)
===================
10:00-11:30
STAT: An Extensible Intrusion Detection Framework
Giovanni Vigna, (UC Santa Barbara)
11:30-13:00 Lunch
13:00-14:00
PCC with CafeOBJ (Tentative)
Akira Mori and Kokichi Futatsugi (JAIST)
14:00-14:15 Break
14:15-15:15
Formal verification of security protocol
for parallel attacks on multiple sessions
Naoki Yonezaki (Tokyo Institute of Technology)
15:15-15:30 Break
15:30-17:00
Discussion on Secure/Certified Mail System
Chair: Etsuya Shibayama (Tokyo Institute of Technology)
End of the Workshop
============================================================================
Abstracts of Talks by Overseas Speakers
============================================================================
Security Protocol Analysis for Unicast and Multicast
Using the CAPSL Integrated Protocol Environment
Grit Denker, SRI International
(Joint work with Jon Millen)
ABSTRACT:
CAPSL, a Common Authentication Protocol Specification Language, is a
high-level language to support security analysis of cryptographic
authentication and key distribution protocols. The CAPSL Integrated
Protocol Environment provides parser, type checker and connectors to
analysis tools like the PVS theorem prover, and the model checkers
Athena and Maude. CAPSL employs an intermediate language, CIL, that
expresses state transitions with term-rewriting rules. Our experience
has shown that this is an appropriate representation easily adaptable
for many analysis tools. I will report on the current status of the
protocol environment. In particular I will address optimization issues
in the process of translating CAPSL to CIL in order to make analysis
feasible. I will also illustrate how connectors to formal analysis
tools can be designed and implemented using the existing support of
writing connectors in Java.
The current version of CAPSL is restricted to unicast protocols where
each message has a single addressee. We are currently investigating
extensions of CAPSL in order to handle group management
protocols. These protocols impose new challenges for modelling and
analysis techniques. Group management includes such activities as
enrolling and disenrolling group members, designating a leader and
changing that designation, distributing a common encryption key, and
achieving full or majority consensus. I will report on our first
results to extend CAPSL with powerful and elegant constructs for
expressing secure group multicast protocols.
======================================================================
How to Build an Insecure System
Drew Dean, Xerox PARC
ABSTRACT:
It is very difficult to build a secure system, and certainly something
impossible to cover in a single talk. However, certain approaches to
system design & implementation will inevitably lead to an insecure
system: failing to use cryptography where it's needed, not considering
availability, and failing to monitor deployed systems. With various
collaborators, I've been working in related areas, and I will discuss
our recent work to overcome these problematic subjects.
======================================================================
STAT: An Extensible Intrusion Detection Framework
Giovanni Vigna
http://www.cs.ucsb.edu/~vigna
University of California, Santa Barbara
ABSTRACT:
Although significant progress has been made towards securing computer
systems, the truth is that all computer systems are vulnerable to
abuse and attacks. To address this problem, intrusion detection
systems have been developed to detect malicious activities aimed at
violating the security of information systems. Originally, intrusion
detection systems were limited to hosts and their operating systems.
However, as networks have grown in importance, the focus of intrusion
detection systems has broadened accordingly, resulting in distributed
and network-based intrusion detection systems. Most systems, however,
still address a single domain -- either the hosts or the network --
and are tailored to a particular environment, such as a particular
operating system or platform. It is desirable to have a more
comprehensive approach that would be able to address both host-based
and network-based intrusion detection in a systematic and integrated
way. An intrusion detection system should also be easily ported to
different environments to address the heterogeneous nature of modern
computer networks.
This talk presents a suite of intrusion detection tools developed by
the Reliable Software Group at UCSB. The tool suite is based on the
State Transition Analysis Technique (STAT). The STAT approach is a
method to describe computer penetrations as sequences of actions that
cause transitions in the security state of a system. This general
approach has been extended and tailored to perform intrusion detection
in different domains and environments. The STAT-based intrusion
detection systems were developed following a framework-based approach,
and the resulting design uses a ``core'' module that embodies the
domain-independent characteristics of the STAT approach. This generic
core is then extended in a well-defined way to implement intrusion
detection systems for different domains and environments. The approach
supports reuse, portability, extendibility, and customization, and it
allows for the optimization of critical functionalities.
======================================================================
======================================================================