Today, I had a look at Verifpal, an experimental software to do some analysis on cryptographic protocols. Because it's designed for non-experts (unlike proven formal verification tools), I thought I could try to model some parts of SaltyRTC.
Honestly, I am not sure if I've done it right and if it even makes sense. But perhaps there is some interest and, if useful, we can create a more detailed/better model.
The analysis on my model didn't bring up any issues. In case you're interested, here is my current model:
attacker[active]
// Setup phase
principal Initiator[
knows private privatePermanentKeyInitiator
knows private authenticationToken
publicPermanentKeyInitiator = G^privatePermanentKeyInitiator
]
principal Server[
knows private privatePermanentKeyServer
publicPermanentKeyServer = G^privatePermanentKeyServer
]
principal Responder[
knows private privatePermanentKeyResponder
knows private authenticationToken
publicPermanentKeyResponder = G^privatePermanentKeyResponder
]
// Let's assume the public key is exchanged securely to responder.
Initiator -> Responder: [publicPermanentKeyInitiator]
// 1) Initiator connects to server
Initiator -> Server: publicPermanentKeyInitiator
principal Server[
generates privateSessionKeyForInitiator
publicSessionKeyServerForInitiator = G^privateSessionKeyForInitiator
sessionSharedKeyServerInitiator = publicSessionKeyServerForInitiator^publicPermanentKeyInitiator
]
// 2) 'server-hello' message from server to initiator
Server -> Initiator: publicSessionKeyServerForInitiator
// 3) 'client-auth' message from initiator to server
principal Initiator[
knows private clientAuthMessage1
sessionSharedKeyInitiatorServer = publicSessionKeyServerForInitiator^publicPermanentKeyInitiator
secretBoxClientAuthInitiator = AEAD_ENC(sessionSharedKeyInitiatorServer, clientAuthMessage1, nil)
]
Initiator -> Server: secretBoxClientAuthInitiator
principal Server[
clientAuthMessageFromInitiator = AEAD_DEC(sessionSharedKeyServerInitiator, secretBoxClientAuthInitiator, nil)?
]
// 4) 'server-auth' message from server to initiator
principal Server[
knows private serverAuthMessage1
secretBoxServerAuthToInitiator = AEAD_ENC(sessionSharedKeyServerInitiator, serverAuthMessage1, nil)
]
Server -> Initiator: secretBoxServerAuthToInitiator
principal Initiator[
serverAuthMessageToInitiator = AEAD_DEC(sessionSharedKeyInitiatorServer, secretBoxServerAuthToInitiator, nil)?
]
// 5) Responder connects to server
// 6) 'server-hello' message from server to responder
principal Server[
generates privateSessionKeyServerForResponder
publicSessionKeyServerForResponder = G^privateSessionKeyServerForResponder
]
Server -> Responder: publicSessionKeyServerForResponder
// 7) 'client-hello' message from responder to server
Responder -> Server: publicPermanentKeyResponder
principal Server[
sessionSharedKeyServerResponder = publicSessionKeyServerForResponder^publicPermanentKeyResponder
]
// 8) 'client-auth' message from responder to server
principal Responder[
knows private clientAuthMessage2
sessionSharedKeyResponderServer = publicSessionKeyServerForResponder^publicPermanentKeyResponder
secretBoxClientAuthResponder = AEAD_ENC(sessionSharedKeyResponderServer, clientAuthMessage2, nil)
]
Responder -> Server: secretBoxClientAuthResponder
principal Server[
clientAuthMessageFromResponder = AEAD_DEC(sessionSharedKeyServerResponder, secretBoxClientAuthResponder, nil)?
]
// 9) 'server-auth' message from server to responder
principal Server[
knows private serverAuthMessage2
secretBoxServerAuthToResponder = AEAD_ENC(sessionSharedKeyServerResponder, serverAuthMessage2, nil)
]
Server -> Responder: secretBoxServerAuthToResponder
principal Responder[
serverAuthMessageToResponder = AEAD_DEC(sessionSharedKeyResponderServer, secretBoxServerAuthToResponder, nil)?
]
// 10) 'new-responder' message from server to initiator
principal Server[
knows private newResponderMessage1
secretBoxNewResponderToInitiator = AEAD_ENC(sessionSharedKeyServerInitiator, newResponderMessage1, nil)
]
Server -> Initiator: secretBoxNewResponderToInitiator
principal Initiator[
newResponderMessageToInitiator = AEAD_DEC(sessionSharedKeyInitiatorServer, secretBoxNewResponderToInitiator, nil)?
]
// 11) 'token' message from responder to server to initiator
principal Responder[
knows private tokenMessage1
secretBoxTokenResponderToInitiator = AEAD_ENC(authenticationToken, tokenMessage1, nil)
]
Responder -> Initiator: secretBoxTokenResponderToInitiator
principal Initiator[
tokenMessageToInitiator1 = AEAD_DEC(authenticationToken, secretBoxTokenResponderToInitiator, nil)?
]
// TODO: In case Initiator could decrypt, he knows the publicPermanentKey of responder
Responder -> Initiator: [publicPermanentKeyResponder]
// 12) 'key' message from responder to server to initiator
principal Responder[
generates privateSessionKeyResponderForInitiator
publicSessionKeyResponderForInitiator = G^privateSessionKeyResponderForInitiator
knows private keyMessage1
secretBoxKeyResponderToInitiator = AEAD_ENC(publicPermanentKeyResponder^publicPermanentKeyInitiator, keyMessage1, nil)
]
Responder -> Initiator: secretBoxKeyResponderToInitiator
principal Initiator[
keyMessageToInitiator1 = AEAD_DEC(publicPermanentKeyInitiator^publicPermanentKeyResponder, secretBoxKeyResponderToInitiator, nil)?
]
// TODO: In case Initiator could decrypt, he knows the publicSessionKeyResponderForInitiator
Responder -> Initiator: [publicSessionKeyResponderForInitiator]
// 13) 'key' message from initiator to server to responder
principal Initiator[
generates privateSessionKeyInitiatorForResponder
publicSessionKeyInitiatorForResponder = G^privateSessionKeyInitiatorForResponder
sessionSharedKeyInitiatorResponder = publicSessionKeyInitiatorForResponder^publicSessionKeyresponderForInitiator
knows private keyMessage2
secretBoxKeyInitiatorToResponder = AEAD_ENC(publicPermanentKeyInitiator^publicPermanentKeyResponder, keyMessage2, nil)
]
Initiator -> Responder: secretBoxKeyInitiatorToResponder
principal Responder[
keyMessageToResponder1 = AEAD_DEC(publicPermanentKeyResponder^publicPermanentKeyInitiator, secretBoxKeyInitiatorToResponder, nil)?
]
// TODO: In case Responder could decrypt, he knows the publicSessionKeyInitiatorForResponder
Initiator -> Responder: [publicSessionKeyInitiatorForResponder]
principal Responder[
sessionSharedKeyResponderInitiator = publicSessionKeyResponderForInitiator^publicSessionKeyInitiatorForResponder
]
// 14) 'auth' message from responder to server to initiator
principal Responder[
knows private authMessage1
secretBoxAuthResponderToInitiator = AEAD_ENC(sessionSharedKeyResponderInitiator, authMessage1, nil)
]
Responder -> Initiator: secretBoxAuthResponderToInitiator
principal Initiator[
authMessageToInitiator1 = AEAD_DEC(sessionSharedKeyInitiatorResponder, secretBoxAuthResponderToInitiator, nil)?
]
// 15) 'auth' message from initiator to server to responder
principal Initiator[
knows private authMessage2
secretBoxAuthInitiatorToResponder = AEAD_ENC(sessionSharedKeyInitiatorResponder, authMessage2, nil)
]
Initiator -> Responder: secretBoxAuthInitiatorToResponder
principal Responder[
authMessageToResponder1 = AEAD_DEC(sessionSharedKeyResponderInitiator, secretBoxAuthInitiatorToResponder, nil)?
]
queries[
confidentiality? sessionSharedKeyInitiatorResponder
confidentiality? sessionSharedKeyResponderInitiator
confidentiality? tokenMessage1
confidentiality? keyMessage1
confidentiality? keyMessage2
confidentiality? authMessage1
confidentiality? authMessage2
authentication? Responder -> Initiator: secretBoxTokenResponderToInitiator
authentication? Responder -> Initiator: secretBoxKeyResponderToInitiator
authentication? Initiator -> Responder: secretBoxKeyInitiatorToResponder
authentication? Responder -> Initiator: secretBoxAuthResponderToInitiator
authentication? Initiator -> Responder: secretBoxKeyInitiatorToResponder
]
The text was updated successfully, but these errors were encountered:
Today, I had a look at Verifpal, an experimental software to do some analysis on cryptographic protocols. Because it's designed for non-experts (unlike proven formal verification tools), I thought I could try to model some parts of SaltyRTC.
Honestly, I am not sure if I've done it right and if it even makes sense. But perhaps there is some interest and, if useful, we can create a more detailed/better model.
The analysis on my model didn't bring up any issues. In case you're interested, here is my current model:
The text was updated successfully, but these errors were encountered: