nts-c030ut.pvl 12.29 KiB
(*---------------------------------------------+
|--- DEFINITION OF CRYPTOGRAPHIC PRIMITIVES ---|
|----------- PROTOCOL-INDEPENDENT -------------|
|----------------------------------------------|
|-----------------[NTS v0.3.0ut]---------------|
+---------------------------------------------*)
(* Basics: Keys [No Hostnames, as opposed to v0.3.0]. *)
type key.
(* Symmetric Encryption *)
fun senc(bitstring, key): bitstring.
reduc forall m: bitstring, k: key; sdec(senc(m,k),k) = m.
(* Asymmetric Encryption *)
type skey.
type pkey.
fun sk_of(bitstring): skey [private].
fun pk(skey): pkey.
letfun pk_of(X: bitstring) = pk(sk_of(X)).
fun aenc(bitstring, pkey): bitstring.
reduc forall m: bitstring, k: skey; adec(aenc(m, pk(k)), k) = m.
(* Asymmetric Signatures *)
type sskey.
type spkey.
fun ssk_of(bitstring): sskey [private].
fun spk(sskey): spkey.
letfun spk_of(X: bitstring) = spk(ssk_of(X)).
fun sign(bitstring, sskey): bitstring.
reduc forall m: bitstring, k: sskey; getmess(sign(m,k)) = m.
reduc forall m: bitstring, k: sskey; checksign(sign(m,k), spk(k)) = m.
letfun signed_message(m: bitstring, k: sskey) = (m, sign(m, k)).
(* Hash and HMAC Functions *)
fun hash(bitstring): bitstring.
fun keyhash(pkey): bitstring.
fun seed_of(bitstring): bitstring [private].
fun cookie_gen(bitstring, bitstring): key.
fun hmac(key, bitstring): bitstring.
(*----------------------------------+
|--- DEFINITION OF THE PROTOCOL: ---|
|----------- VARIABLES -------------|
|-----------------------------------|
|------------[NTS v0.3.0ut]---------|
+----------------------------------*)
(* The Channel for All "Network" Protocol Communications *)
free c: channel.
(* The Channel and Bitstring for Communication with the TA *)
free ta: channel.
free TA: bitstring.
(* Two Possible Version Identifiers *)
free version_1: bitstring.
free version_2: bitstring.
(*----------------------------------+
|--- DEFINITION OF THE PROTOCOL: ---|
|------------- EVENTS --------------|
|-----------------------------------|
|------------[NTS v0.3.0ut]---------|+----------------------------------*)
(* Server Side Events *)
event serverError().
event serverHasOwnCert(bitstring, pkey, spkey).
event serverRespondsTime(bitstring, bitstring, bitstring).
event serverSaysCookie(key, pkey, bitstring).
event serverGeneratesCookie(key, bitstring).
event serverAcceptsCert(bitstring).
event serverRejectsCert().
(* Client Side Events *)
event clientError().
event clientHasOwnCert(bitstring, pkey, spkey).
event clientAcceptsCookie(key, bitstring, bitstring).
event clientAcceptsSomeCookie().
event clientRejectsCookie(key, bitstring, bitstring).
event clientRejectsSomeCookie().
event cookieCompromised(key).
event clientAcceptsCert(bitstring, spkey).
event clientRejectsCert().
event client_timereq(bitstring).
event clientAcceptsTime(bitstring, bitstring, bitstring).
event clientDiscards(bitstring).
(* Authority Side Event(s) *)
event authorityGivesCert(bitstring, pkey, spkey).
(* Stupid Debugging Event*)
event check().
(*----------------------------------+
|--- DEFINITION OF THE PROTOCOL: ---|
|------------ PROCESSES ------------|
|-----------------------------------|
|-------------[NTS v0.3.0ut]--------|
+----------------------------------*)
(*-------------------------------------+
|--- Trusted Authority Side Process ---|
+-------------------------------------*)
(* [Process] ::: TRUSTED AUTHORITY ::: [NTS v0.3]
|: Gives out certificates on request. *)
let authority() =
let skTA = ssk_of(TA) in
(* The authority receives a certificate request. *)
in(ta, H: bitstring);
(* The authority determines the correct public keys. *)
let pkH = pk(sk_of(H)) in
let spkH = spk(ssk_of(H)) in
(* The authority assembles and signs the certificate. *)
let certificate = (H, pkH, spkH) in
let signature = sign(certificate, skTA) in
let certificate_sig = (certificate, signature) in
(* The authority sends the response back to the requesting party. *) event authorityGivesCert(H, pkH, spkH);
out(ta, certificate_sig).
(*----------------------------+
|--- Server Side Processes ---|
+----------------------------*)
(* [Process] ::: SERVER CERTIFIER MODULE ::: [NTS v0.3]
|: Replies to a client_cert message with a server_cert
|: message as specified. *)
let server_certifier(B: bitstring, pkB: spkey, skB: sskey) =
(* The server acquires the TA's public key. *)
let pkTA = spk(ssk_of(TA)) in
(* The server receives a client's certification request. *)
in (c, X_client_cert: bitstring);
(* The server extracts the necessary information. *)
let (version_x: bitstring, A_x: bitstring) = X_client_cert in
(* [ATTENTION] [TODO] The server creates a signature of the
received version number. *)
(* let version_signature = sign(version_x, skB) in *)
(* The server requests its certificate chain from the TA
and performs a validity check on the response it receives. *)
out (ta, B);
in (ta, Z_certificate: bitstring);
let (=B, some_key: pkey, =pkB, Z_cert_signature: bitstring) = Z_certificate in
if (B, some_key, pkB) <> checksign(Z_cert_signature, pkTA)
then event serverError()
else event serverHasOwnCert(B, some_key, pkB);
(* The server creates a server_cert response as specified. *)
let msg_server_cert = (A_x, Z_certificate) in
let msg_server_cert_sign = (A_x, Z_certificate, sign(A_x, skB)) in
(* The server sends the composed response to the requesting client. *)
out(c, msg_server_cert_sign).
(* [Process] ::: SERVER COOKIE MODULE ::: [NTS v0.3]
|: Takes a client_cook request, generates the approproate cookie
|: and replies with a server_cook message as specified. *)
let server_cookie(B: bitstring, pkB: spkey, skB: sskey, seed: bitstring) =
(* The server acquires the TA's public key. *)
let pkTA = spk(ssk_of(TA)) in
(* The server receives a client's cookie request. *)
in(c, X_cook: bitstring);
(* The server matches it to the specified message pattern
and extracts the necessary information. *)
let (n_x: bitstring, pkA_x: pkey) = X_cook in
(* The server builds the cookie for the received client
(identified via its public [encryption] key pkA. *)
let cookie = cookie_gen(keyhash(pkA_x), seed) in
(* It builds the appropriate response *)
let response = (cookie, n_x) in
(* It constructs its signature and attaches it to the response. *)
let signature = sign(response, skB) in
let response_sig = (response, signature) in
(* It encrypts it. *) let response_sig_enc = aenc(response_sig, pkA_x) in
(* It sends it back to the client. *)
event serverGeneratesCookie(cookie, B);
event serverSaysCookie(cookie, pkA_x, B);
out(c, response_sig_enc).
(* [Process] ::: SERVER TIMESYNC MODULE ::: [NTS v0.3]
|: replies to a time_request message with a time_response
|: message as specified in NTS v0.3. *)
let server_time_response(B: bitstring, pkB: spkey, skB: sskey, seed: bitstring) =
(* The server receives a client's time_request message. *)
in(c, Y: bitstring);
(* It extracts the necessry data. *)
let (t1_y: bitstring, n_y: bitstring, pkA_hash_y: bitstring) = Y in
(* It creates the appropriate time sync data for its response. *)
new t2: bitstring;
(* It re-computes the cookie. *)
let cookie = cookie_gen(pkA_hash_y, seed) in
(* It composes its response. *)
let response = (n_y, t1_y, t2, hmac(cookie, (n_y, t1_y, t2))) in
(* It sends its response back to the requesting client. *)
event serverRespondsTime(n_y, t1_y, t2);
out(c, response).
(* [Process] ::: SERVER GLOBAL PROCESS ::: [NTS v0.3]
executes all server modules at once, running arbitrarily
many instantiations of each of them in parallel. *)
let server(B: bitstring) =
(* Before running any modules, the server generates an
unpredictable seed value and remembers its key pair. *)
let seed = seed_of(B) in
let skB = ssk_of(B) in
let pkB = spk(skB) in
(* The server then runs all modules. *)
(* !server_associator(B, pkB) | *)
!server_certifier(B, pkB, skB) |
!server_cookie(B, pkB, skB, seed) |
!server_time_response(B, pkB, skB, seed).
(*----------------------------+
|--- Client Side Processes ---|
+----------------------------*)
(* [Process] ::: CLIENT TIMESYNC MODULE ::: [NTS v0.3]
|: Generates time_request messages as specified in NTS v0.3 and
|: sends them to a time server. It then awaits a time_response message
|: on which it performs the necessary checks, as specified. *)
let client_time_request(A: bitstring, pkA: pkey, B: bitstring, cookie: key) =
(* The client generates time data and a nonce. *)
new t1: bitstring;
new n1: bitstring;
event client_timereq(t1);
(* The client constructs its time_request message and sends it. *)
let request = (t1, n1, keyhash(pkA)) in
out(c, request);
(* It receives a time_response message and
extracts the necessary information. *)
in(c, X: bitstring);
let(=n1, =t1, t2x: bitstring, hmacx: bitstring) = X in
(* Depending on the result of validity checks, it either
accepts the response as authentic or discards it. *)
if hmacx = hmac(cookie, (n1, t1, t2x))
then event clientAcceptsTime(n1, t1, t2x)
else event clientDiscards(X).
(* [Process] ::: CLIENT GLOBAL PROCESS ::: [NTS v0.3]
|: Executes the association, certification and cookie exchange steps,
|: one of each and sequentially. Then it executes the client timesync
|: module, running arbitrarily many instances of it in parallel. *)
let client(A: bitstring, B: bitstring) =
let skA = sk_of(A) in
let pkA = pk(skA) in
let pkTA = spk(ssk_of(TA)) in
(* CERTIFICATE PHASE ----------------------------------------------*)
(* The client sends a client_cert message,
as specified in NTS v0.3. *)
let msg_client_cert = (A) in
out(c, msg_client_cert);
(* The client receives a response of type server_cert. *)
in(c, X_server_cert: bitstring);
(* The client extracts data from the response. *)
let (=A, certificate_x: bitstring, signature_x: bitstring) = X_server_cert in
(* The client reads the certificate. *)
let (=B, other_key: pkey, spkB_x: spkey, cert_signature: bitstring) = certificate_x in
(* The clients performs the necessary test. At failure, it
exits with an error. At success, the client accepts the
public key given in the certificate as B's public key. *)
event check();
if ((B, other_key, spkB_x) <> checksign(cert_signature, pkTA))
|| ( A <> checksign(signature_x, spkB_x))
then event clientRejectsCert()
else event clientAcceptsCert(B, spkB_x);
let pkB = spkB_x in
(* COOKIE PHASE ---------------------------------------------------*)
(* The client sends a client_cook message,
as specified (in NTS v0.3). *)
new n_cook: bitstring;
let msg_client_cook = (n_cook, pkA) in
out(c, msg_client_cook);
(* The client receives a response of type server_cook. *)
in(c, X_server_cook: bitstring);
(* It decodes the response and extracts
the data from it. *)
let X_dec = adec(X_server_cook, skA) in
let ((cookie_x: key, =n_cook), signature_x: bitstring) = X_dec in
(* It performs the necessary checks as specified. On success,
it starts sending out time_request messages as specified.*)
(if (cookie_x, n_cook) = checksign(signature_x, pkB) then event clientAcceptsCookie(cookie_x, A, B)
(* TIMESYNC PHASE ------------------------------------*)
| !client_time_request(A, pkA, B, cookie_x)
| ( in(c, =cookie_x); event cookieCompromised(cookie_x) )
else event clientRejectsCookie(cookie_x, A, B)).