diff options
| author |   Kevin Milner <kamilner@kamilner.ca> | 2017-05-04 23:19:17 +0100 |
|---|---|---|
| committer | Kevin Milner <kamilner@kamilner.ca> | 2017-05-04 23:19:17 +0100 |
| commit | f9f4205defcc79d6243aa896ea39d9c2ee2eb41f (patch) | |
| tree | cffb8010f939a1d976522180ced469c5738ea209 | |
| parent | Manual proof for heuristic hackery (diff) | |
| download | wireguard-tamarin-f9f4205defcc79d6243aa896ea39d9c2ee2eb41f.tar.xz wireguard-tamarin-f9f4205defcc79d6243aa896ea39d9c2ee2eb41f.zip | |
Without heuristic hackery
| -rw-r--r-- | wireguard.m4 | 81 |
1 files changed, 5 insertions, 76 deletions
diff --git a/wireguard.m4 b/wireguard.m4 index 4e2bbf5..3cb8f9f 100644 --- a/wireguard.m4 +++ b/wireguard.m4 @@ -40,7 +40,7 @@ define(StateInvariants, F_StateInvariants($*)) // case, typically agent state can come from just about anywhere so it creates // a ton of case distinctions when we're usually only interested in the current // session anyway. -define(State, L_State($*)) +dnl define(State, L_State($*)) //Pre-established trust relationships restriction pairings_unique: @@ -140,7 +140,7 @@ rule Handshake_Init: , !EphKeytoReveal(~ekI) //This is a heuristic hack, so that the heuristic can prioritize solving for //the init rule without prioritizing the State() fact. - , F_SolveInit(~id,psk,<'init',~sidI,~ekI,ci2,ki2,hi1>) +// , F_SolveInit(~id,psk,<'init',~sidI,~ekI,ci2,ki2,hi1>) , Out(m1) ] @@ -188,7 +188,7 @@ rule Handshake_Resp: [ State(~id,psk,<'transport_unconfirmed',~sidR,pekI,pekR,cr6>) //This is a heuristic hack, so that the heuristic can prioritize solving for //the resp rule without prioritizing the State() fact. - , F_SolveResp(~id,psk,<'transport_unconfirmed',~sidR,pekI,pekR,cr6>) +// , F_SolveResp(~id,psk,<'transport_unconfirmed',~sidR,pekI,pekR,cr6>) , !EphKeytoReveal(~ekR) , Out(m2) ] @@ -214,7 +214,7 @@ rule Handshake_Complete: //in it are public except the key used to encrypt. mtr = <'4',sidR,aead(ci6,'message','0')> in [ State(~id,psk,<'init',sidI,~ekI,ci2,ki2,hi1>) - , F_SolveInit(~id,psk,<'init',sidI,~ekI,ci2,ki2,hi1>) +// , F_SolveInit(~id,psk,<'init',sidI,~ekI,ci2,ki2,hi1>) , !StateInvariants(~id,~ltkI,pkR,sisr) , In(m2) ]--[ @@ -236,7 +236,7 @@ rule Handshake_Complete: rule R_ConfirmedTransportMessage: let mtr = <'4',sid,data> in [ State(~id,psk,<'transport_unconfirmed',sidR,pekI,pekR,cr>) - , F_SolveResp(~id,psk,<'transport_unconfirmed',sidR,pekI,pekR,cr>) +// , F_SolveResp(~id,psk,<'transport_unconfirmed',sidR,pekI,pekR,cr>) , !StateInvariants(~id,~ltkR,pkI,sisr) , In(mtr) ]--[ @@ -332,77 +332,6 @@ lemma identity_hiding: lemma psk_invariant_helper[reuse,use_induction]: "All psk #i. UsingPSK(psk) @ i ==> Ex #j. #j < #i & PSKey(psk) @ j" -induction - case empty_trace - by contradiction /* from formulas */ -next - case non_empty_trace - simplify - solve( (last(#i)) ∥ - (∃ #j. (PSKey( psk ) @ #j) ∧ (¬(last(#j))) ∧ (#j < #i)) ) - case case_1 - solve( UsingPSK( psk ) @ #i ) - case Handshake_Complete - solve( L_State( ~id, psk, - <'init', sidI, ~ekI, ci2, ki2, hi1> - ) ▶₀ #i ) - case Handshake_Init - by contradiction /* from formulas */ - qed - next - case Handshake_Init - solve( L_State( ~id, psk, anything ) ▶₀ #i ) - case AddPublicKey - by contradiction /* from formulas */ - next - case ChangePSK_case_1 - by contradiction /* from formulas */ - next - case ChangePSK_case_2 - by contradiction /* from formulas */ - next - case Handshake_Complete - by contradiction /* from formulas */ - next - case Handshake_Init - by contradiction /* from formulas */ - next - case Handshake_Resp - by contradiction /* from formulas */ - next - case R_ConfirmedTransportMessage - by contradiction /* from formulas */ - qed - next - case Handshake_Resp - solve( L_State( ~id, psk, anything ) ▶₀ #i ) - case AddPublicKey - by contradiction /* from formulas */ - next - case ChangePSK_case_1 - by contradiction /* from formulas */ - next - case ChangePSK_case_2 - by contradiction /* from formulas */ - next - case Handshake_Complete - by contradiction /* from formulas */ - next - case Handshake_Init - by contradiction /* from formulas */ - next - case Handshake_Resp - by contradiction /* from formulas */ - next - case R_ConfirmedTransportMessage - by contradiction /* from formulas */ - qed - qed - next - case case_2 - by contradiction /* from formulas */ - qed -qed lemma disagreement_implies_noPSK_or_compromisedPSK[reuse]: "(All pki pkr peki pekr psk ck #i. |