| While there have been remarkable advances in proving real-world cryptographic protocols such as IKE [26], IEEE 802.11i [43], and TLS [18, 38, 43, 59] secure, the cryptographic community usually models the protocol under analysis in a simplistic manner, routinely omitting aspects that are potentially security-relevant, such as parameter negotiations, protocol options, authenticated message fields, or key derivation arguments.;To allow more accurate representations, yet tame the complexity of real-world protocols, we propose a framework of partially specified protocols (PSPs). In this approach, we divide such complex protocols into the protocol core (PC), a compact component that performs functions essential for the cryptographic goal of interest, and protocol details (PD), which handle the remainder. The PC may contain calls to the PD in order to delegate complexities irrelevant to the analysis or model behavior that is optional or unspecified. Security is defined by running the PC in a Bellare-Rogaway-style prescriptive model, but having the adversary service the PD calls. The idea behind PSPs translates to other models, too.;To demonstrate the PSP approach, we present models for mutual authentication (MA) and authenticated key establishment (AKE) in both asymmetric and symmetric trust models, expanding on an earlier publication [68]. Our goals include the distribution of associated data (AD), information that is authenticated but not confidential. In our experience, all real-world mutual authentication protocols also distribute AD.;Both our models and protocols are described in code, while our proofs use code-based games. We find this setup helps avoid ambiguous and verbose definitions.;To test the PSP approach, we extend the Needham-Schroeder-Lowe public-key authentication protocol to a PSP we name NSL2, adding in AD and calls to the PD so that it could be embellished as if it were specified in an industry standard. We prove NSL2 provides MA if the underlying encryption scheme is CCA-secure.;Finally, we model the AMPE protocol from the IEEE 802.11s draft standard for mesh networking [70] as a PSP. Exemplifying the complexities of real-life protocols, AMPE negotiates multiple kinds of AD, contains underspecified parts, and shares its authentication keys with a separate protocol. Despite these challenges, the PSP methodology allows us to reduce the AKE security of AMPE to the underlying deterministic authenticated-encryption (DAE) scheme and pseudorandom function. We show that the PSP indeed is an abstraction of the standard by giving an implementation of the PD. For the case when AMPE is based on the DAE scheme SIV built from a blockcipher B and its key derivation uses a Merkle-Damgard hash function H in HMAC mode, we reduce the security of AMPE to the security of blockcipher B and the round function of H.;In the process, we discover that the AMPE specification declares as AD data which does not appear to be distributed by the protocol, a potential security vulnerability. |
