VU Amsterdam Logo

THE IPDL PROVER

This work is supported by NGI Zero Core, a fund established by NLnet with financial support from the European Commission's Next Generation Internet program.

NLnet foundation logo NGI Zero Logo

The IPDL Prover is a tool for composable simulation-based security proofs for distributed message-passing cryptographic protocols such as Multi-Party Computation (MPC). The proofs follow the style of Universal Composability (UC): we prove that a protocol is secure by showing that it is computationally indistinguishable from an idealization composed with a simulator. We establish the indistinguishability by equational reasoning as sequence of rewrite steps. These steps are sound with respect to a low-level computational semantics for IPDL protocols in terms of Turing Machines (see our latest paper).

The IPDL framework delivers concrete security bounds on the probability that an adversary can subvert the cryptographic mechanism employed by the protocol. For each indistinguishability assumption (such as the Decisional Diffie-Hellman assumption), the tool tracks two parameters: count counts the number of times the assumption has been invoked, and context is the maximum size of the protocol context in which the assumption has been invoked, where size refers to the number of symbols needed to encode the protocol on a Turing Machine tape. Our main result uses the count and context parameters to derive the final bound on the probability that the adversary will distinguish the protocol from its idealization (plus the simulator).

Installation

This software is under development; please use it at your own risk. Comments and bug reports welcome.

IPDL is an open-source project, with the sources available at the IPDL GitHub repository.

We use Maude 3.5 patched with a bugfix that has not been yet included in the main distribution of Maude, therefore we provided Maude as an archive.

In the folder IPDL-Spex of the repository, run

unzip -d maude Maude-linux.zip
export MAUDE_LIB=./maude/:./IPDL-Spex/lib:./IPDL-Spex/src

To run the examples, do

maude/maude -no-banner -allow-files run-SpeX

then at the resulting prompt enter

load dhke-otp.ipdl or load auth-to-secure.ipdl or load coin-toss.ipdl

Note that the latter is a strict equality proof and therefore no bounds are displayed.

To run the multi-party GWM case study, do

maude/maude -no-banner -allow-files BaseGMWN.maude run-SpeX

then load GMW-N.ipdl

We have tested these steps on Ubuntu Linux 24.04.

Case Studies

"Hello World" Example

In our simplest example, the IPDL Hello World analogue, Alice receives a Boolean message, encodes it by xor-ing it with a randomly generated Boolean, and leaks the encoding to the adversary. We show that this is equal to leaking a randomly generated ciphertext.

View Protocol Specification

Case study in IPDL

Alice wants to communicate q messages to Bob using an authenticated channel. The authenticated channel is not secure: it leaks each message to Eve, and waits to receive an ok message back from her before delivering the in-flight message. Thus, Eve cannot modify any of the messages but can read and delay them for any amount of time. To transmit information securely, Alice sends encryptions of her messages, which Bob decrypts using a shared key not known to Eve.

View Protocol Specification

Case study in IPDL

In symmetric-key encryption, the sender (Alice) and the receiver (Bob) need to agree on a shared secret key. One such key-agreement protocol is the Diffie-Hellman Key Exchange (DHKE). We then use the Diffie-Hellman Key Exchange protocol to turn an authenticated channel into a one-time pad that delivers a single secret message from Alice to Bob.

View Protocol Specification

Case study in IPDL

The El Gamal protocol is a CPA-secure public-key encryption schema based on the Diffie-Hellman Key Exchange. As in our previous case studies, Alice wants to communicate q messages to Bob using an authenticated channel. In the symmetric-key setting, the two parties had to agree on a secret shared key that was used both for encryption and decryption. In the public-key setting of El Gamal, Bob generates two keys: the public key is used for encryption and is known to both Alice and the adversary, whereas the secret key is used for decryption and known only to Bob.

View Protocol Specification

Case study in IPDL

We implement a protocol where N + 2 parties labeled 0, ..., N + 1 reach a Boolean consensus. We prove the protocol secure against a malicious attacker in the case when party N is corrupt, party N + 1 is honest, and any other party is arbitrarily honest or corrupt.

View Protocol Specification

Case study in IPDL

In the multi-party GMW protocol, N + 2 parties labeled 0, ... , N + 1 jointly compute the value of a given Boolean circuit built out of xor-, and-, and not gates. The inputs to the circuit are divided among the parties, and no party has access to the inputs of any other. Analogously to the two-party case, party n maintains its share of the actual value v computed by each gate, and summing up the shares n := 0, . . . , N + 1 yields back v. We prove the protocol secure in the case when party N is semi-honest, party N + 1 is honest, and any other party is arbitrarily honest or semi-honest.

Case study in IPDL

Documentation

The IPDL user manual can be found here.

A preprint describing the updated theory and the current implementation can be found here.

Our core logic paper on IPDL has been accepted at POPL 2023. The open access version can be found here.

Team

Acknowledgements

We thank Ionut Tutu for helping us integrate IPDL in SpeX and Ruben Rubio for providing a Maude bugfix.