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

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

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.