We present a framework in which different notions of security can be defined in a uniform and modular way. Each definition of security is formalized as a security predicate by ass...
Schneider's work on rank functions [14] provides a formal approach to verification of certain properties of a security protocol. However, he illustrates the approach only wit...
We propose an approach to support confidentiality for mobile implementations of security-sensitive protocols using Java/JVM. An applet which receives and passes on confidential in...
We consider the problem of assembling concurrent software systems from untrusted or partially trusted o -the-shelf components, using wrapper programs to encapsulate components and...
In this paper we develop a language of mobile agents called uPLAN for describing the capabilities of active (programmable) networks. We use a formal semantics for uPLAN to demonst...
A type flaw attack on a security protocol is an attack where a field that was originally intended to have one type is subsequently interpreted as having another type. A number o...
One protocol (called the primary protocol) is independent of other protocols (jointly called the secondary protocol) if the question whether the primary protocol achieves a securi...
Some of the non interference properties studied in [4, 6, 18] for information flow analysis in computer systems, notably Æ , are reformulated here in a realtime setting. This is...
We analyze the notion of “local names” in SPKI/SDSI. By interpreting local names as distributed groups, we develop a simple logic program for SPKI/SDSI’s linked localname sc...
In this paper we present an improved logic for analysing authentication properties of cryptographic protocols, based on the SVO logic of Syverson and van Oorschot. Such logics are...