TACL Seminar Spring '03
Spring '03 Schedule
|Feb 24||Amal Ahmed||Reasoning about Hierarchical Storage||Abstract|
|Mar 24||Koji Hasebe - Keito Univ||A Logical Verification Method for Security Protocols Based on Linear Logic and BAN Logic||Abstract|
|Apr 7||Jay Ligatti||Run-time Policy Enforcement with Security Automata||Abstract|
Reasoning about Hierarchical Storage
In this paper, we develop a new substructural logic that can encode invariants necessary for reasoning about hierarchical storage. We show how the logic can be used to describe the layout of bits in a memory word, the layout of memory words in a region, the layout of regions in an address space, or even the layout of address spaces in a multiprocessing environment. We provide a semantics for our formulas and then apply the semantics and logic to the task of developing a type system for Mini-KAM, a simplified version of the abstract machine used in the ML Kit with regions.
This is joint work with Limin Jia and David Walker.
A Logical Verification Method for Security Protocols Based on Linear Logic and BAN Logic
A process following a security protocol is represented by a formal proof (of a fragment of linear logic based on the multiset rewriting model), modifying the idea by Cervesato-Durgin-Lincoln-Mitchell-Scedrov, while the (modified) BAN logic (which was first introduced by Burrows-Abadi-Needham) is used as an evaluation semantics on security-properties for processes.
By this method, we can get rid of the so called 'idealization' step in the verification procedure of the BAN framework. In particular, we classify BAN-style belief-inferences into two categories; the inferences which only require some syntactic structure of a process observed by a participant on one hand, and the inferences which require a participant's knowledge on the structure of a protocol and a certain honesty assumption. We call the latter the honesty inferences. We shall show how such honesty inferences are used in the evaluation semantics for the security verification. We also point out that the evaluation inferences on freshness of nonces/keys/messages are classified as in the first category but that some of such inferences lack the information how to evaluate due to the lack of a certain concrete time-constraint setting.
We introduce a natural time-constraint setting in our process/protocol descriptions and enrich the expressive power of the freshness evaluation.