三田ロジックセミナー 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.
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.