三田ロジックセミナー John Mitchell教授，Anupam Datta教授講演会 (4月10日) のお知らせ |
CosyProofs09 の機会に来日されたスタンフォード大学の John Mitchell 氏と カーネギーメロン大学の Anupam Datta 氏を迎えて次のようなテーマのセミナーと 討論会を開催いたします． (それぞれの講演のアブストラクトを下に添付しています．) 参加は自由(無料，登録不要)ですので，興味をお持ちの方はお気軽にご参加下さい．
なお，seminar についてのお問い合わせは security at abelard.flet.keio.ac.jp へ御連絡下さい．
コーディネータ: 杉本雄太郎，中山茂之 (慶應義塾大学文学部哲学専攻岡田光弘研究室）
Network security protocols are simple distribute programs that exchange data between separate computers on the network. Protocols that exchange cryptographic keys are notoriously difficult to design and debug. This talk will summarize two logical methods for analyzing and verifying protocols and discuss some case studies carried out over the past several years. One method is a relatively simple automated finite-state approach that has been used by our research group, others, and several years of students in a project course at Stanford to find flaws and develop improvements in a wide range of protocols and security mechanisms. The second method, Protocol Composition Logic (PCL), is a way of reasoning about protocols that is designed to make it possible to prove security properties of large practical protocols. The two methods are complementary, since the first method can find errors, but only the second is suitable for proving correctness.
Organizations, such as businesses, non-profits, government agencies, hospitals, banks, and universities, collect and use personal information from a range of sources, shared with specific expectations about how it will be managed and used. Accordingly, they must find ways to comply with expectations, which may be complex and varied, as well as with relevant privacy laws and regulations, while they minimize operational risk and carry out core functions of the organization efficiently and effectively.
In this talk, I will report on a principled approach for expressing and enforcing privacy policies in complex organizational processes. The starting point of our work is "contextual integrity", a conceptual framework for understanding privacy expectations and their implications developed in the literature on law, public policy, and political philosophy. We formalize some aspects of contextual integrity in a logical framework for expressing norms of transmission of personal information. The technical approach is based on temporal logic with semantics defined over concurrent game structures. In comparison with access control and privacy policy frameworks such as RBAC, EPAL, and P3P, these norms focus on who personal information is about, how it is transmitted, and past and future actions by both the subject and the users of the information. Our logic is expressive enough to capture naturally many notions of privacy found in legislation, including those found in HIPAA, COPPA, and GLBA. In addition to privacy, we formalize a notion of "utility" that captures the goals of the organization, e.g. since a hospital’s goal is to provide health care, certain flows of personal information are necessary. We also develop automated support for policy compliance, audit, and policy analysis.
While contextual integrity and its formalization focuses on personal information about individuals, privacy policies also refer to aggregate or anonymized information about groups of individuals. I will describe some of our ongoing work on integrating database privacy concepts into formal policy models and languages. Specifically, I will report on our experiences with formalizing and lifting differential privacy (a promising recent approach to database privacy) to reactive organizational processes.
This document was translated from LATEX by HEVEA.