diff --git a/asylo/examples/secure_grpc/README.md b/asylo/examples/secure_grpc/README.md index 6aa8aeca6..729ff0381 100644 --- a/asylo/examples/secure_grpc/README.md +++ b/asylo/examples/secure_grpc/README.md @@ -359,7 +359,7 @@ authorized to make the RPC. example. * An explanation of [SGX local attestation](https://software.intel.com/en-us/node/702983). -* See [A Formal Analysis of EKEP](/asylo/examples/secure_grpc/ekep_analysis/README.md) +* See [A Formal Analysis of EKEP](https://github.com/google/ekep-analysis/) for a ProVerif-based security analysis of the EKEP protocol. diff --git a/asylo/examples/secure_grpc/ekep_analysis/README.md b/asylo/examples/secure_grpc/ekep_analysis/README.md index 68e859327..7a29c98a3 100644 --- a/asylo/examples/secure_grpc/ekep_analysis/README.md +++ b/asylo/examples/secure_grpc/ekep_analysis/README.md @@ -1,460 +1,3 @@ # A Formal Analysis of EKEP -## Introduction - -Trustworthy Computing requires trustworthy connections between remote parties. -Normally, remote parties base symmetric trust on public-key infrastructure -(PKI): certificates attest to the provenance of private keys held by each party -and key-exchange protocols bootstrap from that trust to establish a private -session key to use for communication. However, Trustworthy Computing supports a -stronger notion of trust: remote attestation, by which a party may demonstrate -not only that their key is trusted, but that the software using the key matches -known properties and is running on known hardware. - -Key exchange and remote attestation compose naturally in sequence: a protocol -may require remote attestation as the first communication on a secure channel -and close the connection if attestation fails. However, this adds unnecessary -complexity and requires an external PKI to certify the original keys for the -exchange. Instead, the [Enclave Key Exchange -Protocol](https://asylo.dev/docs/concepts/ekep.html) (EKEP) integrates remote -attestation with key exchange to establish a channel with trust based entirely -on Trustworthy Computing. - -Participants in EKEP create ephemeral public/private key pairs, attest to those -pairs using remote attestation technology like Intel's Software Guard -Extensions (SGX), and use those attestations to establish a session key for -communication. - -To gain confidence in EKEP, we modeled it in -[ProVerif](https://bblanche.gitlabpages.inria.fr/proverif/), a tool for formal -verification in the [applied](https://arxiv.org/abs/1609.03003) -[π-calculus](https://en.wikipedia.org/wiki/%CE%A0-calculus). We used this model -to prove security properties of EKEP, including perfect forward secrecy (PFS). -As part of this work, we used the C preprocessor to implement macros for -modularization and convenient tuple data types and operations. We also added a -simple test framework that allows us to check library models independently of -the main protocol. - -We chose ProVerif because there was an existing ProVerif analysis of the [ALTS -handshake](https://cloud.google.com/docs/security/encryption-in-transit/application-layer-transport-security#handshake_protocol) -by Bruno Blanchet; we started by working through this analysis to understand -the properties that it verified. Our analysis was initially inspired by that -analysis, though our final ProVerif model shares little with Blanchet's. - - -## An overview of EKEP - -EKEP performs a handshake with 6 messages in (conceptually[^1]) 3 rounds: - -1. Precommit: agree on attestation and session-key requirements. -2. Attestation: attest to identities and the keys used to establish the channel. -3. Finish: compute the session key. - -The handshake may halt at any message due to inconsistencies or cryptographic -failures. The following sequence diagram (from the EKEP documentation) shows the -full handshake. - -![EKEP Handshake](ekep-handshake.svg "The EKEP Handshake") - -This protocol is originally based on the ALTS handshake with the -addition of attestation to ephemeral keys. - -The derivation of record protocol secrets computes an `HMAC-SHA256` using a -derived key over input that includes a full transcript of the handshake through -the `CLIENT_FINISH` message. Our EKEP model includes a step that uses the -record key to send a fresh message. - - -## EKEP Events and Queries - -ProVerif analysis is based on events that label points in a protocol. -Properties of protocols are modeled as relations between these events. - -We define the following events in the protocol, where `G` is the group used for -Diffie-Hellman key exchange, and `Name` represents the identity of a party in -the protocol. `Transcript5` is a typed bitstring that represents the last -transcript sent in the protocol, and `bitstring` is the ProVerif built-in type -for uninterpreted strings. - - -``` -(** The server says that its Transcript5 is |transcript| in a session with -the Diffie-Hellman shared key |dh|. *) -event serverTranscript5((*dh=*)G, Transcript5). - -(** The client says that its Transcript5 is |transcript| in a session with -the Diffie-Hellman shared key |dh|. *) -event clientTranscript5((*dh=*)G, Transcript5). - -(** The |client| says that it agreed on a |sharedSecret| with the |server|. *) -event clientBoundIdentity( - (*server=*)Name, (*client=*)Name, (*sharedSecret=*)G). - -(** The |server| says that it agreed on a |sharedSecret| with the |client|. *) -event serverBoundIdentity( - (*server=*)Name, (*client=*)Name, (*sharedSecret=*)G). - -(** The client sent |message| on a channel established by EKEP. *) -event clientSentMessage((*message=*)bitstring). - -(** The server received |message| on a channel established by EKEP. *) -event serverReceivedMessage((*message=*)bitstring). -``` - - -The `serverTranscript5` and `clientTranscript5` are the 6th transcript messages -(using 0-based indexing) from the beginning of the protocol, and they should -agree if the two parties saw the same messages. We represent this basic -correctness property in ProVerif as follows: - - -``` -(** If the client and server compute |cTranscript| and |sTranscript| -respectively as the Transcript5 values in the same EKEP session (identified by -the Diffie-Hellman shared key |dh|), then the client and server computed the -same transcripts. -*) -query dh: G, cTranscript: Transcript5, sTranscript: Transcript5; - (event(clientTranscript5(dh, cTranscript)) && - event(serverTranscript5(dh, sTranscript))) ==> - (cTranscript = sTranscript). -``` - - -The next property shows that EKEP protects against mis-identification attacks: -the server and client agree about identities that they got from a connection -using a given shared secret. - - -``` -(** If the client and server get public identities from a given connection, then -those identities match. *) -query idS: Name, idC: Name, idXS: Name, idXC: Name, ss: G; - (event(clientBoundIdentity(idXS, idC, ss)) && - event(serverBoundIdentity(idS, idXC, ss))) ==> - (idXS = idS && idXC = idC). -``` - - -Next, we show that the adversary cannot perform man-in-the-middle attacks: a -server that receives a message on an EKEP channel can be sure that it was sent -by the client (and, due to the previous properties, this means that the message -was sent by the client with the expected identity). - - -``` -(** If the client and server establish a connection and the server receives a -message on that connects, then the client sent that message. *) -query ss: G, m: bitstring; - event(serverReceivedMessage(m)) ==> - inj-event(clientSentMessage(m)). -``` - - -Finally, we show that an adversary cannot learn any messages sent on an -established channel. This kind of query is supported directly in ProVerif as -follows: - - -``` -(** The attacker cannot obtain the unique secret message exchanged between -client and server. *) -query attacker(new message). -``` - - -Note that we add a second phase to the protocol in which the long-term -identities from the first part of the protocol are leaked. In this case, those -long-term keys are represent as MAC keys used to represent SGX-based identity. -Even in this case, the adversary cannot learn the message from the previous -round. This demonstrates that EKEP satisfies Perfect Forward Secrecy. - - -## Representing Trustworthy Identities - -Our model represents SGX with a new principal that provides SGX attestations -for the client, the server, and any other arbitrary party. It represents the -identities as secret HMAC keys: the client and server each provide a MAC on a -message they want attested as coming from their identity. - - -``` -(** SgxAttestationForClient provides SGX signatures for clients. *) -let SgxAttestationForClient(clientSgxMacKey: HmacKey, sgxPrivKey: SigningKey) = - in(c, (message: ClientSgxMessage, tag: HmacAuthTag)); - let kind = ClientSgxMessage_kind(message) in - if kind = kClientId then - if hmacClientSgxVerify(clientSgxMacKey, message, tag) then - out(c, signClientSgx(sgxPrivKey, message)). - -(** SgxAttestationForServer provides SGX signatures for servers. *) -let SgxAttestationForServer(serverSgxMacKey: HmacKey, sgxPrivKey: SigningKey) = - in(c, (message: ServerSgxMessage, tag: HmacAuthTag)); - if ServerSgxMessage_kind(message) = kServerId then - if hmacServerSgxVerify(serverSgxMacKey, message, tag) then - out(c, signServerSgx(sgxPrivKey, message)). - -(** SgxAttestationForOther provides SGX signatures for the adversary. *) -let SgxAttestationForOther(sgxPrivKey: SigningKey) = - in(c, (name: Name, publicKey: G, transcript: bitstring)); - out(c, sign(sgxPrivKey, (name, kOtherId, publicKey, transcript))). -``` - - -Note that these implementations are not secret: the adversary can call -`SgxAttestationForClient` and can even replay old tagged messages. But all this -gives the adversary is the same public attested (signed) message as before, and -it already gets this message when the client performs attestation normally. The -only secret is the MAC key that represents the party's identity. - -Note also that this model is not exposed in the events or queries from the -previous section: it is critical to the security of the protocol, but it works -underneath the level of events and queries to guarantee the security of -identities and hence the security of the protocol. - -Finally, note that while this implementation calls itself "SGX", it is an -abstraction that more generally represents a Trustworthy Computing system that -can cryptographically attest to statements by identified parties. - - -## Development and Testing - -ProVerif has limited support for standard development methodologies. As part of -the EKEP modeling project, we added support for some utilities that are of -general interest: textual include files, macro-based named-tuple data types, -and unit testing. - - -### Include Files - -ProVerif does not support modular development; there is a `-lib` flag for the -`proverif` binary that allows callers to specify a single file for textual -inclusion, but not multiple files. It also doesn't support recursive inclusion -of files. These facilities are standard in modern programming languages. - -We created a simple run script that uses the C preprocessor to support textual -inclusion of ProVerif library files (`.pvl`) in ProVerif (`.pv`) and ProVerif -library files. This allowed us to develop libraries of cryptographic and -utility functions separately from the main EKEP model and kept the EKEP model -clean. Our current libraries are `diffie_hellman.pvl`, -`authenticated_encryption.pvl`, `named_tuples.pvl`, and `list.pvl`. We also -have an `ekep.pvl` file that implements separable parts of the EKEP protocol so -that the top-level implementation of the protocol is clear. - - -### Named Tuples - -We also used the C preprocessor to create useful macros to implement data -structures. In particular, we implemented strongly-typed named tuples, which -allow callers to extract named fields from the tuples. This drastically -increases the readability of the model. Unfortunately, one limitation is that -the macros must be defined for each possible length of the named tuple. - -For example, the following implementation shows how to implement 2-tuples in C -preprocessor macros. - - -``` -#define REDUCE_FORALL2(TypeName, field, result, var0, type0, var1, type1) \ - reduc forall var0: type0, var1: type1; \ - TypeName##_##field(Build##TypeName(var0, var1)) = result - -#define DEFINE_DATA_TYPE2(TypeName, var0, type0, var1, type1) \ - type TypeName. \ - fun Build##TypeName(type0, type1): TypeName [data]. \ - REDUCE_FORALL2(TypeName, var0, var0, var0, type0, var1, type1). \ - REDUCE_FORALL2(TypeName, var1, var1, var0, type0, var1, type1) -``` - - -The `REDUCE_FORALL2` macro produces a reduction that provides a function to -extract a field with name `field` from a named tuple with type name `TypeName`. -The top-level macro `DEFINE_DATA_TYPE2` implements a new named-tuple type -`TypeName` with a `BuildTypeName` function to construct a new instance of the -tuple and reductions for accessing each of its fields. - - -### Unit Testing - -After modularization, we wanted to test our libraries separately from their use -in the EKEP model. So, we devised a simple test framework: a test consists of a -set of processes, each of which uses the functionality provided by a library -and checks properties of the reductions exposed by the library. If the property -succeeds, then the process sends the message `Success` to the channel. If the -property fails, then the process sends the message `Fail` to the channel. - -The sole query in the test file is the secrecy of the `Fail` message: if the -adversary can get `Fail` on the channel, then one of the properties of the -library does not hold, and the test has failed. The trace produced by ProVerif -shows which property failed. - -Here is a sample, minimal test of some functionality from the `list.pvl` -library, using our `test_helpers.pvl` library that provides unit-test functions -like `EXPECT_EQ`. - - -``` -#include "list.pvl" - -#include "test_helpers.pvl" - -free b0: bitstring. -free b1: bitstring. - -(** Checks that List_elem works on List1. *) -let TestElemList1() = - let l1_0 = List1(b0) in - EXPECT_TRUE(List_elem(b0, l1_0)); - EXPECT_FALSE(List_elem(b1, l1_0)). - -(** Checks that List_some_intersection works on List1, List1 arguments. *) -let TestFirstIntersection1_1() = - let l1_0 = List1(b0) in - EXPECT_EQ(b0, List_some_intersection(l1_0, l1_0)). - -process - ( TestElemList1() - | TestFirstIntersection1_1() - | TestEq1() - | TestHasIntersection1() - | TestIsSubset1() - ) -``` - - - -### Speed - -Our current EKEP model performs its analysis in less than 1 second. Here is the -summary output of `time ./run_proverif.sh ekep.pv`: - - -``` --------------------------------------------------------------- -Verification summary: - -Query event(clientTranscript5(dh,cTranscript)) && event(serverTranscript5(dh,sTranscript)) ==> cTranscript = sTranscript is true. - -Query event(clientBoundIdentity(idXS,idC,ss)) && event(serverBoundIdentity(idS,idXC,ss)) ==> idXS = idS && idXC = idC is true. - -Query inj-event(serverReceivedMessage(m)) ==> inj-event(clientSentMessage(m)) is true. - -Query not attacker_p1(message[]) is true. - --------------------------------------------------------------- - -./run_proverif.sh ekep.pv 0.29s user 0.04s system 98% cpu 0.332 total -``` - - - -### Utility - -Changing the EKEP protocol to introduce some bugs causes ProVerif to catch -these bugs. For example, if we change the client to not check the -cryptographically validated origin of its messages, then properties fail. - -More precisely, if we add the function `getClientSgxMessage` as follows: - - -``` -reduc forall message: ClientSgxMessage, key: VerifyingKey, anyKey: SigningKey; - getClientSgxMessage(key, signClientSgx(anyKey, message)) = message. -``` - - -and we replace the client validation call `checkClientSgxSignature` with this -call (thus ignoring the signature and just extracting the message), we get the -following result from ProVerif: - - -``` --------------------------------------------------------------- -Verification summary: - -Query event(clientTranscript5(dh,cTranscript)) && event(serverTranscript5(dh,sTranscript)) ==> cTranscript = sTranscript is true. - -Query event(clientBoundIdentity(idXS,idC,ss)) && event(serverBoundIdentity(idS,idXC,ss)) ==> idXS = idS && idXC = idC is false. - -Query inj-event(serverReceivedMessage(m)) ==> inj-event(clientSentMessage(m)) is false. - -Query not attacker_p1(message[]) is true. - --------------------------------------------------------------- -``` - - -These errors say that it's no longer the case that the client and server agree -on who they're talking to and that just because a client received a message, it -doesn't mean that the server sent that message. In other words, an adversary -can now forge messages in the protocol. - - -### Limitations - -The main limitation of our EKEP model is that our list implementation only -supports lists of length 1.[^2] This means that the model does not test cases -where, for example, a client proposes multiple possible attestation methods, -and the server selects one. - - -## Conclusions - -EKEP has been shown to satisfy strong security properties, including PFS. We -are releasing this model under the Apache 2 license, and we welcome -contributions and comments. - - -## Notes - -[^1]: - Other variants of this handshake are possible; this document only analyzes - the public version of EKEP. - -[^2]: - ProVerif takes a very long time (hours to days) to complete when used in - our analysis for lists of length 2 and appears to never terminate for - lists of length 3 or more. - - -# Running the Analysis and Tests - -To run a file in ProVerif, use the script `run_proverif.sh`. This script -assumes that ProVerif is installed on the local machine. The typical usage is: - -```bash -$ ./run_proverif.sh list_test.pv -``` - -NOTE: You can only run `.pv` files, and not `.pvl` (library) files. - -## Debugging syntax errors - -If the ProVerif script has a syntax error, the output will refer to a line in -one of the generated files. The temporary files will be automatically cleaned up -after the script finishes. To disable this automatic cleanup, set the -environment variable `PROVERIF_NO_CLEANUP`. For example: - -```bash -$ PROVERIF_NO_CLEANUP=1 ./run_proverif.sh list_test.pv -``` - -## Running ProVerif Interactively - -The `run_proverif.sh` script supports an environment variable -`PROVERIF_INTERACT`. If this variable is set, then `run_proverif.sh` will call -`proverif_interact` on the generated file instead of `proverif`. This brings up -an interactive GUI that allows the user to act as the adversary in a protocol. -For example: - -```bash -$ PROVERIF_INTERACT=1 ./run_proverif.sh ekep.pv -``` - -To facilitate the job of the adversary in interactive mode, the `ekep.pvl` file -conditionally defines helper functions that support generating some of the -messages that would otherwise be tedious and error-prone to type. See the -`ifdef ENABLE_DEBUG_FUNCTIONS` block in `ekep.pvl` for these functions. - -The `run_proverif.sh` script always defines `ENABLE_DEBUG_FUNCTIONS` when -`PROVERIF_INTERACT` is set. +Moved to [its own repository](https://github.com/google/ekep-analysis) diff --git a/asylo/examples/secure_grpc/ekep_analysis/authenticated_encryption.pvl b/asylo/examples/secure_grpc/ekep_analysis/authenticated_encryption.pvl deleted file mode 100644 index 2fae7332b..000000000 --- a/asylo/examples/secure_grpc/ekep_analysis/authenticated_encryption.pvl +++ /dev/null @@ -1,31 +0,0 @@ -(** -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. -*) - -#ifndef _AUTHENTICATED_ENCRYPTION_PVL -#define _AUTHENTICATED_ENCRYPTION_PVL - -(** A key for authenticated encryption. *) -type RecordKey. - -(** Encrypts plaintext to ciphertext. *) -fun enc(RecordKey, (*plaintext=*)bitstring): (*ciphertext=*)bitstring. - -(** Decrypts ciphertext to plaintext. *) -fun dec(RecordKey, (*ciphertext=*)bitstring): (*plaintext=*)bitstring -reduc - forall k: RecordKey, msg: bitstring; dec(k, enc(k, msg)) = msg. - -#endif /* _AUTHENTICATED_ENCRYPTION_PVL */ diff --git a/asylo/examples/secure_grpc/ekep_analysis/diffie_hellman.pvl b/asylo/examples/secure_grpc/ekep_analysis/diffie_hellman.pvl deleted file mode 100644 index 967483d9c..000000000 --- a/asylo/examples/secure_grpc/ekep_analysis/diffie_hellman.pvl +++ /dev/null @@ -1,42 +0,0 @@ -(** -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. -*) - -#ifndef _DIFFIE_HELLMAN_PVL -#define _DIFFIE_HELLMAN_PVL - -(** The base group used in Diffie-Hellman *) -type G. - -(** The exponent field used in Diffie-Hellman. *) -type Z. - -(** Converts a field element in Z to a bitstring. *) -fun Z2b(Z): bitstring [data, typeConverter]. - -(** Converts a group element in G to a bitstring. *) -fun G2b(G): bitstring [data, typeConverter]. - -(** A constant, public base element for Diffie-Hellman computations. *) -const g:G [data]. - -(** Computes the exponentiation |base|^|exponent|. *) -fun exp((*base=*)G, (*exponent=*)Z): G. - -(* Adds the fact that (g^x)^y = (g^y)^x to the equational theory. *) -equation forall x: Z, y: Z; - exp(exp(g, x), y) = exp(exp(g, y), x). - -#endif /* _DIFFIE_HELLMAN_PVL */ diff --git a/asylo/examples/secure_grpc/ekep_analysis/diffie_hellman_test.pv b/asylo/examples/secure_grpc/ekep_analysis/diffie_hellman_test.pv deleted file mode 100644 index 67f89b4c6..000000000 --- a/asylo/examples/secure_grpc/ekep_analysis/diffie_hellman_test.pv +++ /dev/null @@ -1,34 +0,0 @@ -(** -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. -*) - -#include "diffie_hellman.pvl" - -#include "test_helpers.pvl" - -free exp0: Z. -free exp1: Z. - -DEFINE_EXPECT_EQ_FUN(G). - -(* Tests that the equational theory has been extended to capture equality of -(g^x)^y and (g^y)^x. *) -let TestExp() = - let k01 = exp(exp(g, exp0), exp1) in - let k10 = exp(exp(g, exp1), exp0) in - EXPECT(Eq_G(k01, k10)). - -process - (TestExp()) diff --git a/asylo/examples/secure_grpc/ekep_analysis/ekep-handshake.svg b/asylo/examples/secure_grpc/ekep_analysis/ekep-handshake.svg deleted file mode 100644 index 40b1264ef..000000000 --- a/asylo/examples/secure_grpc/ekep_analysis/ekep-handshake.svg +++ /dev/null @@ -1 +0,0 @@ -Created with Raphaël 2.2.0ClientClientServerServerCLIENT_PRECOMMITServer validation ofCLIENT_PRECOMMITSERVER_PRECOMMITClient validation ofSERVER_PRECOMMITGenerate verifiableclient identity basedon previous messagesCLIENT_IDServer validation ofCLIENT_IDGenerate verifiableserver identity basedon previous messagesSERVER_IDDerive EKEP secretsClient validation ofSERVER_IDDerive EKEP secretsSERVER_FINISHClient validation ofSERVER_FINISHCLIENT_FINISHServer validation ofCLIENT_FINISHDerive record protocol secrets \ No newline at end of file diff --git a/asylo/examples/secure_grpc/ekep_analysis/ekep.pv b/asylo/examples/secure_grpc/ekep_analysis/ekep.pv deleted file mode 100644 index 9cc27fec8..000000000 --- a/asylo/examples/secure_grpc/ekep_analysis/ekep.pv +++ /dev/null @@ -1,262 +0,0 @@ -(** -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. -*) - -#include "authenticated_encryption.pvl" -#include "diffie_hellman.pvl" -#include "ekep.pvl" - -channel c. - -(** The server says that its Transcript5 is |transcript| in a session with -the Diffie-Hellman shared key |dh|. *) -event serverTranscript5((*dh=*)G, Transcript5). - -(** The client says that its Transcript5 is |transcript| in a session with -the Diffie-Hellman shared key |dh|. *) -event clientTranscript5((*dh=*)G, Transcript5). - -(** The |client| says that it agreed on a |sharedSecret| with the |server|. *) -event clientBoundIdentity( - (*server=*)Name, (*client=*)Name, (*sharedSecret=*)G). - -(** The |server| says that it agreed on a |sharedSecret| with the |client|. *) -event serverBoundIdentity( - (*server=*)Name, (*client=*)Name, (*sharedSecret=*)G). - -event clientSentMessage((*message=*)bitstring). -event serverReceivedMessage((*message=*)bitstring). - -(** If the client and server compute |cTranscript| and |sTranscript| -respectively as the Transcript5 values in the same EKEP session (identified by -the Diffie-Hellman shared key |dh|), then the client and server computed the -same transcripts. -*) -query dh: G, cTranscript: Transcript5, sTranscript: Transcript5; - (event(clientTranscript5(dh, cTranscript)) && - event(serverTranscript5(dh, sTranscript))) ==> - (cTranscript = sTranscript). - -(** If the client and server get public identities from a given connection, then -those identities match. *) -query idS: Name, idC: Name, idXS: Name, idXC: Name, ss: G; - (event(clientBoundIdentity(idXS, idC, ss)) && - event(serverBoundIdentity(idS, idXC, ss))) ==> - (idXS = idS && idXC = idC). - -(** If the client and server establish a connection and the server receives a -message on that connects, then the client sent that message. *) -query ss: G, m: bitstring; - event(serverReceivedMessage(m)) ==> - inj-event(clientSentMessage(m)). - -(** The attacker cannot obtain the unique secret message exchanged between -client and server. *) -query attacker(new message). - -(** Implements the client side of EKEP. *) -let Client(clientName: Name, clientSgxKey: HmacKey, sgxPubKey: VerifyingKey, - message: bitstring) = - (* Send Client Precommit. *) - new clientPrecommit: Challenge; - out(c, clientPrecommit); - let transcript0 = CreateTranscript0(clientPrecommit) in - - (* Receive Server Precommit. *) - in(c, serverPrecommit: Challenge); - let transcript1 = ExtendToTranscript1(transcript0, serverPrecommit) in - - (* Compute Client Id. *) - new clientPrivateKey: Z; - let clientPublicKey = exp(g, clientPrivateKey) in - - (* Create a message for SGX to sign, and create an HMAC of this message that - SGX can verify as coming from the client. This models the channel that SGX has - with the client software. *) - let clientSgxMessage = BuildClientSgxMessage( - clientName, kClientId, clientPublicKey, transcript1) in - let clientSgxTag = hmacClientSgx(clientSgxKey, clientSgxMessage) in - out(c, (clientSgxMessage, clientSgxTag)); - in(c, clientId: Signature); - - (* Make sure that the signature is valid, comes from SGX, and is for the right - message. *) - let (=clientSgxMessage) = checkClientSgxSignature(sgxPubKey, clientId) in - - (* Send Client Id. *) - out(c, clientId); - let transcript2 = ExtendToTranscript2(transcript1, clientId) in - - (* Receive Server Id. *) - in(c, serverId: Signature); - - (* Check that the Server Id is a valid signature from SGX for the kServerId - IdentityKind. *) - let serverSgxMessage = checkServerSgxSignature(sgxPubKey, serverId) in - if ServerSgxMessage_kind(serverSgxMessage) <> kServerId then - out(c, kBadAssertion) else - let xName = ServerSgxMessage_name(serverSgxMessage) in - let serverPublicKey = ServerSgxMessage_publicKey(serverSgxMessage) in - let transcript3 = ExtendToTranscript3(transcript2, serverId) in - - (* Derive EKEP secrets. *) - let sharedSecret = exp(serverPublicKey, clientPrivateKey) in - let masterSecret = hkdfMaster(EkepHandshakeV1, sharedSecret, transcript3) in - let authKey = hkdfAuth(EkepHandshakeV1, sharedSecret, transcript3) in - - (* Receive Server Finish. *) - in(c, serverFinish: HmacAuthTag); - let transcript4 = ExtendToTranscript4(transcript3, serverFinish) in - - (* Validate Server Finish. *) - if not(hmacVerify(authKey, EkepHandshakeV1ServerFinish, serverFinish)) then - out(c, kBadAuthenticator) else - event clientBoundIdentity(xName, clientName, sharedSecret); - - (* Compute Client Finish. *) - let clientFinish = hmac(authKey, EkepHandshakeV1ClientFinish) in - out(c, clientFinish); - let transcript5 = ExtendToTranscript5(transcript4, clientFinish) in - event clientTranscript5(sharedSecret, transcript5); - - (* Derive Record key. *) - let recordKey = - hkdfRecordKey(EkepRecordProtocolV1, masterSecret, transcript5) in - - (* The EKEP handshake ends here. After this, the client sends a message using - the negotiated record protocol. *) - event clientSentMessage(message); - out(c, enc(recordKey, message)). - -(** Implements the server side of EKEP. *) -let Server(serverName: Name, serverSgxKey: HmacKey, sgxPubKey: VerifyingKey) = - (* Receive Client Precommit. *) - in(c, clientPrecommit: Challenge); - let transcript0 = CreateTranscript0(clientPrecommit) in - - (* Send Server Precommit. *) - new serverPrecommit: Challenge; - out(c, serverPrecommit); - let transcript1 = ExtendToTranscript1(transcript0, serverPrecommit) in - - (* Receive Client Id. *) - in(c, clientId: Signature); - - (* Check that the Client Id is a valid signature from SGX for the kClientId - IdentityKind. *) - let clientSgxMessage = checkClientSgxSignature(sgxPubKey, clientId) in - if ClientSgxMessage_kind(clientSgxMessage) <> kClientId then - out(c, kBadAssertion) else - let xName = ClientSgxMessage_name(clientSgxMessage) in - let clientPublicKey = ClientSgxMessage_publicKey(clientSgxMessage) in - let transcript2 = ExtendToTranscript2(transcript1, clientId) in - - (* Compute Server Id *) - new serverPrivateKey: Z; - let serverPublicKey = exp(g, serverPrivateKey) in - - (* Create a message for SGX to sign, and create an HMAC of this message that - SGX can verify as coming from the client. This models the channel that SGX has - with the server software. *) - let serverSgxMessage = BuildServerSgxMessage( - serverName, kServerId, serverPublicKey, transcript2) in - let serverSgxTag = hmacServerSgx(serverSgxKey, serverSgxMessage) in - out(c, (serverSgxMessage, serverSgxTag)); - in(c, serverId: Signature); - - (* Make sure that the signature is valid, comes from SGX, and is for the right - message. *) - let (=serverSgxMessage) = checkServerSgxSignature(sgxPubKey, serverId) in - - (* Send Server Id. *) - out(c, serverId); - let transcript3 = ExtendToTranscript3(transcript2, serverId) in - - (* Derive EKEP secrets. *) - let sharedSecret = exp(clientPublicKey, serverPrivateKey) in - let masterSecret = hkdfMaster(EkepHandshakeV1, sharedSecret, transcript3) in - let authKey = hkdfAuth(EkepHandshakeV1, sharedSecret, transcript3) in - - (* Compute Server Finish. *) - let serverFinish = hmac(authKey, EkepHandshakeV1ServerFinish) in - - (* Send Server Finish. *) - out(c, serverFinish); - let transcript4 = ExtendToTranscript4(transcript3, serverFinish) in - - (* Receive Client Finish. *) - in(c, clientFinish: HmacAuthTag); - let transcript5 = ExtendToTranscript5(transcript4, clientFinish) in - if not(hmacVerify(authKey, EkepHandshakeV1ClientFinish, clientFinish)) then - (* Note that the server is not allowed to send an error if client validation - fails. Instead, it silently closes the connection. *) - 0 else - event serverTranscript5(sharedSecret, transcript5); - - (* Derive Record key. *) - event serverBoundIdentity(serverName, xName, sharedSecret); - let recordKey = - hkdfRecordKey(EkepRecordProtocolV1, masterSecret, transcript5) in - - (* The EKEP handshake ends here. After this, the server receives a message - using the negotiated record protocol. *) - in(c, encryptedClientMessage: bitstring); - let decryptedClientMessage = dec(recordKey, encryptedClientMessage) in - event serverReceivedMessage(decryptedClientMessage). - -(** SgxAttestationForClient provides SGX signatures for clients. *) -let SgxAttestationForClient(clientSgxMacKey: HmacKey, sgxPrivKey: SigningKey) = - in(c, (message: ClientSgxMessage, tag: HmacAuthTag)); - let kind = ClientSgxMessage_kind(message) in - if kind = kClientId then - if hmacClientSgxVerify(clientSgxMacKey, message, tag) then - out(c, signClientSgx(sgxPrivKey, message)). - -(** SgxAttestationForServer provides SGX signatures for servers. *) -let SgxAttestationForServer(serverSgxMacKey: HmacKey, sgxPrivKey: SigningKey) = - in(c, (message: ServerSgxMessage, tag: HmacAuthTag)); - if ServerSgxMessage_kind(message) = kServerId then - if hmacServerSgxVerify(serverSgxMacKey, message, tag) then - out(c, signServerSgx(sgxPrivKey, message)). - -(** SgxAttestationForOther provides SGX signatures for the adversary. *) -let SgxAttestationForOther(sgxPrivKey: SigningKey) = - in(c, (name: Name, publicKey: G, transcript: bitstring)); - out(c, sign(sgxPrivKey, (name, kOtherId, publicKey, transcript))). - -process - new clientSgxMacKey: HmacKey; - new serverSgxMacKey: HmacKey; - - new serverName: Name; - new clientName: Name; - out(c, clientName); - out(c, serverName); - - new sgxPrivKey: SigningKey; - let sgxPubKey = pubKey(sgxPrivKey) in - out(c, sgxPubKey); - - new message: bitstring; - - ( (! Server(serverName, serverSgxMacKey, sgxPubKey) ) - | (! Client(clientName, clientSgxMacKey, sgxPubKey, message) ) - | (! SgxAttestationForClient(clientSgxMacKey, sgxPrivKey) ) - | (! SgxAttestationForServer(serverSgxMacKey, sgxPrivKey) ) - | (! SgxAttestationForOther(sgxPrivKey) ) - (* Expose the client and server's long-term identity keys in phase 1 to test - perfect forward secrecy in the protocol. *) - | ( phase 1; out(c, clientSgxMacKey); out(c, serverSgxMacKey) ) - ) diff --git a/asylo/examples/secure_grpc/ekep_analysis/ekep.pvl b/asylo/examples/secure_grpc/ekep_analysis/ekep.pvl deleted file mode 100644 index 0377e5053..000000000 --- a/asylo/examples/secure_grpc/ekep_analysis/ekep.pvl +++ /dev/null @@ -1,212 +0,0 @@ -(** -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. -*) - -#ifndef _EKEP_PVL -#define _EKEP_PVL - -#include "authenticated_encryption.pvl" -#include "diffie_hellman.pvl" -#include "named_tuples.pvl" - -(* This library defines all the types used only in EKEP. - * Cryptographic types and data structures are defined in their own headers. - *) - -(** Alerts. *) -type Alert. -const kBadMessage: Alert [data]. -const kDeserializationFailed: Alert [data]. -const kBadProtocolVersion: Alert [data]. -const kBadHandshakeCipher: Alert [data]. -const kBadRecordProtocol: Alert [data]. -const kBadAuthenticator: Alert [data]. -const kBadAssertionType: Alert [data]. -const kBadAssertion: Alert [data]. -const kProtocolError: Alert [data]. -const kInternalError: Alert [data]. -const kBadEphemeralParameters: Alert [data]. -(* The kOk message is used to handle status cases that are not errors. *) -const kOk: Alert [data]. - -(** HMAC context strings are represented as bitstrings. *) -type HkdfContext. -const EkepHandshakeV1: HkdfContext [data]. -const EkepRecordProtocolV1: HkdfContext [data]. - -(** Sentinel strings for HMAC. *) -const EkepHandshakeV1ServerFinish: bitstring [data]. -const EkepHandshakeV1ClientFinish: bitstring [data]. - -(** Names of principals. *) -type Name. - -(** Kinds of identities of principals. Anyone can get a signed Identity from -SGX that binds a public key to a Name. However, only the client can get -identities of kind kClientId, and only the server can get identities of kind -kServerId. This part of the type system models the notion of being able to -learn from SGX about properties of a communicating remote or local party, and -it is one of the features of EKEP that distinguishes it from previous -key-exchange protocols. *) -type IdentityKind. -const kClientId: IdentityKind. -const kServerId: IdentityKind. -const kOtherId: IdentityKind. - -(** Descriptions of Assertions. *) -type AssertionDescription. -const kSgxAssertionDescription: AssertionDescription [data]. - -(** Empty options for the precommit. *) -type Options. -const kEmptyOptions: Options [data]. - -(** An explicit type for challenges. *) -type Challenge. - -(** Transcripts are used as part of the material that key derivation operates -on. *) -type Transcript0. -type Transcript1. -type Transcript2. -type Transcript3. -type Transcript4. -type Transcript5. - -(* Signing and verification with asymmetric algorithms. *) - -(** Keys used for signing in an (unspecified) asymmetric algorithm. *) -type SigningKey. - -(** Keys used for verification in an (unspecified) asymmetric algorithm. *) -type VerifyingKey. - -(** Produces the public key that corresponds to a signing key. *) -fun pubKey(SigningKey): VerifyingKey. - -type Signature. - -(** Signs |message| with a key, producing a signature. *) -fun sign(SigningKey, (*message=*)bitstring): Signature. - -(** Gets the |message| from a signature under key |k|. *) -reduc forall message: bitstring, key: SigningKey; - getMessage(sign(key, message)) = message. - -(** Checks a signature under a |key| and produces its |message| if the signature -passes verification. *) -reduc forall message: bitstring, key: SigningKey; - checkSignature(pubKey(key), sign(key, message)) = message. - -(** An Id associates a public key with a list of assertions. *) -DEFINE_DATA_TYPE2(Id, - publicKey, G, - assertion, Signature). - -(** A ClientSgxMessage is sent from a client to SGX to get an assertion. *) -DEFINE_DATA_TYPE4(ClientSgxMessage, - name, Name, - kind, IdentityKind, - publicKey, G, - transcript, Transcript1). - -(** A ServerSgxMessage is sent from a server to SGX to get an assertion. *) -DEFINE_DATA_TYPE4(ServerSgxMessage, - name, Name, - kind, IdentityKind, - publicKey, G, - transcript, Transcript2). - -fun signClientSgx(SigningKey, ClientSgxMessage): Signature. -reduc forall message: ClientSgxMessage, key: SigningKey; - checkClientSgxSignature(pubKey(key), signClientSgx(key, message)) = message. - -fun signServerSgx(SigningKey, ServerSgxMessage): Signature. -reduc forall message: ServerSgxMessage, key: SigningKey; - checkServerSgxSignature(pubKey(key), signServerSgx(key, message)) = message. - -(** HmacAuthTag is the symmetric equivalent of a digital signature. *) -type HmacAuthTag. - -(** HmacKey is the type of keys used to compute HMACs. *) -type HmacKey. - -(** Computes an HMAC for a given bitstring message. *) -fun hmac(HmacKey, (*message=*)bitstring): HmacAuthTag. - -fun hmacVerify(HmacKey, (*message=*)bitstring, HmacAuthTag): bool -reduc - forall key: HmacKey, message: bitstring; - hmacVerify(key, message, hmac(key, message)) = true otherwise - forall key: HmacKey, message: bitstring, tag: HmacAuthTag; - hmacVerify(key, message, tag) = false. - -fun hmacClientSgx(HmacKey, ClientSgxMessage): HmacAuthTag. -fun hmacClientSgxVerify(HmacKey, ClientSgxMessage, HmacAuthTag): bool -reduc - forall key: HmacKey, message: ClientSgxMessage; - hmacClientSgxVerify( - key, message, hmacClientSgx(key, message)) = true otherwise - forall key: HmacKey, message: ClientSgxMessage, tag: HmacAuthTag; - hmacClientSgxVerify(key, message, tag) = false. - -fun hmacServerSgx(HmacKey, ServerSgxMessage): HmacAuthTag. -fun hmacServerSgxVerify(HmacKey, ServerSgxMessage, HmacAuthTag): bool -reduc - forall key: HmacKey, message: ServerSgxMessage; - hmacServerSgxVerify( - key, message, hmacServerSgx(key, message)) = true otherwise - forall key: HmacKey, message: ServerSgxMessage, tag: HmacAuthTag; - hmacServerSgxVerify(key, message, tag) = false. - - -(** MasterSecret is produced from the output of HKDF1. *) -type MasterSecret. - -(** Produces a master key using HKDF. *) -fun hkdfMaster(HkdfContext, (*secret=*)G, Transcript3): MasterSecret. - -(** Produces an auth key using HKDF. *) -fun hkdfAuth(HkdfContext, (*secret=*)G, Transcript3): HmacKey. - -(** Produces a record key using HKDF. *) -fun hkdfRecordKey(HkdfContext, MasterSecret, Transcript5): RecordKey. - -(** Creates Transcript 0 from a client precommit message. *) -fun CreateTranscript0(Challenge): Transcript0 [data, typeConverter]. - -(** Extends Transcript 0 to Transcript 1, using a server precommit message. *) -fun ExtendToTranscript1(Transcript0, Challenge): Transcript1 [data]. - -(** Extends Transcript 1 to Transcript 2, using a client ID message. *) -fun ExtendToTranscript2( - Transcript1, (*clientId=*)Signature): Transcript2 [data]. - -(** Extends Transcript 2 to Transcript 3, using a server ID message. *) -fun ExtendToTranscript3( - Transcript2, (*serverId=*)Signature): Transcript3 [data]. - -(** Extends Transcript 3 to Transcript 4, using an HMAC auth tag from the server -finish message. *) -fun ExtendToTranscript4(Transcript3, (*serverFinish=*)HmacAuthTag): - Transcript4 [data]. - -(** Extends Transcript 4 to Transcript 5, using an HMAC auth tag from the client -finish message. *) -fun ExtendToTranscript5(Transcript4, (*clientFinish=*)HmacAuthTag): - Transcript5 [data]. - - -#endif /* _EKEP_PVL */ diff --git a/asylo/examples/secure_grpc/ekep_analysis/ekep_test.pv b/asylo/examples/secure_grpc/ekep_analysis/ekep_test.pv deleted file mode 100644 index f2a82ba88..000000000 --- a/asylo/examples/secure_grpc/ekep_analysis/ekep_test.pv +++ /dev/null @@ -1,43 +0,0 @@ -(** -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. -*) - -#include "ekep.pvl" - -#include "test_helpers.pvl" - -free m0: bitstring. -free m1: bitstring. - -free k0: HmacKey. -free k1: HmacKey. - -DEFINE_EXPECT_EQ_FUN(HmacAuthTag). - -(** Checks that HMAC verification works and fails in its expected cases. *) -let TestHmac() = - let t0 = hmac(k0, m0) in - let t1 = hmac(k0, m1) in - let tk1 = hmac(k1, m0) in - EXPECT(Eq_HmacAuthTag(t0, t0)); - EXPECT_TRUE(hmacVerify(k0, m0, t0)); - EXPECT_TRUE(hmacVerify(k0, m1, t1)); - EXPECT_FALSE(hmacVerify(k0, m0, t1)); - EXPECT_FALSE(hmacVerify(k0, m1, t0)); - EXPECT_FALSE(hmacVerify(k1, m0, t0)); - EXPECT_FALSE(hmacVerify(k0, m0, tk1)). - -process - TestHmac() diff --git a/asylo/examples/secure_grpc/ekep_analysis/list.pvl b/asylo/examples/secure_grpc/ekep_analysis/list.pvl deleted file mode 100644 index d4ff6a666..000000000 --- a/asylo/examples/secure_grpc/ekep_analysis/list.pvl +++ /dev/null @@ -1,77 +0,0 @@ -(** -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. -*) - -#ifndef _LIST_PVL -#define _LIST_PVL - -(** List is used in protocols for holding configuration options. Note that -instances of this List can never be empty, by construction. Also note that this -is actually a bounded List, of max length 1. *) -type List. - -(** Constructs a List with one element. *) -fun List1(bitstring): List [data, typeConverter]. - -(* Checks if a given bitstring is an element of a List. *) -fun List_elem(bitstring, List): bool -reduc - (* Lists of length 1. *) - forall x0: bitstring, l: List; - List_elem(x0, List1(x0)) = true otherwise - forall x0: bitstring, l0: List; - List_elem(x0, l0) = false. - -(** Gets some element that is in the intersection of two Lists. Fails if there -is no such element. *) -fun List_some_intersection(List, List): bitstring -reduc - forall x0: bitstring; - List_some_intersection(List1(x0), List1(x0)) = x0. - -(** Check if the first list is a subset of the second. *) -fun List_is_subset(List, List): bool -reduc - forall x0: bitstring; - List_is_subset(List1(x0), List1(x0)) = true otherwise - forall l0: List, l1: List; - List_is_subset(l0, l1) = false. - -(** Checks the equality of two lists. Equality depends on order as well as -contents. *) -fun List_eq(List, List): bool -reduc - forall x0: bitstring; - List_eq(List1(x0), List1(x0)) = true otherwise - forall l0: List, l1: List; - List_eq(l0, l1) = false. - -(** Catches failed list operations and reports whether failure occurred. *) -fun List_is_fail(List): bool -reduc - List_is_fail(fail) = true otherwise - forall l: List; List_is_fail(l) = false. - -(** Catches failed bitstring operations and reports whether failure occurred. *) -fun bitstring_is_fail(bitstring): bool -reduc - bitstring_is_fail(fail) = true otherwise - forall b: bitstring; bitstring_is_fail(b) = false. - -(** Checks whether or not two lists intersect. *) -letfun List_has_intersection(l0: List, l1: List) = - not(bitstring_is_fail(List_some_intersection(l0, l1))). - -#endif /* _LIST_PVL */ diff --git a/asylo/examples/secure_grpc/ekep_analysis/list_test.pv b/asylo/examples/secure_grpc/ekep_analysis/list_test.pv deleted file mode 100644 index 3aa8917a9..000000000 --- a/asylo/examples/secure_grpc/ekep_analysis/list_test.pv +++ /dev/null @@ -1,66 +0,0 @@ -(** -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. -*) - -#include "list.pvl" - -#include "test_helpers.pvl" - -free b0: bitstring. -free b1: bitstring. -free b2: bitstring. -free b3: bitstring. -free b4: bitstring. - -(** Checks that List_elem works on List1. *) -let TestElemList1() = - let l1_0 = List1(b0) in - EXPECT_TRUE(List_elem(b0, l1_0)); - EXPECT_FALSE(List_elem(b1, l1_0)). - -(** Checks that List_some_intersection works on List1, List1 arguments. *) -let TestFirstIntersection1_1() = - let l1_0 = List1(b0) in - let l1_1 = List1(b1) in - EXPECT_EQ(b0, List_some_intersection(l1_0, l1_0)). - -(** Checks that List_eq works on all List1 cases. *) -let TestEq1() = - let l1_0 = List1(b0) in - let l1_1 = List1(b1) in - EXPECT_TRUE(List_eq(l1_0, l1_0)); - EXPECT_FALSE(List_eq(l1_0, l1_1)). - -(** Checks that List_has_intersection works for List1. *) -let TestHasIntersection1() = - let l1_0 = List1(b0) in - let l1_0_again = List1(b0) in - let l1_1 = List1(b1) in - EXPECT_TRUE(List_has_intersection(l1_0, l1_0)); - EXPECT_TRUE(List_has_intersection(l1_0, l1_0_again)); - EXPECT_FALSE(List_has_intersection(l1_1, l1_0)). - -(** Checks that List_is_subset works for List1. *) -let TestIsSubset1() = - EXPECT_TRUE(List_is_subset(List1(b0), List1(b0))); - EXPECT_FALSE(List_is_subset(List1(b0), List1(b1))). - -process - ( TestElemList1() - | TestFirstIntersection1_1() - | TestEq1() - | TestHasIntersection1() - | TestIsSubset1() - ) diff --git a/asylo/examples/secure_grpc/ekep_analysis/named_tuples.pvl b/asylo/examples/secure_grpc/ekep_analysis/named_tuples.pvl deleted file mode 100644 index 77e8e5540..000000000 --- a/asylo/examples/secure_grpc/ekep_analysis/named_tuples.pvl +++ /dev/null @@ -1,95 +0,0 @@ -(** -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. -*) - -#ifndef _NAMED_TUPLES_PVL -#define _NAMED_TUPLES_PVL - -#define REDUCE_FORALL2(TypeName, field, result, var0, type0, var1, type1) \ - reduc forall var0: type0, var1: type1; \ - TypeName##_##field(Build##TypeName(var0, var1)) = result - -#define DEFINE_DATA_TYPE2(TypeName, var0, type0, var1, type1) \ - type TypeName. \ - fun Build##TypeName(type0, type1): TypeName [data]. \ - REDUCE_FORALL2(TypeName, var0, var0, var0, type0, var1, type1). \ - REDUCE_FORALL2(TypeName, var1, var1, var0, type0, var1, type1) - -#define REDUCE_FORALL3(TypeName, field, result, var0, type0, var1, type1, var2, type2) \ - reduc forall var0: type0, var1: type1, var2: type2; \ - TypeName##_##field(Build##TypeName(var0, var1, var2)) = result - -#define DEFINE_DATA_TYPE3(TypeName, var0, type0, var1, type1, var2, type2) \ - type TypeName. \ - fun Build##TypeName(type0, type1, type2): TypeName [data]. \ - REDUCE_FORALL3(TypeName, var0, var0, var0, type0, var1, type1, var2, type2). \ - REDUCE_FORALL3(TypeName, var1, var1, var0, type0, var1, type1, var2, type2). \ - REDUCE_FORALL3(TypeName, var2, var2, var0, type0, var1, type1, var2, type2) - -#define REDUCE_FORALL4(TypeName, field, result, var0, type0, var1, type1, var2, type2, var3, type3) \ - reduc forall var0: type0, var1: type1, var2: type2, var3: type3; \ - TypeName##_##field(Build##TypeName(var0, var1, var2, var3)) = result - -#define DEFINE_DATA_TYPE4(TypeName, var0, type0, var1, type1, var2, type2, var3, type3) \ - type TypeName. \ - fun Build##TypeName(type0, type1, type2, type3): TypeName [data]. \ - REDUCE_FORALL4(TypeName, var0, var0, var0, type0, var1, type1, var2, type2, var3, type3). \ - REDUCE_FORALL4(TypeName, var1, var1, var0, type0, var1, type1, var2, type2, var3, type3). \ - REDUCE_FORALL4(TypeName, var2, var2, var0, type0, var1, type1, var2, type2, var3, type3). \ - REDUCE_FORALL4(TypeName, var3, var3, var0, type0, var1, type1, var2, type2, var3, type3) - -#define REDUCE_FORALL5(TypeName, field, result, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4) \ - reduc forall var0: type0, var1: type1, var2: type2, var3: type3, var4: type4; \ - TypeName##_##field(Build##TypeName(var0, var1, var2, var3, var4)) = result - -#define DEFINE_DATA_TYPE5(TypeName, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4) \ - type TypeName. \ - fun Build##TypeName(type0, type1, type2, type3, type4): TypeName [data]. \ - REDUCE_FORALL5(TypeName, var0, var0, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4). \ - REDUCE_FORALL5(TypeName, var1, var1, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4). \ - REDUCE_FORALL5(TypeName, var2, var2, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4). \ - REDUCE_FORALL5(TypeName, var3, var3, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4). \ - REDUCE_FORALL5(TypeName, var4, var4, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4) - -#define REDUCE_FORALL6(TypeName, field, result, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4, var5, type5) \ - reduc forall var0: type0, var1: type1, var2: type2, var3: type3, var4: type4, var5: type5; \ - TypeName##_##field(Build##TypeName(var0, var1, var2, var3, var4, var5)) = result - -#define DEFINE_DATA_TYPE6(TypeName, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4, var5, type5) \ - type TypeName. \ - fun Build##TypeName(type0, type1, type2, type3, type4, type5): TypeName [data]. \ - REDUCE_FORALL6(TypeName, var0, var0, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4, var5, type5). \ - REDUCE_FORALL6(TypeName, var1, var1, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4, var5, type5). \ - REDUCE_FORALL6(TypeName, var2, var2, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4, var5, type5). \ - REDUCE_FORALL6(TypeName, var3, var3, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4, var5, type5). \ - REDUCE_FORALL6(TypeName, var4, var4, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4, var5, type5). \ - REDUCE_FORALL6(TypeName, var5, var5, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4, var5, type5) - -#define REDUCE_FORALL7(TypeName, field, result, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4, var5, type5, var6, type6) \ - reduc forall var0: type0, var1: type1, var2: type2, var3: type3, var4: type4, var5: type5, var6: type6; \ - TypeName##_##field(Build##TypeName(var0, var1, var2, var3, var4, var5, var6)) = result - -#define DEFINE_DATA_TYPE7(TypeName, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4, var5, type5, var6, type6) \ - type TypeName. \ - fun Build##TypeName(type0, type1, type2, type3, type4, type5, type6): TypeName [data]. \ - REDUCE_FORALL7(TypeName, var0, var0, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4, var5, type5, var6, type6). \ - REDUCE_FORALL7(TypeName, var1, var1, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4, var5, type5, var6, type6). \ - REDUCE_FORALL7(TypeName, var2, var2, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4, var5, type5, var6, type6). \ - REDUCE_FORALL7(TypeName, var3, var3, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4, var5, type5, var6, type6). \ - REDUCE_FORALL7(TypeName, var4, var4, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4, var5, type5, var6, type6). \ - REDUCE_FORALL7(TypeName, var5, var5, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4, var5, type5, var6, type6). \ - REDUCE_FORALL7(TypeName, var6, var6, var0, type0, var1, type1, var2, type2, var3, type3, var4, type4, var5, type5, var6, type6) - -#endif /* _NAMED_TUPLES_PVL */ diff --git a/asylo/examples/secure_grpc/ekep_analysis/named_tuples_test.pv b/asylo/examples/secure_grpc/ekep_analysis/named_tuples_test.pv deleted file mode 100644 index 137cf56a8..000000000 --- a/asylo/examples/secure_grpc/ekep_analysis/named_tuples_test.pv +++ /dev/null @@ -1,123 +0,0 @@ -(** -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. -*) - -#include "named_tuples.pvl" - -#include "list.pvl" -#include "test_helpers.pvl" - -type key. -type userData. - -DEFINE_EXPECT_EQ_FUN(key). -DEFINE_EXPECT_EQ_FUN(userData). - -free k: key. -free ud: userData. - -DEFINE_DATA_TYPE2(NamedTuple2, secretKey, key, context, userData). - -(** Checks that the accessors defined by DEFINE_DATA_TYPE2 work. *) -let TestDataType2() = - let nt = BuildNamedTuple2(k, ud) in - EXPECT(Eq_key(k, NamedTuple2_secretKey(nt))); - EXPECT(Eq_userData(ud, NamedTuple2_context(nt))). - -free d: bitstring. -free pk: key. -free t: bitstring. - -DEFINE_DATA_TYPE3(Assertion, description, bitstring, publicKey, key, - transcript, bitstring). - -let TestDataType3() = - let a = BuildAssertion(d, pk, t) in - EXPECT_EQ(d, Assertion_description(a)); - EXPECT(Eq_key(pk, Assertion_publicKey(a))); - EXPECT_EQ(t, Assertion_transcript(a)). - -(** Constants to use in the tests. *) -free version: bitstring. -free cipher: bitstring. -free protocol: bitstring. -free ad: bitstring. -free offer: bitstring. -free request: bitstring. -free c: bitstring. - -DEFINE_DATA_TYPE5(Params, ekepVersions, List, handshakeCiphers, List, - nextProtocols, List, offers, List, requests, List). - -(** Checks that the accessors defined by DEFINE_DATA_TYPE5 work. *) -let TestDataType5() = - let ev = List1(version) in - let hc = List1(cipher) in - let np = List1(protocol) in - let o = List1(offer) in - let r = List1(request) in - let p = BuildParams(ev, hc, np, o, r) in - EXPECT_TRUE(List_eq(ev, Params_ekepVersions(p))); - EXPECT_TRUE(List_eq(hc, Params_handshakeCiphers(p))); - EXPECT_TRUE(List_eq(np, Params_nextProtocols(p))); - EXPECT_TRUE(List_eq(o, Params_offers(p))); - EXPECT_TRUE(List_eq(r, Params_requests(p))). - -DEFINE_DATA_TYPE6(Precommit, ekepVersions, List, handshakeCiphers, List, - nextProtocols, List, aad, bitstring, offers, List, requests, - List). - -(** Checks that the accessors defined by DEFINE_DATA_TYPE6 work. *) -let TestDataType6() = - let ev = List1(version) in - let hc = List1(cipher) in - let np = List1(protocol) in - let o = List1(offer) in - let r = List1(request) in - let p = BuildPrecommit(ev, hc, np, ad, o, r) in - EXPECT_TRUE(List_eq(ev, Precommit_ekepVersions(p))); - EXPECT_TRUE(List_eq(hc, Precommit_handshakeCiphers(p))); - EXPECT_TRUE(List_eq(np, Precommit_nextProtocols(p))); - EXPECT_EQ(ad, Precommit_aad(p)); - EXPECT_TRUE(List_eq(o, Precommit_offers(p))); - EXPECT_TRUE(List_eq(r, Precommit_requests(p))). - -DEFINE_DATA_TYPE7(P7, ekepVersions, List, handshakeCiphers, List, - nextProtocols, List, aad, bitstring, offers, List, requests, - List, challenge, bitstring). - -(** Checks that the accessors defined by DEFINE_DATA_TYPE7 work. *) -let TestDataType7() = - let ev = List1(version) in - let hc = List1(cipher) in - let np = List1(protocol) in - let o = List1(offer) in - let r = List1(request) in - let p = BuildP7(ev, hc, np, ad, o, r, c) in - EXPECT_TRUE(List_eq(ev, P7_ekepVersions(p))); - EXPECT_TRUE(List_eq(hc, P7_handshakeCiphers(p))); - EXPECT_TRUE(List_eq(np, P7_nextProtocols(p))); - EXPECT_EQ(ad, P7_aad(p)); - EXPECT_TRUE(List_eq(o, P7_offers(p))); - EXPECT_TRUE(List_eq(r, P7_requests(p))); - EXPECT_EQ(c, P7_challenge(p)). - - -process - ( TestDataType2() - | TestDataType3() - | TestDataType5() - | TestDataType6() - | TestDataType7() ) diff --git a/asylo/examples/secure_grpc/ekep_analysis/run_proverif.sh b/asylo/examples/secure_grpc/ekep_analysis/run_proverif.sh deleted file mode 100755 index 6401298d1..000000000 --- a/asylo/examples/secure_grpc/ekep_analysis/run_proverif.sh +++ /dev/null @@ -1,52 +0,0 @@ -#!/bin/sh - -# Copyright 2022 Google LLC - -# Licensed under the Apache License, Version 2.0 (the "License"); -# you may not use this file except in compliance with the License. -# You may obtain a copy of the License at - - # https://www.apache.org/licenses/LICENSE-2.0 - -# Unless required by applicable law or agreed to in writing, software -# distributed under the License is distributed on an "AS IS" BASIS, -# WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -# See the License for the specific language governing permissions and -# limitations under the License. - -set -o errexit -set -o pipefail -set -o nounset - -if [[ "$#" != "1" ]]; then - echo "Usage: $0 " - exit 1 -fi - -readonly file="$1" -readonly TEMP_DIR="$(mktemp -d)" - -function cleanup() { - rm -rf "${TEMP_DIR}" -} - -if [[ -z "${PROVERIF_NO_CLEANUP:-}" ]]; then - trap cleanup EXIT -else - echo "Output in ${TEMP_DIR}" -fi - -if [[ -n "${PROVERIF_INTERACT:-}" ]]; then - cpp -DENABLE_DEBUG_FUNCTIONS -E "${file}" \ - | grep -v "^#" > "${TEMP_DIR}/${file}" -else - cpp -E "${file}" | grep -v "^#" > "${TEMP_DIR}/${file}" -fi - -if [[ ! -z "${PROVERIF_INTERACT:-}" ]]; then - proverif_interact "${TEMP_DIR}/${file}" -elif [[ ! -z "${PROVERIF_HTML_DIR:-}" ]]; then - proverif -color -html "${PROVERIF_HTML_DIR}" "${TEMP_DIR}/${file}" -else - proverif -color "${TEMP_DIR}/${file}" -fi diff --git a/asylo/examples/secure_grpc/ekep_analysis/style_guide.md b/asylo/examples/secure_grpc/ekep_analysis/style_guide.md deleted file mode 100644 index 265c6137d..000000000 --- a/asylo/examples/secure_grpc/ekep_analysis/style_guide.md +++ /dev/null @@ -1,298 +0,0 @@ -# ProVerif Style Guide - -## Overview - -ProVerif implements a version of the [applied -π-calculus](https://en.wikipedia.org/wiki/%CE%A0-calculus), a formal language -that is used to reason about cryptographic protocols (among other things). This -document provides guidelines for writing uniform, consistent ProVerif code. - -## Details - -### Spacing - -The rules for spacing try to remain close to Google style for other programming -languages. - -#### Indentation - -Use two spaces for indentation. - -```proverif -let MyProcess() = - new b: bitstring; - out(c, b). -``` - -#### Continued lines - -Indent line continuations with 4 spaces, to distinguish between continuations -and subsequent lines in a new scope. - -```proverif -if x <> ComputeSomeReallyLongValue(theFirstVariable, theSecondVariable, - theThirdVariable) then ( - new b0: bitstring; - out(c, b0) -) else ( - new b1: bitstring; - out(c, b1) -). -``` - -The second half of a reduction should always be written on a new line, for -clarity, so it should only be indented by two spaces, not four. - -```proverif -fun fst((*first=*)bitstring, (*second=*)bitstring): (*element=*)bitstring -reduc - forall x0: bitstring, x1: bitstring; - fst(x0, x1) = x0. -``` - -The following version indents by too many spaces. - -```proverif {.bad} -fun fst((*first=*)bitstring, (*second=*)bitstring): (*element=*)bitstring -reduc - forall x0: bitstring, x1: bitstring; - (* Incorrect 4-space indentation. *) - fst(x0, x1) = x0. -``` - -You may also align continued lines for clarity. In the following example, the -query aligns the `event` expressions in the same parenthesized expression. - -```proverif {.good} -query x: FieldElt, y: FieldElt, idS: Identity, idC: Identity; - (event(ClientKey(x)) && event(ServerKey(y)) && - event(ServerBinds(exp(g, mul(x, y)), idC, idS))) ==> - event(ClientBinds(exp(g, mul(x, y)), idC, idS)). -``` - -#### Alignment - -Do not add horizontal space to align columns of text. - -```proverif -const d0: bitstring [data]. -const longerName: bitstring [data]. -``` - -The following version correctly keeps regular spacing. - -```proverif -const d0: bitstring [data]. -const longerName: bitstring [data]. -``` - -#### Type annotations - -Separate the type name from the variable name and colon with one space. - -```proverif -type Key. -new k: Key. - -in(c, (k: key, m: bitstring)). -``` - -The following version does not include a space between the variable name, the -colon, and the type. - -```proverif -type Key. -new k:Key. -``` - -### Naming - -ProVerif has several kinds of non-keyword names: functions, events, processes, -variables. These names use the following styles - -- PascalCase - - types (`TypeName`) - - events (`EventName`) - - processes (`ProcessName`) -- camelCase - - variables (`variableName`) - - arguments (`argumentName`) - - functions (`functionName`) - -#### Acronyms and initialisms - -This style guide follows the main Google convention for naming acronyms and -initialisms: treat them like words. This decision means that acronyms and -initialisms do not always have consistent case, but it matches the majority of -the languages used at Google. - -```proverif -type AesKey. - -let AesReceiver() = - in(c, (aesUserKey: AesKey)). -``` - -The following incorrect version uses a style that is more like Go. - -```proverif -type AESKey. - -let AESReceiver() = - in(c, (aesUserKey: AESKey)). -``` - -### Comments - -#### Documentation comments - -Comments on types, events, processes, and functions should follow OCaml -documentation style: start the comment with two stars instead of one. - -```proverif -(** Computes an exponentiation of |base|^|exponent|. *) -fun exp((*base=*)GroupElt, (*exponent=*)FieldElt): GroupElt. -``` - -```proverif -(* Incorrect single-star comment on a function. *) - -(* Computes an exponentiation of |base|^|exponent|. *) -fun exp((*base=*)GroupElt, (*exponent=*)FieldElt): GroupElt. -``` - -#### Process and function comments - -Each process should have a documentation comment that starts with a verb in the -present tense. This is analogous to function comments in Google style for -languages like C++. - -```proverif -(** Computes an exponentiation of |base|^|exponent|. *) -fun exp((*base=*)GroupElt, (*exponent=*)FieldElt): GroupElt. - -(** Sends a fresh bitstring on channel |c|. *) -let Server() = - new value: bitstring; - out(c, value). -``` - -#### Event comments - -ProVerif events are critical to its security modeling, and they have -correspondingly high requirements for the clarity of their comments. Event -comments should be formulated as "says" statements: a given principal "says" a -given fact. This style helps interpret the comments, especially in the context -of queries. - -```proverif -(** The server says that a |secret| comes from communication between itself -(|serverId|) and |clientId|. *) -event ServerBinds((*secret=*)GroupElt, (*clientId=*)Identity, - (*serverId=*)Identity). -``` - -The following incorrect example uses a function-style comment to describe an -event. - -```proverif -(* Incorrect function-style comment. *) - -(** Binds a secret to identities. *) -event ServerBinds((*secret=*)GroupElt, (*clientId=*)Identity, - (*serverId=*)Identity). -``` - -#### End-of-line comments - -As in other Google style guides, end-of-line comments should be separated from -the end of the line of code by 2 spaces. - -```proverif -new k: Key. (* A signing key for the server. *) -``` - -The following incorrect example only uses one space between the declaration and -its comment. - -```proverif {.bad} -new k: Key. (* A signing key for the server. *) -``` - -#### Bitstring comments - -ProVerif protocols often use uninterpreted bitstrings, and these can be hard -to interpret, especially in function definitions, where no argument names are -given. So, use inline comments to add argument names for all bitstring -arguments. Inline comments are allowed for other types if they improve the -readability of the function definition. - -```proverif -fun sign(Key, (*message=*)bitstring): (*signature=*)bitstring. -``` - -The following definitions demonstrate incorrect ways to write comments in -functions. - -```proverif -(* Superfluous comment on key repeats the type name. *) -fun sign((*key=*)Key, (*message=*)bitstring): (*signature=*)bitstring. - -(* Lack of comments makes it hard to interpret. *) -fun sign(Key, bitstring): bitstring. -``` - -### Specific Constructions - -#### Reductions - -The set of possible reductions of a function are given after that function. If -the reduction only has one case, then it can be put on the same line as the -`reduc` keyword. Otherwise, it should be put on the next line, indented by two -spaces. - -All instances of the `otherwise` keyword should be at the end of the line so -that the variable statements `forall` line up. - -```proverif -fun sign(Key, (*message=*)bitstring): (*signature=*)bitstring. - -fun checkSign(key, (*signature=*)bitstring): bool -reduc - forall k: Key, m: bitstring; - checkSign(publicKey(k), sign(k, m)) = true otherwise - forall k: Key, s: bitstring; - checkSign(k, s) = false. -``` - -#### Queries - -Queries often have long lines. They are also conceptually similar to reductions -and should be visually similar. Like the `forall` in a reduction, the query -may be given on a single line if it is short enough. Otherwise, the statement of -the query should be given on a new line, indented with 2 spaces. The arrow in -the query (`==>`) should be at the end of the line. - -```proverif -query x: FieldElt, y: FieldElt, idS: Identity, idC: Identity; - (event(ClientKey(x)) && event(ServerKey(y)) && - event(ServerBinds(exp(g, mul(x, y)), idC, idS))) ==> - event(ClientBinds(exp(g, mul(x, y)), idC, idS)). -``` - -The following examples demonstrate incorrect ways to write queries. - -```proverif -(* Incorrect 4-space indentation for the query statement. *) -query x: FieldElt, y: FieldElt, idS: Identity, idC: Identity; - (event(ClientKey(x)) && event(ServerKey(y)) && - event(ServerBinds(exp(g, mul(x, y)), idC, idS))) ==> - event(ClientBinds(exp(g, mul(x, y)), idC, idS)). - -(* Incorrect placement of the arrow. *) -query x: FieldElt, y: FieldElt, idS: Identity, idC: Identity; - (event(ClientKey(x)) && event(ServerKey(y)) && - event(ServerBinds(exp(g, mul(x, y)), idC, idS))) - ==> - event(ClientBinds(exp(g, mul(x, y)), idC, idS)). -``` diff --git a/asylo/examples/secure_grpc/ekep_analysis/test_helpers.pvl b/asylo/examples/secure_grpc/ekep_analysis/test_helpers.pvl deleted file mode 100644 index adbb4a6df..000000000 --- a/asylo/examples/secure_grpc/ekep_analysis/test_helpers.pvl +++ /dev/null @@ -1,63 +0,0 @@ -(** -Copyright 2022 Google LLC - -Licensed under the Apache License, Version 2.0 (the "License"); -you may not use this file except in compliance with the License. -You may obtain a copy of the License at - - https://www.apache.org/licenses/LICENSE-2.0 - -Unless required by applicable law or agreed to in writing, software -distributed under the License is distributed on an "AS IS" BASIS, -WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. -See the License for the specific language governing permissions and -limitations under the License. -*) - -#ifndef _TEST_HELPERS_PVL -#define _TEST_HELPERS_PVL - -(** A fixed channel that the adversary listens on to get Success and Failure -messages. *) -channel test_channel. - -(** Success is a constant used by the test code; it represents a successful -test. *) -free Success: bitstring [private]. - -(** Failure is a constant used by the test code; it represents a failed test. *) -free Failure: bitstring [private]. - -(** A test succeeds if the attacker cannot get the Failure bitstring. *) -query attacker(Failure). - -(** Converts a predicate into Success/Failure. *) -letfun Expect(predicate: bool) = - if predicate then Success else Failure. - -(** Outputs Success/Failure on test_channel if the predicate is true. *) -#define EXPECT_TRUE(p) \ - out(test_channel, Expect(p)) - -(** Outputs Success/Failure on test_channel if the predicate is false. *) -#define EXPECT_FALSE(p) \ - out(test_channel, Expect(not(p))) - -(** Defines a function Eq_ that works in tests and converts equality to -Success/Failure. *) -#define DEFINE_EXPECT_EQ_FUN(t) \ - letfun Eq_##t(lhs: t, rhs: t) = \ - if lhs = rhs then Success else Failure - -(** Converts equality to Success/Failure. *) -letfun Eq_bitstring(lhs: bitstring, rhs: bitstring) = - if lhs = rhs then Success else Failure. - -(** Expects the truth of a general predicate, using Eq_* *) -#define EXPECT(predicate) \ - out(test_channel, predicate) - -(** EXPECT_EQ is EXPECT on bitstrings. *) -#define EXPECT_EQ(lhs, rhs) EXPECT(Eq_bitstring(lhs, rhs)) - -#endif /* _TEST_HELPERS_PVL */