S
, R
, and A
are all programs sharing a communication channel
A
is typically a polynomially bounded computational entity
Sender (S) network> Receiver (R)
^


v
Adversary (A)
When R
accepts a message m
from S
only when S
actually sent m
S:send m
or R:receive m
R:receive m
event in a trace is preceded by a S:send m
No information about any secrets sent by S
is leaked to A
A
are independent of the secrets
val sender (secret:bytes) (public:bytes) : bytes
let no_leakage = forall s0 s1 p. sender s0 p == sender s1 p
S
cannot communicate anything useful about its secret to the R
if the messages carries no information about R
!
But, using cryptography, we can prove probabilistic security guarantees
A
cannot distinguish the bytes exhanged by S
and R
from a random
string of bytes, except perhaps with a small probability.
A game G
is a program with several procedures and shared state
Adversary A
interacts with G
A
wins if they get G
some procedure to emit a specific result (e.g., true
)
Goal: Show that the probability of A
winning is low
I found the following resources useful:
Secrecy property for encryption schemes
let ind_cpa (encrypt : key > msg > cipher) =
(* A secret key and secret bit *)
let key = sample_random_key () in
let b : bool = random_sample_bit () in
(* Encrypt either message, depending on the bit *)
let left_or_right (m0, m1) =
if b
then encrypt key m0
else encrypt key m1 in
(* Check the attacker's guess *)
let check guess = b=guess in
left_or_right,
check
Attacker's advantage is the probability of guessing right more than half the time
The definition of INDCPA is meant to be selfevidently useful notion of ciphertext indistinguishability
Sometimes, it is possible to prove semantic security (like INDCPA) of some encryption schemes based on other assumptions
But, this is out of scope for us
Usually, one assumes that certain schemes (e.g., AES with IVs) are INDCPA, for some symbolic
An authenticity property for MessageAuthentication Codes (MACs)
A MAC: t = mac m k
could only be effectively produced through
knowledge of the secret key k
, i.e., t
cannot be forged.
Authentication by “log lookup”: UFCMA secure if the probability of an adversary forging a tag is .
let uf_cma (mac: key > msg > tag, verify: key > msg > tag > bool) =x
(* Sample a random key *)
let k = sample_random_key () in
(* Allocate a log *)
let log : ref (list (msg * tag)) = alloc [] in
(* mac wrapper: call mac and log it *)
let mac (m:msg) =
let t = mac m k in
log := (m, t) :: !log;
t in
(* verify wrapper: correct verify using the log *)
let verify (m:msg) (t:tag) =
let b = verify k m t in
b && (m, t) `notin` !log in
mac, verify
We want
ae_enc
that:
ae_dec
that:
And prove that it is semantically secure with an advantage proportionate to
HMACSHA1 as a total function in F*
let hmac_sha1 (k:sha1_key) (m:msg) : tag =
let x5c = byte_of_int 92 in
let x36 = byte_of_int 54 in
let opad = Seq.create blocksize x5c in
let ipad = Seq.create blocksize x36 in
let xor_key_opad = xor keysize k opad in
let xor_key_ipad = xor keysize k ipad in
sha1 (xor_key_opad `Seq.append`
(sha1 (xor_key_ipad `Seq.append` m)))
We're going to assume that HMACSHA1 is UFCMA secure
But, how best to state that assumption?
let mac_verify () =
let key = sample_random_key ()
let log = ref [] in
let mac k m =
let t = hmac_sha1 k m in
if Flag.idealizing uf_cma (* BRANCHING HERE IS A CRYPTO HYPOTHESIS *)
then log := (m, t) :: !log;
t
in
let verify k m t =
let ok = (t = hmac_sha1 k m) in
if Flag.idealizing uf_cma (* BRANCHING HERE IS A CRYPTO HYPOTHESIS *)
then ok && (!log `contains` (m, t))
else ok
in
mac, verify
mac_verify[uf_cma=true]
mac_verify[uf_cma=false]
concrete_ae
=
ae [ideal_ae=false]
=
mac_verify[uf_cma=false] . enc_dec[ind_cpa=false]
~_e
mac_verify[uf_cma=true] . enc_dec[ind_cpa=false]
~_e'
mac_verify[uf_cma=true] . enc_dec[ind_cpa=true]
=
ae [ideal_ae=true]
val f : 'a > 'a
. What is (f 0)
?
val g : 'a > int
. What is (g 0)
? What is (g 1)
?
Welltyped code gains no information about its parametrically typed arguments
module Plain
val plain : Type
module Client
val f : plain > int
Client.f p
?
Client.f q
Plain.plain
module Plain
val plain : Type
val repr (p:plain{not ind_cpa}) : bytes (* cannot break confidentiality if ind_cpa *)
val coerce (b:bytes{not uf_cma}) : plain (* cannot break integrity if uf_cma *)
repr
that allows breaking confidentiality
ideal_ind_cpa = false
)
coerce
that allows breaking integrity
ideal_uf_cma = false
)
let ind_cpa () =
let key = sample_random_key () in
let log = ref [] in
let encrypt (p:Plain.plain) : bytes =
let q =
if Idealizing.ind_cpa (*!!! AUDIT, Crypto Hypothesis *)
then zeroes
else Plain.repr p
in
let cipher = encrypt key q in
if ideal_ind_cpa (*!!! AUDIT, Crypto Hypothesis *)
then log := (p, cipher)::!log;
cipher
in
(* MEANT TO BE USED ONLY WITH AUTHENTIC CIPHERS *)
let decrypt (c:cipher) : option Plain.plain =
let q = decrypt key c in
if Idealizing.ind_cpa (*!!! AUDIT, Crypto Hypothesis *)
then match find !log (fun (_, c') > c=c') with
 None > None
 Some (p, _) > Some p
...