Creating and sharing knowledge for telecommunications

Modeling and Analyzing Security in the Presence of Compromising Adversaries


on 26-02-2010

... Cas Cremers (ETH Zurich).

February 26, 2010, Friday, 16h15m.

Abstract: We present a framework for modeling adversaries in security protocol analysis, in which we define a hierarchy of adversary models. These
models range from a Dolev-Yao style adversary to more powerful adversaries who can reveal different parts of principals' states during protocol
execution. Our adversary models unify and generalize many existing security notions from both the computational and symbolic settings and lead to new, previously unexplored security notions. We extend an existing symbolic protocol-verification tool with our adversary models. This is the first tool
that systematically supports notions such as weak perfect forward secrecy, key compromise impersonation, and adversaries capable of state-reveal queries. In extensive case studies, we automatically find new attacks and rediscover known attacks that previously required detailed manual analysis.
Joint work with David Basin.

Location: Room P3.10, Mathematics Building.

http://people.inf.ethz.ch/cremersc/index.html More Information..

Reasoning about the Consequences of Authorization Policies in a Linear Epistemic Logic.


on 25-02-2010

... Frank Pfenning (Carnegie Mellon University, USA).

Note excepcional week day, time and location. Joint session with the Information Security Seminar.

February 25, 2010, Thursday, 18h.

Abstract: Authorization policies are not stand-alone objects: they are used to selectively permit actions that change the state of a system. Thus, it is desirable to have a framework for reasoning about the semantic consequences of policies. To this end, we extend a rewriting interpretation of linear logic with connectives for modeling affirmation, knowledge, and possession. To cleanly confine semantic effects to the rewrite sequence, we introduce a monad. The result is a richly expressive logic that elegantly integrates policies and their effects. After presenting this logic and its metatheory, we demonstrate its utility by proving properties that relate a simple file system's policies to their semantic consequences. [This talk represents joint work with Henry DeYoung]
More Information..