2016-10-14 09:05:37 +00:00
|
|
|
|
|
|
|
(*
|
|
|
|
* Formal definition to verify the Fenrir protocol.
|
|
|
|
* to be used with ProVerif
|
|
|
|
*
|
|
|
|
* This is to verify the correctness of the full 3-RTT handshake.
|
|
|
|
* DNSSEC is NOT verified, as it is assumed to be correct.
|
|
|
|
*
|
|
|
|
* compared to the handshakes, we have a lot less to check, so the tests are very quick
|
|
|
|
*)
|
|
|
|
|
|
|
|
(*
|
|
|
|
* ==============
|
|
|
|
* Type definition
|
|
|
|
* ==============
|
|
|
|
*)
|
|
|
|
|
|
|
|
type pubKey. (* public key for asymmetric key encryption *)
|
|
|
|
type privKey. (* private key for asymmetric key encryption *)
|
|
|
|
type sKey. (* symmetric key *)
|
|
|
|
type nonce. (* just a nonce *)
|
|
|
|
|
|
|
|
const leak: channel. (* to leak private material *)
|
|
|
|
const cs_xor: channel. (* service-fenrir channel for xor otp auth *)
|
|
|
|
|
|
|
|
(* various stuff that should remain private *)
|
|
|
|
const prS: privKey [private]. (* service private key *)
|
|
|
|
const OTP: sKey [private].
|
|
|
|
free csKey: sKey [private].
|
|
|
|
|
|
|
|
|
|
|
|
(*
|
|
|
|
* ==============
|
|
|
|
* Function definition
|
|
|
|
* ==============
|
|
|
|
*)
|
|
|
|
|
|
|
|
(* any to bitstring conversion *)
|
|
|
|
fun fromKey(sKey) : bitstring.
|
|
|
|
reduc forall a : sKey; toKey(fromKey(a)) = a.
|
|
|
|
|
|
|
|
|
|
|
|
(* symmetric key encription *)
|
|
|
|
fun sEnc(bitstring, sKey): bitstring. (* encrypt with symmetric key *)
|
|
|
|
reduc forall c: bitstring, k: sKey; sDec(sEnc(c,k),k) = c. (* decrypt with symmetric key *)
|
|
|
|
|
|
|
|
(* public key definition *)
|
|
|
|
fun genPub(privKey): pubKey. (* public keys are generated from private ones *)
|
|
|
|
fun aEnc(bitstring, pubKey): bitstring. (* encrypt with asymmetric public key *)
|
|
|
|
reduc forall c: bitstring, k: privKey; aDec(aEnc(c,genPub(k)),k) = c. (* decrypt with private key *)
|
|
|
|
(* public key signing *)
|
|
|
|
fun sign(bitstring, privKey): bitstring.
|
|
|
|
reduc forall c: bitstring, k: privKey; ver(c, sign(c, k), genPub(k)) = true. (* verify signature *)
|
|
|
|
(* integrity for encrypt then mac *)
|
|
|
|
fun int(bitstring, sKey): bitstring.
|
|
|
|
reduc forall c: bitstring, k: sKey; verint(c, int(c, k), k) = true.
|
|
|
|
|
|
|
|
(* some key exchange based on public keys *)
|
|
|
|
fun exchange(privKey, pubKey) : sKey.
|
|
|
|
equation forall p1 : privKey, p2 : privKey; exchange(p1, genPub(p2)) = exchange(p2, genPub(p1)).
|
|
|
|
|
|
|
|
(* hash used by OTP, sKey based *)
|
|
|
|
fun hash(sKey) : sKey.
|
|
|
|
|
|
|
|
(* xor function *)
|
|
|
|
(* note: this xor function doe not handle associativity as proverif would loop,
|
|
|
|
* so we pay attention to use it in a way that does not require associativity
|
|
|
|
*)
|
|
|
|
fun xor(sKey, sKey) : sKey.
|
|
|
|
reduc forall a : sKey, b : sKey; unxor(xor(a, b), b) = a.
|
|
|
|
reduc forall a : sKey, b : sKey; unxor2(xor(a, b), a) = b. (* created for proverif, not used for simplicity *)
|
|
|
|
|
|
|
|
|
|
|
|
(*
|
|
|
|
* ==============
|
|
|
|
* Events -- used for correlation
|
|
|
|
* ==============
|
|
|
|
*)
|
|
|
|
event clientConnect(sKey).
|
|
|
|
event serviceConnect(sKey).
|
|
|
|
|
|
|
|
|
|
|
|
(* rekeying algorithm *)
|
|
|
|
|
|
|
|
let client_rekey (key: sKey, chan: channel, pb : pubKey) =
|
|
|
|
new rekey_p1: privKey;
|
|
|
|
new rekey_n1: nonce;
|
|
|
|
out (chan, sEnc((rekey_n1, genPub(rekey_p1)), key));
|
|
|
|
in (chan, enc: bitstring);
|
|
|
|
let (=rekey_n1, srv_eph : pubKey, signed : bitstring) = sDec(enc, key) in
|
|
|
|
if ver((rekey_n1, srv_eph), signed, pb) then
|
|
|
|
let (new_Key) = exchange(rekey_p1, srv_eph) in
|
|
|
|
out (chan, sEnc((OTP, OTP), new_Key)) (* test secrecy *)
|
|
|
|
.
|
|
|
|
|
|
|
|
let server_rekey (key: sKey, chan: channel, pr : privKey) =
|
|
|
|
new rekey_s_p: privKey;
|
|
|
|
in (chan, enc: bitstring);
|
|
|
|
let (client_n1: nonce, client_p: pubKey) = sDec (enc, key) in
|
|
|
|
out (chan, sEnc((client_n1, genPub(rekey_s_p), sign((client_n1, genPub(rekey_s_p)), pr)), key));
|
|
|
|
let (new_Key) = exchange(rekey_s_p, client_p) in
|
|
|
|
in (chan, enc2: bitstring);
|
|
|
|
let (=OTP, =OTP) = sDec(enc2, new_Key)
|
|
|
|
.
|
|
|
|
|
|
|
|
|
|
|
|
(* test the OTP between the service and client. Assume that the authentication server
|
|
|
|
* has been compromised. *)
|
|
|
|
|
|
|
|
(* assume that the client and service have not yet setup an OTP *)
|
|
|
|
|
|
|
|
let service_no_otp() =
|
|
|
|
(* this first sent/received messages are relayed to the service/client by the AS *)
|
|
|
|
in (cs_xor, (enc: bitstring, pb: pubKey));
|
|
|
|
let key = exchange(prS, pb) in
|
|
|
|
let bitOTP = sDec(enc, key) in
|
|
|
|
let sOTP = toKey(bitOTP) in
|
|
|
|
(* this should be cskey XOR hash(OTP), but proverif can't handle XOR.
|
|
|
|
* so we treat it as encryption, as it has the same properties in our case *)
|
|
|
|
let xored = xor(csKey, hash(sOTP)) in
|
|
|
|
out (cs_xor, xored);
|
|
|
|
in (cs_xor, enc2 : bitstring);
|
|
|
|
let is_OTP = sDec(enc2, csKey) in
|
|
|
|
if sOTP = toKey(is_OTP) then
|
|
|
|
event clientConnect(csKey);
|
|
|
|
server_rekey(csKey, cs_xor, prS).
|
|
|
|
|
|
|
|
let client_no_otp(OTP: sKey, pbS: pubKey) =
|
|
|
|
(* this first message is actually sent to the AS, but gets relayed to the service *)
|
|
|
|
new pr : privKey;
|
|
|
|
out (cs_xor, sEnc(fromKey(OTP), exchange(pr, pbS)));
|
|
|
|
in (cs_xor, xored : sKey);
|
|
|
|
let xorKey = unxor(xored, hash(OTP)) in
|
|
|
|
event serviceConnect(xorKey);
|
|
|
|
out (cs_xor, sEnc(fromKey(OTP), xorKey));
|
|
|
|
client_rekey(xorKey, cs_xor, pbS).
|
|
|
|
|
|
|
|
(* now assume that there is a shared OTP *)
|
|
|
|
|
|
|
|
let service_otp(OTP : sKey) =
|
|
|
|
(* this should be cskey XOR hash(OTP), but proverif can't handle XOR.
|
|
|
|
* so we treat it as encryption, as it has the same properties in our case *)
|
|
|
|
let xorK = sEnc(fromKey(csKey), hash(OTP)) in
|
|
|
|
out (cs_xor, (xorK, xorK));
|
|
|
|
in (cs_xor, enc2 : bitstring);
|
|
|
|
let is_OTP = sDec(enc2, csKey) in
|
|
|
|
if OTP = toKey(is_OTP) then
|
|
|
|
event clientConnect(csKey);
|
|
|
|
server_rekey(csKey, cs_xor, prS).
|
|
|
|
|
|
|
|
let client_otp(OTP: sKey, pbS: pubKey) =
|
|
|
|
in (cs_xor, enc : bitstring);
|
|
|
|
let xorKey = sDec(enc, hash(OTP)) in
|
|
|
|
event serviceConnect(toKey(xorKey));
|
|
|
|
out (cs_xor, sEnc(fromKey(OTP), toKey(xorKey)));
|
|
|
|
client_rekey(toKey(xorKey), cs_xor, pbS).
|
2023-02-10 14:45:12 +00:00
|
|
|
|
|
|
|
|
2016-10-14 09:05:37 +00:00
|
|
|
(*
|
|
|
|
* Event correlation:
|
|
|
|
*)
|
|
|
|
query k : sKey; event(clientConnect(k)) ==> event(serviceConnect(k)).
|
|
|
|
|
|
|
|
(*
|
|
|
|
* ==============
|
|
|
|
* What should be secret?
|
|
|
|
* ==============
|
|
|
|
*)
|
|
|
|
|
|
|
|
query attacker(OTP). (* client-service OTP data. *)
|
|
|
|
|
|
|
|
(*
|
|
|
|
* ==============
|
|
|
|
* Run the verification
|
|
|
|
* ==============
|
|
|
|
*)
|
|
|
|
|
|
|
|
(* make it easy to deactivate single parts, like the 2-RTT login, which has unproven events problems *)
|
|
|
|
|
|
|
|
(* TODO: fix PFS: must leak both server and client public key *)
|
|
|
|
process
|
|
|
|
(!service_no_otp()) | (!client_no_otp(OTP, genPub(prS)))
|
|
|
|
| phase 1; (!service_otp(OTP)) | (!client_otp(OTP, genPub(prS)))
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|