adding identity hiding improvements:

seperate files for responder and initiator tests
test file that shows other participants leaking info has an effect
general code clean up
performance improvement: initiator and responder tests now run in ~10s

analysis/03_identity_hiding_initiator.entry.mpv

@@ -0,0 +1,25 @@
+#define INITIATOR_TEST 1
+
+#include "rosenpass/03_identity_hiding.mpv"
+
+// nounif a:Atom, s:seed, a2:Atom;
+// 	ConsumeSeed(a, s, a2) / 6300[conclusion].
+
+nounif v:seed_prec;   attacker(prepare_seed(trusted_seed( v )))/6217[hypothesis].
+nounif v:seed;        attacker(prepare_seed( v ))/6216[hypothesis].
+nounif v:seed;        attacker(rng_kem_sk( v ))/6215[hypothesis].
+nounif v:seed;        attacker(rng_key( v ))/6214[hypothesis].
+nounif v:key_prec;    attacker(prepare_key(trusted_key( v )))/6213[hypothesis].
+nounif v:kem_sk_prec; attacker(prepare_kem_sk(trusted_kem_sk( v )))/6212[hypothesis].
+nounif v:key;         attacker(prepare_key( v ))/6211[hypothesis].
+nounif v:kem_sk;      attacker(prepare_kem_sk( v ))/6210[hypothesis].
+nounif Spk:kem_sk_tmpl;
+  attacker(Creveal_kem_pk(Spk))/6110[conclusion].
+nounif sid:SessionId, Ssskm:kem_sk_tmpl, Spsk:key_tmpl, Sspkt:kem_sk_tmpl, Seski:seed_tmpl, Ssptr:seed_tmpl;
+  attacker(Cinitiator( *sid, *Ssskm, *Spsk, *Sspkt, *Seski, *Ssptr ))/6109[conclusion].
+nounif sid:SessionId, biscuit_no:Atom, Ssskm:kem_sk_tmpl, Spsk:key_tmpl, Sspkt:kem_sk_tmpl, Septi:seed_tmpl, Sspti:seed_tmpl, ih:InitHello_t;
+  attacker(Cinit_hello( *sid, *biscuit_no, *Ssskm, *Spsk, *Sspkt, *Septi, *Sspti, *ih ))/6108[conclusion].
+nounif rh:RespHello_t;
+  attacker(Cresp_hello( *rh ))/6107[conclusion].
+nounif Ssskm:kem_sk_tmpl, Spsk:key_tmpl, Sspkt:kem_sk_tmpl, ic:InitConf_t;
+  attacker(Cinit_conf( *Ssskm, *Spsk, *Sspkt, *ic ))/6106[conclusion].

analysis/03_identity_hiding_responder.entry.mpv

@@ -0,0 +1,96 @@
+#define RESPONDER_TEST 1
+
+#include "rosenpass/03_identity_hiding.mpv"
+
+// select k:kem_pk,ih: InitHello_t;         attacker(prf(prf(prf(prf(key0, PROTOCOL), MAC), kem_pk2b(k) ), IH2b(ih))) phase 1/6300[hypothesis].
+
+// select epki:kem_pk, sctr:bits, pidiC:bits, auth:bits, epki2:kem_pk, sctr2:bits, pidiC2:bits, auth2:bits;
+// 	mess(D, prf(prf(prf(prf(key0,PROTOCOL),MAC),kem_pk2b(kem_pub(trusted_kem_sk(responder1)))),
+// 			IH2b(InitHello(secure_sidi, *epki, *sctr, *pidiC, *auth)))
+// 		) [hypothesis, conclusion].
+
+// select epki:kem_pk, sctr:bits, pidiC:bits, auth:bits, epki2:kem_pk, sctr2:bits, pidiC2:bits, auth2:bits;
+// attacker(choice[prf(prf(prf(prf(key0,PROTOCOL),MAC),kem_pk2b(kem_pub(trusted_kem_sk(responder1)))),
+// 		IH2b(InitHello(secure_sidi, *epki, *sctr, *pidiC, *auth))),
+
+// 		prf(prf(prf(prf(key0,PROTOCOL),MAC),kem_pk2b(kem_pub(trusted_kem_sk(responder2)))),
+// 				IH2b(InitHello(secure_sidi, *epki2, *sctr2, *pidiC2, *auth2)))]
+// 	) [hypothesis, conclusion].
+
+// select 
+// attacker(prf(prf(key0,PROTOCOL),MAC)) [hypothesis, conclusion].
+
+// select 
+// attacker(prf(key0,PROTOCOL)) [conclusion].
+
+// select  
+// attacker(key0) [conclusion].
+
+// select  
+// attacker(PROTOCOL) [conclusion].
+
+// select 
+// attacker(kem_pub(trusted_kem_sk(responder1))) /9999 [hypothesis, conclusion].
+
+// select 
+// attacker(kem_pub(trusted_kem_sk(responder2))) /9999 [hypothesis, conclusion].
+
+// nounif ih:InitHello_t;
+// 	attacker(ih) / 9999 [hypothesis].
+
+// nounif rh:RespHello_t;
+// 	attacker(rh) / 9999 [hypothesis].
+
+// nounif ic:InitConf_t;
+// 	attacker(ic) / 9999 [hypothesis].
+
+// nounif k:key;
+// attacker(ck_hs_enc( *k )) [hypothesis, conclusion].
+
+// nounif k:key;
+// attacker(ck_hs_enc( *k )) phase 1   [hypothesis, conclusion].
+
+// nounif k:key, b:bits;
+// attacker(ck_mix( *k , *b ))   [hypothesis, conclusion].
+
+// nounif k:key, b:bits;
+// attacker(ck_mix( *k , *b ))phase 1   [hypothesis, conclusion].
+
+// // select k:kem_pk, epki2:kem_pk, sctr2:bits, pidiC2:bits, auth2:bits, epki:kem_pk, sctr:bits, pidiC:bits, auth:bits;
+// // attacker(choice[Envelope(prf(prf(prf(prf(key0,PROTOCOL),MAC),kem_pub(trusted_kem_sk(responder1))),
+// // 	InitHello(secure_sidi, *epki2, *sctr2, *pidiC2, *auth2)
+// // 	), InitHello(secure_sidi, *epki2, *sctr2, *pidiC2, *auth2))
+// // 	Envelope(prf(prf(prf(prf(key0,PROTOCOL),MAC),kem_pub(trusted_kem_sk(responder2))),
+// // 		InitHello(secure_sidi, *epki, *sctr, *pidiC, *auth)),
+// // 		InitHello(secure_sidi, *epki, *sctr, *pidiC, *auth))
+// // 	]) / 9999[hypothesis, conclusion].
+
+// nounif k:key, b1:bits, b2:bits;
+// 	attacker(xaead_enc( *k, *b1, *b2)) / 9999[hypothesis,conclusion].
+
+// nounif pk:kem_pk, k:key; 
+// 	attacker(kem_enc( *pk , *k )) / 9999[hypothesis,conclusion].
+
+// nounif sid:SessionId, biscuit_no:Atom, Ssskm:kem_sk_tmpl, Spsk:key_tmpl, Sspkt:kem_sk_tmpl, Septi:seed_tmpl, Sspti:seed_tmpl, ih:InitHello_t;
+//   attacker(Cinit_hello( *sid, *biscuit_no, *Ssskm, *Spsk, *Sspkt, *Septi, *Sspti, *ih ))/9999[hypothesis, conclusion].
+// nounif Ssskm:kem_sk_tmpl, Spsk:key_tmpl, Sspkt:kem_sk_tmpl, ic:InitConf_t;
+//   attacker(Cinit_conf( *Ssskm, *Spsk, *Sspkt, *ic ))/9999[hypothesis, conclusion].
+// nounif sid:SessionId, Ssskm:kem_sk_tmpl, Spsk:key_tmpl, Sspkt:kem_sk_tmpl, Seski:seed_tmpl, Ssptr:seed_tmpl;
+//   attacker(Cinitiator( *sid, *Ssskm, *Spsk, *Sspkt, *Seski, *Ssptr )) /9999 [hypothesis, conclusion].
+
+// nounif sid:SessionId, biscuit_no:Atom, Ssskm:kem_sk_tmpl, Spsk:key_tmpl, Sspkt:kem_sk_tmpl, Septi:seed_tmpl, Sspti:seed_tmpl, ih:InitHello_t;
+//   mess(C, Cinit_hello( *sid, *biscuit_no, *Ssskm, *Spsk, *Sspkt, *Septi, *Sspti, *ih ))/9999[hypothesis, conclusion].
+// nounif Ssskm:kem_sk_tmpl, Spsk:key_tmpl, Sspkt:kem_sk_tmpl, ic:InitConf_t;
+//   mess(C, Cinit_conf( *Ssskm, *Spsk, *Sspkt, *ic ))/9999[hypothesis, conclusion].
+// nounif sid:SessionId, Ssskm:kem_sk_tmpl, Spsk:key_tmpl, Sspkt:kem_sk_tmpl, Seski:seed_tmpl, Ssptr:seed_tmpl;
+//   mess(C, Cinitiator( *sid, *Ssskm, *Spsk, *Sspkt, *Seski, *Ssptr )) /9999 [hypothesis, conclusion].
+// nounif rh:RespHello_t;
+//   attacker(Cresp_hello( *rh ))[conclusion].
+// nounif v:seed_prec;   attacker(prepare_seed(trusted_seed( v )))/6217[hypothesis].
+// nounif v:seed;        attacker(prepare_seed( v ))/6216[hypothesis].
+// nounif v:seed;        attacker(rng_kem_sk( v ))/6215[hypothesis].
+// nounif v:seed;        attacker(rng_key( v ))/6214[hypothesis].
+// nounif v:key_prec;    attacker(prepare_key(trusted_key( v )))/6213[hypothesis].
+// nounif v:kem_sk_prec; attacker(prepare_kem_sk(trusted_kem_sk( v )))/6212[hypothesis].
+// nounif v:key;         attacker(prepare_key( v ))/6211[hypothesis].
+// nounif v:kem_sk;      attacker(prepare_kem_sk( v ))/6210[hypothesis].

analysis/03_identity_hiding_test.entry.mpv

@@ -0,0 +1,29 @@
+#define INITIATOR_TEST 1
+#define CUSTOM_MAIN 1
+
+#include "rosenpass/03_identity_hiding.mpv"
+
+let Oinitiator_bad_actor_inner(sk_tmp:kem_sk_prec) =
+
+  in(C, Cinitiator(sidi, Ssskm, Spsk, Sspkt, Seski, Ssptr));
+
+  #if RANDOMIZED_CALL_IDS
+    new call:Atom;
+  #else
+    call <- Cinitiator(sidi, Ssskm, Spsk, Sspkt, Seski, Ssptr);
+  #endif
+
+  in(C, last_cookie:key);
+  tmpl <- make_trusted_kem_sk(sk_tmp);
+  out(C, setup_kem_sk(tmpl));
+  Oinitiator_inner(sidi, Ssskm, Spsk, tmpl, Seski, Ssptr, last_cookie, C, call).
+
+let Oinitiator_bad_actor() =
+  Oinitiator_bad_actor_inner(responder1) | Oinitiator_bad_actor_inner(responder2) | Oinitiator_bad_actor_inner(initiator1) | Oinitiator_bad_actor_inner(initiator2).
+
+
+let identity_hiding_main2() = 
+  0 | Oinitiator_bad_actor() | rosenpass_main2() | participants_communication() | phase 1; secretCommunication().
+
+
+let main = identity_hiding_main2.

analysis/rosenpass/03_identity_hiding.mpv

@@ -28,7 +28,6 @@
   In this case the test uses secure rng and a fresh secure biscuit key.
 */
 
-
 #include "config.mpv"
 
 #define CHAINING_KEY_EVENTS 1
@@ -44,7 +43,6 @@
 #include "rosenpass/oracles.mpv"
 #include "crypto/kem.mpv"
 
-#define INITIATOR_TEST
 #define NEW_TRUSTED_SEED(name)            \
   new MCAT(name, _secret_seed):seed_prec; \
   name <- make_trusted_seed(MCAT(name, _secret_seed)); \
@@ -57,52 +55,86 @@ free initiator1, initiator2:kem_sk_prec.
 free responder1, responder2:kem_sk_prec.
 
 let secure_init_hello(initiator: kem_sk_tmpl, sidi : SessionId, psk: key_tmpl, responder: kem_sk_tmpl) =
+
+  new epkit:kem_pk;    // epki
+  new sctrt:bits;      // sctr 
+  new pidiCt:bits;      // pidiC
+  new autht:bits;       // auth
+
   NEW_TRUSTED_SEED(seski_trusted_seed)
   NEW_TRUSTED_SEED(ssptr_trusted_seed)
-  Oinitiator_inner(sidi, initiator, psk, responder, seski_trusted_seed, ssptr_trusted_seed, D).
+  new last_cookie:key;
+  new call:Atom;
+
+  Oinitiator_inner(sidi, initiator, psk, responder, seski_trusted_seed, ssptr_trusted_seed, last_cookie, D, call).
+
+let secure_resp_hello(initiator: kem_sk_tmpl, responder: kem_sk_tmpl, sidi:SessionId, sidr:SessionId, biscuit_no:Atom, psk:key_tmpl) =
+
+  in(D, InitHello(=secure_sidi, epki, sctr, pidiC, auth));
 
-let secure_resp_hello(initiator: kem_sk_tmpl, responder: kem_sk_tmpl, sidr:SessionId, sidi:SessionId, biscuit_no:Atom, psk:key_tmpl) =
-  in(D, Envelope(k, IH2b(InitHello(=sidi, epki, sctr, pidiC, auth))));
   ih <- InitHello(sidi, epki, sctr, pidiC, auth);
   NEW_TRUSTED_SEED(septi_trusted_seed)
   NEW_TRUSTED_SEED(sspti_trusted_seed)
-  Oinit_hello_inner(sidr, biscuit_no, responder, psk, initiator, septi_trusted_seed, sspti_trusted_seed, ih, D).
+  new last_cookie:key;
+  new call:Atom;
+
+  Oinit_hello_inner(sidr, biscuit_no, responder, psk, initiator, septi_trusted_seed, sspti_trusted_seed, ih, last_cookie, D, call).
 
 let secure_init_conf(initiator: kem_sk_tmpl, responder: kem_sk_tmpl, psk:key_tmpl, sidi:SessionId, sidr:SessionId) =
-  in(D, Envelope(k3, IC2b(InitConf(=sidi, =sidr, biscuit, auth3))));
+  in(D,  InitConf(=sidi, =sidr, biscuit, auth3));
   ic <- InitConf(sidi,sidr,biscuit, auth3);
   NEW_TRUSTED_SEED(seski_trusted_seed)
   NEW_TRUSTED_SEED(ssptr_trusted_seed)
-  Oinit_conf_inner(initiator, psk, responder, ic).
+  new last_cookie:key;
+  call <- Cinit_conf(initiator, psk, responder, ic);
 
-let secure_communication(initiator: kem_sk_tmpl, responder:kem_sk_tmpl) =
-  secure_key <- prepare_key(secure_psk);
-  (!secure_init_hello(initiator, secure_sidi, secure_key, responder))
-  | !secure_resp_hello(initiator, responder, secure_sidr, secure_sidi, secure_biscuit_no, secure_key)
-  | !(secure_init_conf(initiator, responder, secure_key, secure_sidi, secure_sidr)).
+  Oinit_conf_inner(initiator, psk, responder, ic, call).
+
+let secure_communication(initiator: kem_sk_tmpl, responder:kem_sk_tmpl, key:key) =
+  key_tmpl <- prepare_key(key);
+  (!secure_init_hello(initiator, secure_sidi, key_tmpl, responder))
+  | !secure_resp_hello(initiator, responder, secure_sidi, secure_sidr, secure_biscuit_no, key_tmpl)
+  | !(secure_init_conf(initiator, responder, key_tmpl, secure_sidi, secure_sidr)).
+
+let participant_communication_initiator(participant:kem_sk_tmpl) =
+  in(C, responder:kem_sk_tmpl);
+  in(C, k:key);
+  secure_communication(participant, responder, k).
+
+let participant_communication_responder(participant:kem_sk_tmpl) =
+  in(C, initiator:kem_sk_tmpl);
+  in(C, k:key);
+  secure_communication(initiator, participant, k).
+
+let participants_communication() =
+  initiator1_tmpl <- make_trusted_kem_sk(initiator1);
+  initiator2_tmpl <- make_trusted_kem_sk(initiator2);
+  responder1_tmpl <- make_trusted_kem_sk(responder1);
+  responder2_tmpl <- make_trusted_kem_sk(responder2);
+
+  !participant_communication_initiator(initiator1_tmpl) | !participant_communication_responder(initiator1_tmpl)
+  | !participant_communication_initiator(initiator2_tmpl) | !participant_communication_responder(initiator2_tmpl)
+  | !participant_communication_initiator(responder1_tmpl) | !participant_communication_responder(responder1_tmpl)
+  | !participant_communication_initiator(responder2_tmpl) | !participant_communication_responder(responder2_tmpl).
 
 let pipeChannel(D:channel, C:channel) =
   in(D, b:bits);
   out(C, b).
 
-fun kem_private(kem_pk): kem_sk
-  reduc forall sk_tmpl:kem_sk;
-    kem_private(kem_pub(sk_tmpl)) = sk_tmpl[private].
-
 let secretCommunication() =
+
 #ifdef INITIATOR_TEST
-  initiator_pk <- choice[setup_kem_pk(make_trusted_kem_sk(initiator1)), setup_kem_pk(make_trusted_kem_sk(initiator2))];
-  initiator_seed <- prepare_kem_sk(kem_private(initiator_pk)); 
+  initiator_seed <- choice[make_trusted_kem_sk(initiator1), make_trusted_kem_sk(initiator2)];
 #else
-  initiator_seed <- prepare_kem_sk(trusted_kem_sk(initiator1));
+  initiator_seed <- make_trusted_kem_sk(initiator1);
 #endif
 #ifdef RESPONDER_TEST
-  responder_pk <- choice[setup_kem_pk(make_trusted_kem_sk(responder1)), setup_kem_pk(make_trusted_kem_sk(responder2))];
-  responder_seed <- prepare_kem_sk(kem_private(responder_pk));
+  responder_seed <- choice[make_trusted_kem_sk(responder1), make_trusted_kem_sk(responder2)];
 #else
-  responder_seed <- prepare_kem_sk(trusted_kem_sk(responder1));
+  responder_seed <- make_trusted_kem_sk(responder1);
 #endif
-  secure_communication(initiator_seed, responder_seed) | !pipeChannel(D, C).
+
+  secure_communication(initiator_seed, responder_seed, secure_psk) | !pipeChannel(D, C).
 
 let reveal_pks() =
   out(C, setup_kem_pk(make_trusted_kem_sk(responder1)));
@@ -116,6 +148,8 @@ let rosenpass_main2() =
   | REP(RESPONDER_BOUND, Oinit_conf).
 
 let identity_hiding_main() = 
-  0 | reveal_pks() |  rosenpass_main2() | phase 1; secretCommunication().
+  0 | reveal_pks() | rosenpass_main2() | participants_communication() | phase 1; secretCommunication().
 
+#ifndef CUSTOM_MAIN
 let main = identity_hiding_main.
+#endif