Network on Formal Methods and Cryptography: CryptoForma 2.

CryptoForma 2的目的是维持和扩展一个卓越的网络，以支持用于建模和分析现代密码协议的形式化符号、方法和技术的发展，并提高其在国内和国际上的知名度。该网络汇集了密码学家、安全协议开发人员和形式化方法社区，他们希望形式化、分析和验证这些协议。这项工作提高了这些协议及其应用程序的安全性和可信度，从而使协议设计者、企业、政府和应用程序用户受益。因此，通过促进通过网络传输和存储在设备和服务器中的信息安全性的研究，该网络将有助于RCUK全球不确定性，特别是网络安全的更广泛的研究议程。传统上，英国在正式方法的研究和应用方面一直处于世界领先地位。在英国，语言和符号（如CSP、pi-calculus和Z）的基础工作导致了它们在工业关键系统开发中的广泛应用。英国也以拥有顶尖的密码学专家而闻名。在过去的二十年里，英国在流密码设计、对称密码（微分和代数密码分析）、椭圆曲线密码、基于身份的密码、全同态加密和协议方面做了重要的工作。在20世纪90年代的英国，形式化方法被成功地应用于高层次抽象的安全协议的建模和验证。然而，现代密码协议包含概率和复杂性理论方面，需要不同的抽象。此后出现了许多处理这一问题的方法，包括：自动证明检查；组成技术;证明结构;计算模型的抽象；还有专门的逻辑。CryptoForma网络汇集了来自英国6个创始网站的研究小组，参加了来自其他8个英国网站和欧洲其他地方的会议。这项新提案旨在继续将英国的研究小组聚集在一起，旨在从其（现在的）12个站点进一步发展，并在国际上建立强大的形象和联系。它将继续在不同的工作领域之间进行系统和有效的相互促进。该联盟包括数学家和计算机科学家，密码学、形式化方法及其互连方面的专家，以及来自学术界和工业界的实用密码学协议的开发人员。一个拥有如此广泛专业知识的小组能够(A)通过数学分析告知/加强实际发展，以及(b)通过基于实践的需求和要求激励基础分析。为此，网络将围绕基本和更直接适用的问题组织会议，例如：加密原语，例如全同态加密；专门的规范符号；抽象的概念和逻辑，允许安全属性的表达和推理；实用协议，例如电子投票、云安全和访问控制。考虑到这些问题，CryptoForma 2的总体目标是：-将对形式化方法应用于加密协议的规范、开发和验证感兴趣的学者和实业家聚集在一起；-促进个人和团体之间以及与国际研究界的合作，以解决实际和基础研究问题；-向密码学和形式化方法领域的研究人员和实践者以及更广泛的社区传播问题和结果。为了实现这一目标，计划了各种研究会议和研讨会，这将促进合作和传播。

The purpose of CryptoForma 2 is to sustain and expand a network of excellence for supporting the development of formal notations, methods and techniques for modelling and analysing modern cryptographic protocols, and to increase its national and international profile. The network brings together cryptographers, developers of security protocols, and the formal methods community which looks to formalise, analyse, and verify such protocols. This work increases security and confidence in such protocols and their applications, to the benefit of protocol designers, businesses, governments, and application users. The network will thus contribute to the wider research agenda of RCUK Global Uncertainties and in particular Cyber Security, by stimulating research that increases security of information as it is transmitted through networks, and stored in appliances and servers.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 has 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 important work was done in the UK in stream cipher design, symmetric ciphers (differential and algebraic cryptanalysis), elliptic curve cryptography, identity based cryptography, full homomorphic encryption, and in protocols.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 different abstractions. Many approaches for dealing with this have appeared since, including: automated proof-checking; compositional techniques; proof structuring; abstractions of computational models; and specialised logics.The CryptoForma network brought together research groups in the UK from the 6 founding sites, with meetings attended from 8 other UK sites and elsewhere in Europe. This new proposal aims to continue to bring together research groups in the UK, aiming at further growth from its (now) 12 sites, and strong profiling and connections internationally. It will continue 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 broad spectrum of expertise enables both (a) informing/ strengthening practical developments by 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:cryptographic primitives, e.g. full homomorphic encryption;specialised specification notations;abstract concepts and logics that allow the expression of security properties and reasoning about them;practical protocols, e.g. for e-voting, cloud security, and access control.With these issues in mind, the overall aims of CryptoForma 2 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, and with the international research community, in order to tackle both practical and foundational research questions;- disseminate problems and results to researchers and practitioners in the field and to the wider communities in cryptography and formal methods.To achieve this a variety of research meetings and workshops are planned whichwill foster collaboration and dissemination.