////////////////////////////////////////////////////////////////////////////
// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved
//
// Licensed under the Apache License, Version 2.0 (the "License").
// You may not use this file except in compliance with the License.
// A copy of the License is located at
//
//  http://aws.amazon.com/apache2.0
//
// or in the "license" file accompanying this file. This file 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.
//
////////////////////////////////////////////////////////////////////////////
//
// This file executes all s2n TLS handshake proofs, including:
// - the TLS handshake state machine
// - proper corking / uncorking during the TLS handshake
//
////////////////////////////////////////////////////////////////////////////

include "spec/handshake/handshake.saw";

prove_handshake_io_lowlevel;
prove_state_machine;
prove_cork_uncork;