Closed dbosk closed 5 years ago
I suppose we should do this if we want to go more formal. Not sure yet as to how formal we can be, due to reasoning about complex architectures.
We should be able to do the main part of the algorithm to prove unlinkability etc. Then we can have TS as an oracle.
I suppose we should do this if we want to go more formal. Not sure yet as to how formal we can be, due to reasoning about complex architectures.
We should be able to do the main part of the algorithm to prove unlinkability etc. Then we can have TS as an oracle.