Hi Hammell, This is interesting. Thank you for doing this work to systematically confirm the logic and the state machine of the protocol update.
You assumptions are correct. - The Have_PPK indeed means we have a PPK configured for the PPK_ID sent in the initiator's notification. - The PPK Mandatory indeed is there to prevent downgrades when configured but also allow for backwards compatibility when disabled. Rgs, Panos -----Original Message----- From: IPsec <ipsec-boun...@ietf.org> On Behalf Of Hammell, Jonathan F Sent: Thursday, November 01, 2018 2:43 PM To: 'ipsec@ietf.org' <ipsec@ietf.org> Subject: [IPsec] Verification of IKEv2 PPK Classification: UNCLASSIFIED Researchers at the Canadian Centre for Cyber Security (CCCS) have modeled the state machine of the IKEv2 PPK I-D draft-ietf-ipsecme-qr-ikev2-04 in order to verify the logic. The attached file qr_ppk_responder.smv contains a model written for NuSMV (http://nusmv.fbk.eu) of an asynchronous finite-state machine modelling the responder role described in the I-D. The file also contains CTL specifications of the 7 conditions presented in the table on page 8 of the draft. To run, please install a recent version of NuSMV and run the command ./NuSMV qr_ppk_responder.smv The output shows the results of the application of the CTL specifications to the model. We also include several CTL sanity checks for the model, but they are currently disabled in order to be clear about the claims. Comments about the implementation of the draft: The table on page 8 was found to be essential in developing a working model.. Several of the table conditions needed some interpretation and we hope ours is correct. "Have PPK" Our interpretation was that "Have PPK" specifies whether a Responder shared a valid PPK with an Initiator. We noted that in order for determination to be made whether he did nor not, the Responder would first need to receive an ID either in the PPK_IDENTITY notification or from the IDi payload (if configured to do so), and then check whether the ID was known and if it was whether or not a PPK was configured for this ID. In our implementation for example, we modelled that a Responder shared a PPK with the initiator with the condition: NOTIFY.PPK_ID = TRUE & VERIFY.PPK_ID_KNOWN =TRUE Which states that a PPK_ID notify was received and that the ID from the notify was known Equivalently he could use the ID from the Idi payload if configured appropriately, which is expressed as follows NOTIFY.PPK_ID = TRUE & VERIFY.PPK_ID_KNOWN = FALSE & VERIFY.PAYLOAD_ID_KNOWN = TRUE & CONFIG.USE_ID_PAYLOAD = TRUE In both cases after a successful ID check, they will then check whether they actually share a PPK i.e VERIFY.HAVE_PPK = TRUE "PPK Mandatory" Our interpretation is that PPK Mandatory limits successful completion of the handshake to cases where the parties share a PPK, in this case no downgrade is possible. The check occurs after a successful ID check and at the same time as the check to see if they share a PPK. If it is mandatory, the only non-error path is when they share a PPK. CONFIG.PPK_MANDATORY = TRUE & VERIFY.HAVE_PPK = TRUE If you have comments/questions, reply to the list or we can chat in Bangkok.. Jonathan Hammell Canadian Centre for Cyber Security https://cyber.gc.ca _______________________________________________ IPsec mailing list IPsec@ietf.org https://www.ietf.org/mailman/listinfo/ipsec
