============================================================================
2nd INTERNATIONAL WORKSHOP
ON
FOUNDATIONS FOR SECURE/SURVIVABLE SYSTEMS AND NETWORKS
October 26th (Fri), 27th (Sat), 2001
Conference Hall in West 8(E) Building , Tokyo Institute of Technology
Tokyo, Japan
supported by
Secure Information Foundation Project,
A Grant-In-Aid for Scientific Research
and
JSPS-NSF joint project on
the Logical Methods for Formal Verification of Software
Organizers:
Kokichi Futatsugi kokichi@jaist.ac.jp
Mitsu Okada mitsu@abelard.flet.mita.keio.ac.jp
Andre Scedrov scedrov@saul.cis.upenn.edu
Naoki Yonezaki yonezaki@fmx.cs.titech.ac.jp
============================================================================
PROGRAM
============================================================================
October 26 (Friday)
=====================
10:00-10:20 Opening
Aki Yonezawa (the leader of SIFP) and Organizers
10:20-12:10
-- Private Authentication
by Martin Abadi abadi@cs.ucsc.edu
-- Authentication Protocol based on Timing of Binding
by Takamichi Saito saito@yu.is.noda.sut.ac.jp
Masami Hagiya hagiya@is.s.u-tokyo.ac.jp
Fumio Mizoguchi mizo@ia.noda.sut.ac.jp
-- Defining anonymity
by Vitaly Shmatikov shmat@CS.Stanford.EDU
12:10-14:00 Lunch
14:00-15:50
-- Encoding Generic Judgments
by Dale Miller dale@cse.psu.edu
-- Checking/Verifying Safety with Behavioral Specifications
by Akira Mori amori@carc.aist.go.jp
Kazuhiro Ogata ogata@jaist.ac.jp
Kokichi Futatsugi kokichi@jaist.ac.jp
-- Constraint-Solving for Cryptographic Protocol Analysis
by Jon Millen millen@csl.sri.com
15:50-16:10 break
16:10-17:20
-- The Impact of Synchronisation on Secure Information Flow in
Concurrent Programs
by Andrei Sabelfeld andrei@cs.chalmers.se
-- Logical Verifications of Timed Multiset Rewritings for
Real-Time Systems and for Security Protocols with Time-Stamps,
by Mitsu Okada mitsu@abelard.flet.keio.ac.jp
Koji Hasebe @abelard.flet.keio.ac.jp
17:20-17:50 Discussions for the first Day
End of the First Day
============================================================================
October 27 (Saturday)
=====================
10:00 Start of the Second Day
10:00-11:10
-- CCured: Type Safe Retrofitting of Legacy Code
by George Necula necula@eecs.berkeley.edu
-- Resource Usage Analysis
by Atsushi Igarashi igarashi@graco.c.u-tokyo.ac.jp
Naoki Kobayashi kobayasi@kb.cs.titech.ac.jp
11:10-11:20 break
11:20-12:30
-- A Heap Bounded Assembly Language
by Adriana Compagnoni abc@cs.stevens-tech.edu
-- Fail-Safe C: [ A talk from Prof. Yonezawa's Group of U.Tokyo ]
12:30-14:00 Lunch
14:00-15:50
-- Abstract Specification of Crypto-Protocols and their Attack
Models
by Iliano Cervesato iliano@itd.nrl.navy.mil
-- [ A talk from Prof. Yonezaki's Group of Titech ]
-- A probabilistic polynomial-time calculus for analysis of
cryptographic protocols
by Andre Scedrov scedrov@cis.upenn.edu
15:50-16:10 break
16:10-17:00 Discussions for the workshop
End of the Workshop
============================================================================
Abstracts of the Talks
============================================================================
Private Authentication
Martin Abadi abadi@cs.ucsc.edu
Frequently, communication between two principals reveals their
identities and presence to third parties. These privacy breaches can
occur even if security protocols are in use; indeed, they may even be
caused by security protocols. However, with some care, security
protocols can provide authentication for principals that wish to
communicate while protecting them from monitoring by third parties.
This talk discusses the problem of private authentication and presents
two protocols for private authentication of mobile principals. In
particular, the protocols allow two mobile principals to communicate
when they meet at a location if they wish to do so, without the danger
of tracking by third parties. The protocols do not make the (dubious)
assumption that the principals share a long-term secret or that they
get help from an infrastructure of ubiquitous on-line authorities.
==============================================================================
Authentication Protocol based on Timing of Binding
Takamichi Saito saito@yu.is.noda.sut.ac.jp
Masami Hagiya hagiya@is.s.u-tokyo.ac.jp
Fumio Mizoguchi mizo@ia.noda.sut.ac.jp
In this paper, we discuss authentication protocols using public-key
cryptography. When initiator and responder communicate securely, they
authenticate each other and exchange a session key. There are lots of
authentication protocols for this purpose. However, some protocols
may have critical flaw. Therefore, we provide requirements and
framework for secure authentication protocol, and design some
protocols derived from the framework. Moreover, we introduce the
concept of late binding, which is based on timing of binding in a
protocol. Finally, we propose some protocols based on the binding,
and check the safty of the protocols by the requirements.
============================================================================
Defining anonymity
Vitaly Shmatikov shmat@CS.Stanford.EDU
It is widely recognized that anonymity and privacy are important
properties of communication protocols. There is, however, no
universally accepted definition of what it means for a protocol to be
"anonymous". Protocol designers employ different notions of
anonymity, resulting in incompatible and misunderstood protocols. In
my talk, I will give uniform, precise definitions of several anonymity
and privacy properties. The definitions are formally expressed as
observational equivalences between processes and enable formal
verification of anonymity.
============================================================================
Encoding Generic Judgments
Dale Miller dale@cse.psu.edu
Specifications of operational semantics in programming languages or of
symbolic specifications for security aspects in protocols often
require handling abstractions that arise from name restriction, bound
variables, and nonces. As is well known, various syntactic details of
such specifications can be greatly simplified by using a meta-logic
that incorporates term-level abstractions (lambda-abstraction) and
proof-level abstractions (eigenvariables). We shall attempt to extend
this specification setting to include the problem of specifying not
only relations capturing operational semantics, such as one-step
evaluation, but also properties and relations about the semantics,
such as simulation. Central to our approach is the encoding of generic
object-level judgments (universally quantified formulas) as suitable
atomic meta-level judgments. We shall encode both the one-step
transition semantics and simulation of (finite) pi-calculus to
illustrate our approach.
==============================================================================
Checking/Verifying Safety with Behavioral Specifications
Akira Mori amori@carc.aist.go.jp
Kazuhiro Ogata ogata@jaist.ac.jp
Kokichi Futatsugi kokichi@jaist.ac.jp
Checking/verifying safety properties has became important in many
application areas, and it is desirable to check/verify the properties
in the abstraction level which is close to applications. CafeOBJ is
the first algebraic specification language which incorporates
behavioral/observational specifications. Behavioral/observational
specifications can be considered to express specifications close to
the application level. In this talk, we present several techniques
which can check/verify safety properties based on behavioral
/observational specifications.
============================================================================
Constraint-Solving for Cryptographic Protocol Analysis
Jon Millen millen@csl.sri.com
The reachability problem for cryptographic protocols with non-atomic
keys can be solved via a simple constraint satisfaction procedure.
==============================================================================
The Impact of Synchronisation on Secure Information Flow in Concurrent
Programs
Andrei Sabelfeld andrei@cs.chalmers.se
The issue of secure information flow in programs has become especially
important with the growing popularity of mobile code and networked
information systems. For distributed programming, the use of
multi-threaded programming languages has become extremely popular.
However, in the setting of a shared-memory multi-threaded language,
little has been done in treating secure programming with
synchronisation. Because synchronisation is fundamental to concurrent
programs, it is highly desirable to have a robust security
specification and tools that aid in the design of secure programs with
synchronisation. To fill this gap, this talk presents a compositional
timing-sensitive confidentiality specification for multi-threaded
programs with synchronisation and proposes a type-based analysis
improving on previous approaches to reject insecure programs.
==============================================================================
Logical Verifications of Timed Multiset Rewritings for
Real-Time Systems and for Security Protocols with Time-Stamps,
Mitsu Okada mitsu@abelard.flet.keio.ac.jp
Koji Hasebe @abelard.flet.keio.ac.jp
A framework of timed multiset rewritings can be used for formal
specifications of some type of dynamic real-time systems and of some
type of security protocols with time-stamps. We study verification
problems in this framework, with the help of linear logic techniques.
In particular, we analyze conditions on decidability and
semi-decidability of some verification problems in this framework and
present our on-going research on their applications to verifications
of real-time systems and of security protocols with time-stamps.
============================================================================
CCured: Type Safe Retrofitting of Legacy Code
George Necula necula@eecs.berkeley.edu
In this talk we describe a scheme that combines program analysis and
run-time checking to bring type safety to existing C programs by
trading off some performance.
We describe the CCured type system that extends that of C by
separating pointer types according to their usage. This type system
allows both pointers whose usage can be verified statically to be type
safe and pointers whose safety must be checked at run time. We prove a
type soundness result and then present a surprisingly simple type
inference algorithm that is able to infer the appropriate pointer
kinds for existing C programs. Our experience with the CCured system
shows that the inference is extremely effective for most C programs
and is able to infer that 60-100% of the pointers are used
safely. Using CCured we have discovered array out-of-bounds errors in
established C programs such as the SPEC95 benchmarks {\tt go} and {\tt
compress}, in contexts in which purely dynamic-checking tools such as
Purify would not be effective.
==============================================================================
Resource Usage Analysis
Atsushi Igarashi igarashi@graco.c.u-tokyo.ac.jp
Naoki Kobayashi kobayasi@kb.cs.titech.ac.jp
It is an important criterion of program correctness that a program
accesses resources in a valid manner. For example, a memory region
that has been allocated should be eventually deallocated, and after
the deallocation, the region should no longer be accessed. A file that
has been opened should be eventually closed. So far, most of the
methods to analyze this kind of property have been proposed in rather
specific contexts (like studies of memory management and verification
of usage of lock primitives), and it was not so clear what is the
essence of those methods or how methods proposed for individual
problems are related. To remedy this situation, we formalize a general
problem of analyzing resource usage as a resource usage analysis
problem, and propose a type-based method as a solution to the problem.
============================================================================
A Heap Bounded Assembly Language
Adriana Compagnoni abc@cs.stevens-tech.edu
The pioneering work of Necula and Lee on Proof-Carrying Code motivated
recent developments in typed intermediate languages and typed assembly
languages that enforce various security policies during code
execution.
In this talk we present ongoing joint work with David Aspinall on the
development of a typed assembly language for safe memory space reuse,
to be used in a Proof Carrying Code environment.
We present a typed assembly language, HBAL, which has a type system
with features for managing space usage. In contrast to other typed
assembly languages, HBAL allows memory areas to be reused for values
of differing types. We ensure type safety by using a type system with
linearity constraints to prevent aliasing of heap locations, together
with special pseudo-instructions for altering types at isolated points
in the code. The reuse discipline is controlled by compilation from a
high-level language, and we demonstrate a compilation from a
prototypical first-order functional language, LFPL, due to Hofmann.
==============================================================================
Fail-Safe C: [ A talk from Prof. Yonezawa's Group of U.Tokyo ]
============================================================================
Abstract Specification of Crypto-Protocols and their Attack Models
Iliano Cervesato iliano@itd.nrl.navy.mil
We undertake a detailed examination of the familiar Dolev-Yao
abstraction of cryptographic protocols. We concentrate on the
specification of the often neglected issue of what data can be
accessed by which principal. Given these premises, we extend our
study to the related notion of the Dolev-Yao intruder, an abstraction
underlying most successes in protocol analysis. We prove that the
Dolev-Yao intruder can emulate the actions of an arbitrary attacker
that operates within the boundaries of the Dolev-Yao model. We show
that there is no such thing as a universal Dolev-Yao intruder, but
that its allowable capabilities depends on the protocol at hand and
that, furthermore, they can be automatically generated from the
protocol's data access policy. Finally, we hint at the possibility of
inferring the rules that govern data access from a sufficiently
detailed specification of a protocol and the operations it relies on.
As an example, we use MSR throughout, a strongly typed specification
framework for security protocols based on multiset rewriting.
Further reading: papers dated 2001 in
http://www.cs.stanford.edu/~iliano/byYear.html
http://www.cs.stanford.edu/~iliano/forthcoming.html
==============================================================================
[ A talk from Prof. Yonezaki's Group of Titech ]
============================================================================
A probabilistic polynomial-time calculus for analysis of cryptographic
protocols
Andre Scedrov scedrov@cis.upenn.edu
We describe properties of a process calculus that has been developed
for the purpose of analyzing security protocols. The process calculus
is a restricted form of pi-calculus, with bounded replication and
probabilistic polynomial-time expressions allowed in messages and
boolean tests. In order to avoid problems expressing security in the
presence of nondeterminism, messages are scheduled probabilistically
instead of nondeterministically. We prove that evaluation may be
completed in probabilistic polynomial time and develop properties of a
form of asymptotic protocol equivalence that allows security to be
specified using observational equivalence, a standard relation from
programming language theory that involves quantifying over possible
environments that might interact with the protocol. We also relate
process equivalence to cryptographic concepts such as pseudo-random
number generators and polynomial-time statistical tests. The work has
been carried out in collaboration with P. Lincoln, J. Mitchell,
M. Mitchell, A. Ramanathan, and V. Teague.
==============================================================================