I went to the Cryptology ePrint Archive and searched for papers with the word "provable" in either the title, abstract or key-words; the search returned about 80 papers. I then looked at the abstracts of the first 50 papers in that list, and for each paper I extracted a sentence or two that best represent in my eyes the "provable security" claims made in that abstract.

The list below is what I found. As you can see, in pretty much all cases the provable-security claims are quite accurate, rather technical, and very far from being hyped (in fact I find most to be quite nerdy). I do not think that even one of them can be called a "marketing ploy". Similarly, I did not see a tendency to "take the models too seriously". But don't take my word for it, read the list below and judge for yourselves.

-- Shai

- The end result is that we bring provable security in the realm of password-authenticated key exchange one step closer to practical.
- This paper deals with setting up a security framework for mobile networks and argues that in the context of mobility, composability is an essential security feature.
- Security proofs are invaluable tools in assuring protocol implementers about the security properties of protocols. We note, however, that many existing security proofs of previously published identity-based protocols entail lengthy and complicated mathematical proofs. In this paper, our proof adopts a modular approach and, hence, simpler to follow.
- We show that hardness of average-case complexity of the underlying problem is irrelevant in collision search by presenting a linearization method that can be used to produce collisions in a matter of seconds on a desktop PC for the variant of FSB with claimed $2^128$ security.
- To the best of our knowledge this is the first paper which aims to combine the paradigm of provable security in the cryptographic sense with the task of information aggregation in WSNs.
- We take a close look at Kerberos' encryption and confirm that most of the options in the current version provably provide privacy and authenticity, some with slight modification that we suggest.
- The NAKE protocol is provably secure in CK security model, thus it inherits the corresponding security attributes in CK security model.
- We introduce a model for {\em provable data possession} ($\pdp$) that allows a client that has stored data at an untrusted server to verify that the server possesses the original data without retrieving it. [...] We present two provably-secure $\pdp$ schemes that are more efficient than previous solutions, even when compared with schemes that achieve weaker guarantees.
- Proofs are given to show that the proposed protocol is secure against forging and chosen message attacks in the case of without actually running a dictionary attack.
- The main contribution of this paper is in determining, by proof or counterexample, which of these seven notions is preserved by each of eleven existing iterations.
- At last, we give formal proofs for this new improved Generalized Signcryption in our attacking model.
- In this paper two new and general concepts, named "relevant anonymity" and "relevant security", are defined. Based-upon these concepts some general results on anonymity in public-key encryption are proved [...]
- Moreover, we present a simple and intuitive proof that CMQV is secure in the LaMacchia-Lauter-Mityagin model.
- We prove that our scheme meets chosen ciphertext security in the random oracle model, assuming the intractability of a modified version of the Bilinear Diffie-Hellman (\textsf{BDH}) problem.
- Using the proof technique of signature unforgeability against adaptive chosen-message attack, our protocol fully supports Session-Key Reveal queries and partially supports Session-State Reveal queries (which leaks ephemeral secret and keying material for session key derivation), without gap assumption or any unrealistic restriction.
- Our constructions use as a building block any provably-secure hierarchical key assignment scheme without temporal constraints and exhibit a tradeoff among the amount of private information held by each class, the amount of public data, the complexity of key derivation, and the computational assumption on which their security is based.
- In this paper we design and analyze hierarchical key assignment schemes which are provably-secure and support dynamic updates to the hierarchy with local changes to the public information and without requiring any private information to be re-distributed.
- We present the first two provably secure protocols for this problem in the standard model under the DDH assumption;
- We investigate the security properties of "isotropic channels", broadcast media in which a receiver cannot reliably determine whether a message originated from any particular sender and a sender cannot reliably direct a message away from any particular receiver.
- We prove its semantic security and unforgeability under the Gap Diffie-Hellman problem assumption in the random oracle model.
- We propose a full security notion and give efficient implementations meeting this notion under different pairing-related assumptions, both in the random oracle model and in the standard model.
- Our observation is that all provably-secure constant-round GKE protocols providing forward secrecy thus far are not fully scalable, but have a computational complexity that scales only linearly in group size. Motivated by this observation, we propose a new GKE protocol that not only offers full scalability in all directions but also attains provable security against active adversaries.
- This paper examines methods for formally proving the security of cryptographic schemes.
- We discuss the question of how to interpret reduction arguments in cryptography. We give some examples to show the subtlety and difficulty of this question.
- These appear to be the first constructions for time-bound hierarchical key assignment schemes which are simultaneously practical and provably-secure.
- We apply metareductions that show if such reductions existed, then RSA-OAEP would be OW-CCA2 insecure, or even worse, that the RSA problem would solvable. Therefore, it seems unlikely that such reductions could exist.
- We suggest that key-wrap's goal is security in the sense of deterministic authenticated-encryption (DAE), a notion that we put forward.
- To bring theory closer to practice, we present a simple modification to the proof of security by Fischlin and Schnorr of an RSA-based PRG, which shows that one can obtain an RSA-based PRG which outputs $\Omega(n)$ bits per multiply and has provable pseudorandomness security assuming the hardness of a well-studied variant of the RSA inversion problem, where a constant fraction of the plaintext bits are given.
- Formal models that allow one to understand side-channel attacks and are also directly meaningful to practice have been an open question. Motivated by this challenge, this work proposes a practice oriented framework for the analysis of cryptographic implementations against such attacks.
- Our work includes a developed security model of time capsule signature, a novel way of construction based on the bipartite ring signature, which is proven secure in the random oracle model and a concrete realization of the scheme.
- In this paper, we examine the notion of ``reforgeability'' for MACs. We first give a definition for this new notion, then examine some of the most widely-used and well-known MACs under our definition.
- We present a 2-round group key agreement protocol that can be proven secure in the random oracle model if a certain group-theoretical problem is hard. The security proof builds on a framework of Bresson et al., and explicitly addresses some issues concerning malicious insiders and also forward secrecy.
- We introduce a framework for reasoning about this question. [...] We introduce the notion of substitution-friendly protocols and show that such protocols remain secure after substitution in our framework.
- We examine the popular proof models for group key establishment of Bresson et al. and point out missing security properties that are present in some models for two-party key establishment. [...] Next to giving a formal definition of these extended security properties, we prove a variant of the explored proposal from ASIACRYPT 2004 secure in this stricter sense.
- Our scheme does not rely on the availability of globally verifiable signatures or arbitrary point-to-point connections, and its security against active adversaries is proven in the standard model under the Decision Diffie Hellman assumption.
- Proofs are invaluable tools in assuring protocol implementers about the security properties of protocols. However, several instances of undetected flaws in the proofs of protocols (resulting in flawed protocols) undermine the credibility of provably-secure protocols. In this work, we examine several protocols with claimed proofs of security [...] Using these protocols as case studies, we reveal previously unpublished flaws in these protocols and their proofs. We hope our analysis will enable similar mistakes to be avoided in the future.
- Provable security of a block cipher against differential/linear cryptanalysis is based on the \emph{maximum expected differential/linear probability} (MEDP/MELP) over $T \geq 2$ core rounds. [...] We show that the \emph{exact} value of the 2-round MEDP/MELP for the AES is equal to the best known lower bound: $53/2^{34} \approx 1.656 \times 2^{-29}$/ $109,953,193/2^{54} \approx 1.638 \times 2^{-28}$.
- We formally prove that the scheme is unforgeable, in the random oracle model, assuming that the Computational co-Diffie-Hellman problem is hard to solve.
- Title: Provable Efficient Certificateless Public Key Encryption
- We apply this theory to the Cramer-Shoup hybrid scheme acting on fixed length messages and deduce that the Cramer-Shoup scheme is plaintext-aware in the standard model.
- This work is intended to build confidence in the security of the Sakai-Kasahara IBE scheme. [...] We then prove that SK-IBE has chosen ciphertext security in the random oracle model based on a reasonably well-explored hardness assumption.
* We present a fully symmetric constant round authenticated group key agreement protocol in dynamic scenario. Our proposed scheme achieves forward secrecy and is provably secure under DDH assumption in the security model of Bresson {\em et al.} providing, we feel, better security guarantee than previously published results.
- We introduce VSH, {\em very smooth hash}, a new $S$-bit hash function that is provably collision-resistant assuming the hardness of finding nontrivial modular square roots of very smooth numbers modulo an $S$-bit composite.
- We prove that the original scheme is existentially unforgeable under adaptive chosen message attack. Moreover, we present an improved version which has three advantages: It is provably forward secure. [...]
- We present a provably secure tree based authenticated group key agreement protocol in dynamic scenario. [...] We prove that our protocol is provably secure in the standard security model of Bresson et al.
- In this work we point out that there is a flawed step in the security reduction exhibited by the authors. Fortunately, it is possible to fix it without changing the scheme or the underlying assumption.
- A security model with precise and formal definitions is presented, and an RSA-based efficient and provably secure verifiable probabilistic signature scheme is proposed.
- In this paper, we present an attack on the aggregate-signature-based proxy signature schemes, then point out there are two flaws in BPW notion of security for proxy signature. [...] We construct a new proxy signature scheme and prove that it is secure against existentially forgery on adaptively chosen-message attacks and adaptively chosen-warrant attacks under the random oracle model.
- We establish that the SDHP is almost as hard as the associated discrete logarithm problem. We do this by giving a reduction that shows that if the SDHP can be solved then the associated private key can be found.
- In this paper, we propose a new scheme that achieves the best performance of previous schemes and is provably secure under a comprehensive security model.
- This paper proposes a new scheme for partially blind signature based on the difficulty in solving the discrete logarithm problem. Under the assumption of the generic model, random oracle model, and intractable ROS-problem, this paper formally proves that the proposed scheme is secure against one-more signature forgery under the adaptively parallel attack.