-
Notifications
You must be signed in to change notification settings - Fork 1
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
* Add real versus simulated KEMTLS SAUTH for deniability * Deniability for all variants * Conditional full versions for deniability * Fix bug in m4 macro * Give long-term secret keys to deniability adversary * Missing message in KEMTLS PDK MUTUAL deniability * Add comments/documentation about deniability * Add results from deniability runs * Reorganize output files
- Loading branch information
Showing
25 changed files
with
26,377 additions
and
8 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,3 +1,4 @@ | ||
| /deniability/generated* | ||
| /generated_corekt.spthy | ||
| /generated_corekt_pdk.spthy | ||
| client_session_key.aes |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,42 @@ | ||
| /* This file models the offline deniability of KEMTLS in mutual authentication mode. */ | ||
|
|
||
| changequote(<!,!>) | ||
|
|
||
| theory corekt_deniability_mutual | ||
| begin | ||
|
|
||
| include(../protocol/primitives.spthy) | ||
|
|
||
| include(../protocol/kemtls_keygen.spthy) | ||
|
|
||
| include(../protocol/kemtls_mutual_defines.spthy) | ||
| include(kemtls_mutual_real.spthy) | ||
| include(kemtls_mutual_simulated.spthy) | ||
|
|
||
| /* This lemma captures the offline deniability of KEMTLS in mutual authentication mode. | ||
| * Offline deniability means that a judge, when given a protocol transcript and all of the | ||
| * keys involved, cannot tell whether the transcript is genuine or forged. | ||
| * | ||
| * This is modelled in Tamarin by having one rule that generates real transcripts | ||
| * uses real secret keys to decapsulate, and another rule that generates simulated | ||
| * transcripts only using public keys. The adversary is given the transcripts, | ||
| * as well as derived session keys and the parties' long-term public and private keys. | ||
| * | ||
| * If the M4 macro FULL is defined, then the transcript covers the full protocol | ||
| * run and all session keys are given to the adversary. | ||
| * If the M4 macro FULL is not defined, then the transcript only covers up until | ||
| * the last calculation involving either a real or simulated key, and then all | ||
| * subsequent messages and keys that can clearly be publicly computed are omitted | ||
| * to make things easier for Tamarin to prove. | ||
| */ | ||
| rule real_vs_simulated: | ||
| [ | ||
| RealTranscript(transcript_real, session_keys_real, long_term_keys), | ||
| FakeTranscript(transcript_simulated, session_keys_simulated, long_term_keys) | ||
| ] | ||
| --[]-> | ||
| [ | ||
| Out(diff(<transcript_real, session_keys_real, long_term_keys>, <transcript_simulated, session_keys_simulated, long_term_keys>)) | ||
| ] | ||
|
|
||
| end |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,68 @@ | ||
| /* This rule generates a *real* transcript for KEMTLS in mutual | ||
| * authentication mode, using the client's and server's long-term secret keys | ||
| * to decapsulate. | ||
| */ | ||
| rule KEMTLS_MUTUAL_real: | ||
| let | ||
| pk_e = KEM_e_PK(~sk_e) | ||
| CLIENT_HELLO = <'ClientHello', pk_e, ~r_c> | ||
| ct_e = KEM_e_Encaps_ct(pk_e, ~coins_e) | ||
| ss_e = KEM_e_Encaps_ss(pk_e, ~coins_e) | ||
| SERVER_HELLO = <'ServerHello', ct_e, ~r_s> | ||
| ES = HKDFExtract('0', '0') | ||
| dES = HKDFExpand(ES, 'derived', '0') | ||
| HS = HKDFExtract(dES, ss_e) | ||
| ifdef(<!FULL!>, <! | ||
| CHTS = HKDFExpand(HS, 'c_hs_traffic', M_KEMTLS_MUTUAL_STAGE1_TRANSCRIPT) | ||
| SHTS = HKDFExpand(HS, 's_hs_traffic', M_KEMTLS_MUTUAL_STAGE2_TRANSCRIPT) | ||
| !>) | ||
| dHS = HKDFExpand(HS, 'derived', '0') | ||
| CERTIFICATE_REQUEST = <'CertificateRequest'> | ||
| SERVER_CERTIFICATE = <'ServerCertificate', pk_S> | ||
| ct_S = KEM_s_Encaps_ct(pk_S, ~coins_S) | ||
| ss_S = KEM_s_Decaps(ct_S, sk_S) | ||
| CLIENT_KEM_CIPHERTEXT = <'ClientKEMCiphertext', ct_S> | ||
| AHS = HKDFExtract(dHS, ss_S) | ||
| ifdef(<!FULL!>, <! | ||
| CAHTS = HKDFExpand(AHS, 'c_ahs_traffic', M_KEMTLS_MUTUAL_STAGE3_TRANSCRIPT) | ||
| SAHTS = HKDFExpand(AHS, 's_ahs_traffic', M_KEMTLS_MUTUAL_STAGE4_TRANSCRIPT) | ||
| !>) | ||
| dAHS = HKDFExpand(AHS, 'derived', '0') | ||
| CLIENT_CERTIFICATE = <'ClientCertificate', pk_C> | ||
| ct_C = KEM_c_Encaps_ct(pk_C, ~coins_C) | ||
| ss_C = KEM_c_Decaps(ct_C, sk_C) | ||
| SERVER_KEM_CIPHERTEXT = <'ServerKEMCiphertext', ct_C> | ||
| MS = HKDFExtract(dAHS, ss_C) | ||
| ifdef(<!FULL!>, <! | ||
| fk_c = HKDFExpand(MS, 'c_finished', '0') | ||
| fk_s = HKDFExpand(MS, 's_finished', '0') | ||
| CF = HMAC(fk_c, M_KEMTLS_MUTUAL_CF_TRANSCRIPT) | ||
| CLIENT_FINISHED = <'ClientFinished', CF> | ||
| CATS = HKDFExpand(MS, 'c_ap_traffic', M_KEMTLS_MUTUAL_STAGE5_TRANSCRIPT) | ||
| SF = HMAC(fk_s, M_KEMTLS_MUTUAL_SF_TRANSCRIPT) | ||
| SERVER_FINISHED = <'ServerFinished', SF> | ||
| SATS = HKDFExpand(MS, 's_ap_traffic', M_KEMTLS_MUTUAL_STAGE6_TRANSCRIPT) | ||
| !>) | ||
| in | ||
| [ | ||
| !Ltk($C, pk_C, sk_C, 'KEM_c'), | ||
| !Ltk($S, pk_S, sk_S, 'KEM_s'), | ||
| Fr(~sk_e), | ||
| Fr(~r_c), | ||
| Fr(~r_s), | ||
| Fr(~coins_e), | ||
| Fr(~coins_C), | ||
| Fr(~coins_S) | ||
| ] | ||
| --[]-> | ||
| [ | ||
| RealTranscript( | ||
| <CLIENT_HELLO, SERVER_HELLO, CERTIFICATE_REQUEST, SERVER_CERTIFICATE, CLIENT_KEM_CIPHERTEXT, CLIENT_CERTIFICATE, SERVER_KEM_CIPHERTEXT | ||
| ifdef(<!FULL!>, <!, CLIENT_FINISHED, SERVER_FINISHED!>) | ||
| >, | ||
| <HS, AHS, MS | ||
| ifdef(<!FULL!>, <!, CHTS, SHTS, CAHTS, SAHTS, CATS, SATS!>) | ||
| >, | ||
| <pk_C, sk_C, pk_S, sk_S> | ||
| ) | ||
| ] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,67 @@ | ||
| /* This rule generates a *simulated* transcript for KEMTLS in mutual | ||
| * authentication mode, without using any party's long-term secret keys. | ||
| */ | ||
| rule KEMTLS_MUTUAL_simulated: | ||
| let | ||
| pk_e = KEM_e_PK(~sk_e) | ||
| CLIENT_HELLO = <'ClientHello', pk_e, ~r_c> | ||
| ct_e = KEM_e_Encaps_ct(pk_e, ~coins_e) | ||
| ss_e = KEM_e_Encaps_ss(pk_e, ~coins_e) | ||
| SERVER_HELLO = <'ServerHello', ct_e, ~r_s> | ||
| ES = HKDFExtract('0', '0') | ||
| dES = HKDFExpand(ES, 'derived', '0') | ||
| HS = HKDFExtract(dES, ss_e) | ||
| ifdef(<!FULL!>, <! | ||
| CHTS = HKDFExpand(HS, 'c_hs_traffic', M_KEMTLS_MUTUAL_STAGE1_TRANSCRIPT) | ||
| SHTS = HKDFExpand(HS, 's_hs_traffic', M_KEMTLS_MUTUAL_STAGE2_TRANSCRIPT) | ||
| !>) | ||
| dHS = HKDFExpand(HS, 'derived', '0') | ||
| CERTIFICATE_REQUEST = <'CertificateRequest'> | ||
| SERVER_CERTIFICATE = <'ServerCertificate', pk_S> | ||
| ct_S = KEM_s_Encaps_ct(pk_S, ~coins_S) | ||
| ss_S = KEM_s_Encaps_ss(pk_S, ~coins_S) | ||
| CLIENT_KEM_CIPHERTEXT = <'ClientKEMCiphertext', ct_S> | ||
| AHS = HKDFExtract(dHS, ss_S) | ||
| ifdef(<!FULL!>, <! | ||
| CAHTS = HKDFExpand(AHS, 'c_ahs_traffic', M_KEMTLS_MUTUAL_STAGE3_TRANSCRIPT) | ||
| SAHTS = HKDFExpand(AHS, 's_ahs_traffic', M_KEMTLS_MUTUAL_STAGE4_TRANSCRIPT) | ||
| !>) | ||
| dAHS = HKDFExpand(AHS, 'derived', '0') | ||
| CLIENT_CERTIFICATE = <'ClientCertificate', pk_C> | ||
| ct_C = KEM_c_Encaps_ct(pk_C, ~coins_C) | ||
| ss_C = KEM_c_Encaps_ss(pk_C, ~coins_C) | ||
| SERVER_KEM_CIPHERTEXT = <'ServerKEMCiphertext', ct_C> | ||
| MS = HKDFExtract(dAHS, ss_C) | ||
| ifdef(<!FULL!>, <! | ||
| fk_c = HKDFExpand(MS, 'c_finished', '0') | ||
| fk_s = HKDFExpand(MS, 's_finished', '0') | ||
| CF = HMAC(fk_c, M_KEMTLS_MUTUAL_CF_TRANSCRIPT) | ||
| CLIENT_FINISHED = <'ClientFinished', CF> | ||
| CATS = HKDFExpand(MS, 'c_ap_traffic', M_KEMTLS_MUTUAL_STAGE5_TRANSCRIPT) | ||
| SF = HMAC(fk_s, M_KEMTLS_MUTUAL_SF_TRANSCRIPT) | ||
| SERVER_FINISHED = <'ServerFinished', SF> | ||
| SATS = HKDFExpand(MS, 's_ap_traffic', M_KEMTLS_MUTUAL_STAGE6_TRANSCRIPT) | ||
| !>) | ||
| in | ||
| [ | ||
| !Ltk($C, pk_C, sk_C, 'KEM_c'), | ||
| !Ltk($S, pk_S, sk_S, 'KEM_s'), | ||
| Fr(~sk_e), | ||
| Fr(~r_c), | ||
| Fr(~r_s), | ||
| Fr(~coins_e), | ||
| Fr(~coins_C), | ||
| Fr(~coins_S) | ||
| ] | ||
| --[]-> | ||
| [ | ||
| FakeTranscript( | ||
| <CLIENT_HELLO, SERVER_HELLO, CERTIFICATE_REQUEST, SERVER_CERTIFICATE, CLIENT_KEM_CIPHERTEXT, CLIENT_CERTIFICATE, SERVER_KEM_CIPHERTEXT | ||
| ifdef(<!FULL!>, <!, CLIENT_FINISHED, SERVER_FINISHED!>) | ||
| >, | ||
| <HS, AHS, MS | ||
| ifdef(<!FULL!>, <!, CHTS, SHTS, CAHTS, SAHTS, CATS, SATS!>) | ||
| >, | ||
| <pk_C, sk_C, pk_S, sk_S> | ||
| ) | ||
| ] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,42 @@ | ||
| /* This file models the offline deniability of KEMTLS-PDK in mutual authentication mode. */ | ||
|
|
||
| changequote(<!,!>) | ||
|
|
||
| theory corekt_deniability_pdk_mutual | ||
| begin | ||
|
|
||
| include(../protocol/primitives.spthy) | ||
|
|
||
| include(../protocol/kemtls_keygen.spthy) | ||
|
|
||
| include(../protocol/kemtls_pdk_mutual_defines.spthy) | ||
| include(kemtls_pdk_mutual_real.spthy) | ||
| include(kemtls_pdk_mutual_simulated.spthy) | ||
|
|
||
| /* This lemma captures the offline deniability of KEMTLS-PDK in mutual authentication mode. | ||
| * Offline deniability means that a judge, when given a protocol transcript and all of the | ||
| * keys involved, cannot tell whether the transcript is genuine or forged. | ||
| * | ||
| * This is modelled in Tamarin by having one rule that generates real transcripts | ||
| * uses real secret keys to decapsulate, and another rule that generates simulated | ||
| * transcripts only using public keys. The adversary is given the transcripts, | ||
| * as well as derived session keys and the parties' long-term public and private keys. | ||
| * | ||
| * If the M4 macro FULL is defined, then the transcript covers the full protocol | ||
| * run and all session keys are given to the adversary. | ||
| * If the M4 macro FULL is not defined, then the transcript only covers up until | ||
| * the last calculation involving either a real or simulated key, and then all | ||
| * subsequent messages and keys that can clearly be publicly computed are omitted | ||
| * to make things easier for Tamarin to prove. | ||
| */ | ||
| rule real_vs_simulated: | ||
| [ | ||
| RealTranscript(transcript_real, session_keys_real, long_term_keys), | ||
| FakeTranscript(transcript_simulated, session_keys_simulated, long_term_keys) | ||
| ] | ||
| --[]-> | ||
| [ | ||
| Out(diff(<transcript_real, session_keys_real, long_term_keys>, <transcript_simulated, session_keys_simulated, long_term_keys>)) | ||
| ] | ||
|
|
||
| end |
Oops, something went wrong.