Jonas/coprf pv

proofs/Makefile

@@ -0,0 +1,14 @@
+src_files := $(wildcard *.pv)
+res_files :=  $(src_files:%.pv=%.res)
+
+all: $(res_files)
+
+%.res: %.pv scrambledb.pvl
+	@echo "=> Analysis: " $<
+	@proverif -lib scrambledb $< > $@
+	@grep -A100 -e 'Verification summary:' $@
+
+
+.PHONY: clean
+clean:
+	rm -f $(wildcard *.res)

proofs/scrambledb.pvl

@@ -0,0 +1,212 @@
+(* This model is a sketch of the Convertible Oblivious PRF
+functionality given by Anja Lehmann in "ScrambleDB: Oblivious
+(Chameleon) Pseudonymization-as-a-Service" as part of the ScrambleDB
+system. *)
+
+channel c.
+
+type group_element.
+fun h2g(bitstring): group_element. (* Hash-to-Group *)
+
+(* PRF *)
+type coprf_msk.
+type coprf_key.
+
+fun coprf_derive_key(coprf_msk, bitstring): coprf_key.
+fun coprf_evaluate(coprf_key, group_element): group_element.
+fun coprf_convert(coprf_key, coprf_key, group_element): group_element.
+
+(* Blinding *)
+type blinding_pk.
+type blinding_sk.
+fun bsk2bpk(blinding_sk): blinding_pk.
+
+type blind_input.
+type blind_output.
+fun bi2g(blind_input): group_element [typeConverter].
+fun bo2g(blind_output): group_element [typeConverter].
+
+fun coprf_blind_(blinding_pk, group_element, bitstring): blind_input.
+letfun coprf_blind_input(bpk: blinding_pk, x: bitstring) = new r:bitstring; coprf_blind_(bpk, h2g(x), r).
+letfun coprf_blind_output(bpk: blinding_pk, x: group_element) = new r:bitstring; coprf_blind_(bpk, x, r).
+
+fun coprf_blind_evaluate(coprf_key, blinding_pk, blind_input): blind_output.
+fun coprf_blind_convert(coprf_key, coprf_key, blinding_pk, blind_input): blind_output.
+fun coprf_unblind(blinding_sk, blind_output): group_element.
+
+equation forall bsk: blinding_sk, k: coprf_key, x: group_element, r: bitstring;
+         coprf_unblind(bsk, coprf_blind_evaluate(k, bsk2bpk(bsk), coprf_blind_(bsk2bpk(bsk), x, r))) = coprf_evaluate(k, x).
+
+equation forall bsk: blinding_sk, k1: coprf_key, k2: coprf_key, x: group_element, r: bitstring;
+         coprf_unblind(bsk, coprf_blind_convert(k1, k2, bsk2bpk(bsk), coprf_blind_(bsk2bpk(bsk), x, r))) = coprf_convert(k1, k2, x).
+
+
+(* Public Key Encryption *)
+type pubkey.
+type privkey.
+fun pk(privkey): pubkey.
+fun penc_(pubkey, bitstring, bitstring): bitstring.
+letfun penc(pk: pubkey, msg: bitstring) = new r:bitstring; penc_(pk, msg, r).
+reduc forall sk: privkey, msg: bitstring, r: bitstring; 
+      pdec(sk, penc_(pk(sk), msg, r)) = msg.
+
+(* PRP for pseudonym hardening *)
+type prp_key.
+type nym.
+fun prp(prp_key, group_element): nym.
+reduc forall k_prp: prp_key, x: group_element; prp_inv(k_prp, prp(k_prp, x)) = x.
+
+
+
+(* Model of ScrambleDB *)
+(* Protocol Messages *)
+
+(* IdentifiableData = (orthonym, attribute_type, value)*)
+fun identifiable_data(bitstring, bitstring, bitstring): bitstring [data].
+
+(* BlindedIdentifiableData = (blinded_orthonym, attribute_type, encrypted_value) *)
+fun blinded_identifiable_data(blind_input, bitstring, bitstring): bitstring [data].
+
+(* BlindedPseudonymizedOutputData = (blinded_pseudonym, attribute_type, encrypted_value) *)
+fun blinded_pseudonymized_output_data(blind_output, bitstring, bitstring): bitstring [data].
+
+(* BlindedPseudonymizedInputData = (blinded_pseudonym, attribute_type, encrypted_value) *)
+fun blinded_pseudonymized_input_data(blind_input, bitstring, bitstring): bitstring [data].
+
+(* PseudonymizedData = (nym, attribute_type, encrypted_value) *)
+fun pseudonymized_data(nym, bitstring, bitstring): bitstring [data].
+
+(* DataAvailable = (attribute_type) *)
+fun data_available(bitstring): bitstring [data].
+
+(* DataRequest = (conversion_target, attribute_type, bpk_receiver, ek_receiver) *)
+fun data_request(bitstring, bitstring, blinding_pk, pubkey): bitstring [data].
+
+(* ConversionRequest = (conversion_target, blinded_pseudonymized_data, bpk_reveiver, ek_receiver) *)
+fun conversion_request(bitstring, bitstring, blinding_pk, pubkey): bitstring [data].
+
+(* Data Transformations *)
+letfun blind_identifiable_data(input: bitstring, bpk: blinding_pk, ek: pubkey) =
+    let identifiable_data(orthonym, attribute_type, data_value) = input in
+    let blinded_orthonym = coprf_blind_input(bpk, orthonym) in
+    let encrypted_value = penc(ek, data_value) in
+    blinded_identifiable_data(blinded_orthonym, attribute_type, encrypted_value).
+
+letfun blind_pseudonymized_data(input: bitstring, bpk: blinding_pk, ek: pubkey, k_prp: prp_key) =
+    let pseudonymized_data(pseudonym, attribute_type, data_value) = input in
+    let blinded_pseudonym = coprf_blind_output(bpk, prp_inv(k_prp, pseudonym)) in
+    let encrypted_value = penc(ek, data_value) in
+    blinded_pseudonymized_input_data(blinded_pseudonym, attribute_type, encrypted_value).
+
+letfun pseudonymize_blinded_data(input: bitstring, msk: coprf_msk, bpk: blinding_pk, ek: pubkey) =
+    let blinded_identifiable_data(blinded_orthonym, attribute_type, encrypted_value) = input in
+    let k = coprf_derive_key(msk, attribute_type) in
+    let reencrypted_value = penc(ek, encrypted_value) in
+    let blinded_pseudonym = coprf_blind_evaluate(k, bpk, blinded_orthonym) in
+    blinded_pseudonymized_output_data(blinded_pseudonym, attribute_type, reencrypted_value).
+
+letfun convert_blinded_data(input: bitstring, msk: coprf_msk, bpk: blinding_pk, ek: pubkey, conversion_target: bitstring) =
+    let blinded_pseudonymized_input_data(blinded_input_pseudonym, attribute_type, encrypted_value) = input in
+    let k_original = coprf_derive_key(msk, attribute_type) in
+    let k_conversion = coprf_derive_key(msk, conversion_target) in
+    let reencrypted_value = penc(ek, encrypted_value) in
+    let blinded_output_pseudonym = coprf_blind_convert(k_original, k_conversion, bpk, blinded_input_pseudonym) in
+    blinded_pseudonymized_output_data(blinded_output_pseudonym, attribute_type, reencrypted_value).
+
+letfun finalize_pseudonymized_data(input: bitstring, bsk: blinding_sk, dk: privkey, k_prp: prp_key) =
+    let blinded_pseudonymized_output_data(blinded_pseudonym, attribute_type, reencrypted_value) = input in
+    let pseudonym = prp(k_prp, coprf_unblind(bsk, blinded_pseudonym)) in
+    let value = pdec(dk, pdec(dk, reencrypted_value)) in 
+    pseudonymized_data(pseudonym, attribute_type, value).
+
+table lake_data(nym, bitstring, bitstring).
+
+(* Events *)
+event BlindedOrthonym(bitstring).
+event Pseudonymized(bitstring, bitstring).
+event Finalized(bitstring).
+
+event BlindedPseudonym(bitstring).
+event Converted(bitstring, bitstring).
+event Joined(bitstring).
+
+event ConverterLeak(bitstring).
+event LeakLakeKeys().
+event LeakProcessorKeys().
+
+(* Protocol Participants *)
+let DataSource(input: bitstring, bpk: blinding_pk, ek: pubkey) =
+    let blinded_identifiable_data(blinded_orthonym, attribute_type, encrypted_value) = blind_identifiable_data(input, bpk, ek) in 
+    event BlindedOrthonym(input);
+    out(c, blinded_identifiable_data(blinded_orthonym, attribute_type, encrypted_value)).
+
+
+(* Parameter `leak_input` controls whether the Converter leaks the
+unprocessed inputs to the adversary.*)
+let Converter(msk: coprf_msk, bpk_lake: blinding_pk, ek_lake: pubkey, leak_input: bool) =
+    (
+        (* Pseudonymization *)
+        in(c, input: bitstring);
+        let output = pseudonymize_blinded_data(input, msk, bpk_lake, ek_lake) in
+        event Pseudonymized(input, output);
+        out(c, output);
+        if leak_input then
+           event ConverterLeak(input);  
+           out(c, input)
+   ) | (
+       (* Conversion *)
+        in(c, input: bitstring);
+        let conversion_request(conversion_target, blind_pseudonymized_input, bpk, ek) = input in
+        let output = convert_blinded_data(blind_pseudonymized_input, msk, bpk, ek, conversion_target) in
+        event Pseudonymized(blind_pseudonymized_input, output);
+        out(c, output);
+        if leak_input then
+           event ConverterLeak(input);
+           out(c, input)
+   ).
+
+
+(* Parameter `leak_keys` controls whether the secret keys are leaked to the adversary. *)
+let DataLake(bsk: blinding_sk, dk: privkey, k_prp: prp_key, leak_keys: bool) =
+    (
+        (* Pseudonym Finalization *)
+        in(c, input: bitstring);
+        let pseudonymized_data(pseudonym, attribute_type, value) = finalize_pseudonymized_data(input, bsk, dk, k_prp) in
+        event Finalized(pseudonymized_data(pseudonym, attribute_type, value));
+        insert lake_data(pseudonym, attribute_type, value);
+        out(c, data_available(attribute_type))
+    ) | (
+        (* Blind Pseudonymized Data *)
+        in(c, request: bitstring);
+        let data_request(conversion_target, attribute_type, bpk_receiver, ek_receiver) = request in
+        get lake_data(pseudonym, =attribute_type, value) in
+        let input = pseudonymized_data(pseudonym, attribute_type, value) in
+        let blinded_output = blind_pseudonymized_data(input, bpk_receiver, ek_receiver, k_prp) in
+        event BlindedPseudonym(blinded_output);
+        out(c, conversion_request(conversion_target, blinded_output, bpk_receiver, ek_receiver))
+    ) | (
+        if leak_keys then
+            event LeakLakeKeys();
+            out(c, bsk);
+            out(c, dk) 
+    ).
+
+(* Parameter `leak_keys` controls whether the secret keys are leaked to the adversary. *)
+let DataProcessor(bsk: blinding_sk, dk: privkey, k_prp: prp_key, leak_keys: bool) =
+    (
+        (* Request Available data for conversion *)
+        in(c, input: bitstring);
+        let data_available(attribute_type) = input in
+        new conversion_target: bitstring;
+        out(c, data_request(conversion_target, attribute_type, bsk2bpk(bsk), pk(dk)))
+    ) | (
+        (* Join Finalization *)
+        in(c, input: bitstring);    
+        let pseudonymous_data = finalize_pseudonymized_data(input, bsk, dk, k_prp) in
+        event Joined(pseudonymous_data)
+    ) | (
+        if leak_keys then
+            event LeakProcessorKeys();
+            out(c, bsk);
+            out(c, dk)
+    ).

proofs/scrambledb_input_indistinguishability.pv

@@ -0,0 +1,19 @@
+const orthonym_0: bitstring.
+const orthonym_1: bitstring.
+const data_value: bitstring.
+const attribute_type: bitstring.
+
+process
+    new bsk: blinding_sk;
+    new dk: privkey;
+    new k_prp: prp_key;
+    new msk: coprf_msk;
+    let bpk = bsk2bpk(bsk) in
+    let ek = pk(dk) in
+    out(c, (bpk, ek));
+    let input_0= identifiable_data(orthonym_0, attribute_type, data_value) in
+    let input_1= identifiable_data(orthonym_1, attribute_type, data_value) in  
+    (DataSource(diff[input_0, input_1], bpk, ek) |
+    DataLake(bsk, dk, k_prp, false) |
+    Converter(msk, bpk, ek, false)  |
+    (new bsk: blinding_sk; new dk: privkey; new k_prp: prp_key; DataProcessor(bsk, dk, k_prp, false)))

proofs/scrambledb_passive_reachability.pv

@@ -0,0 +1,18 @@
+set attacker=passive.
+query attribute_id: bitstring, pseudonym: group_element, attribute_value: bitstring;
+       event(LakeReceived(final_data(attribute_id, pseudonym, attribute_value))).
+
+const attribute_id: bitstring.
+const uid: group_element.
+const attribute_value: bitstring.
+
+process
+    new bsk: blinding_sk;
+    new dk: privkey;
+    new msk: prf_msk;
+    let bpk = blinding_sk_to_pk(bsk) in
+    let ek = pk(dk) in
+    let input = input_data(attribute_id, uid, attribute_value) in
+    (DataSource(input, bpk, ek) |
+    (in (c, lake_input: bitstring); DataLake(lake_input, bsk, dk, false)) |
+    (in (c, converter_input: bitstring); Converter(converter_input, msk, ek)))

proofs/scrambledb_pseudonymity.pv

@@ -0,0 +1,12 @@
+process
+    new bsk: blinding_sk;
+    new dk: privkey;
+    new msk: prf_msk;
+    let bpk = blinding_sk_to_pk(bsk) in
+    let ek = pk(dk) in
+    out(c, (bpk, ek));
+    (
+        (in (c, source_input: bitstring);     DataSource(source_input, bpk, ek))     |
+        (in (c, lake_input: bitstring);       DataLake(lake_input, bsk, dk, false))  |
+        (in (c, converter_input: bitstring);  Converter(converter_input, msk, ek))
+    )  

proofs/scrambledb_reachability.pv

@@ -0,0 +1,25 @@
+query attribute_id: bitstring, uid: group_element, pseudonym: group_element, attribute_value: bitstring;
+       event(LakeReceived(final_data(attribute_id, pseudonym, attribute_value)));
+       event(LakeReceived(final_data(attribute_id, pseudonym, attribute_value)))
+       ==> event(SourceSent(input_data(attribute_id, uid, attribute_value))).
+
+query attribute_id: bitstring, pseudonym: group_element, attribute_value: bitstring;
+       event(SourceSent(input_data(attribute_id, pseudonym, attribute_value))).
+
+query x: bitstring, y: bitstring;
+       event(Converted(x, y)).
+
+const attribute_id: bitstring.
+const uid: group_element.
+const attribute_value: bitstring.
+
+process
+    new bsk: blinding_sk;
+    new dk: privkey;
+    new msk: prf_msk;
+    let bpk = blinding_sk_to_pk(bsk) in
+    let ek = pk(dk) in
+    let input = input_data(attribute_id, uid, attribute_value) in
+    (DataSource(input, bpk, ek) |
+    (in (c, lake_input: bitstring); DataLake(lake_input, bsk, dk, false)) |
+    (in (c, converter_input: bitstring); Converter(converter_input, msk, ek)))