some code using ur/web, a language/web framework based on dependent types (ie, Coq, Agda, etc) - a login mechanism with salting — http://www.impredicative.com/ur/
some demo code for ur/web, demonstrating user authentication/sessions.
- 30th december 2009 - daniel patterson (http://dbpatterson.com)
- 16th december 2011 - all code that I've written is put in the public domain. enjoy!
to build, first make the c libraries:
$ make
(NOTE: this uses the absolute url for the urweb libraries - if you did not install
urweb to the default location, edit the makefile!)
and then compile the main program (shown here to use sqlite):
$ urweb -dbms sqlite -db userpass.db userpass
and then to run it, first populate the database:
$ sqlite3 userpass.db < userpass.sql
and if you want it to be useful, grab a sha512 hash of some example password with a salt
prepended to it, and insert it, along with a username and the salt, into the db,
here is an example:
$ sqlite3 userpass.db
...
sqlite> insert into uw_Userpass_u (uw_user, uw_salt, uw_password) values ("name", "12345", "6e784ee231562819f1c01968c08db395a17470b44594314804b2358ef448f783a1aba2a4be16529be1e80ba6f310f6881738c1cc6c7790e6652dd9cd94d25a56"
(that is the hash for the password 12345, with the salt also 12345)
then run it:
$ ./userpass.exe
and visit in your webbrowser http://localhost:8080/Userpass/main
and you should be able to log in with the credentials you set up in the database, with a
session set up via cookie, backed by the uw_Userpass_s table in the database.