International Association for Cryptologic Research

International Association
for Cryptologic Research

IACR News

Updates on the COVID-19 situation are on the Announcement channel.

Here you can see all recent updates to the IACR webpage. These updates are also available:

RSS symbol icon
via RSS feed
Twitter bird icon
via Twitter
Weibo icon
via Weibo
Facebook icon
via Facebook

24 September 2023

Marc Fischlin, Felix Rohrbach
ePrint Report ePrint Report
Extremely Lossy Functions (ELFs) are families of functions that, depending on the choice during key generation, either operate in injective mode or instead have only a polynomial image size. The choice of the mode is indistinguishable to an outsider. ELFs were introduced by Zhandry (Crypto 2016) and have been shown to be very useful in replacing random oracles in a number of applications.

One open question is to determine the minimal assumption needed to instantiate ELFs. While all constructions of ELFs depend on some form of exponentially-secure public-key primitive, it was conjectured that exponentially-secure secret-key primitives, such as one-way functions, hash functions or one-way product functions, might be sufficient to build ELFs. In this work we answer this conjecture mostly negative: We show that no primitive, which can be derived from a random oracle (which includes all secret-key primitives mentioned above), is enough to construct even moderately lossy functions in a black-box manner. However, we also show that (extremely) lossy functions themselves do not imply public-key cryptography, leaving open the option to build ELFs from some intermediate primitive between the classical categories of secret-key and public-key cryptography.
Expand
Sara Logsdon
ePrint Report ePrint Report
This paper offers a mathematical introduction to fully homomorphic encryption, a concept that enables computation on encrypted data. We trace the historical development of FHE, describe Fully Homomorphic Encryption over the Torus (TFHE) and how it performs certain mathematical operations, and explore bootstrapping and the possibility for adjusting computational depth. This paper equips readers with a brief understanding of FHE's evolution and the essential mechanisms facilitating practical implementation.
Expand
Roman Langrehr
ePrint Report ePrint Report
Non-interactive key exchange (NIKE) schemes like the Diffie-Hellman key exchange are a widespread building block in several cryptographic protocols. Since the Diffie-Hellman key exchange is not post-quantum secure, it is important to investigate post-quantum alternatives.

We analyze the security of the LWE-based NIKE by Ding et al. (ePrint 2012) and Peikert (PQCrypt 2014) in a multi-user setting where the same public key is used to generate shared keys with multiple other users. The Diffie-Hellman key exchange achieves this security notion. The mentioned LWE-based NIKE scheme comes with an inherent correctness error (Guo et al., PKC 2020), and this has significant implications for the multi-user security, necessitating a closer examination.

Single-user security generically implies multi-user security when all users generate their keys honestly for NIKE schemes with negligible correctness error. However, the LWE-based NIKE requires a super-polynomial modulus to achieve a negligible correctness error, which makes the scheme less efficient. We show that - generically, single-user security does not imply multi-user security when the correctness error is non-negligible, but despite this - the LWE-based NIKE with polynomial modulus is multi-user secure for honest users when the number of users is fixed in advance. This result takes advantage of the leakage-resilience properties of LWE.

We then turn to a stronger model of multi-user security that allows adversarially generated public keys. For this model, we consider a variant of the LWE-based NIKE where each public key is equipped with a NIZKPoK of the secret key. Adding NIZKPoKs is a standard technique for this stronger model and Hesse et al. (Crypto 2018) showed that this is sufficient to achieve security in the stronger multi-user security model for perfectly correct NIKEs (which the LWE-based NIKE is not). We show that - for certain parameters that include all parameters with polynomial modulus, the LWE-based NIKE can be efficiently attacked with adversarially generated public keys, despite the use of NIZKPoKs, but - for suitable parameters (that require a super-polynomial modulus), this security notion is achieved by the LWE-based NIKE with NIZKPoKs. This stronger security notion has been previously achieved for LWE-based NIKE only in the QROM, while all our results are in the standard model.
Expand
Calvin Abou Haidar, Alain Passelègue, Damien Stehlé
ePrint Report ePrint Report
Updatable public key encryption has recently been introduced as a solution to achieve forward-security in the context of secure group messaging without hurting efficiency, but so far, no efficient lattice-based instantiation of this primitive is known.

In this work, we construct the first LWE-based UPKE scheme with polynomial modulus-to-noise rate, which is CPA-secure in the standard model. At the core of our security analysis is a generalized reduction from the standard LWE problem to (a stronger version of) the Extended LWE problem. We further extend our construction to achieve stronger security notions by proposing two generic transforms. Our first transform allows to obtain CCA security in the random oracle model and adapts the Fujisaki-Okamoto transform to the UPKE setting. Our second transform allows to achieve security against malicious updates by adding a NIZK argument in the update mechanism. In the process, we also introduce the notion of Updatable Key Encapsulation Mechanism (UKEM), as the updatable variant of KEMs. Overall, we obtain a CCA-secure UKEM in the random oracle model whose ciphertext sizes are of the same order of magnitude as that of CRYSTALS-Kyber.
Expand

21 September 2023

Aurel Page, Benjamin Wesolowski
ePrint Report ePrint Report
The supersingular Endomorphism Ring problem is the following: given a supersingular elliptic curve, compute all of its endomorphisms. The presumed hardness of this problem is foundational for isogeny-based cryptography. The One Endomorphism problem only asks to find a single non-scalar endomorphism. We prove that these two problems are equivalent, under probabilistic polynomial time reductions.

We prove a number of consequences. First, assuming the hardness of the endomorphism ring problem, the Charles–Goren–Lauter hash function is collision resistant, and the SQIsign identification protocol is sound. Second, the endomorphism ring problem is equivalent to the problem of computing arbitrary isogenies between supersingular elliptic curves, a result previously known only for isogenies of smooth degree. Third, there exists an unconditional probabilistic algorithm to solve the endomorphism ring problem in time $\tilde O(p^{1/2})$, a result that previously required to assume the generalized Riemann hypothesis.

To prove our main result, we introduce a flexible framework for the study of isogeny graphs with additional information. We prove a general and easy-to-use rapid mixing theorem.
Expand
Nina Bindel, Nicolas Gama, Sandra Guasch, Eyal Ronen
ePrint Report ePrint Report
FIDO2 is currently the main initiative for passwordless authentication in web servers. It mandates the use of secure hardware authenticators to protect the authentication protocol’s secrets from compromise. However, to ensure that only secure authenticators are being used, web servers need a method to attest their properties. The FIDO2 specifications allow for authenticators and web servers to choose between different attestation modes to prove the characteristics of an authenticator, however the properties of most these modes have not been analysed in the context of FIDO2. In this work, we analyse the security and privacy properties of FIDO2 when different attestation modes included in the standard are used, and show that they lack good balance between security, privacy and revocation of corrupted devices. For example, the basic attestation mode prevents remote servers from tracing user’s actions across different services while requiring reduced trust assumptions. However in case one device is compromised, all the devices from the same batch (e.g., of the same brand or model) need to be recalled, which can be quite complex (and arguably impractical) in consumer scenarios. As a consequence we suggest a new attestation mode based on the recently proposed TokenWeaver, which provides more convenient mechanisms for revoking a single token while maintaining user privacy.
Expand
Kaiyi Zhang, Qingju Wang, Yu Yu, Chun Guo, Hongrui Cui
ePrint Report ePrint Report
Picnic is a NIST PQC Round 3 Alternate signature candidate that builds upon symmetric primitives following the MPC-in-the-head paradigm. Recently, researchers have been exploring more secure/efficient signature schemes from conservative one-way functions based on AES, or new low complexity one-way functions like Rain (CCS 2022) and AIM (CCS 2023). The signature schemes based on Rain and AIM are currently the most efficient among MPC-in-the-head-based schemes, making them promising post-quantum digital signature candidates.

However, the exact hardness of these new one-way functions deserves further study and scrutiny. This work presents algebraic attacks on RAIN and AIM for certain instances, where one-round Rain can be compromised in $2^{n/2}$ for security parameter $n\in \{128,192,256\}$, and two-round Rain can be broken in $2^{120.3}$, $2^{180.4}$, and $2^{243.1}$ encryptions, respectively. Additionally, we demonstrate an attack on AIM-III (which aims at 192-bit security) with a complexity of $2^{186.5}$ encryptions. These attacks exploit the algebraic structure of the power function over fields with characteristic 2, which provides potential insights into the algebraic structures of some symmetric primitives and thus might be of independent interest.
Expand
David Jacquemin, Anisha Mukherjee, Ahmet Can Mert, Sujoy Sinha Roy
ePrint Report ePrint Report
The long running time of isogeny-based cryptographic constructions has proved to be a boon in disguise for one particular type of primitive called Verifiable Delay Functions (VDFs). VDFs are characterised by sequential function evaluation but an immediate output verification. In order to ensure secure use of VDFs in real-world applications, it is important to determine the fastest implementation. Considering the point of view of an attacker (say with unbounded resources), this paper aims to achieve the fastest possible hardware implementation of isogeny-based VDFs. It is the first work that implements the $2^T$-isogeny walk involved in the evaluation step of an isogeny VDF. To meet our goal, we use redundant representations of integers and introduce a new lookup table-based algorithm for modular reduction. We also provide a survey of elliptic curve arithmetic to arrive at the most cost-effective curve computations and propose an improvement of the point doubling algorithm for better parallelism. The evaluation step of a VDF is defined to be sequential, which means that there is limited scope for parallelism. Nevertheless, taking this constraint into account our proposed design targets the highest levels of parallelism possible on an architectural level of an isogeny VDF implementation. We provide detailed analysis of all our arithmetic modules as well as estimates for their critical path delays and area consumption. Our 28nm ASIC design computes a $4^{100} = 2^{200}$-isogeny in 7.1$\mu s$. It is the first high-performance ASIC implementation for evaluation of isogeny VDFs.
Expand
Ronan Lashermes, Hélène Le Bouder
ePrint Report ePrint Report
We introduce a novel side-channel-based reverse engineering technique capable of reconstructing a procedure solely from inputs, outputs, and traces of execution. Beyond generic restrictions, we do not assume any prior knowledge of the procedure or the chip it operates on. These restrictions confine our analysis to 8-bit RISC constant-time software implementations.

Specifically, we demonstrate the feasibility of reconstructing a symmetric cryptographic cipher, even in scenarios where traces are sampled with information loss and noise, such as when measuring the power consumption of the chip.
Expand
EURECOM; Sophia Antipolis, France
Job Posting Job Posting
EURECOM is seeking a highly motivated and talented PhD student to join our research team under the supervision of Prof. Antonio Faonio. The selected candidate will work on a challenging and innovative research project focused on zero-knowledge proofs (ZKPs) and their applications in cloud scenarios. The primary objectives of this position are to advance the state-of-the-art in ZKPs, with a particular emphasis on zkSNARKs, and to explore novel applications of such protocols.

Closing date for applications:

Contact: Antonio Faonio

More information: https://www.eurecom.fr/en/job/zero-knowledge-proofs

Expand
NUS-Singapore and the University of Sheffield, UK
Job Posting Job Posting
NUS-Singapore is seeking a highly motivated PhD candidate in the field of cyber security with an emphasis on embedded and hardware security. Candidates with experience in one or more of the following are preferred: PUF, lightweight cryptography, post-quantum cryptography; designing novel cryptographic primitives and protocols; digital design on ASIC or FPGA platforms using hardware description languages; computer architectures and embedded software; side-channel analysis and fault attacks; and machine learning and artificial intelligence especially for security applications. Research topics include but are not limited to Physical unclonable function (PUF) secure cryptographic implementations in hardware and software; mechanisms against side-channel analysis and fault attacks security and privacy for IoT systems; post-quantum cryptography; In the first instance, candidates can discuss applications with Dr. Prosanta Gope via email (p.gope@sheffield.ac.uk). Who can Apply? (i) You should possess a strong research background, evidenced by accomplishments like publications in reputable research venues. (ii) You should exhibit high levels of motivation.

Closing date for applications:

Contact: Dr Prosanta Gope (p.gope@sheffield.ac.uk)

Expand
University of Luxembourg, Esch-sur-Alzette, Luxembourg
Job Posting Job Posting

The CryptoLux group of the University of Luxembourg has a vacancy for a post-doctoral researcher in the area of security/privacy of blockchains and smart contracts. The successful candidate will contribute to a research project entitled Advanced Cryptography for Finance and Privacy (CryptoFin), which is funded by the Fonds National de la Recherche (FNR). Starting in September 2023, CryptoFin will run over a period of 3 years and be carried out in collaboration with the cryptography teams of Stanford University and Ethereum foundation. The mission of the CryptoFin project is to develop innovative solutions for some of the most pressing research problems in the blockchain domain, especially in the context of layer-2 protocols for off-chain transactions and the design of advanced cryptographic techniques like verifiable delay functions, proof-of-X systems with special features, and new MPC/SNARK-friendly primitives.

Candidates must hold a Ph.D. degree in cryptography, IT security, or a related field. Preference will be given to candidates with a strong publication record that includes at least one paper at an IACR conference/workshop or one of the top-4 security conferences. Experience in blockchains and/or smart contracts is a plus. Candidates with an interest to conduct research in one of the following areas are particularly encouraged to apply:

  • Applied cryptography (especially design/analysis of symmetric cryptosystems)
  • Cryptofinance and cryptoeconomics
  • Privacy and anonymity on the Internet

The position is initially offered for 1 year, but an extension by 2 years is possible. The University of Luxembourg offers excellent working conditions and a highly competitive salary. Interested candidates are invited to send their application by email to Prof. Alex Biryukov before October 15, 2023 (early submission is encouraged). The application material should contain a cover letter explaining the candidate's research interests, a CV (incl. photo), a list of publications, scans of diploma certificates, and contact details of 3 references.

Closing date for applications:

Contact: Prof. Alex Biryukov (alex.biryukov@uni.lu)

Expand
AIT Austrian Institute of Technology; Vienna, Austria
Job Posting Job Posting
AIT is Austria's largest non-universitary research institute. Its Cyber Security team focuses on various aspects of security, including anomaly detection, cyber ranges, penetration testing, and cryptography. The cryptography group is conducting research in various directions, including secure communication, privacy-enhancing technologies, and long-term and post-quantum security. The group seeks to grow and thus has a vacancy for a researcher in related areas.

Requirements:
  • PhD degree in Computer Science, Cyber Security, or a related field, with a specialization on cryptology
  • Profound knowledge in (public key) cryptography, including, e.g., federated computation, long-term and post-quantum secure communication, privacy-enhancing technologies, real-world crypto, zero-knowledge proofs and zkSNARKs
  • Strong track record with publications at competitive academic conferences or journals (e.g., Crypto, Eurocrypt, Asiacrypt, TCC, PKC, CCS, S&P, USENIX, ESORICS, ...)
  • Experience in the acquisition and execution of national and transnational research projects (e.g., H2020) is a plus
  • Good knowledge of a programming language (e.g., C/C++, Rust, Java, Python) and software development is a plus
  • Very good written and oral English skills; knowledge of German is not a requirement but willingness to learn German is expected
The salary starts from ~61k€/year, depending on experience. The review process will begin immediately and will continue open until the position has been filled.

Please submit your application including CV, cover letter, full list of publications, and contact details of at least 2 references via email to: stephan.krenn[at]ait.ac.at

Closing date for applications:

Contact: Stephan Krenn; stephan.krenn[at]ait.ac.at

Expand
University of Birmingham, UK
Job Posting Job Posting

This is an exciting opportunity to join the University of Birmingham’s Centre for Cyber Security and Privacy on the EPSRC funded project "IOTEE: Securing and analysing trusted execution beyond the CPU", led by Prof Oswald and Prof Ryan.

Trusted Execution Environments (TEEs) allow users to run their software in a secure enclave while assuring the integrity and confidentiality of data and applications. However, cloud computing these days relies heavily on peripherals (connected through PCIe) such as GPUs and FPGAs. In this project, together with researchers at the University of Southampton, we will thoroughly evaluate the security guarantees of the new TEE support in the PCIe standard. This could involve the use of formal modelling, as well as researching various software and hardware attacks and countermeasures against them.

We are looking for a person with a PhD in cyber security/computer science/electrical engineering. The candidate must have experience areas such as embedded security, binary analysis, physical attacks such as side-channel analysis and fault injection, and/or formal modelling. This needs to be evidenced through publications in highly ranked conferences/journals in the field. We also welcome experience in writing system level or low-level code in programming languages such as C, C++, or Rust.

The successful candidate will be employed on a full-time, fixed-term contract up to August 2026. Full-time starting salary is normally in the range £33,348 to £43,155. (Some) remote work is possible, depending on the circumstances. The University provides a range of employee benefits, as well as opportunities for career development and training. The project includes substantial funding for conference travel and equipment.

The post-doc will be working in the Centre for Cyber Security and Privacy, which currently has 14 permanent academics as well as 21 postdocs/PhD students.

The application deadline is 12 Oct 2023. Applications have to be made online at: https://edzz.fa.em3.oraclecloud.com/hcmUI/CandidateExperience/en/sites/CX_6001/job/2681/

Closing date for applications:

Contact: Informal enquiries can be made to David Oswald d.f.oswald@bham.ac.uk.

More information: https://edzz.fa.em3.oraclecloud.com/hcmUI/CandidateExperience/en/sites/CX_6001/job/2681/

Expand
Paderborn University, Department of Computer Science, Paderborn, Germany
Job Posting Job Posting
With the Institute for Photonic Quantum Systems (PhoQS), Paderborn University wants to establish an international research centre in the field of photonic quantum technologies. The aim is to develop new technologies for photon-based quantum applications as well as new theoretical and experimental concepts and research approaches. Ultimately, the focus is on understanding and controlling photonic quantum simulators and quantum computers.

Postdoc (f/m/d) (salary is according to E13 TV-L)

A position with 100 % of the regular working hours is available as of the next possible date. The employment is initially limited to three years and is based on the legal regulations of the Wissen-schaftszeitvertragsgesetzes (WissZeitVG).

Your duties and responsibilities:
• Establishment and expansion of an infrastructure for the integration of quantum computing in high-performance computing.
• Interface of PhoQS to the Paderborn Center for Parallel Computing (PC2) of the Paderborn University
• Supporting users, especially in the natural sciences, in the development and implementation of quantum algorithms
• Optimisation of quantum software platforms for photonic and gate-based quantum computing such as Strawberry Fields, Parceval or Qiskit in collaboration with HPC experts of the PC2
• Organisation and delivery of tutorials and workshops on the use of quantum software plat-forms (basic to advanced)
• Leading a team for the technical integration of quantum computing and high-performance computing

Hiring requirements:
• Completed PhD in computer science, mathematics or physics or comparable qualification
• Solid understanding of many-body quantum mechanics
• Practical experience in high-performance computing and/or in the use of quantum software platforms
• High motivation and willingness for interdisciplinary cooperation between computer science and physics
• Good knowledge of German and English, both written and spoken
• Friendliness, flexibility, ability to work in a team, initiative and willingness to work independently

Closing date for applications:

Contact: Please send your application including a CV (preferably in a single pdf file) using the Ref. No. 6105 by 30th September, 2023 to: bloemer@upb.de

More information: https://cs.uni-paderborn.de/en/cuk

Expand

18 September 2023

Omer Paneth, Rafael Pass
ePrint Report ePrint Report
Non-interactive delegation schemes enable producing succinct proofs (that can be efficiently verified) that a machine $M$ transitions from $c_1$ to $c_2$ in a certain number of deterministic steps. We here consider the problem of efficiently \emph{merging} such proofs: given a proof $\Pi_1$ that $M$ transitions from $c_1$ to $c_2$, and a proof $\Pi_2$ that $M$ transitions from $c_2$ to $c_3$, can these proofs be efficiently merged into a single short proof (of roughly the same size as the original proofs) that $M$ transitions from $c_1$ to $c_3$? To date, the only known constructions of such a mergeable delegation scheme rely on strong non-falsifiable ``knowledge extraction" assumptions. In this work, we present a provably secure construction based on the standard LWE assumption.

As an application of mergeable delegation, we obtain a construction of incrementally verifiable computation (IVC) (with polylogarithmic length proofs) for any (unbounded) polynomial number of steps based on LWE; as far as we know, this is the first such construction based on any falsifiable (as opposed to knowledge-extraction) assumption. The central building block that we rely on, and construct based on LWE, is a rate-1 batch argument (BARG): this is a non-interactive argument for NP that enables proving $k$ NP statements $x_1,..., x_k$ with communication/verifier complexity $m+o(m)$, where $m$ is the length of one witness. Rate-1 BARGs are particularly useful as they can be recursively composed a super-constant number of times.
Expand
Prashant Agrawal, Kabir Tomer, Abhinav Nakarmi, Mahabir Prasad Jhanwar, Subodh Sharma, Subhashis Banerjee
ePrint Report ePrint Report
In this paper we address the problem of recovery from failures without re-running entire elections when elections fail to verify. We consider the setting of $\textit{dual voting}$ protocols, where the cryptographic guarantees of end-to-end verifiable voting (E2E-V) are combined with the simplicity of audit using voter-verified paper records (VVPR). We first consider the design requirements of such a system and then suggest a protocol called $\textit{OpenVoting}$, which identifies a verifiable subset of error-free votes consistent with the VVPRs, and the polling booths corresponding to the votes that fail to verify with possible reasons for the failures.
Expand
Yi Liu, Junzuo Lai, Qi Wang, Xianrui Qin, Anjia Yang, Jian Weng
ePrint Report ePrint Report
Protocols with \emph{publicly verifiable covert (PVC) security} offer high efficiency and an appealing feature: a covert party may deviate from the protocol, but with a probability (\eg $90\%$, referred to as the \emph{deterrence factor}), the honest party can identify this deviation and expose it using a publicly verifiable certificate. These protocols are particularly suitable for practical applications involving reputation-conscious parties.

However, in the cases where misbehavior goes undetected (\eg with a probability of $10\%$), \emph{no security guarantee is provided for the honest party}, potentially resulting in a complete loss of input privacy and output correctness.

In this paper, we tackle this critical problem by presenting a highly effective solution. We introduce and formally define an enhanced notion called \emph{robust PVC security}, such that even if the misbehavior remains undetected, the malicious party can only gain an additional $1$-bit of information about the honest party's input while maintaining the correctness of the output. We propose a novel approach leveraging \emph{dual execution} and \emph{time-lock puzzles} to design a robust PVC-secure two-party protocol with \emph{low overhead} (depending on the deterrence factor). For instance, with a deterrence factor of $90\%$, our robust PVC-secure protocol incurs \emph{only additional ${\sim}10\%$ overhead} compared to the state-of-the-art PVC-secure protocol.

Given the stronger security guarantees with low overhead, our protocol is highly suitable for practical applications of secure two-party computation.
Expand
Zhenzhen Bao, Jinyu Lu, Yiran Yao, Liu Zhang
ePrint Report ePrint Report
In CRYPTO 2019, Gohr showed that well-trained neural networks could perform cryptanalytic distinguishing tasks superior to differential distribution table (DDT)-based distinguishers. This suggests that the differential-neural distinguisher (ND) may use additional information besides pure ciphertext differences. However, the explicit knowledge beyond differential distribution is still unclear. In this work, we provide explicit rules that can be used alongside DDTs to enhance the effectiveness of distinguishers compared to pure DDT-based distinguishers. These rules are based on strong correlations between bit values in right pairs of XOR-differential propagation through addition modulo $2^n$. Interestingly, they can be closely linked to the earlier study of the multi-bit constraints and the recent study of the fixed-key differential probability. In contrast, combining these rules does not improve the NDs' performance. This suggests that these rules or their equivalent form have already been exploited by NDs, highlighting the power of neural networks in cryptanalysis. In addition, we find that to enhance the differential-neural distinguisher's accuracy and the number of rounds, regulating the differential propagation is imperative. Introducing differences into the keys is typically believed to help eliminate differences in encryption states, resulting in stronger differential propagations. However, differential-neural attacks differ from traditional ones as they don't specify output differences or follow a single differential trail. This questions the usefulness of introducing differences in a key in differential-neural attacks and the resistance of Speck against such attacks in the related-key setting. This work shows that the power of differential-neural cryptanalysis in the related-key setting can exceed that in the single-key setting by successfully conducting a 14-round key recovery attack on Speck32/64.
Expand
Théophile Wallez, Jonathan Protzenko, Karthikeyan Bhargavan
ePrint Report ePrint Report
Data formats used for cryptographic inputs have historically been the source of many attacks on cryptographic protocols, but their security guarantees remain poorly studied. One reason is that, due to their low-level nature, formats often fall outside of the security model. Another reason is that studying all of the uses of all of the formats within one protocol is too difficult to do by hand, and requires a comprehensive, automated framework.

We propose a new framework, “Comparse”, that specifically tackles the security analysis of data formats in cryptographic protocols. Comparse forces the protocol analyst to systematically think about data formats, formalize them precisely, and show that they enjoy strong enough properties to guarantee the security of the protocol.

Our methodology is developed in three steps. First, we introduce a high-level cryptographic API that lifts the traditional game-based cryptographic assumptions over bitstrings to work over high-level messages, using formats. This allows us to derive the conditions that secure formats must obey in order for their usage to be secure. Second, equipped with these security criteria, we implement a framework for specifying and verifying secure formats in the F* proof assistant. Our approach is based on format combinators, which enable compositional and modular proofs. In many cases, we relieve the user of having to write those combinators by hand, using compile-time term synthesis via Meta-F*. Finally, we show that our F* implementation can replace the symbolic notion of message formats previously implemented in the DY* protocol analysis framework. Our newer, bit-level precise accounting of formats closes the modeling gap, and allows DY* to reason about concrete messages and identify protocol flaws that it was previously oblivious to.

We evaluate Comparse over several classic and real-world protocols. Our largest case studies use Comparse to formalize and provide security proofs for the formats used in TLS 1.3, as well as upcoming protocols like MLS and Compact TLS 1.3 (cTLS), providing confidence and feedback in the design of these protocols.
Expand
◄ Previous Next ►