Not a direct answer to your question, but you might want to take a look at:
https://github.com/phillord/tawny-owl This tool wraps OWL, which is a standard language for knowledge representation, that maps to a formal logic underneath, which is machine interpretable and reasonable. I don't know enough about cryptography to know whether the semantics of OWL would be rich enough, but you should be able to specific that a thing that knows a public key of someone is also a subclass of a thing that knows the encrypted nonce. There are some limitations of OWL -- it is not full first order logic, but in return, it has better computational properties that logic. The reasoners are also highly developed and will scale to 10's or 100's of thousands of statements. Phil Adam Saleh <adamthecam...@gmail.com> writes: > I am trying to implement a simple knowledge derivation program in > clojure.core.logic, > and I am not sure how to approach it. To be more specific, after I am done, > it will be used as a toy cryptographic protocol verifier, > that tries to infer what knowledge can attacker get based on some initial > knowledge and some rules. > > For example, I might denote [:pk A] a knowledge of public key of somebody > and [:pcrypted [:pk A] :nonce] an encrypted nonce sent to this person. > > Then I'd like be able to somehow specify, that if I know [:pk A], I know as > well [:pcrypted [:pk A] [:nonce A]] and therefore my program would derive > from initial knowledge > > [ [:pk :a] [:pk :b] ] the full knowledge [[:pk :a] [:pk :b] [:pcrypted > [:pk :a] [:nonce :a]] [:pcrypted [:pk :b] [:nonce :b]]] > > Or in slightly more difficult case to specify that if I know a secret key > [:sk A] and encrypted nonce [:pcrypted [:pk A] [:nonce A]], I also know the > [:nonce a]. > > Anybody has any hints? > > So far I managed to implement some of this, but it is a tangled mess of > recursive pattern matching, membero, nonmembero and macros :-/ > > Thanks for any pointers, > > Adam > > -- -- Phillip Lord, Phone: +44 (0) 191 222 7827 Lecturer in Bioinformatics, Email: phillip.l...@newcastle.ac.uk School of Computing Science, http://homepages.cs.ncl.ac.uk/phillip.lord Room 914 Claremont Tower, skype: russet_apples Newcastle University, twitter: phillord NE1 7RU -- -- You received this message because you are subscribed to the Google Groups "Clojure" group. To post to this group, send email to clojure@googlegroups.com Note that posts from new members are moderated - please be patient with your first post. To unsubscribe from this group, send email to clojure+unsubscr...@googlegroups.com For more options, visit this group at http://groups.google.com/group/clojure?hl=en --- You received this message because you are subscribed to the Google Groups "Clojure" group. To unsubscribe from this group and stop receiving emails from it, send an email to clojure+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/groups/opt_out.
