权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Formal Methods and Cryptography: The Next Generation of Abstractions (CryptoForma)

形式化方法和密码学：下一代抽象 (CryptoForma)

基本信息

批准号：
EP/G069875/1
负责人：
Eerke Boiten
金额：
$ 9.41万
依托单位：
University of Kent
依托单位国家：
英国
项目类别：
Research Grant
财政年份：
2009
资助国家：
英国
起止时间：
2009 至无数据
项目状态：
已结题

来源：
https://gtr.ukri.org/projects?ref=EP%2FG069875%2F1
关键词：
Formal Methods Cryptography Next Generation

项目摘要

The purpose of CryptoForma is to build an expanding network in computer science and mathematics to support the development of formal notations, methods and techniques for modelling and analysing modern cryptographic protocols. This work increases security and confidence in such protocols and their applications (e.g. in e-commerce and voting), to the benefit of protocol designers, businesses, governments, and application users.The United Kingdom has traditionally been a world leader in research into, and applications of, formal methods. Work in the UK on the foundations of languages and notations such as CSP, pi-calculus, and Z have led to their widespread use in critical systems development in industry.The UK is also well known to contain leading experts in cryptography. In the last two decades we have done important work in stream cipher design, symmetric ciphers (differential and algebraic cryptanalysis), elliptic curve cryptography, identity based cryptography and in protocols (e.g. in the mobile phone industry).In the 1990s in the UK, formal methods were successfully applied to the modelling and verification of security protocols at a high level of abstraction. However, modern cryptographic protocols contain probabilistic and complexity theoretic aspects which require a different set of abstractions. Several approaches for dealing with this have appeared since, including: automated proof-checking; compositional techniques; higher level proof structures; abstractions of computational models; and specialised logics.The network aims to bring together research groups working in the UK in these areas, starting with 7 sites and expanding rapidly from that.It will allow a systematic and effective cross-fertilisation between the differing strands of work. The consortium contains mathematicians and computer scientists, experts on cryptography, on formal methods, and on their interconnection, and developers of practical cryptographic protocols both from academia and from industry. A group with such a very broad spectrum of expertise will enable both(a) informing/strengthening practical developments by solid mathematical analysis, and (b) motivating foundational analysis by practice-based needs and requirements.To do so the network will organise meetings around both fundamental and more directly applicable issues, such as:- adequate abstractions of cryptographic primitives;- specialised specification notations with notions of probability, timing, and complexity;- abstract concepts and logics that allow the expression of security properties and reasoning about them;- practical protocols, e.g. e-voting, trust management, and those involving zero-knowledge proofs and commitments which formal methods cannot currently deal with.With these interests and questions in mind, the overall aims of CryptoForma are to:- bring together academics and industrialists interested in the application of formal methods to the specification, development and verification of cryptographic protocols;- stimulate collaboration between individuals and groups in order to tackle the questions highlighted above;- disseminate problems and results to researchers and practitioners in the field and to the wider communities in cryptography and formal methods.To achieve this research meetings and workshops are planned which will foster collaboration and disseminate key results.This proposal is timely and important because- society has recently experienced a reduced confidence in protection of electronic data, and in applications such ase-commerce and e-voting;- a critical mass of researchers in this area exists in the UK but this is not being exploited;- the subject is high on the agenda of research institutions, industries and academics world-wide. This is evidenced by the letters of support and the enthusiasm for the preliminary meeting of the network in January 2009 where all partners and 10 others will meet.

CryptoForma的目的是在计算机科学和数学领域建立一个不断扩展的网络，以支持用于建模和分析现代密码协议的正式符号、方法和技术的发展。这项工作增加了安全性和信心，在这样的协议和他们的应用程序（例如，在电子商务和投票），协议设计者，企业，政府和应用程序users.The英国的利益一直是世界领先的研究和应用，正式的方法。在英国，CSP、π演算和Z等语言和符号的基础工作使它们在工业关键系统开发中得到广泛应用。英国也以拥有密码学方面的领先专家而闻名。在过去的二十年里，我们做了重要的工作，在流密码设计，对称密码（差分和代数密码分析），椭圆曲线密码，基于身份的密码和协议（例如，在移动的电话行业）。在20世纪90年代在英国，形式化方法被成功地应用于建模和验证的安全协议在一个高层次的抽象。然而，现代密码协议包含概率和复杂性理论方面，需要一组不同的抽象。从那时起，出现了几种处理这种问题的方法，包括：自动校对;组合技术;更高层次的证明结构;计算模型的抽象;和专门的逻辑。该网络旨在将在英国从事这些领域工作的研究小组聚集在一起，从7个站点开始，并迅速扩大。它将允许不同工作链之间系统和有效的交叉施肥。该联盟包括数学家和计算机科学家，密码学专家，正式方法及其互连，以及来自学术界和工业界的实用密码协议开发人员。一个拥有如此广泛专业知识的小组将能够（a）通过坚实的数学分析来通知/加强实际发展，以及（B）通过基于实践的需求和要求来激励基础分析。为此，网络将围绕基本和更直接适用的问题组织会议，例如：- 具有概率、时间和复杂性概念的专门规范符号;-允许表达安全属性并对其进行推理的抽象概念和逻辑;- 实用的协议，例如电子投票，信任管理，以及那些涉及零知识证明和承诺的正式方法目前无法处理。考虑到这些利益和问题，CryptoForma的总体目标是：- 召集对应用正式方法来说明、发展和验证密码协议感兴趣的学者和工业家;-鼓励个人和团体之间的合作，以解决上述问题;- 向该领域的研究人员和从业人员以及密码学和正规方法的更广泛社区传播问题和结果。这项建议是及时和重要的，因为-社会最近对保护电子数据以及电子商务和电子投票等应用的信心有所下降;-英国在这一领域有大量研究人员，但没有得到利用;-这一主题是世界各地研究机构、工业界和学术界的重要议程。支持信和对2009年1月网络初步会议的热情证明了这一点，届时所有伙伴和其他10个伙伴将举行会议。