Analysing Security and Privacy Properties

分析安全和隐私属性

• 批准号: EP/H005501/1
• 负责人: Mark Ryan
• 金额: $ 126.32万
• 依托单位: University of Birmingham
• 依托单位国家: 英国
• 项目类别: Fellowship
• 财政年份: 2010
• 资助国家: 英国
• 起止时间: 2010 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FH005501%2F1
• 关键词: Analysing; Security; Privacy; Properties

Security systems break because design practices focus too much on mechanisms, at the expense of clearly-defined properties. The vision of this research is to bring about a shift of emphasis to highlight the properties that security systems are expected to provide. This will be done by developing methods for verification of security systems. I will focus on a selection of interconnected real-world problems that are of great importance to society, but that are currently in need of greater industry/academe cooperation. The combination of fundamental research with close collaboration with industry, government and users is expected to achieve significant results and impact. I will develop and apply new methods and techniques to create and analyse solutions in three areas:* Trusted computing is an industry-led technology that aims to root security in hardware. Since its launch, academics including me have discovered significant issues that threaten to undermine its potential at providing a range of security benefits. This has arisen because industry does not have the expertise to analyse the protocols.* Electronic voting is an application currently attracting significant interest from government and industry, but numerous security issues have resulted in failure of confidence among politicians, commentators and public alike.* Privacy for citizens using electronic services is hotly debated by journalists and user groups and politicians, but has been substantially eroded by new technologies and policies.In these three areas, there is currently the risk of significant waste of resources on inappropriate or unaccepted technologies, resulting in user disempowerment and exclusion. The outcomes of this fellowship are intended to address that risk.A distinguishing feature of the proposal is the substantial engagement with industry and user groups that are active in these three areas. As a result of discussions with them, several organisations have committed significant resources, including cash contribution, manager and developer time, and access to users and experts.

安全系统的崩溃是因为设计实践过于关注机制，而牺牲了明确定义的属性。这项研究的愿景是实现重点的转移，以突出安全系统预计将提供的属性。这将通过制定核查安全系统的方法来实现。我将集中讨论一些对社会非常重要的相互关联的现实问题，但这些问题目前需要更大的行业/企业合作。基础研究与工业、政府和用户的密切合作相结合，有望取得重大成果和影响。我将开发和应用新的方法和技术来创建和分析三个领域的解决方案：* 可信计算是一种行业领先的技术，旨在将安全性植根于硬件。自推出以来，包括我在内的学者发现了一些重大问题，这些问题可能会破坏其提供一系列安全利益的潜力。之所以出现这种情况，是因为工业界没有分析协议的专门知识。电子投票是目前吸引政府和行业极大兴趣的应用，但众多安全问题导致政治家、评论员和公众对电子投票失去信心。使用电子服务的公民的隐私是记者、用户团体和政治家激烈辩论的问题，但新技术和新政策大大侵蚀了隐私，在这三个领域，目前存在着将大量资源浪费在不适当或不被接受的技术上的风险，导致用户丧失权力和被排斥。该研究金的成果旨在解决这一风险。该提案的一个显著特点是与活跃在这三个领域的行业和用户团体进行了实质性接触。经过与他们的讨论，一些组织已经承诺投入大量资源，包括现金捐款、管理人员和开发人员的时间，以及与用户和专家的接触。

项目成果

Analysis of privacy in mobile telephony systems

移动电话系统中的隐私分析

• DOI: 10.1007/s10207-016-0338-9
• 发表时间: 2016
• 期刊: International Journal of Information Security
• 影响因子: 3.2
• 作者: Arapinis M

StatVerif: Verification of Stateful Processes

StatVerif：状态进程的验证

• DOI: 10.1109/csf.2011.10
• 发表时间: 2011
• 作者: Arapinis M

Stateful applied pi calculus: Observational equivalence and labelled bisimilarity

有状态应用 pi 演算：观察等价性和标记的双相似性

• DOI: 10.1016/j.jlamp.2017.03.001
• 发表时间: 2017
• 期刊: Journal of Logical and Algebraic Methods in Programming
• 影响因子: 0.9
• 作者: Arapinis M