| theory Diffie_Hellman | |
| begin | |
| builtins: diffie-hellman | |
| // | |
| // Rules | |
| // | |
| rule client_init: | |
| let pubKey = 'g'^~privKey | |
| in | |
| [Fr(~privKey)] | |
| --[]-> | |
| [InitClient(~privKey, pubKey), Out(pubKey)] | |
| rule server_response: | |
| [Fr(~privKey), In(clientPubKey)] | |
| --[SessionCreateServer(clientPubKey^~privKey)]-> | |
| [Out('g'^~privKey), Session(clientPubkey^~privKey)] | |
| rule client_receive: | |
| [InitClient(~privKey, pubKey), In(serverPubKey)] | |
| --[SessionCreateClient(serverPubKey^~privKey)]-> | |
| [Session(serverPubKey^~privKey)] | |
| rule terminate: | |
| [Session(A)] | |
| --> | |
| [] | |
| // | |
| // Lemmas | |
| // | |
| // just making sure it works | |
| lemma ExchangeWorks: | |
| exists-trace | |
| "Ex S #i #j. SessionCreateClient(S) @ #i & SessionCreateServer(S) @ #j & #j < #i & not(Ex #k. K(S) @ #k)" | |
| lemma RecoverSessionKeyImpossible: | |
| "All S #i #j. (SessionCreateClient(S) @ #i & SessionCreateServer(S) @ #j & #j < #i) ==> not(Ex #k. K(S) @ #k)" | |
| lemma MITMImpossible: | |
| "All S1 S2 #i #j. (SessionCreateClient(S1) @ #i & SessionCreateServer(S2) @ #j & #j < #i) ==> not(Ex #k1 #k2. K(S1) @ #k1 & K(S2) @ #k2)" | |
| // | |
| end |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment