Skip to content

Instantly share code, notes, and snippets.

@jadephilipoom

jadephilipoom/Combinators.v

Last active October 7, 2019 17:07
Show Gist options
  • Save jadephilipoom/d95b83b1071f7e2ce7f69132b30d5931 to your computer and use it in GitHub Desktop.
Save jadephilipoom/d95b83b1071f7e2ce7f69132b30d5931 to your computer and use it in GitHub Desktop.
Download ZIP
Record of the "protocols" branch of fiat-crypto
Raw
Combinators.v
Require Import Coq.Lists.List.
Create HintDb trace_combinators discriminated.
Fixpoint holds_of_messages_around_nth_messages_matching_aux
(is_n : nat -> Prop)
(if_none_found : Prop)
{T}
(matcher : T -> Prop)
(property : list T -> T -> list T -> Prop)
(pre_trace : list T)
(trace : list T)
: Prop
:= match trace with
| nil => if_none_found
| m :: ms
=> (matcher m ->
(is_n 0 -> property pre_trace m ms)
/\ holds_of_messages_around_nth_messages_matching_aux
(fun n' => is_n (S n'))
(is_n 0 \/ if_none_found)
matcher
property
(pre_trace ++ m::nil)
ms)
/\ (~matcher m
-> holds_of_messages_around_nth_messages_matching_aux
is_n
if_none_found
matcher property (pre_trace ++ (m::nil)) ms)
end%list.
Class reverse_search := do_reverse : bool.
Definition holds_of_messages_around_nth_messages_matching
{rev : reverse_search}
(is_n : nat -> Prop)
(if_none_found : Prop)
{T}
(matcher : T -> Prop)
(property : list T -> T -> list T -> Prop)
(trace : list T)
: Prop
:= holds_of_messages_around_nth_messages_matching_aux
is_n if_none_found
matcher
(fun pre m post
=> if rev
then property (List.rev post) m (List.rev pre)
else property pre m post)
nil
(if rev then List.rev trace else trace).
Hint Unfold holds_of_messages_around_nth_messages_matching : trace_combinators.
Notation holds_of_messages_around_nth_message_matching n
:= (holds_of_messages_around_nth_messages_matching (fun n' => n = n') True).
Definition holds_of_messages_before_nth_messages_matching
{rev : reverse_search}
(is_n : nat -> Prop)
(if_none_found : Prop)
{T}
(matcher : T -> Prop)
(property : list T -> T -> Prop)
(trace : list T)
: Prop
:= holds_of_messages_around_nth_messages_matching
is_n if_none_found matcher (fun before m after => property before m) trace.
Hint Unfold holds_of_messages_before_nth_messages_matching : trace_combinators.
Notation holds_of_messages_before_nth_message_matching n
:= (holds_of_messages_before_nth_messages_matching (fun n' => n = n') True).
Notation holds_of_messages_before_all_messages_matching
:= (holds_of_messages_before_nth_messages_matching (fun _ => True) True).
Definition holds_of_nth_messages_matching
{rev : reverse_search}
(is_n : nat -> Prop)
(if_none_found : Prop)
{T}
(matcher : T -> Prop)
(property : T -> Prop)
(trace : list T)
: Prop
:= holds_of_messages_around_nth_messages_matching
is_n if_none_found matcher (fun _ m _=> property m) trace.
Hint Unfold holds_of_nth_messages_matching : trace_combinators.
Definition holds_of_nth_messages_matching_if_they_exist {rev} is_n {T}
:= holds_of_nth_messages_matching (rev:=rev) is_n True (T:=T).
Hint Unfold holds_of_nth_messages_matching_if_they_exist : trace_combinators.
Definition holds_of_nth_message_matching {rev} n {T}
:= @holds_of_nth_messages_matching rev (fun n' => n = n') True T.
Hint Unfold holds_of_nth_message_matching : trace_combinators.
Definition holds_of_nth_to_last_message_matching n {T}
:= holds_of_nth_message_matching n (rev:=true) (T:=T).
Hint Unfold holds_of_nth_to_last_message_matching : trace_combinators.
Definition holds_of_all_messages_matching {T}
:= @holds_of_nth_messages_matching false (fun _ => True) True T.
Hint Unfold holds_of_all_messages_matching : trace_combinators.
Definition holds_of_all_messages {T}
:= @holds_of_all_messages_matching T (fun _ => True).
Hint Unfold holds_of_all_messages : trace_combinators.
Definition holds_of_nth_message_matching_which_must_exist {rev} n {T}
:= @holds_of_nth_messages_matching rev (fun n' => n = n') False T.
Hint Unfold holds_of_nth_message_matching_which_must_exist : trace_combinators.
Definition holds_of_nth_to_last_message_matching_which_must_exist n {T}
:= holds_of_nth_message_matching_which_must_exist n (rev:=true) (T:=T).
Hint Unfold holds_of_nth_to_last_message_matching_which_must_exist : trace_combinators.
Definition nth_message_matching_exists {rev} n {T} matcher
:= @holds_of_nth_message_matching_which_must_exist rev n T matcher (fun _ => True).
Hint Unfold nth_message_matching_exists : trace_combinators.
Definition holds_of_messages_after_nth_messages_matching
{rev : reverse_search}
(is_n : nat -> Prop)
(if_none_found : Prop)
{T}
(matcher : T -> Prop)
(property : T -> list T -> Prop)
(trace : list T)
: Prop
:= holds_of_messages_around_nth_messages_matching
is_n if_none_found matcher (fun before m after => property m after) trace.
Hint Unfold holds_of_messages_after_nth_messages_matching : trace_combinators.
Notation holds_of_messages_after_nth_message_matching n
:= (holds_of_messages_after_nth_messages_matching (fun n' => n = n') True).
Definition on_input {input output T} (f : input -> T) : input * output -> T
:= fun '(i, o) => f i.
Hint Unfold on_input : trace_combinators.
Definition on_output {input output T} (f : output -> T) : input * output -> T
:= fun '(i, o) => f o.
Hint Unfold on_output : trace_combinators.
Definition holds_of_all_messages_after_nth_messages_matching_gen
{rev : reverse_search}
(include_nth_msg : bool)
(is_n : nat -> Prop)
(if_none_found : Prop)
{T}
(matcher : T -> Prop)
(property : T (* nth_msg *) -> T (* other message *) -> Prop)
(trace : list T)
: Prop
:= holds_of_messages_after_nth_messages_matching
is_n
if_none_found
matcher
(fun m after
=> List.Forall (property m) (if include_nth_msg then m::after else after))
trace.
Hint Unfold holds_of_all_messages_after_nth_messages_matching_gen : trace_combinators.
Notation holds_of_all_messages_after_nth_messages_matching
:= (holds_of_all_messages_after_nth_messages_matching_gen true).
Notation holds_of_all_messages_after_nth_message_matching n
:= (holds_of_all_messages_after_nth_messages_matching (fun n' => n = n') True).
Notation holds_of_all_messages_strictly_after_nth_messages_matching
:= (holds_of_all_messages_after_nth_messages_matching_gen false).
Notation holds_of_all_messages_strictly_after_nth_message_matching n
:= (holds_of_all_messages_strictly_after_nth_messages_matching (fun n' => n = n') True).
Definition holds_of_some_message_before_nth_messages_matching_gen
{rev : reverse_search}
(include_nth_message : bool)
(is_n : nat -> Prop)
(if_none_found : Prop)
{T}
(matcher : T -> Prop)
(property : T (* nth_msg *) -> T (* other message *) -> Prop)
(trace : list T)
: Prop
:= holds_of_messages_before_nth_messages_matching
is_n
if_none_found
matcher
(fun before m
=> List.Exists (property m) (if include_nth_message then (before ++ (m::nil))%list else before))
trace.
Hint Unfold holds_of_some_message_before_nth_messages_matching_gen : trace_combinators.
Notation holds_of_some_message_before_nth_messages_matching
:= (holds_of_some_message_before_nth_messages_matching_gen true).
Notation holds_of_some_message_before_nth_message_matching n
:= (holds_of_some_message_before_nth_messages_matching (fun n' => n = n') True).
Notation holds_of_some_message_strictly_before_nth_messages_matching
:= (holds_of_some_message_before_nth_messages_matching_gen false).
Notation holds_of_some_message_strictly_before_nth_message_matching n
:= (holds_of_some_message_strictly_before_nth_messages_matching (fun n' => n = n') True).
Global Instance default_rev : reverse_search := false.
Raw
git_log.txt
commit 39c8e50a0509bdf300fd65d44355407ca2d63895
Author: Jason Gross <[email protected]>
Date: Wed Sep 20 21:35:35 2017 -0400
WIP on SpecWithAPI
_CoqProject | 1 +
src/Protocols/SigmaKeyExchange/Combinators.v | 175 +++--
src/Protocols/SigmaKeyExchange/SpecWithAPI.v | 731 +++++++++++++++++++++
.../SigmaKeyExchange/SpecWithSanitization.v | 58 +-
4 files changed, 885 insertions(+), 80 deletions(-)
commit ab3943b6873b35c00e120b965db0fd53ff66cffd
Author: Jason Gross <[email protected]>
Date: Wed Sep 20 15:08:39 2017 -0400
Add src/Protocols/SigmaKeyExchange/SpecWithSanitization.v
_CoqProject | 1 +
.../SigmaKeyExchange/SpecWithSanitization.v | 382 +++++++++++++++++++++
2 files changed, 383 insertions(+)
commit ddf8c19f8c84f523fd4976e92163be85a9d72be6
Author: Jason Gross <[email protected]>
Date: Wed Sep 20 13:36:18 2017 -0400
Factor out combinators
_CoqProject | 1 +
src/Protocols/SigmaKeyExchange/Combinators.v | 115 +++++++++++++++
src/Protocols/SigmaKeyExchange/Spec.v | 212 +++++++++------------------
3 files changed, 184 insertions(+), 144 deletions(-)
commit 0196c5b3fbc8da27e6ccf87589e29797b6a5ba91
Author: Jason Gross <[email protected]>
Date: Wed Aug 30 19:58:15 2017 -0400
More stateful constraints in Coq
src/Protocols/SigmaKeyExchange/Spec.v | 92 +++++++++++++++++++++++++++++++----
1 file changed, 83 insertions(+), 9 deletions(-)
commit 56b9a1095dea486107cb1cdaaa4e4eb8290dd340
Author: Jason Gross <[email protected]>
Date: Wed Aug 30 19:05:42 2017 -0400
Spec more of Sigma KE
src/Protocols/SigmaKeyExchange/Spec.v | 273 ++++++++++++++++++++++++++++++++--
1 file changed, 258 insertions(+), 15 deletions(-)
commit 77c3f7321d6e32b39221e48f009b132762333f5f
Author: Jason Gross <[email protected]>
Date: Wed Aug 30 17:48:06 2017 -0400
Add TLS Secrets notes
src/Protocols/TLSSecretsNotes.txt | 14 ++++++++++++++
1 file changed, 14 insertions(+)
commit a76c80b4873257ac108f8a82bfd920fa2ac28321
Author: Jason Gross <[email protected]>
Date: Sun Aug 27 18:44:05 2017 -0400
WIP on SigmaKeyExchange
src/Protocols/SigmaKeyExchange/Spec.v | 53 +++++++++++++++++++++++++++++++++++
1 file changed, 53 insertions(+)
commit ee54e8df037e860078466ea6af0f729e0ee86f17
Author: Jason Gross <[email protected]>
Date: Sun Aug 27 16:36:33 2017 -0400
Add Sigma Key Exchange spec
_CoqProject | 2 ++
src/Protocols/SigmaKeyExchange/Spec.v | 28 ++++++++++++++++++++++++++++
2 files changed, 30 insertions(+)
commit 9417aa435414b61a47695121c35f75751d2db8c8
Author: Jason Gross <[email protected]>
Date: Sat Aug 26 19:37:49 2017 -0400
More spec'ing constraints
src/Protocols/TLS13/Spec.v | 205 +++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 205 insertions(+)
commit 76cacf84a81fb9f66db9a7a10be76974f20e6b18
Author: Jason Gross <[email protected]>
Date: Fri Aug 25 18:33:55 2017 -0400
Add Spec.v for tls 1.3, start picking out bits to formalize
src/Protocols/TLS13/Spec.v | 430 +++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 430 insertions(+)
commit 3b189e42114e2440ea5458e9e23cac5d41876a67
Author: Jason Gross <[email protected]>
Date: Wed Aug 23 17:59:17 2017 -0400
Add another comment
src/Protocols/TLS13/TraceSynthesis.v | 4 ++++
1 file changed, 4 insertions(+)
commit 071697dfaecbc4ad8b5f3a9185299d605cdcf7f1
Author: Jason Gross <[email protected]>
Date: Wed Aug 23 17:41:58 2017 -0400
Add some standing questions
src/Protocols/TLS13/TraceSynthesis.v | 8 ++++++++
1 file changed, 8 insertions(+)
commit 24e98b82263e33b4bf99f5177d9c6843161d72ce
Author: Jason Gross <[email protected]>
Date: Sun Aug 13 17:43:46 2017 -0400
A bit more work on modularity in trace specs
src/Protocols/TLS13/Structures.v | 2 +-
src/Protocols/TLS13/TraceSynthesis.v | 29 +++++++++++++++++++++++++++++
2 files changed, 30 insertions(+), 1 deletion(-)
commit 480f0f374bc408beb649e60af99c4b40ff1a93af
Author: Jason Gross <[email protected]>
Date: Sun Aug 13 17:26:42 2017 -0400
Fix a missing import
src/Protocols/TLS13/TraceSynthesis.v | 5 +++++
1 file changed, 5 insertions(+)
commit a2c7f518edad6026e36fb291d17a5033db8e0cd1
Author: Jason Gross <[email protected]>
Date: Sun Aug 13 17:25:37 2017 -0400
Split up Trace.v
_CoqProject | 1 +
src/Protocols/TLS13/TraceSynthesis.v | 211 +++++++++++++++++++++++++++++++++++
src/Spec/Trace.v | 209 ----------------------------------
3 files changed, 212 insertions(+), 209 deletions(-)
commit 28440cf0aa68d160f0d5fa797f1be39ce2cf9842
Author: Jason Gross <[email protected]>
Date: Sun Aug 13 17:14:28 2017 -0400
add preliminary structure definitions for ClientHello, ServerHello
_CoqProject | 1 +
src/Protocols/TLS13/Structures.v | 201 +++++++++++++++++++++++++++++++++++++++
2 files changed, 202 insertions(+)
commit a2a0e3dd2f50917e23821075b901548fac1e70fd
Author: Jason Gross <[email protected]>
Date: Sun Aug 13 17:11:38 2017 -0400
More WIP on synthesis
src/Spec/Trace.v | 127 ++++++++++++++++++++++++++++++++++++++++++++++---------
1 file changed, 106 insertions(+), 21 deletions(-)
commit 0f2dd3cc8931719cffa69e280e8c5ee88a4754cb
Author: Jason Gross <[email protected]>
Date: Sun Aug 13 16:28:10 2017 -0400
Finish a proof in Trace.v
src/Spec/Trace.v | 97 ++++++++++++++++++++++++++++++++++++++++++--------------
1 file changed, 74 insertions(+), 23 deletions(-)
commit da4deb8c692baa51cecb6c5d6378a2448d85a692
Author: Jason Gross <[email protected]>
Date: Fri Aug 11 21:30:41 2017 -0400
More WIP on TLS
src/Spec/Trace.v | 38 +++++++++++++++++++++++++++++++-------
1 file changed, 31 insertions(+), 7 deletions(-)
commit 25303a1d1b8b59da7eb061a572ec6e257427e21c
Author: Jason Gross <[email protected]>
Date: Fri Aug 11 21:02:02 2017 -0400
WIP on trace specifications
_CoqProject | 1 +
src/Spec/Trace.v | 65 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++
2 files changed, 66 insertions(+)
commit 9ec08a1cdb368467e5e79bce840686ad845b125c
Author: Jason Gross <[email protected]>
Date: Sat Sep 16 04:22:21 2017 -0400
Check if /sys/devices/system/cpu/intel_pstate/no_turbo exists before searching it
etc/machine.sh | 6 +++++-
1 file changed, 5 insertions(+), 1 deletion(-)
Raw
Spec.v
(* from https://raw.githubusercontent.com/tlswg/tls13-spec/master/draft-ietf-tls-tls13.md *)
(**
# Handshake Protocol
The handshake protocol is used to negotiate the security parameters
of a connection. Handshake messages are supplied to the TLS record layer, where
they are encapsulated within one or more TLSPlaintext or TLSCiphertext structures, which are
processed and transmitted as specified by the current active connection state.
%%% Handshake Protocol
enum {
hello_request_RESERVED(0),
client_hello(1),
server_hello(2),
hello_verify_request_RESERVED(3),
new_session_ticket(4),
end_of_early_data(5),
hello_retry_request(6),
encrypted_extensions(8),
certificate(11),
server_key_exchange_RESERVED(12),
certificate_request(13),
server_hello_done_RESERVED(14),
certificate_verify(15),
client_key_exchange_RESERVED(16),
finished(20),
key_update(24),
message_hash(254),
(255)
} HandshakeType;
struct {
HandshakeType msg_type; /* handshake type */
uint24 length; /* bytes in message */
select (Handshake.msg_type) {
case client_hello: ClientHello;
case server_hello: ServerHello;
case end_of_early_data: EndOfEarlyData;
case hello_retry_request: HelloRetryRequest;
case encrypted_extensions: EncryptedExtensions;
case certificate_request: CertificateRequest;
case certificate: Certificate;
case certificate_verify: CertificateVerify;
case finished: Finished;
case new_session_ticket: NewSessionTicket;
case key_update: KeyUpdate;
};
} Handshake;
Protocol messages MUST be sent in the order defined in
{{the-transcript-hash}} and shown in the diagrams in {{protocol-overview}}.
A peer which receives a handshake message in an unexpected order
MUST abort the handshake with an "unexpected_message" alert.
*)
(* HOW TO ENCODE: Have a function [list of trace-seen-so-far -> list
(sender * HandshakeType)]; encode the list of messages from
{{the-transcript-hash}}; require that one list be a sublist of the
other one. *)
(**
New handshake message types are assigned by IANA as described in
{{iana-considerations}}.
## Key Exchange Messages
The key exchange messages are used to determine the security capabilities
of the client and the server and to establish shared secrets including
the traffic keys used to protect the rest of the handshake and the data.
### Cryptographic Negotiation
In TLS, the cryptographic negotiation proceeds by the client offering the
following four sets of options in its ClientHello:
*)
(* Constraint: Session starts with ClientHello *)
(**
- A list of cipher suites which indicates the AEAD algorithm/HKDF hash
pairs which the client supports.
*)
(* Client Constraint: Per-Connection decision of list of which suites are
supported; list in ClientHello must be Leibniz equal to the list of
supported suites. *)
(**
- A "supported_groups" ({{negotiated-groups}}) extension which indicates the (EC)DHE groups
which the client supports and a "key_share" ({{key-share}}) extension which contains
(EC)DHE shares for some or all of these groups.
*)
(* Client Constraint: Per-Connection decision of list of which
groups/key_share are supported; list in ClientHello must be Leibniz
equal to the list of supported groups/key_share. *)
(* Note: key_share is optional/situation-dependent *)
(* TODO: report issue with wording here *)
(**
- A "signature_algorithms" ({{signature-algorithms}}) extension which indicates the signature
algorithms which the client can accept.
*)
(* Client Constraint: Per-Connection decision of list of which
signature_algorithms are supported; list in ClientHello must be
Leibniz equal to the list chosen. *)
(**
- A "pre_shared_key" ({{pre-shared-key-extension}}) extension which
contains a list of symmetric key identities known to the client and a
"psk_key_exchange_modes" ({{pre-shared-key-exchange-modes}})
extension which indicates the key exchange modes that may be used
with PSKs.
*)
(* Client constraint: long-lived (across connections) global state of
which key identities are known. Note: optional *)
(* How to implement: Global (cross-connection) list of "additions to
pre_shared_key" up to this point (up to the current message); when
filtering multi-connection traces for a particular connection, also
filter the list of additions. Pass in this list of additions, as well
as the initial list (which may or may not be empty), at the
ClientHello, if you send pre_shared_key, the set you send must be a
subset (sublist up to permutation) of the initial list + the list of
additions at the point of the client hello. *)
(**
If the server does not select a PSK, then the first three of these
options are entirely orthogonal: the server independently selects a
cipher suite, an (EC)DHE group and key share for key establishment,
and a signature algorithm/certificate pair to authenticate itself to
the client. If there is no overlap between the received "supported_groups"
and the groups supported by the server then the server MUST abort the
handshake with a "handshake_failure" or an "insufficient_security" alert.
*)
(* Note: these constraints don't mandate a ServerHello; they mandate
that any ServerHello you do send agrees with these decisions. *)
(* Server constraint: per-connection decision: pick option PSK; pick
option (suite+group+key share+sig algorithm/cert pair) *)
(* Server constraint: if you pick group / key_share, the group &
key share MUST be in the lists given by the client. *)
(* Server constraint: if you pick PSK, then it must be in the client's
list *)
(* Server constraint: if PSK is None and other stuff is None, then you
MUST abort with handshake_failure or with insufficient_security. *)
(* Note: The server is not actually required to make the choice
independently, is it? *)
(**
If the server selects a PSK, then it MUST also select a key
establishment mode from the set indicated by client's
"psk_key_exchange_modes" extension (at present, PSK alone or with (EC)DHE). Note
that if the PSK can be used without (EC)DHE then non-overlap in the
"supported_groups" parameters need not be fatal, as it is in the
non-PSK case discussed in the previous paragraph.
*)
(* Server constraint: per-connection choice of option PSK-mode; if PSK
is not none and client presented a psk_key_exchange_modes list, then
the server MUST send a PSK mode that's in the list *)
(**
If the server selects an (EC)DHE group and the client did not offer a
compatible "key_share" extension in the initial ClientHello, the server MUST
respond with a HelloRetryRequest ({{hello-retry-request}}) message.
*)
(* Server constraint: per-connection choice of option group; if the
group has no compatible key_share, next message must be
HelloRetryRequest with the selected group *)
(**
If the server successfully selects parameters and does not require a
HelloRetryRequest, it indicates the selected parameters in the ServerHello as
follows:
*)
(* TODO: Request clarification: can the server send a
HelloRetryRequest with a group for which the client did, in fact,
offer a compatible "key_share" extension? Or is it required to send a
ServerHello if it can, for the selected group? *)
(**
- If PSK is being used, then the server will send a
"pre_shared_key" extension indicating the selected key.
*)
(* Server constraint: ^ *)
(**
- If PSK is not being used, then (EC)DHE and certificate-based
authentication are always used.
*)
(* Server constraint: ^ *)
(**
- When (EC)DHE is in use, the server will also provide a
"key_share" extension.
*)
(* Server constraint: ^ *)
(**
- When authenticating via a certificate, the server will send
the Certificate ({{certificate}}) and CertificateVerify
({{certificate-verify}}) messages. In TLS 1.3
as defined by this document, either a PSK or a certificate
is always used, but not both. Future documents may define how
to use them together.
*)
(* Server constraint: If PSK is None (c.f. bullet point 2), then, if
server Finished appears in the transcript, Certificate and
CertificateVerify must be sent by the server before that *)
(**
If the server is unable to negotiate a supported set of parameters
(i.e., there is no overlap between the client and server parameters),
it MUST abort the handshake with either
a "handshake_failure" or "insufficient_security" fatal alert
(see {{alert-protocol}}).
*)
(* Server constraint: If you send anything other than ServerHello or
HelloRetryRequest, then it must be an abort with handshake_failure or
insufficient_security *)
(**
### Client Hello
When a client first connects to a server, it is REQUIRED to send the
ClientHello as its first message. The client will also send a
ClientHello when the server has responded to its ClientHello with a
HelloRetryRequest. In that case, the client MUST send the same
ClientHello (without modification) except:
*)
(* Duplicate Client Constraint: Session starts with ClientHello *)
(* Client Constraint: If you get HelloRetryRequest, MUST respond with
ClientHello if you respond at all *)
(**
- If a "key_share" extension was supplied in the HelloRetryRequest,
replacing the list of shares with a list containing a single
KeyShareEntry from the indicated group.
*)
(* Client Constraint: ^ *)
(**
- Removing the "early_data" extension ({{early-data-indication}}) if one was
present. Early data is not permitted after HelloRetryRequest.
*)
(* Client Constraint: ^ *)
(**
- Including a "cookie" extension if one was provided in the
HelloRetryRequest.
*)
(* Client Constraint: ^ (Note: Required) *)
(**
- Updating the "pre_shared_key" extension if present by
recomputing the "obfuscated_ticket_age" and binder values
and (optionally) removing
any PSKs which are incompatible with the server's indicated
cipher suite.
*)
(* Client Constraint: Computed pre_shared_key must be re-computed with
new randomness and with the same inputs as before, modulo possibly
removing incompatible keys. *)
(**
Because TLS 1.3 forbids renegotiation, if a server has negotiated TLS
1.3 and receives a ClientHello at any other time, it MUST terminate
the connection with an "unexpected_message" alert.
*)
(* Server constraint: If there's a ClientHello after anything other
than connection start or HelloRetryRequest, abort with
unexpected_message. Note that aborting (but not the alert?) is
mandated by transcript hash. *)
(**
If a server established a TLS connection with a previous version of TLS
and receives a TLS 1.3 ClientHello in a renegotiation, it MUST retain the
previous protocol version. In particular, it MUST NOT negotiate TLS 1.3.
*)
(* Note: We're not implementing any older protocols *)
(**
Structure of this message:
%%% Key Exchange Messages
uint16 ProtocolVersion;
opaque Random[32];
uint8 CipherSuite[2]; /* Cryptographic suite selector */
struct {
ProtocolVersion legacy_version = 0x0303; /* TLS v1.2 */
Random random;
opaque legacy_session_id<0..32>;
CipherSuite cipher_suites<2..2^16-2>;
opaque legacy_compression_methods<1..2^8-1>;
Extension extensions<8..2^16-1>;
} ClientHello;
legacy_version
: In previous versions of TLS, this field was used for version negotiation
and represented the highest version number supported by the client.
Experience has shown that many servers do not properly implement
version negotiation, leading to "version intolerance" in which
the server rejects an otherwise acceptable ClientHello with a version
number higher than it supports.
In TLS 1.3, the client indicates its version preferences in the
"supported_versions" extension ({{supported-versions}}) and the legacy_version field MUST
be set to 0x0303, which is the version number for TLS 1.2.
(See {{backward-compatibility}} for details about backward compatibility.)
random
: 32 bytes generated by a secure random number generator.
See {{implementation-notes}} for additional information.
legacy_session_id
: Versions of TLS before TLS 1.3 supported a "session resumption"
feature which has been merged with Pre-Shared Keys in this version
(see {{resumption-and-psk}}).
This field MUST be ignored by a server negotiating TLS 1.3 and
MUST be set as a zero length vector (i.e., a single zero byte
length field) by clients that do not have a cached session ID
set by a pre-TLS 1.3 server.
*)
(* Note: We're not implementing any older protocols *)
(**
cipher_suites
: This is a list of the symmetric cipher options supported by the
client, specifically the record protection algorithm (including
secret key length) and a hash to be used with HKDF, in descending
order of client preference. If the list contains cipher suites that
the server does not recognize, support or wish to use, the server
MUST ignore those cipher suites and process the remaining ones as
usual. Values are defined in {{cipher-suites}}. If the client is
attempting a PSK key establishment, it SHOULD advertise at least one
cipher suite indicating a Hash associated with the PSK.
*)
(* Note: Ignoring unrecognized cipher suites should get spec'd at the
same location as, e.g., spec'ing that the server isn't allowed to
decide to end connections early based on secret data *)
(**
legacy_compression_methods
: Versions of TLS before 1.3 supported compression with the list of
supported compression methods being sent in this field. For every TLS 1.3
ClientHello, this vector MUST contain exactly one byte set to
zero, which corresponds to the "null" compression method in
prior versions of TLS. If a TLS 1.3 ClientHello is
received with any other value in this field, the server MUST
abort the handshake with an "illegal_parameter" alert. Note that TLS 1.3
servers might receive TLS 1.2 or prior ClientHellos which contain
other compression methods and MUST follow the procedures for
the appropriate prior version of TLS. TLS 1.3 ClientHellos are identified
as having a legacy_version of 0x0303 and a supported_versions extension
present with 0x0304 as the highest version indicated therein.
*)
(* Server constraint: If we recieve ClientHello with anything other
than single zero byte in legacy_compression_methods, we MUST abort
with illegal_parameter. *)
(**
extensions
: Clients request extended functionality from servers by sending
data in the extensions field. The actual "Extension" format is
defined in {{extensions}}. In TLS 1.3, use
of certain extensions is mandatory, as functionality is moved into
extensions to preserve ClientHello compatibility with previous versions of TLS.
Servers MUST ignore unrecognized extensions.
*)
(* Note: Ignoring unrecognized extensions should get spec'd at the
same location as, e.g., spec'ing that the server isn't allowed to
decide to end connections early based on secret data *)
(**
{:br }
All versions of TLS allow an extensions field to optionally follow the
compression_methods field. TLS 1.3 ClientHello
messages always contain extensions (minimally "supported_versions", otherwise
they will be interpreted as TLS 1.2 ClientHello messages).
However, TLS 1.3 servers might receive ClientHello messages without an
extensions field from prior versions of TLS.
The presence of extensions can be detected by determining whether there
are bytes following the compression_methods field at the end of the
ClientHello. Note that this method of detecting optional data differs
from the normal TLS method of having a variable-length field, but it
is used for compatibility with TLS before extensions were defined.
TLS 1.3 servers will need to perform this check first and only
attempt to negotiate TLS 1.3 if a "supported_version" extension
is present.
*)
(* Note: We should be able to encode missing list of extensions as nil
(otherwise as [None : option list]); this happens when decoding
records / wire data. *)
(**
If negotiating a version of TLS prior to 1.3, a server MUST check that
the message either contains no data after legacy_compression_methods
or that it contains a valid extensions block with no data following.
If not, then it MUST abort the handshake with a "decode_error" alert.
In the event that a client requests additional functionality using
extensions, and this functionality is not supplied by the server, the
client MAY abort the handshake.
After sending the ClientHello message, the client waits for a ServerHello
or HelloRetryRequest message. If early data
is in use, the client may transmit early application data
({{zero-rtt-data}}) while waiting for the next handshake message.
*)
(* TODO: Deal with early data *)
(**
### Server Hello {#server-hello}
The server will send this message in response to a ClientHello message
to proceed with the handshake if it is able to negotiate an acceptable
set of handshake parameters based on the ClientHello.
Structure of this message:
%%% Key Exchange Messages
struct {
ProtocolVersion version;
Random random;
CipherSuite cipher_suite;
Extension extensions<6..2^16-1>;
} ServerHello;
version
: This field contains the version of TLS negotiated for this connection. Servers
MUST select a version from the list in ClientHello's supported_versions extension,
or otherwise negotiate TLS 1.2 or a previous version.
A client that receives a version that was not offered MUST abort the handshake.
For this version of the specification, the version is 0x0304. (See
{{backward-compatibility}} for details about backward compatibility.)
random
: 32 bytes generated by a secure random number generator.
See {{implementation-notes}} for additional information.
The last eight bytes MUST be overwritten as described
below if negotiating TLS 1.2 or TLS 1.1, but the
remaining bytes MUST be random.
This structure is generated by the server and MUST be
generated independently of the ClientHello.random.
cipher_suite
: The single cipher suite selected by the server from the list in
ClientHello.cipher_suites. A client which receives a cipher suite
that was not offered MUST abort the handshake with an "illegal_parameter"
alert.
extensions
: A list of extensions. The ServerHello MUST only include extensions
which are required to establish the cryptographic context. Currently
the only such extensions are "key_share" and "pre_shared_key".
All current TLS 1.3 ServerHello messages will contain one of these
two extensions, or both when using a PSK with (EC)DHE key establishment.
The remaining extensions are sent separately in the EncryptedExtensions
message.
{:br }
TLS 1.3 has a downgrade protection mechanism embedded in the server's
random value. TLS 1.3 servers which negotiate TLS 1.2 or below in
response to a ClientHello MUST set the last eight bytes of their
Random value specially.
If negotiating TLS 1.2, TLS 1.3 servers MUST set the last eight bytes of their
Random value to the bytes:
44 4F 57 4E 47 52 44 01
If negotiating TLS 1.1 or below, TLS 1.3 servers MUST and TLS 1.2
servers SHOULD set the last eight bytes of their Random value to the
bytes:
44 4F 57 4E 47 52 44 00
TLS 1.3 clients receiving a ServerHello indicating TLS 1.2 or below
MUST check that the last eight bytes are not equal to either of these values.
TLS 1.2 clients SHOULD also check that the last eight bytes are not
equal to the second value if the ServerHello indicates TLS 1.1 or
below. If a match is found, the client MUST abort the handshake
with an "illegal_parameter" alert. This mechanism provides limited
protection against downgrade attacks over and above what is provided
by the Finished exchange: because the ServerKeyExchange, a message
present in TLS 1.2 and below, includes a signature over both random
values, it is not possible for an active attacker to modify the
random values without detection as long as ephemeral ciphers are used.
It does not provide downgrade protection when static RSA is used.
Note: This is a change from {{RFC5246}}, so in practice many TLS 1.2 clients
and servers will not behave as specified above.
A legacy TLS client performing renegotiation with TLS 1.2 or prior
and which receives a TLS 1.3 ServerHello during renegotiation
MUST abort the handshake with a "protocol_version" alert.
Note that renegotiation is not possible when TLS 1.3 has been
negotiated.
RFC EDITOR: PLEASE REMOVE THE FOLLOWING PARAGRAPH
Implementations of draft versions (see {{draft-version-indicator}}) of this
specification SHOULD NOT implement this mechanism on either client and server.
A pre-RFC client connecting to RFC servers, or vice versa, will appear to
downgrade to TLS 1.2. With the mechanism enabled, this will cause an
interoperability failure.
### Hello Retry Request
The server will send this message in response to a ClientHello message if it is
able to find an acceptable set of parameters but the ClientHello does not
contain sufficient information to proceed with the handshake.
Structure of this message:
%%% Key Exchange Messages
struct {
ProtocolVersion server_version;
CipherSuite cipher_suite;
Extension extensions<2..2^16-1>;
} HelloRetryRequest;
{:br }
The version, cipher_suite, and extensions fields have the
same meanings as their corresponding values in the ServerHello.
The server SHOULD send only the extensions necessary for the client to
generate a correct ClientHello pair. As with ServerHello, a
HelloRetryRequest MUST NOT contain any extensions that were not first
offered by the client in its ClientHello, with the exception of optionally the
"cookie" (see {{cookie}}) extension.
Upon receipt of a HelloRetryRequest, the client MUST verify that the
extensions block is not empty and otherwise MUST abort the handshake
with a "decode_error" alert. Clients MUST abort the handshake with
an "illegal_parameter" alert if the HelloRetryRequest would not result in
any change in the ClientHello. If a client receives a second
HelloRetryRequest in the same connection (i.e., where
the ClientHello was itself in response to a HelloRetryRequest), it
MUST abort the handshake with an "unexpected_message" alert.
Otherwise, the client MUST process all extensions in the HelloRetryRequest and
send a second updated ClientHello. The HelloRetryRequest extensions defined in
this specification are:
- cookie (see {{cookie}})
- key_share (see {{key-share}})
In addition, in its updated ClientHello, the client SHOULD NOT offer
any pre-shared keys associated with a hash other than that of the
selected cipher suite. This allows the client to avoid having to
compute partial hash transcripts for multiple hashes in the second
ClientHello. A client which receives a cipher suite that was not
offered MUST abort the handshake. Servers MUST ensure that they
negotiate the same cipher suite when receiving a conformant updated
ClientHello (if the server selects the cipher suite as the first step
in the negotiation, then this will happen automatically). Upon
receiving the ServerHello, clients MUST check that the cipher suite
supplied in the ServerHello is the same as that in the
HelloRetryRequest and otherwise abort the handshake with an
"illegal_parameter" alert.
*)
Raw
SpecWithAPI.v
Require Import Crypto.Spec.Trace.
Require Import Crypto.Protocols.SigmaKeyExchange.Combinators.
(**
// All single-letter symbols in this comment represent public DH keys.
// Capital letters represent long-term and others are per-connection
// ephemeral. [msg](PK1<>PK2) denotes nacl/box authenticated encryption.
//--> a
//<-- b
//<-- [B,[b,a](B<>a)](a<>b)
//--> [A,[a,b](A<>b)](a<>b)
//--> [data](a<>b)
//<-- [data](a<>b)
*)
(* Parameter: g *)
(* Per-connection parameter: A *)
(* Per-connection choice: x *)
(* Per-connection choice: b *)
(* Per-connection choice: B *)
(* Constraint: if there's a first message on the wire from our side,
then there must be a message from the RNG before that which gives x *)
(* Constraint: if there's a first message on the wire from our side, it
must be g^x *)
(* Constraint: if you recieve more than just [b] before you send [a],
must abort *)
(* Constraint: if you send a non-abort message after sending [a], you
must have recieved [b] (and it must match the choice of [b]) *)
(* Constraint: the form of our second message must be correct *)
(* Constraint: if you send a non-abort message after sending [a] and
"the long message", you must have recieved a long message, and it must
be the message you got immediately after the short message, and it
must match the choice of [B], and the format must be correct *)
(* Secrets constraint: If you recieve a randomness message, you may
immediately emit [g^x] and update the secret-x-value with [x], or you
may do anything which does not depend on the contents of the random
message. (the decision must depend only on public things) *)
(* Secrets constraint: You may at any time emit a message matching
long-form or short-form using the secret-x-value in the appropriate
place and not in other places, or else you must emit somthing not
depending on the secret-x-value (the decision must depend only on
public things) *)
Section spec.
Context (connection_id : Type)
(secret public : Type)
(message ciphertext : Type)
(text_of_pair : message * message -> message)
(text_of_public : public -> message)
(text_of_cipher : ciphertext -> message)
(pair_of_text : message -> message * message)
(public_of_text : message -> public)
(cipher_of_text : message -> ciphertext).
Let random := secret.
Context (keygen : secret -> public) (* Parameter: g *)
(box_seal : secret -> public -> message -> ciphertext)
(box_open : secret -> public -> ciphertext -> option message).
Section per_connection_parameters.
Context (our_longterm_secret : secret).
Let our_longterm_public : public (* Per-connection parameter: A *)
:= keygen our_longterm_secret.
Section per_connection_choices.
Context (our_ephemeral_secret : secret) (* Per-connection choice: x *)
(their_ephemeral_public : public) (* Per-connection choice: b *)
(their_longterm_public : public) (* Per-connection choice: B *).
Let our_ephemeral_public : public
:= keygen our_ephemeral_secret.
Context {state : Type}.
Inductive input :=
| Random (_ : random) | ConnectionStart | RecieveNetwork (_ : message)
| APISendNetwork | APICloseConnection | APIUserOutput.
Inductive pre_output :=
| RequestRandom | SendNetwork (_ : message) | CloseConnection | UserOutput (_ : secret * public * public)
| APIGotRandom | APIGotConnectionStart
| APIGotTheirEphemeralPublic (_ : message) (_ : public)
| APIGotTheirLongtermPublicAndPassedValidation (_ : message) (_ : public)
| APIGotTheirLongformFailedValidation (_ : message)
| APIGotRecieveNetworkGeneric (_ : message).
Let output := option pre_output.
(* Constraint: we don't send anything after CloseConnection *)
Definition close_connection_closed
(trace : list (input * output)) : Prop
:= holds_of_all_messages_strictly_after_nth_message_matching
0
(on_output (fun m_out => m_out = Some CloseConnection))
(fun _ => on_output (fun m_out => m_out = None))
trace.
(* Constraint: if there's a first message on the wire from our
side, then there must be a message from the RNG before that
which gives x *)
Definition get_randomness_spec
(trace : list (input * output)) : Prop
:= holds_of_some_message_before_nth_message_matching
0
(on_output (fun m_out => exists v, m_out = Some (SendNetwork v)))
(fun _ => on_input (fun m_in => m_in = Random our_ephemeral_secret))
trace.
Let Send_a := Some (SendNetwork (text_of_public our_ephemeral_public)).
(* Constraint: if there's a first message on the wire from our
side, it must be g^x *)
Definition output_g_x
(trace : list (input * output)) : Prop
:= holds_of_nth_message_matching
0
(on_output (fun m_out => exists v, m_out = Some (SendNetwork v)))
(on_output (fun m_out => m_out = Send_a))
trace.
(* Constraint: if you recieve more than just [b] before you send
[a], must abort *)
(* Skipped for now *)
(* Constraint: if you send a non-abort message after sending
[a], you must have recieved [b] (and it must match the
choice of [b]) *)
Definition must_set_b
(trace : list (input * output)) : Prop
:= nth_message_matching_exists
1
(on_output (fun m_out => exists v, m_out = Some (SendNetwork v)))
trace
-> holds_of_nth_message_matching
0
(on_input (fun m_in => exists v, m_in = RecieveNetwork v))
(on_input (fun m_in => m_in = RecieveNetwork (text_of_public their_ephemeral_public)))
trace.
Definition must_recieve_b
(trace : list (input * output)) : Prop
:= holds_of_some_message_strictly_before_nth_message_matching
1
(on_output (fun m_out => exists v, m_out = Some (SendNetwork v)))
(fun _ => on_input (fun m_in => m_in = RecieveNetwork (text_of_public their_ephemeral_public)))
trace.
Let longform
:= (text_of_cipher
(box_seal
our_ephemeral_secret
their_ephemeral_public
(text_of_pair
(text_of_public our_longterm_public,
text_of_cipher
(box_seal
our_longterm_secret
their_ephemeral_public
(text_of_pair
(text_of_public our_ephemeral_public,
text_of_public their_ephemeral_public))))))).
(* Constraint: the form of our second message must be correct *)
(* //--> [A,[a,b](A<>b)](a<>b) *)
Definition second_message_correct
(trace : list (input * output)) : Prop
:= holds_of_nth_message_matching
1
(on_output (fun m_out => exists v, m_out = Some (SendNetwork v)))
(on_output
(fun m_out
=> m_out
= Some
(SendNetwork
longform)))
trace.
Let input_passes_validation m_in
:= (forall v boxed_b_a,
m_in = RecieveNetwork v
-> box_open
our_ephemeral_secret
their_ephemeral_public
(cipher_of_text v)
= Some (text_of_pair
(text_of_public their_longterm_public,
text_of_cipher boxed_b_a))
/\ box_open
our_ephemeral_secret
their_longterm_public
boxed_b_a
= Some (text_of_pair
(text_of_public their_ephemeral_public,
text_of_public our_ephemeral_public))).
(* Constraint: if you send a non-abort message after sending [a]
and "the long message", you must have recieved a long
message, and it must be the message you got immediately
after the short message, and it must match the choice of
[B], and the format must be correct *)
(* //<-- [B,[b,a](B<>a)](a<>b) *)
Definition second_message_recieved_correct_form
(trace : list (input * output)) : Prop
:= nth_message_matching_exists
2
(on_output (fun m_out => exists v, m_out = Some (SendNetwork v)))
trace
-> holds_of_nth_message_matching
1
(on_input (fun m_in => exists v, m_in = RecieveNetwork v))
(on_input
(fun m_in
=> forall v boxed_b_a,
m_in = RecieveNetwork v
-> box_open
our_ephemeral_secret
their_ephemeral_public
(cipher_of_text v)
= Some (text_of_pair
(text_of_public their_longterm_public,
text_of_cipher boxed_b_a))
/\ box_open
our_ephemeral_secret
their_longterm_public
boxed_b_a
= Some (text_of_pair
(text_of_public their_ephemeral_public,
text_of_public our_ephemeral_public))))
trace.
(* Also spec output here *)
Definition second_message_recieved
(trace : list (input * output)) : Prop
:= holds_of_some_message_strictly_before_nth_message_matching
0
(on_output (fun m_out => exists v, m_out = Some (UserOutput v)))
(fun _ => on_input input_passes_validation)
trace.
Definition output_correct_form
(trace : list (input * output)) : Prop
:= holds_of_nth_message_matching
0
(on_output (fun m_out => exists v, m_out = Some (UserOutput v)))
(on_output
(fun m_out
=> m_out
= Some
(UserOutput
(our_ephemeral_secret,
their_ephemeral_public,
their_longterm_public))))
trace.
Definition nothing_after_user_output
(trace : list (input * output)) : Prop
:= holds_of_all_messages_strictly_after_nth_message_matching
0
(on_output (fun m_out => exists v, m_out = Some (UserOutput v)))
(fun _ => on_output (fun m_out => m_out = None))
trace.
Definition trace_satisfies_external_SKE_spec (trace : list (input * output)) : Prop
:= close_connection_closed trace
/\ get_randomness_spec trace
/\ output_g_x trace
/\ must_set_b trace
/\ must_recieve_b trace
/\ second_message_correct trace
/\ second_message_recieved_correct_form trace
/\ second_message_recieved trace
/\ output_correct_form trace
/\ nothing_after_user_output trace.
Section secrets.
Definition on_input_Random
(trace : list (input * output)) : Prop
:= holds_of_all_messages
(fun '(m_in, m_out)
=> (exists v, m_in = Random v)
<-> m_out = Some APIGotRandom)
trace.
Definition on_input_ConnectionStart
(trace : list (input * output)) : Prop
:= holds_of_all_messages
(fun '(m_in, m_out)
=> m_in = ConnectionStart
<-> m_out = Some APIGotConnectionStart)
trace.
Definition on_output_CloseConnection
(trace : list (input * output)) : Prop
:= holds_of_all_messages
(fun '(m_in, m_out)
=> m_in = APICloseConnection
<-> m_out = Some CloseConnection)
trace.
Definition on_output_UserOutput
(trace : list (input * output)) : Prop
:= holds_of_all_messages
(fun '(m_in, m_out)
=> m_in = APIUserOutput
<-> (exists v, m_out = Some (UserOutput v)))
trace.
Definition on_output_SendNetwork
(trace : list (input * output)) : Prop
:= holds_of_all_messages
(fun '(m_in, m_out)
=> m_in = APISendNetwork
<-> (exists v, m_out = Some (SendNetwork v)))
trace.
Definition on_input_RecieveNetwork
(trace : list (input * output)) : Prop
:= holds_of_all_messages
(fun '(m_in, m_out)
=> (exists v, m_in = RecieveNetwork v)
<-> match m_in, m_out with
| RecieveNetwork v, Some (APIGotTheirEphemeralPublic v' _)
| RecieveNetwork v, Some (APIGotTheirLongtermPublicAndPassedValidation v' _)
| RecieveNetwork v, Some (APIGotTheirLongformFailedValidation v')
| RecieveNetwork v, Some (APIGotRecieveNetworkGeneric v')
=> v = v'
| _, _ => False
end)
trace.
Definition on_input_RecieveNetwork0
(trace : list (input * output)) : Prop
:= holds_of_nth_message_matching
0
(on_input (fun m_in => exists v, m_in = RecieveNetwork v))
(fun '(m_in, m_out)
=> exists v,
m_in = RecieveNetwork v
/\ m_out = Some (APIGotTheirEphemeralPublic v (public_of_text v)))
trace.
Definition on_input_RecieveNetwork1
(trace : list (input * output)) : Prop
:= holds_of_nth_message_matching
1
(on_input (fun m_in => exists v, m_in = RecieveNetwork v))
(fun '(m_in, m_out)
=> exists v,
m_in = RecieveNetwork v
/\ m_out = Some (APIGotTheirEphemeralPublic v (public_of_text v)))
trace.
Definition on_input_RecieveNetwork2
(trace : list (input * output)) : Prop
:= holds_of_nth_message_matching
2
(on_input (fun m_in => exists v, m_in = RecieveNetwork v))
(fun '(m_in, m_out)
=> exists v,
m_in = RecieveNetwork v
/\ ((input_passes_validation m_in
/\ m_out = Some (APIGotTheirLongtermPublicAndPassedValidation v their_longterm_public))
\/ (~input_passes_validation m_in
/\ m_out = Some (APIGotTheirLongformFailedValidation v))))
trace.
Definition on_input_RecieveNetworkGe3
(trace : list (input * output)) : Prop
:= holds_of_nth_messages_matching_if_they_exist
(fun n => n > 2)
(on_input (fun m_in => exists v, m_in = RecieveNetwork v))
(fun '(m_in, m_out)
=> exists v,
m_in = RecieveNetwork v /\ m_out = Some (APIGotRecieveNetworkGeneric v))
trace.
Definition trace_satisfies_full_SKE_spec (trace : list (input * output)) : Prop
:= trace_satisfies_external_SKE_spec trace
/\ on_input_Random trace
/\ on_input_ConnectionStart trace
/\ on_output_CloseConnection trace
/\ on_output_UserOutput trace
/\ on_output_SendNetwork trace
/\ on_input_RecieveNetwork trace
/\ on_input_RecieveNetwork0 trace
/\ on_input_RecieveNetwork1 trace
/\ on_input_RecieveNetwork2 trace
/\ on_input_RecieveNetworkGe3 trace.
End secrets.
Definition at_most_one {T} (P : T -> Prop)
:= forall x y : T, P x -> P y -> x = y.
Definition is_deterministicT
:= forall (partial_trace : list (input * output))
(m_in : input),
at_most_one
(fun m_out
=> (exists rest : list (input * output),
trace_satisfies_full_SKE_spec (partial_trace ++ (m_in, m_out)::rest))).
Require Import Crypto.Util.Tactics.DestructHead.
Require Import Crypto.Util.Tactics.Test.
Require Import Crypto.Util.Option.
Lemma pull_ex_not {T} (P : T -> Prop)
: (~ex P) <-> forall v, ~P v.
Proof.
split; intros H; [ intros v H' | intros [v H'] ];
eapply H; [ eexists | ]; eassumption.
Qed.
Lemma impl_and_l {A B C : Prop} : (A /\ B -> C) <-> (A -> B -> C).
Proof. tauto. Qed.
Lemma holds_of_messages_around_nth_messages_matching_aux_lift_impl
is_n
(P1 P2 : Prop)
(HP : P1 -> P2)
T
(matcher : _ -> Prop)
(property1 property2 : _ -> _ -> _ -> Prop)
init1 init2
(Hproperty : forall pre m post, matcher m -> property1 (init1 ++ pre)%list m post -> property2 (init2 ++ pre)%list m post)
trace
: @holds_of_messages_around_nth_messages_matching_aux is_n P1 T matcher property1 init1 trace
-> @holds_of_messages_around_nth_messages_matching_aux is_n P2 T matcher property2 init2 trace.
Proof.
clear -Hproperty HP.
revert P1 P2 HP is_n init1 init2 Hproperty; induction trace as [|x xs IHxs]; intros P1 P2 HP is_n init1 init2 Hproperty; simpl.
{ assumption. }
{ pose proof (Hproperty nil).
assert (Hp' : forall pre m post,
matcher m
-> property1 ((init1 ++ x::nil) ++ pre)%list m post
-> property2 ((init2 ++ x::nil) ++ pre)%list m post)
by (intros ???; rewrite <- !List.app_assoc; apply Hproperty).
repeat first [ progress simpl @List.app in *
| progress rewrite !List.app_nil_r in *
| apply conj
| intro
| assumption
| progress destruct_head'_and
| match goal with
| [ H : ?A -> ?B, H' : ?A |- _ ] => specialize (H H')
end
| solve [ eauto ] ].
{ eapply IHxs; [ .. | eassumption ]; [ tauto | eauto ]. } }
Qed.
Lemma holds_of_all_messages_cons {T} P x xs
: @holds_of_all_messages T P (x :: xs)
<-> (P x /\ @holds_of_all_messages T P xs).
Proof.
clear.
repeat autounfold with trace_combinators; simpl.
repeat first [ apply conj
| intro
| assumption
| progress destruct_head'_and
| match goal with
| [ H : True -> _ |- _ ] => specialize (H I)
| [ H : ~True -> _ |- _ ] => clear H
end
| solve [ eauto ]
| eapply holds_of_messages_around_nth_messages_matching_aux_lift_impl; [.. | eassumption ] ].
Qed.
Lemma holds_of_all_messages_app {T} P ls1 ls2
: @holds_of_all_messages T P (ls1 ++ ls2)
<-> (@holds_of_all_messages T P ls1 /\ @holds_of_all_messages T P ls2).
Proof.
clear.
revert ls2; induction ls1 as [|x xs IHxs]; intro ls2.
{ repeat autounfold with trace_combinators; simpl; tauto. }
{ simpl; rewrite !holds_of_all_messages_cons, IHxs; tauto. }
Qed.
Lemma is_deterministic : is_deterministicT.
Proof.
intros partial_trace m_in x y [restx Hx] [resty Hy].
unfold trace_satisfies_full_SKE_spec in *.
unfold on_input_Random, on_input_ConnectionStart, on_output_CloseConnection, on_output_SendNetwork, on_output_UserOutput in *.
(*destruct_head'_and
, trace_satisfies_external_SKE_spec in *.*)
Local Ltac do_unfold :=
repeat first [ progress simpl @List.app in *
| match goal with
| [ H : context[?f _ /\ _] |- _ ]
=> lazymatch type of f with
| list _ -> _ => unfold f in H
end
| [ H : context[_ /\ ?f _] |- _ ]
=> lazymatch type of f with
| list _ -> _ => unfold f in H
end
| [ H : context[~(exists v : ?T, ?m = @?k v) -> _] |- _ ]
=> rewrite (@pull_ex_not T (fun v => m = k v)) in H
| [ H : context[(?A /\ ?B) -> ?C] |- _ ]
=> rewrite (@impl_and_l A B C) in H
end
| progress destruct_head'_and
| progress destruct_head'_prod
| progress repeat autounfold with trace_combinators in *
| progress simpl in *
| progress unfold Send_a in * ].
Local Ltac do_solve :=
repeat match goal with
| [ H : True -> _ |- _ ] => specialize (H I)
| [ H : False |- _ ] => exfalso; exact H
| [ |- ?x = ?x ] => reflexivity
| _ => progress destruct_head'_and
| _ => progress destruct_head'_ex
| _ => progress destruct_head' iff
| _ => progress subst
| [ H : RecieveNetwork _ = RecieveNetwork _ |- _ ]
=> inversion H; clear H
| [ H : SendNetwork _ = SendNetwork _ |- _ ]
=> inversion H; clear H
| [ H : Some _ = Some _ |- _ ]
=> inversion H; clear H
| [ H : (exists v, _ = _) -> _ |- _ ]
=> specialize (H (ex_intro _ _ eq_refl))
| [ H : _ = _ -> _ |- _ ]
=> specialize (H eq_refl)
end.
induction partial_trace as [|m partial_trace IH].
{ do_unfold; pose m_in as m_in'; destruct m_in; do_solve. }
{ simpl @List.app in *.
unfold on_input_RecieveNetwork in *.
repeat match goal with
| [ H : context[@holds_of_all_messages ?T ?P (?x :: ?xs)%list] |- _ ]
=> rewrite (@holds_of_all_messages_cons T P x xs) in H
| [ H : context[@holds_of_all_messages ?T ?P (?ls1 ++ ?ls2)%list] |- _ ]
=> rewrite (@holds_of_all_messages_app T P x xs) in H
end.
repeat first [ progress destruct_head'_prod
| progress destruct_head'_and
| progress destruct_head' iff ].
apply IH; clear IH;
repeat match goal with |- and _ _ => apply conj end; try assumption.
(* Focus 2.
{ assumption.
repeat match goal with
| [ H : _ = _ -> _ |- _ ] => specialize (H eq_refl)
| _ => progress subst
| [ H : (exists v, _ = _) -> _ |- _ ] => specialize (H (ex_intro _ _ eq_refl))
| _ => progress destruct_head'_ex
| [ H : Random _ = Random _ |- _ ] => inversion H; clear H
| [ H : ?x = ?y -> _ |- _ ]
=> is_var x; destruct x
end.
end.
rewrite H' in H4.
(input * option pre_output)
_
m
(partial_trace ++ (m_in, x) :: restx)%list)
in H4.
unfold holds_of_all_messages
{ do_unfold; pose m_in as m_in'; destruct m_in; do_solve. }
destruct partial_trace as [|m0 [|m1 [|m2 [|m3 [|m4 partial_trace].
{ do_unfold; pose m_in as m_in'; destruct m_in; do_solve. }
{ destruct m0 as [m0 ?]; pose m0 as m0'; do_unfold; destruct m0; do_solve.
{ destruct partial_trace as [|m1 partial_trace].*)
(*
{ pose m_in as m_in'; destruct m_in; do_unfold; do_solve.
}
{ do_unfold; pose m_in as m_in'; destruct m_in.
do_solve. }
{ do_unfold; destruct_head' input; do_solve. }
{ do_unfold; pose m_in as m_in'; destruct m_in; do_solve. }
pose m_in as m_in'; destruct m_in;
(*destruct_head input;*)
{ repeat match goal with
| [ H : ~True -> _ |- _ ] => clear H
end.
repeat match goal with
| _ => progress destruct_head'_and
| [ H : (exists v, ?m = @?k v) -> _ |- _ ]
=> specialize (H (ex_intro _ _ eq_refl))
| [ H : context[~(exists v : ?T, ?m = @?k v) -> _] |- _ ]
=> rewrite (@pull_ex_not T (fun v => m = k v)) in H
| [ H : context[(?A /\ ?B) -> ?C] |- _ ]
=> rewrite (@impl_and_l A B C) in H
| [ H : (exists v, ?m = @?k v) -> _ |- _ ]
=> first [ specialize (H (ex_intro _ m eq_refl))
| let H' := fresh in
assert (H' : forall v, m <> k v) by (clear; discriminate);
clear H H' ]
| [ H : Some ?x = Some ?y -> _ |- _ ]
=> first [ specialize (H eq_refl)
| let H' := fresh in
assert (H' : x <> y) by (clear; discriminate);
clear H H' ]
| [ H : ?A, H' : ?A -> ?B |- _ ]
=> specialize (H' H)
| [ H : (forall v, ?m <> @?k v) -> ?P |- _ ]
=> let H' := fresh in
first [ assert (H' : forall v, m <> k v) by (clear; discriminate);
cbv beta in H';
specialize (H H')
(*| clear H*) ]
| [ H : ?x <> ?x -> _ |- _ ]
=> clear H
| [ H : (?x <> ?y) -> ?P |- _ ]
=> let H' := fresh in
assert (H' : x <> y) by (clear; discriminate);
specialize (H H')
| [ H : ?x = ?y -> ?P |- _ ]
=> first [ specialize (H eq_refl)
| let H' := fresh in
assert (H' : x <> y) by (clear; discriminate);
clear H H' ]
| [ H : (?A -> ?B) -> ?C, H' : ?A |- _ ]
=> assert (B -> C) by (intro; apply H; intro; assumption);
clear H
| [ H : ((exists v, ?m = @?k v) -> _) -> ?P |- _ ]
=> assert P
by (apply H; let H' := fresh in intro H'; exfalso; revert H'; apply pull_ex_not; clear; discriminate);
clear H
end.
repeat match goal with
| [ H : False |- _ ] => exfalso; exact H
| [ H : context[List.Exists _ (_ :: _)] |- _ ]
=> rewrite List.Exists_cons in H
| [ H : context[List.Exists _ nil] |- _ ]
=> rewrite List.Exists_nil in H
| [ H : True -> _ |- _ ] => specialize (H I)
| [ H : _ \/ False |- _ ] => destruct H
end.
unfold Send_a in *.
clear H95 H23.
Focus 2.
match goal with
end.
match goal with
| [ H : Some ?x <> Some _ -> (True -> Random _ = ?k) /\ _ |- _ ]
=> is_var x; lazymatch k with Random _ => fail | _ => idtac end;
destruct x
| [ H : ?x <> Some _ -> (True -> Random _ = ?k) /\ _ |- _ ]
=> is_var x; lazymatch k with Random _ => fail | _ => idtac end;
destruct x
end.
{ destruct_head' output.
{ destruct_head' pre_output; try reflexivity.
{ destruct_head' input.
{ repeat match goal with
| _ => progress destruct_head'_and
| [ H : (exists v, ?m = @?k v) -> _ |- _ ]
=> specialize (H (ex_intro _ _ eq_refl))
| [ H : context[~(exists v : ?T, ?m = @?k v) -> _] |- _ ]
=> rewrite (@pull_ex_not T (fun v => m = k v)) in H
| [ H : context[(?A /\ ?B) -> ?C] |- _ ]
=> rewrite (@impl_and_l A B C) in H
| [ H : (exists v, ?m = @?k v) -> _ |- _ ]
=> first [ specialize (H (ex_intro _ m eq_refl))
| let H' := fresh in
assert (H' : forall v, m <> k v) by (clear; discriminate);
clear H H' ]
| [ H : Some ?x = Some ?y -> _ |- _ ]
=> first [ specialize (H eq_refl)
| let H' := fresh in
assert (H' : x <> y) by (clear; discriminate);
clear H H' ]
| [ H : ?A, H' : ?A -> ?B |- _ ]
=> specialize (H' H)
| [ H : (forall v, ?m <> @?k v) -> ?P |- _ ]
=> let H' := fresh in
first [ assert (H' : forall v, m <> k v) by (clear; discriminate);
cbv beta in H';
specialize (H H')
(*| clear H*) ]
| [ H : ?x <> ?x -> _ |- _ ]
=> clear H
| [ H : (?x <> ?y) -> ?P |- _ ]
=> let H' := fresh in
assert (H' : x <> y) by (clear; discriminate);
specialize (H H')
| [ H : ?x = ?y -> ?P |- _ ]
=> first [ specialize (H eq_refl)
| let H' := fresh in
assert (H' : x <> y) by (clear; discriminate);
clear H H' ]
| [ H : (?A -> ?B) -> ?C, H' : ?A |- _ ]
=> assert (B -> C) by (intro; apply H; intro; assumption);
clear H
| [ H : ((exists v, ?m = @?k v) -> _) -> ?P |- _ ]
=> assert P
by (apply H; let H' := fresh in intro H'; exfalso; revert H'; apply pull_ex_not; clear; discriminate);
clear H
end.
repeat match goal with
| [ H : False |- _ ] => exfalso; exact H
| [ H : context[List.Exists _ (_ :: _)] |- _ ]
=> rewrite List.Exists_cons in H
| [ H : context[List.Exists _ nil] |- _ ]
=> rewrite List.Exists_nil in H
| [ H : True -> _ |- _ ] => specialize (H I)
| [ H : _ \/ False |- _ ] => destruct H
end.
SearchAbout List.Exists.
simpl in *.
move H0 at bottom.
repeat match goal with
end.
match goal with
end.
.
intro
clear H14.
match goal with
| [
simpl in *.
=> rewrite pull_ex_not in H
end.
=> assert P; [ apply H; cut (forall v, m <> k v); clear;
[ | discriminate ]
| ]
end.
cut (
test (assert (forall v, m <> k v) by (clear; discriminate));
end.
clear.
discriminate.
progress simpl in *.
unfold unfold trace_satisfies_external_SKE_spec
End
*)
Abort.
End per_connection_choices.
End per_connection_parameters.
Definition synthesis_goal
:= { state : Type
& { init : state -> Prop
& { step : _ (* state -> input -> option pre_output -> state -> Prop *)
| forall trace
(our_longterm_secret : secret),
exists (our_ephemeral_secret : secret)
(their_ephemeral_public their_longterm_public : public),
@allows_behavior state input (option pre_output) init step trace
-> @trace_satisfies_full_SKE_spec our_longterm_secret our_ephemeral_secret their_ephemeral_public their_longterm_public trace
} } }.
End spec.
Raw
SpecWithSanitization.v
Require Import Crypto.Spec.Trace.
Require Import Crypto.Protocols.SigmaKeyExchange.Combinators.
(**
// All single-letter symbols in this comment represent public DH keys.
// Capital letters represent long-term and others are per-connection
// ephemeral. [msg](PK1<>PK2) denotes nacl/box authenticated encryption.
//--> a
//<-- b
//<-- [B,[b,a](B<>a)](a<>b)
//--> [A,[a,b](A<>b)](a<>b)
//--> [data](a<>b)
//<-- [data](a<>b)
*)
(* Parameter: g *)
(* Per-connection parameter: A *)
(* Per-connection choice: x *)
(* Per-connection choice: b *)
(* Per-connection choice: B *)
(* Constraint: if there's a first message on the wire from our side,
then there must be a message from the RNG before that which gives x *)
(* Constraint: if there's a first message on the wire from our side, it
must be g^x *)
(* Constraint: if you recieve more than just [b] before you send [a],
must abort *)
(* Constraint: if you send a non-abort message after sending [a], you
must have recieved [b] (and it must match the choice of [b]) *)
(* Constraint: the form of our second message must be correct *)
(* Constraint: if you send a non-abort message after sending [a] and
"the long message", you must have recieved a long message, and it must
be the message you got immediately after the short message, and it
must match the choice of [B], and the format must be correct *)
(* Secrets constraint: If you recieve a randomness message, you may
immediately emit [g^x] and update the secret-x-value with [x], or you
may do anything which does not depend on the contents of the random
message. (the decision must depend only on public things) *)
(* Secrets constraint: You may at any time emit a message matching
long-form or short-form using the secret-x-value in the appropriate
place and not in other places, or else you must emit somthing not
depending on the secret-x-value (the decision must depend only on
public things) *)
Section spec.
Context (connection_id : Type)
(secret public : Type)
(message ciphertext : Type)
(text_of_pair : message * message -> message)
(text_of_public : public -> message)
(text_of_cipher : ciphertext -> message)
(pair_of_text : message -> message * message)
(public_of_text : message -> public)
(cipher_of_text : message -> ciphertext).
Let random := secret.
Context (keygen : secret -> public) (* Parameter: g *)
(box_seal : secret -> public -> message -> ciphertext)
(box_open : secret -> public -> ciphertext -> option message).
Section per_connection_parameters.
Context (our_longterm_secret : secret).
Let our_longterm_public : public (* Per-connection parameter: A *)
:= keygen our_longterm_secret.
Section per_connection_choices.
Context (our_ephemeral_secret : secret) (* Per-connection choice: x *)
(their_ephemeral_public : public) (* Per-connection choice: b *)
(their_longterm_public : public) (* Per-connection choice: B *).
Let our_ephemeral_public : public
:= keygen our_ephemeral_secret.
Inductive input :=
Random (_ : random) | ConnectionStart | RecieveNetwork (_ : message).
Inductive pre_output :=
RequestRandom | SendNetwork (_ : message) | CloseConnection | UserOutput (_ : secret * public * public).
Let output := option pre_output.
(* Constraint: we don't send anything after CloseConnection *)
Definition close_connection_closed
(trace : list (input * output)) : Prop
:= holds_of_all_messages_strictly_after_nth_message_matching
0
(on_output (fun m_out => m_out = Some CloseConnection))
(fun _ => on_output (fun m_out => m_out = None))
trace.
(* Constraint: if there's a first message on the wire from our
side, then there must be a message from the RNG before that
which gives x *)
Definition get_randomness_spec
(trace : list (input * output)) : Prop
:= holds_of_some_message_before_nth_message_matching
0
(on_output (fun m_out => exists v, m_out = Some (SendNetwork v)))
(fun _ => on_input (fun m_in => m_in = Random our_ephemeral_secret))
trace.
Let Send_a := Some (SendNetwork (text_of_public our_ephemeral_public)).
(* Constraint: if there's a first message on the wire from our
side, it must be g^x *)
Definition output_g_x
(trace : list (input * output)) : Prop
:= holds_of_nth_message_matching
0
(on_output (fun m_out => exists v, m_out = Some (SendNetwork v)))
(on_output (fun m_out => m_out = Send_a))
trace.
(* Constraint: if you recieve more than just [b] before you send
[a], must abort *)
(* Skipped for now *)
(* Constraint: if you send a non-abort message after sending
[a], you must have recieved [b] (and it must match the
choice of [b]) *)
Definition must_set_b
(trace : list (input * output)) : Prop
:= nth_message_matching_exists
1
(on_output (fun m_out => exists v, m_out = Some (SendNetwork v)))
trace
-> holds_of_nth_message_matching
0
(on_input (fun m_in => exists v, m_in = RecieveNetwork v))
(on_input (fun m_in => m_in = RecieveNetwork (text_of_public their_ephemeral_public)))
trace.
Definition must_recieve_b
(trace : list (input * output)) : Prop
:= holds_of_some_message_strictly_before_nth_message_matching
1
(on_output (fun m_out => exists v, m_out = Some (SendNetwork v)))
(fun _ => on_input (fun m_in => m_in = RecieveNetwork (text_of_public their_ephemeral_public)))
trace.
(* Constraint: the form of our second message must be correct *)
(* //--> [A,[a,b](A<>b)](a<>b) *)
Definition second_message_correct
(trace : list (input * output)) : Prop
:= holds_of_nth_message_matching
1
(on_output (fun m_out => exists v, m_out = Some (SendNetwork v)))
(on_output
(fun m_out
=> m_out
= Some
(SendNetwork
(text_of_cipher
(box_seal
our_ephemeral_secret
their_ephemeral_public
(text_of_pair
(text_of_public our_longterm_public,
text_of_cipher
(box_seal
our_longterm_secret
their_ephemeral_public
(text_of_pair
(text_of_public our_ephemeral_public,
text_of_public their_ephemeral_public))))))))))
trace.
(* Constraint: if you send a non-abort message after sending [a]
and "the long message", you must have recieved a long
message, and it must be the message you got immediately
after the short message, and it must match the choice of
[B], and the format must be correct *)
(* //<-- [B,[b,a](B<>a)](a<>b) *)
Definition second_message_recieved_correct_form
(trace : list (input * output)) : Prop
:= nth_message_matching_exists
2
(on_output (fun m_out => exists v, m_out = Some (SendNetwork v)))
trace
-> holds_of_nth_message_matching
1
(on_input (fun m_in => exists v, m_in = RecieveNetwork v))
(on_input
(fun m_in
=> forall v boxed_b_a,
m_in = RecieveNetwork v
-> box_open
our_ephemeral_secret
their_ephemeral_public
(cipher_of_text v)
= Some (text_of_pair
(text_of_public their_longterm_public,
text_of_cipher boxed_b_a))
/\ box_open
our_ephemeral_secret
their_longterm_public
boxed_b_a
= Some (text_of_pair
(text_of_public their_ephemeral_public,
text_of_public our_ephemeral_public))))
trace.
(* Also spec output here *)
Definition second_message_recieved
(trace : list (input * output)) : Prop
:= holds_of_some_message_strictly_before_nth_message_matching
0
(on_output (fun m_out => exists v, m_out = Some (UserOutput v)))
(fun _
=> on_input
(fun m_in
=> forall v boxed_b_a,
m_in = RecieveNetwork v
-> box_open
our_ephemeral_secret
their_ephemeral_public
(cipher_of_text v)
= Some (text_of_pair
(text_of_public their_longterm_public,
text_of_cipher boxed_b_a))
/\ box_open
our_ephemeral_secret
their_longterm_public
boxed_b_a
= Some (text_of_pair
(text_of_public their_ephemeral_public,
text_of_public our_ephemeral_public))))
trace.
Definition output_correct_form
(trace : list (input * output)) : Prop
:= holds_of_nth_message_matching
0
(on_output (fun m_out => exists v, m_out = Some (UserOutput v)))
(on_output
(fun m_out
=> m_out
= Some
(UserOutput
(our_ephemeral_secret,
their_ephemeral_public,
their_longterm_public))))
trace.
Definition nothing_after_user_output
(trace : list (input * output)) : Prop
:= holds_of_all_messages_strictly_after_nth_message_matching
0
(on_output (fun m_out => exists v, m_out = Some (UserOutput v)))
(fun _ => on_output (fun m_out => m_out = None))
trace.
(* grep Definition src/Protocols/SigmaKeyExchange/SpecWithSanitization.v | sed s'/Definition//g' | sed s'/^\s*//g' | sed s'|^|/\\\\ |g' | sed s'/\s*$/ trace/g' *)
Definition trace_satisfies_full_SKE_spec (trace : list (input * output)) : Prop
:= close_connection_closed trace
/\ get_randomness_spec trace
/\ output_g_x trace
/\ must_set_b trace
/\ must_recieve_b trace
/\ second_message_correct trace
/\ second_message_recieved_correct_form trace
/\ second_message_recieved trace
/\ output_correct_form trace
/\ nothing_after_user_output trace.
Section sanitized.
Inductive secret_free_input :=
| SFFreshPublic (_ : public)
| SFConnectionStart
| SFRecieveTheirEphemeralPublic (_ : message) (_ : public)
| SFRecieveTheirLongtermPublic
(_ : message)
(their_longterm_public : public)
(their_ephemeral_public : public)
(claimed_our_emphemeral_public : public)
| SFRecieveCorruptedTheirLongtermPublic (_ : message)
| SFRecieveExtraMessage (_ : message).
Inductive seal_with := ephemeral | longterm.
Inductive secret_free_pre_output :=
| SFRequestRandom
| SFSendOurEphemeralPublic (_ : public)
| SFSendNestedBox
(outer_boxes : list (seal_with * public * (message -> message)))
(inner_msg : message)
(inner_seal : seal_with * public)
| SFCloseConnection
| SFUserOutputWithOurEphemeralSecret (_ : public * public).
Inductive RNGState := next_random_is_keypair.
Inductive ExpectingNextNetworkState :=
NTheirEphemeralPublic | NTheirLongtermPublic | NOther.
Definition init_st : RNGState * ExpectingNextNetworkState
:= (next_random_is_keypair, NTheirEphemeralPublic).
Definition sanitize_input (st_msg : (RNGState * ExpectingNextNetworkState) * input) : (RNGState * ExpectingNextNetworkState) * secret_free_input
:= let '((rng_st, net_st), msg) := st_msg in
match rng_st, net_st, msg with
| next_random_is_keypair, _, Random x
=> ((rng_st, net_st), SFFreshPublic (keygen x))
| _, _, ConnectionStart
=> ((next_random_is_keypair, NTheirEphemeralPublic), SFConnectionStart)
| _, NTheirEphemeralPublic, RecieveNetwork m
=> ((rng_st, NTheirLongtermPublic), SFRecieveTheirEphemeralPublic m (public_of_text m))
| _, NTheirLongtermPublic, RecieveNetwork v
=> ((rng_st, NOther),
match box_open
our_ephemeral_secret
their_ephemeral_public
(cipher_of_text v)
with
| Some m
=> let '(p, c) := pair_of_text m in
let their_longterm_public := public_of_text p in
match box_open
our_ephemeral_secret
their_longterm_public
(cipher_of_text c)
with
| Some m'
=> let '(t, o) := pair_of_text m' in
let their_ephemeral_public := public_of_text t in
let claimed_our_ephemeral_public := public_of_text o in
SFRecieveTheirLongtermPublic
v
their_longterm_public
their_ephemeral_public
claimed_our_ephemeral_public
| None
=> SFRecieveCorruptedTheirLongtermPublic v
end
| None => SFRecieveCorruptedTheirLongtermPublic v
end)
| _, NOther, RecieveNetwork v
=> ((rng_st, net_st), SFRecieveExtraMessage v)
end.
Definition enrich_output (msg : secret_free_pre_output) : pre_output
:= match msg with
| SFRequestRandom => RequestRandom
| SFSendOurEphemeralPublic v
=> SendNetwork (text_of_public v)
| SFSendNestedBox outer_boxes inner_msg (inner_seal, inner_pub)
=> let secret_of_seal seal :=
match seal with
| ephemeral => our_ephemeral_secret
| longterm => our_longterm_secret
end in
let do_seal seal pub msg
:= text_of_cipher
(box_seal
(secret_of_seal seal)
pub
msg) in
let m := do_seal inner_seal inner_pub inner_msg in
SendNetwork
(List.fold_right
(fun '(seal, pub, f) msg
=> do_seal seal pub (f msg))
m
outer_boxes)
| SFCloseConnection
=> CloseConnection
| SFUserOutputWithOurEphemeralSecret (p1, p2)
=> UserOutput (our_ephemeral_secret, p1, p2)
end.
End sanitized.
End per_connection_choices.
End per_connection_parameters.
Definition synthesis_goal
:= { state : Type
& { init : state -> Prop
& { step : _ (* state -> input -> option pre_output -> state -> Prop *)
& { state_public : Type
& { pr_public : state -> state_public
& { init_public : state_public -> Prop
& { step_public : _
| forall trace
(our_longterm_secret : secret),
exists (our_ephemeral_secret : secret)
(their_ephemeral_public their_longterm_public : public),
@allows_behavior state input (option pre_output) init step trace
-> @trace_satisfies_full_SKE_spec our_longterm_secret our_ephemeral_secret their_ephemeral_public their_longterm_public trace
/\ exists trace_public,
@allows_behavior state_public secret_free_input (option secret_free_pre_output) init_public step_public trace_public
/\ List.map (fun '(i, o) => option_map (enrich_output our_longterm_secret our_ephemeral_secret) o) trace_public
= List.map (fun '(i, o) => o) trace
/\ List.map (fun '(i, o) => i) trace_public
= list_rect
(fun _ => RNGState * ExpectingNextNetworkState
-> list secret_free_input)
(fun st => nil)
(fun msg_in _ rec st
=> let '(st, m) := sanitize_input our_ephemeral_secret their_ephemeral_public (st, msg_in) in
(m :: rec st)%list)
(List.map (fun '(i, o) => i) trace)
init_st
} } } } } } }.
End spec.
Raw
Structures.v
Require Import Nat Program Omega.
Definition uint8 := { n | n < 2^8 }.
Definition uint16 := { n | n < 2^16 }.
Definition uint24 := { n | n < 2^24 }.
Definition uint32 := { n | n < 2^32 }.
Axiom tuple : Type -> nat -> Type.
Local Infix "^" := tuple.
Definition ProtocolVersion := uint16.
Definition Random := uint8^32.
Definition CipherSuite := uint8^2.
(* Definition Extension := list uint8. *)
Variant HandshakeType :=
| client_hello
| server_hello
| new_session_ticket
| end_of_early_data
| hello_retry_request
| encrypted_extensions
| certificate
| certificate_request
| certificate_verify
| finished
| key_update
| message_hash.
(*
Obligation Tactic := program_simpl; omega.
Program Definition encode (t:HandshakeType) : uint8 :=
match t with
| client_hello => 1
| server_hello => 2
| new_session_ticket => 4
| end_of_early_data => 5
| hello_retry_request => 6
| encrypted_extensions => 8
| certificate => 11
| certificate_request => 13
| certificate_verify => 15
| finished => 20
| key_update => 24
| message_hash => 254
end.
*)
Variant ExtensionType :=
| server_name (* RFC 6066 *)
| max_fragment_length (* RFC 6066 *)
| status_request (* RFC 6066 *)
| supported_groups (* RFC 4492, 7919 *)
| signature_algorithms (* RFC 5246 *)
| use_srtp (* RFC 5764 *)
| heartbeat (* RFC 6520 *)
| application_layer_protocol_negotiation (* RFC 7301 *)
| signed_certificate_timestamp (* RFC 6962 *)
| client_certificate_type (* RFC 7250 *)
| server_certificate_type (* RFC 7250 *)
| padding (* RFC 7685 *)
| key_share (* [[TLS13] *)
| pre_shared_key (* [[TLS13] *)
| early_data (* [[TLS13] *)
| supported_versions (* [[TLS13] *)
| cookie (* [[TLS13] *)
| psk_key_exchange_modes (* [[TLS13] *)
| certificate_authorities (* [[TLS13] *)
| oid_filters (* [[TLS13] *)
| post_handshake_auth (* [[TLS13] *)
.
(*
Module ExtensionType.
Program Definition encode (t:ExtensionType) : uint16 :=
match t with
| server_name => 0
| max_fragment_length => 1
| status_request => 5
| supported_groups => 10
| signature_algorithms => 13
| use_srtp => 14
| heartbeat => 15
| application_layer_protocol_negotiation => 16
| signed_certificate_timestamp => 18
| client_certificate_type => 19
| server_certificate_type => 20
| padding => 21
| key_share => 40
| pre_shared_key => 41
| early_data => 42
| supported_versions => 43
| cookie => 44
| psk_key_exchange_modes => 45
| certificate_authorities => 47
| oid_filters => 48
| post_handshake_auth => 49
end.
End ExtensionType.
*)
Variant NamedGroup :=
(*
/* Elliptic Curve Groups (ECDHE) */
secp256r1(0x0017), secp384r1(0x0018), secp521r1(0x0019),
x25519(0x001D), x448(0x001E),
/* Finite Field Groups (DHE) */
ffdhe2048(0x0100), ffdhe3072(0x0101), ffdhe4096(0x0102),
ffdhe6144(0x0103), ffdhe8192(0x0104),
/* Reserved Code Points */
ffdhe_private_use(0x01FC..0x01FF),
ecdhe_private_use(0xFE00..0xFEFF),
(0xFFFF)
*)
.
Module KeyShareEntry.
Structure KeyShareEntry :=
{
group : NamedGroup;
key_exchange : list uint8;
}.
End KeyShareEntry. Notation KeyShareEntry := KeyShareEntry.KeyShareEntry.
Definition KeyShare Handshake_msg_type :=
match Handshake_msg_type with
| client_hello => list KeyShareEntry (* client_shares<0..2^16-1> *)
| hello_retry_request => NamedGroup (* selected_group *)
| server_hello => KeyShareEntry (* server_share *)
| _ => False
end.
Module Extension.
Structure Extension Handshake_msg_type :=
{
extension_type : ExtensionType;
extension_data : match extension_type with
| key_share => KeyShare Handshake_msg_type
| _ => list uint8 (* TODO *)
end
}.
End Extension. Notation Extension := Extension.Extension.
Module ClientHello.
Structure ClientHello :=
{
legacy_version : ProtocolVersion;
random : Random;
legacy_session_id : list uint8;
cipher_suites : list CipherSuite;
legacy_compression_methods : list uint8;
extensions : list (Extension client_hello);
}.
End ClientHello. Notation ClientHello := ClientHello.ClientHello.
Module ServerHello.
Structure ServerHello :=
{
version : ProtocolVersion;
random : Random;
cipher_suite : CipherSuite;
extensions : list (Extension server_hello);
}.
End ServerHello. Notation ServerHello := ServerHello.ServerHello.
Context (
EndOfEarlyData
HelloRetryRequest
EncryptedExtensions
CertificateRequest
Certificate
CertificateVerify
Finished
NewSessionTicket
KeyUpdate
: Type).
Module Handshake.
Structure Handshake :=
{
msg_type : HandshakeType ;
length : uint24;
payload : match msg_type with
| client_hello => ClientHello
| server_hello => ServerHello
| end_of_early_data => EndOfEarlyData
| hello_retry_request => HelloRetryRequest
| encrypted_extensions => EncryptedExtensions
| certificate_request => CertificateRequest
| certificate => Certificate
| certificate_verify => CertificateVerify
| finished => Finished
| new_session_ticket => NewSessionTicket
| key_update => KeyUpdate
| message_hash => list uint8
end
}.
End Handshake. Notation Handshake := Handshake.Handshake.
Raw
TLSSecretsNotes.txt
What secrets do we have?
- long-term signing key (shared across connections)
- long-term pre-shared keys (zero or more per client)
- per-session (optional) Diffie-Hellman secret key
- derived from DH secret, DH shared key (still secret)
Signing key is used to sign some struct involving the DH public key and handshake transcript
DH shared key is used to authenticate the same struct
DH shared is used to authen application messages and decrypt messages from the wire, revealing whether the decryption succeeded and giving data to application.
pre-shared keys are used like DH shared keys, once
pre-shared keys are created based on some condition and then given to an authenticated client over an encrypted channel
both kinds of shared keys go through some splitting/key derivations for this...
there is a per-connection random value, used to distinguish between different connections
Raw
Trace.v
Require Import Coq.Lists.List.
Section Trace.
Context {state input output : Type}
(init : state -> Prop)
(step : state -> input -> output -> state -> Prop).
Inductive multistep : state -> list (input*output) -> state -> Prop :=
| multistep_nil (s:state) : multistep s nil s
| multistep_snoc (s0 s1 s2:state) l (i:input) (o:output)
(_:multistep s0 l s1)
(_:step s1 i o s2) :
multistep s0 (l++(i,o)::nil) s2.
Definition allows_behavior l :=
exists s0 s1, init s0 /\ multistep s0 l s1.
End Trace.
Raw
TraceSynthesis.v
Require Import Coq.Lists.List.
Require Import Crypto.Spec.Trace.
Require Import Crypto.Protocols.TLS13.Structures.
Require Import Crypto.Util.Decidable.
Require Import Crypto.Util.Tactics.DestructHead.
Require Import Crypto.Util.Tactics.SpecializeBy.
Require Import Crypto.Util.Tactics.GetGoal.
(* 1. Synthesize "intersection negotiation" of options, e.g., choose
curve
2. same as 1, but with "forall stream" quantifiers for multiple
connections Alternatively, we might parameterize over a record that is
FMap-like, but allows add to fail (to allow fixed number of
connections)
3. randomness - get g^x, g^y, send g^(x*y) *)
Notation eta x := (fst x, snd x).
(* TODO: multiple other messages *)
Definition output_in_list_and_previous_input_matching_satisfies
{input output} (matcher : output -> Prop) (R : input -> output -> Prop)
trace
:= forall message : input * output,
List.In message trace
-> matcher (snd message)
-> exists other_message : input * output,
List.In other_message trace
/\ R (fst other_message) (snd message).
Lemma output_in_list_and_previous_input_matching_satisfies_nil
{input output matcher R}
: @output_in_list_and_previous_input_matching_satisfies input output matcher R nil.
Proof.
intros ? H; inversion H.
Qed.
Lemma output_in_list_and_previous_input_matching_satisfies_snoc
{input output matcher R}
trace msg
: @output_in_list_and_previous_input_matching_satisfies input output matcher R trace
-> (matcher (snd msg)
-> exists other_message,
List.In other_message (trace ++ (msg::nil))
/\ R (fst other_message) (snd msg))
-> @output_in_list_and_previous_input_matching_satisfies input output matcher R (trace ++ (msg::nil)).
Proof.
unfold output_in_list_and_previous_input_matching_satisfies.
setoid_rewrite in_app_iff; simpl.
intros H0 H1 message Hin Hmatcher.
destruct_head'_or; destruct_head' False; subst; eauto.
{ specialize (H0 message); specialize_by_assumption.
destruct_head'_ex; destruct_head'_and; eauto. }
Qed.
Section Example_1_Negotiation.
Definition trace_satisfies_negotiation_spec
(trace : list (list nat (*input*) * option nat (*output*))) : Prop
:= output_in_list_and_previous_input_matching_satisfies
(fun output => True)
(fun i o => i <> nil -> exists v, o = Some v -> List.In v i)
trace.
Definition trace_satisfies_negotiation_spec_error
(trace : list (list nat (*input*) * option nat (*output*))) : Prop
:= output_in_list_and_previous_input_matching_satisfies
(fun output => True)
(fun i o => i = nil -> o = None)
trace.
End Example_1_Negotiation.
Section Example_1_Negotiation_Synthesis.
Opaque output_in_list_and_previous_input_matching_satisfies.
Lemma handle_stateless {state input output init}
{trace matcher} {R : _ -> _ -> Prop}
(handler : input -> output)
(step : state -> input -> output -> state -> Prop
:= fun _ i o _ => handler i = o)
(handler_ok : forall i, R i (handler i))
: (forall st0 st1 io, step st0 (fst io) (snd io) st1
-> R (fst io) (snd io))
-> (@allows_behavior state input output init step trace
-> output_in_list_and_previous_input_matching_satisfies
matcher R trace).
Proof.
subst step; cbv beta.
intros Hstep Hbehavior.
repeat first [ progress destruct_head_hnf' ex
| progress destruct_head'_and ].
let H := match goal with H : multistep _ _ _ _ |- _ => H end in
induction H as [|??????? IH]; subst.
{ apply output_in_list_and_previous_input_matching_satisfies_nil. }
{ repeat first [ progress specialize_by_assumption
| assumption
| apply output_in_list_and_previous_input_matching_satisfies_snoc
| setoid_rewrite List.in_app_iff
| intro
| eexists
| apply conj
| eapply (Hstep (_, _)); simpl; reflexivity
| solve [ auto ]
| progress simpl ]. }
Qed.
Lemma handle_membership_with_first {T} (default : T)
: forall i : list T, i <> nil -> In (hd default i) i.
Proof. intros [|? ?] ?; simpl; auto; congruence. Qed.
Lemma handle_membership_with_first_alt {T} (default : T) handler
: (forall i : list T, i <> nil -> handler i = Some (hd default i))
-> forall i : list T, i <> nil -> exists v, handler i = Some v -> In v i.
Proof.
intros H ls Hnil; specialize (H ls Hnil); rewrite H; clear H.
exists (hd default ls); intros _.
destruct ls; simpl; auto; congruence.
Qed.
Lemma handle_decidable_equality {T} (val : T) {Hdec : forall v, Decidable (v = val)} {U} (retv : U) handler
: forall v : T, v = val -> (if dec (v = val) then retv else handler v) = retv.
Proof.
intros; subst.
edestruct dec; congruence.
Qed.
Ltac start :=
repeat match goal with
| [ |- sigT _ ] => eexists
| [ |- sig _ ] => eexists
end.
Ltac hnf_under_and G :=
match G with
| ?A /\ ?B
=> hnf_under_and A; hnf_under_and B
| _ => let G' := (eval hnf in G) in
change G with G'
end.
Ltac hnf_under_and_goal :=
let G := get_goal in
hnf_under_and G.
Ltac start_unfold :=
lazymatch goal with
| [ |- forall trace, allows_behavior ?init ?step trace -> ?satisfies ]
=> let H := fresh in
intros ? H; hnf_under_and_goal; revert H
end.
Ltac split_and_under_arrow :=
lazymatch goal with
| [ |- allows_behavior _ _ _ -> _ ]
=> let H := fresh in
intro H; repeat apply conj; revert H
end.
Ltac handle_decidable_equality :=
lazymatch goal with
| [ |- forall v, v = ?k -> ?handler v = ?retv ]
=> is_evar handler;
let lem := constr:(@handle_decidable_equality _ k _) in
eapply (lem _ retv _)
| [ |- forall v, (if dec (@?p v = ?k) then ?retv else _) = @?q v -> @?p v = ?k -> @?q v = ?retv ]
=> intro; edestruct dec; congruence
end.
Lemma strip_handle_decidable_equality {T} (val : T) {Hdec : forall v, Decidable (v = val)} {U} (retv : U) handler (P : U -> T -> Prop)
: (forall v : T, v <> val -> P (if dec (v = val) then retv else handler v) v)
<-> (forall v : T, v <> val -> P (handler v) v).
Proof.
split; intros H v Hval; specialize (H v Hval);
edestruct dec; try assumption; congruence.
Qed.
Ltac strip_handle_decidable_equality :=
lazymatch goal with
| [ |- forall ls : ?T, ls <> ?val -> _ ]
=> let ls' := fresh ls in
let H := fresh in
intros ls' H;
lazymatch goal with
| [ |- context[if (@dec (ls' = val) ?Hdec) then ?t else ?f] ]
=> pattern (if (@dec (ls' = val) Hdec) then t else f);
let P := lazymatch goal with |- ?P _ => P end in
let P := lazymatch (eval pattern ls' in P) with ?P _ => P end in
let f := lazymatch (eval pattern ls' in f) with ?f _ => f end in
revert ls' H;
apply (proj2 (@strip_handle_decidable_equality _ val _ _ t f (fun a b => P b a)))
end
end.
Goal { state : Type
& { init : state -> Prop
& { step : _
| forall trace,
@allows_behavior state (list nat) (option nat) init step trace
-> @trace_satisfies_negotiation_spec trace
/\ @trace_satisfies_negotiation_spec_error trace} } }.
Proof.
start.
start_unfold.
split_and_under_arrow;
(eapply handle_stateless; [ | intros ?? ]);
[ > repeat first [ handle_decidable_equality
| progress cbv beta
| strip_handle_decidable_equality ].. ];
[ > repeat first [ handle_decidable_equality
| progress cbv beta
| strip_handle_decidable_equality ].. ].
{ eapply handle_membership_with_first_alt; reflexivity. }
{ cbv beta.
intros [? ?]; intros; edestruct dec; try congruence; simpl in *; subst.
eexists; intro H; inversion H; subst.
destruct_one_head list; auto; congruence. }
Grab Existential Variables.
exact 0.
exact 0.
exact (fun _ => True).
exact unit.
Defined.
End Example_1_Negotiation_Synthesis.
Import EqNotations.
Section Example_2_ServerNegotiateDH.
Context (decision_dataT : Type)
(using_diffie_hellman : decision_dataT -> bool).
Definition server_negotiation_DH_spec
(global_data : decision_dataT)
(trace : list (Handshake (*input*) * Handshake (*output*))) : Prop
:= forall io, List.In io trace
-> forall length hello,
snd io = {| Handshake.msg_type := server_hello;
Handshake.length := length;
Handshake.payload := hello |}
-> using_diffie_hellman global_data = true
<-> exists extension,
List.In extension (ServerHello.extensions hello)
/\ Extension.extension_type _ extension = key_share.
Definition server_negotiation_DH_spec'
(global_data : decision_dataT)
(trace : list (Handshake (*input*) * Handshake (*output*))) : Prop
:= forall io, List.In io trace
-> forall length hello,
snd io = {| Handshake.msg_type := server_hello;
Handshake.length := length;
Handshake.payload := hello |}
-> using_diffie_hellman global_data = true
<-> exists extension,
List.In extension (ServerHello.extensions hello)
/\ Extension.extension_type _ extension = supported_groups.
(** Sending server hello spec: if you recieve a client hello and you
send a message after it, then the message immediately following the
client hello must be either a RetryHelloRequest or a ServerHello. *)
End Example_2_ServerNegotiateDH.
(** Standing questions:
- Reuse synthesis for security verification + implementation, or separate them?
- How to specify that arbitrary choices must not depend on secret data?
- How do we recognize what data should be transient vs live in the state?
- How big of chunks should we process data in? (in flights?)
A: Probably flights
*)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment