Network on Formal Methods and Cryptography: CryptoForma 2.

形式化方法和密码学网络：CryptoForma 2。

基本信息

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

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

项目摘要

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.

Cryptoforma 2的目的是维持和扩展一个卓越网络，以支持形式的符号，方法和技术建模和分析现代密码协议，并提高其国家和国际知名度。该网络汇集了密码学家，安全协议的开发者以及旨在正式化，分析和验证此类协议的正式方法社区。这项工作提高了对此类协议及其应用程序的安全性和信心，从而使协议设计师，企业，政府和应用程序用户受益。因此，该网络将通过刺激通过网络传输并存储在设备和服务器中的信息的研究来提高RCUK全球不确定性，尤其是网络安全的更广泛的研究议程。英国一直是研究和应用程序领域的世界领导者。在英国为CSP，PI-Calculus和Z等语言和符号的基础工作，导致它们在行业关键系统开发中广泛使用。英国也众所周知，涵盖了密码学领域的领先专家。在过去的二十年中，重要的工作是在英国进行的，以对称密码设计（差分和代数密码分析），椭圆曲线密码学，基于身份的加密编制，完全同质的加密，以及在1990年代的1990年代，正式方法成功地应用于模型的确定性，在1990年代，正式的方法已成功地应用了buld buld，在1990年代，在1990年代，在1990年代，在1990年代，在1990年代，在1990年代，在英国进行了良好的确定，但是，现代的加密协议包含需要不同抽象的概率和复杂性理论方面。此后出现了许多处理此问题的方法，包括：自动化检查；组成技术；证明结构；计算模型的抽象；和专业的逻辑。该网络网络将英国6个创始站点的研究小组聚集在一起，并参加了来自其他8个英国网站和欧洲其他地方的会议。这项新的提案旨在继续将英国的研究小组汇集在一起，旨在从其（现在）的12个地点进一步增长，并在国际上进行了牢固的分析和联系。它将继续在不同的工作链之间进行系统性有效的交叉施用。该财团包含数学家和计算机科学家，密码学专家，有关正式方法及其互连的专家，以及来自学术界和行业的实用加密协议的开发商。具有如此广泛专业知识的团队可以通过数学分析来告知/加强实践发展，以及（b）通过基于实践的需求和要求来激励基础分析。这样做，网络将在基本和更直接的问题上组织会议，例如：加密原始人，例如：e.g。完整的同态加密；专门的规范符号；抽象概念和逻辑，允许表达安全性属性和有关它们的推理；实际协议，例如为了进行电子投票，云安全和访问控制。考虑到这些问题，隐型型2的总体目的是： - 将学者和工业家汇集在一起，对将正式方法应用于附加，开发和验证密码方案的规范，开发和验证；与个人和团体之间的合作以及与国际研究社区之间的合作，以解决练习和界定的问题； - 以解决方案的态度；对于加密和正式方法的更广泛的社区，为了实现这一目标，计划了各种研究会议和讲习班，这将促进合作和传播。