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

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