ikev2-running-neq-completed.spthy

/*
 * Protocol:	IKEv2
 * Modeler:	Tobias Heider & Stefan-Lukas Gazdag & Sophia Grundner-Culemann
 * Date:	09/2021
 * Status:	Done
 */

theory IKEv2
begin

builtins: asymmetric-encryption, diffie-hellman, hashing, signing,
    symmetric-encryption
functions: hmac/2

/* Tells Tamarin that whenever a Eq action occurs the two arguments must be equal */
restriction Eq_check_succeed: "All x y #i. Eq(x,y) @ i ==> x = y"

// IKEv2 Protocol

/*
 * Static Longterm Key generator
 * Keys are bound to an ID i, which is not public
 */

rule generate_static:
	[ Fr(~ltk)
	]
	--[GenStatic(pk(~ltk))]->
	[ !PrivKey($I, ~ltk)
	, !PubKey($I, pk(~ltk))
	, Out(pk(~ltk))
	]

/*
 * Key Reveals as defined in the adversary model
 */
rule reveal_static:
	[ !PrivKey($I, ltk) ]
	--[RevLtk($I)]->
	[ Out(ltk) ]


rule reveal_dh:
	[ !DHtoReveal($I, k) ]
	--[RevDH($I)]->
	[ Out(k) ]

/*
 * IKEv2 Protocol transitions
 */
rule IKE_SA_INIT_I:
let
	epI = 'g'^~eI	// < Initiator DH public share
	msg1 = <~spiI, 'IKE_SA_INIT', '1', 'i', epI, ~nI>
in
	[
	  Fr(~nI)	// < Initiator Nonce
	, Fr(~spiI)	// < Initiator SPI
	, Fr(~eI)	// < Initiator DH private share
	]
	-->
	[
	/*
	 * HDR, SAi1, KEi, Ni  -->
	 */
	  Out(msg1)
	, StateInitI($I, $R, ~spiI, ~eI, ~nI, msg1)
	, !DHtoReveal($I, ~eI)
	]

rule IKE_AUTH_I:
let
	/*
	 * Messages for auth hash
	 */
	msg2 = <spiI, spiR, 'IKE_SA_INIT', '1', 'r', epR, nR>

	/*
	 * Generate Keying Material
	 *
	 * In IKEv2 keys are read bytewise from a procedural generated byte
	 * output. In the model we have no concept of bytes, thus each key
	 * is a single block.
	 */
	k = epR^eI
	keymat = h(<nI, nR>, k)

	/*
	 * Authentication and validity of IKE_SA_INIT
	 */
	signed_octets = <msg1, nR, h(~idI, keymat)>
	auth_pl = sign(signed_octets, skI)

	/*
	 * Encryption and Integrity
	 */
	encr_pl = senc{<~idI, auth_pl, pkI>}keymat
	integ_I = hmac(<spiI, spiR, 'IKE_AUTH', '2', 'i', encr_pl>, keymat)
	msg3 = <spiI, spiR, 'IKE_AUTH', '2', 'i', encr_pl, integ_I>
in
	[ In(msg2)
	, Fr(~idI)
	, StateInitI($I, $R, spiI, eI, nI, msg1)
	, !PrivKey($I, skI)
	, !PubKey($I, pkI)
	]
	--[ Agreed(<spiI, spiR>, $I, 'initiator', $R, <nI, nR>, keymat)
	]->
	[
	/*
	 * HDR, SK {IDi, AUTH, SAi2, TSi, TSr}  -->
	 */
	  Out(msg3)
	, StateAuthI($I, $R, ~idI, spiI, spiR, nI, nR, keymat, msg1, msg2, 'g'^eI, epR)
	]

rule IKE_AUTH_COMPLETE:
let
	signed_octets_R = <msg2, nI, h(idR, keymat)>
	encr_pl_I = senc{<idR, spiC, auth_pl_R, pkR>}keymat
	integ_I = hmac(<spiI, spiR, 'IKE_AUTH', '2', 'r', encr_pl_I>, keymat)
	msg4 = <spiI, spiR, 'IKE_AUTH', '2', 'r', encr_pl_I, integ_I>

	/* Confirmation message (models an ESP packet encrypted with the newly
 	 * derived initial Child SA */
	ck = hmac(keymat, <nI, nR>)
	mTest = <'0', senc('test', ck),
	    hmac(<'0', senc('test',ck)>, ck)>
in
	[ In(msg4)
	, StateAuthI($I, $R, idI, spiI, spiR, nI, nR, keymat, msg1, msg2, epI, epR)
	, !PubKey($R, pkR)
	]
	--[ Eq(verify(auth_pl_R, signed_octets_R, pkR), true)
          , IKeys($I, $R, spiC, ck)
	  , Completed(<spiI, spiR>, $I, 'initiator', $R, keymat)
          , IdentityLearnt(idI)
	  ]->
	[ Out(mTest)
	]

rule IKE_SA_INIT_R:
let
	epR = 'g'^~eR	// < Initiator DH public share

	/*
	 * Generate Keying Material
	 *
	 * In IKEv2 keys are read bytewise from a procedural generated byte
	 * output. In the model we have no concept of bytes, thus each key
	 * is a single block.
	 */
	k = epI^~eR

	/* This is not actually true, actual keys are derived from this hash */
	keymat = h(<nI, ~nR>, k)

	/*
	 * Messages for auth hash
	 */
	msg1 = <spiI, 'IKE_SA_INIT', '1', 'i', epI, nI>
	msg2 = <spiI, ~spiR, 'IKE_SA_INIT', '1', 'r', epR, ~nR>
in
	[ In(msg1)	// < HDR, SAi1, KEi, Ni
	, Fr(~nR)	// < Responder Nonce
	, Fr(~spiR)	// < Responder SPI
	, Fr(~eR)	// < Responder DH private share
	]
	--[ Agreed(<spiI, ~spiR>, $R, 'responder', $I, <nI, ~nR>, keymat)
	]->
	[
	  Out(msg2)	// < HDR, SAr1, KEr, Nr
	, StateInitR($I, $R, spiI, ~spiR, nI, ~nR, keymat, msg1, msg2, epI, epR)
	, !DHtoReveal($R, ~eR)
	]

rule IKE_AUTH_R:
let
	/*
	 * Incoming Payloads
	 */
	signed_octets_I = <msg1, nR, h(idI, keymat)>

	encr_pl_I = senc{<idI, auth_pl_I, pkI>}keymat
	integ_I = hmac(<spiI, spiR, 'IKE_AUTH', '2', 'i', encr_pl_I>, keymat)
	msg3 = <spiI, spiR, 'IKE_AUTH', '2', 'i', encr_pl_I, integ_I>

	/*
	 * Outgoing Payloads
	 */
	signed_octets_R = <msg2, nI, h(~idR, keymat)>
	auth_pl_R = sign(signed_octets_R, skR)
	encr_pl_R = senc{<~idR, ~spiC, auth_pl_R, pkR>}keymat
	integ_R = hmac(<spiI, spiR, 'IKE_AUTH', '2', 'r', encr_pl_R>, keymat)

	msg4 = <spiI, spiR, 'IKE_AUTH', '2', 'r', encr_pl_R, integ_R>
in
	[ In(msg3)		// < Incoming message #3
	, Fr(~idR)
	, Fr(~spiC)
	, StateInitR($I, $R, spiI, spiR, nI, nR, keymat, msg1, msg2, epI, epR)
	, !PrivKey($R, skR)
	, !PubKey($R, pkR)
	, !PubKey($I, pkI)
	]
	--[ Eq(verify(auth_pl_I, signed_octets_I, pkI), true)
	  , Completed(<spiI, spiR>, $R, 'responder', $I, keymat)
          , IdentityLearnt(~idR)
	  ]->
	[ Out(msg4)
	, ChildSAR($I, $R, ~spiC, hmac(keymat, <nI, nR>))
	]

rule ChildSA_Confirm_R:
	[ In(<'0', senc('test', ck),
	    hmac(<'0', senc('test',ck)>, ck)>)
	, ChildSAR($I, $R, spiC, ck)
	]
	--[ RConfirm($I, $R, spiC, ck)
	]->
	[
	]

/*
 * == Validity ===
 */

lemma exists_session: exists-trace
    "Ex I R spi #i #j keymat.
        Completed(spi, R, 'responder', I, keymat) @ #i
        & Completed(spi, I, 'initiator', R, keymat) @ #j
	& i < j"

lemma exists_two_sessions: exists-trace
     "Ex I R spi spi2 ck ck2 #i #j #i2 #j2 .
        IKeys(I, R, spi, ck) @ i
        & RConfirm(I, R, spi, ck) @ j
 	& i < j
        & IKeys(I, R, spi2, ck2) @ i2
        & RConfirm(I, R, spi2, ck2) @ j2
 	& i2 < j2
 	& not (ck=ck2)"

/*
 * === Authentication ===
 *
 * Initiator and Responder are able to complete the handshake and agree on a
 * common key. This follows the work in "A Hierarchy of Authentication
 * Specifications" by Lowe et al.
 */

lemma aliveness[use_induction]:
/* A protocol guarantees to an agent A aliveness of another agent B if,
 * whenever A completes a run of the protocol,
 * apparently with responder B, then B has previously been running the protocol.
 */
    "All spi A B keymat role #i .
        Completed(spi, A, role, B, keymat) @ #i
        & not (Ex #k . RevLtk(B) @ k)
    ==> (Ex spi2 role2 peer nonce keymat2 #j . Agreed(spi2, B, role2, peer, nonce, keymat2) @ #j
        & #j < #i)"

lemma weak_agreement_i[use_induction]:
/* A protocol guarantees to an initiator I weak agreement with
 * another agent R if, whenever I (acting  as  initiator) completes a run of
 * the protocol, apparently with responder R, then R has previously been running
 * the protocol, apparently with I.
 */
    "All spi I R keymat #i .
        Completed(spi, I, 'initiator', R, keymat) @ #i
        & not (Ex #k . RevLtk(R) @ k)
        & not (Ex #k . RevDH(I) @ k)
        & not (Ex #k . RevDH(R) @ k)
    ==> (Ex spi2 role nonce keymat2 #j . Agreed(spi2, R, role, I, nonce, keymat2) @ #j
        & #j < #i)"

lemma weak_agreement_r[use_induction]:
/* A protocol guarantees to a responder R weak agreement with
 * another agent I if, whenever R (acting as responder) completes a run of
 * the protocol, apparently with initiator I, then I has previously been running
 * the protocol, apparently with R.
 */
    "All spi I R keymat #i .
        Completed(spi, R, 'responder', I, keymat) @ #i
        & not (Ex #k . RevLtk(I) @ k)
        & not (Ex #k . RevLtk(R) @ k)
        & not (Ex #k . RevDH(I) @ k)
        & not (Ex #k . RevDH(R) @ k)
    ==> (Ex spi2 role nonce keymat2 #j . Agreed(spi2, I, role, R, nonce, keymat2) @ #j
        & #j < #i)"

lemma agreement_i[use_induction]:
/* A protocol guarantees to an initiator I agreement with a responder R on a
 * set S if, whenever I (acting as initiator) completes a run
 * of the protocol, apparently with responder R, then R has previously been
 * running the protocol, apparently with I, and R was acting as responder in his
 * run, and the two agents agreed on the data values corresponding to all the
 * variables in S, and each such run of I corresponds to a unique run of R.
 */
    "All spi I R keymat #j .
        Completed(spi, I, 'initiator', R, keymat) @ #j
        & not (Ex #k . RevLtk(R) @ k)
        & not (Ex #k . RevDH(I) @ k)
        & not (Ex #k . RevDH(R) @ k)
    ==> (Ex spi2 #k .
        Completed(spi2, R, 'responder', I, keymat) @ #k)"
		
lemma agreement_r[use_induction]:
/* A protocol guarantees to a responder R agreement with an initiator I on a
 * set S if, whenever R (acting as responder) completes a run
 * of the protocol, apparently with initiator I, then I has previously been
 * running the protocol, apparently with R, and I was acting as initiator in his
 * run, and the two agents agreed on the data values corresponding to all the
 * variables in S, and each such run of R corresponds to a unique run of I.
 */
    "All spi I R keymat #j .
        Completed(spi, R, 'responder', I, keymat) @ #j
        & not (Ex #k . RevLtk(I) @ k)
		& not (Ex #k . RevLtk(R) @ k)
        & not (Ex #k . RevDH(I) @ k)
        & not (Ex #k . RevDH(R) @ k)
    ==> (Ex spi2 #k .
        Completed(spi2, I, 'responder', R, keymat) @ #k)"

lemma session_uniqueness:
    "All I R spi spi2 keymat role #j #l.
        Completed(spi, I, role, R, keymat) @ #j
        & Completed(spi2, I, role, R, keymat) @ #l
    ==> (#j = #l)"

/*
 * === Consistency ===
 */

lemma consistency:
    "All spi I R keymat keymat2 #i #j .
        Completed(spi, I, 'initiator', R, keymat) @ #i
        & Completed(spi, R, 'responder', I, keymat2) @ #j
        & not (Ex #k . RevLtk(R) @ k)
    ==> (keymat=keymat2)"

/*
 * === Key Secrecy ===
 */

lemma key_secrecy[reuse]:
    "All spi I R role keymat #j .
        Completed(spi, I, role, R, keymat) @ #j
        & not (Ex #m . RevLtk(R) @ #m)
        & not (Ex #m . RevDH(I) @ #m)
        & not (Ex #m . RevDH(R) @ #m)
    ==> not (Ex #m . K(keymat) @ #m)"

/*
 * === Identity Hiding ===
 */
lemma identity_hiding_R:
    "All spi I R keymat id #i .
        Completed(spi, R, 'responder', I, keymat) @ #i
        & IdentityLearnt(id) @ #i
        & not (Ex #k . RevLtk(I) @ #k)
        & not (Ex #k . RevDH(I) @ #k)
        & not (Ex #k . RevDH(R) @ #k)
    ==> not (Ex #j .  K(id) @ #j)"

end
//vim: ft=spthy