Zulip Chat Archive

Stream: new members

Topic: password for encrypted SSH private key


Scott Morrison (Jul 20 2020 at 11:31):

This sounds right. If you are _sure_ you've never set up an ssh key at github, do let us know, because this is an annoying obstacle in the setup.

Dan Stanescu (Jul 20 2020 at 12:56):

Kevin Buzzard said:

Ok so GitHub is perhaps saying "instead of providing your github password, just let me know that you are you, because you set up an ssh key at some point". I'm not an expert, this is kind of a guess.

I'm pretty sure this is exactly what happens. @Emiel Lanckriet must have set up his GitHub account to use an SSH key sometime in the past. That key is stored in his online GitHub account under Settings/SSH and GPG keys. He can connect from his machine to GitHub (to do git push for example) without further authentication, as long as he types the password to access the key on his local machine. This password is usually stored in a key ring which is many times activated by just logging into the local machine, depending on the settings, so he may have forgotten about it. Just my two cents.

Nevertheless, as opposed to other Lean-related repositories, it is very inconvenient that mathematics_in_lean asks for authentication when attempting a git clone. In my experience, this happens irrespective of whether the person who attempts to clone is set up to use Git with SSH or HTTPS. This must be a setting on the repository itself that should be changed IMO, because it is a deterrent to using the book.

Reid Barton (Jul 20 2020 at 13:20):

It seems like this code is responsible. I don't see how the behavior could be dependent on the repository (name).

Reid Barton (Jul 20 2020 at 13:23):

By the looks of it, if you don't want to push to the repository anyways, then you can just not enter a password and it should fall back to http.

Scott Morrison (Jul 20 2020 at 13:29):

So at the very least we should add a message that says you can just fall back (and perhaps provide the link on github explaining how to use ssh keys?)

Yakov Pechersky (Jul 20 2020 at 14:37):

I added the password prompt, since before, there'd be no way to properly use ssh based git if it was password protected

Yakov Pechersky (Jul 20 2020 at 14:38):

But I can totally understand how those that are unfamiliar with git could be confused why they are being asked for a password if they don't recall setting up an sshe keyed login

Yakov Pechersky (Jul 20 2020 at 14:38):

Perhaps the default should be https with a ssh optional flag

Jeremy Avigad (Jul 20 2020 at 14:59):

I can confirm that the ssh issue caused difficulties with some lftcm users last week, who had set up git in the past and then forgot about it. I can also confirm that we didn't do anything to configure the mathematics_in_lean repository; we just asked github to create a new repository and kept the defaults. (I also just checked the account settings and don't see anything that might help.)

Dima Pasechnik (Jul 20 2020 at 15:05):

Reid Barton said:

It seems like this code is responsible. I don't see how the behavior could be dependent on the repository (name).

I don't quite understand what the code there is doing. IMHO if it is about unlocking a ssh keypair it ought to work with the passphrase rather than password. Certainly, there is also a Github password (for the github account), but as far as I know this password is not used to commincate with a git server, if the comminication is going via ssh.

Dima Pasechnik (Jul 20 2020 at 15:11):

and there is also the password for the local user account (on the client host).

Yakov Pechersky (Jul 20 2020 at 15:14):

It's the passphrase that unlocks the ssh keypair, not the user account. I could have written a more specific prompt. It has nothing to do with any repository and solely has to do with the way git is setup to connect to github on the user's machine.

Dima Pasechnik (Jul 20 2020 at 15:18):

Yakov Pechersky said:

It's the passphrase that unlocks the ssh keypair, not the user account. I could have written a more specific prompt. It has nothing to do with any repository and solely has to do with the way git is setup to connect to github on the user's machine.

but why is it then sent to github as password, rather than passphrase?
[client.connect('github.com', username='git', password=password)]
(https://github.com/leanprover-community/mathlib-tools/blob/77c707eaead3732d0a1527478602649c7e82874e/mathlibtools/leanproject.py#L191)

Yakov Pechersky (Jul 20 2020 at 15:19):

Because that is the name of the kwarg in the paramiko library: http://docs.paramiko.org/en/stable/api/keys.html

Dima Pasechnik (Jul 20 2020 at 15:23):

Yakov Pechersky said:

Because that is the name of the kwarg in the paramiko library: http://docs.paramiko.org/en/stable/api/keys.html

Isn't it rather http://docs.paramiko.org/en/stable/api/client.html ?
Indeed, you invoke connect method of paramiko.client.SSHClient, which has both password= and passphrase= keyword args

Dima Pasechnik (Jul 20 2020 at 15:24):

It says

  • password (str) – Used for password authentication; is also used for private key decryption if passphrase is not given.
  • passphrase (str) – Used for decrypting private keys.

so it looks as if they are different beasts.

Dima Pasechnik (Jul 20 2020 at 15:28):

It's not 100% clear to me what "used for private key decryption" means there. Perhaps it means "treat it as passphrase" - hard to tell without either doing a test of reading the source - but in any event the prompt should ask for passphrase, not password.

Dan Stanescu (Jul 20 2020 at 15:35):

It can ask for either. The ssh key is encrypted with a passphrase. But that passphrase can be stored (at least on Linux machines) in the default key ring of the user, which is either unlocked when the user logs in or can be unlocked later with the local user login password.

Dan Stanescu (Jul 20 2020 at 15:36):

At least that's what I gather.

Dan Stanescu (Jul 20 2020 at 15:38):

The big question though is: why does the mathematics_in_lean repository behave differently than others. Because it really looks like it does.

Yakov Pechersky (Jul 20 2020 at 15:39):

And you did leanproject get mathematics_in_lean; leanproject get other_repo

Dan Stanescu (Jul 20 2020 at 15:44):

Exactly. And it looks like other people have the same experience of different behavior. The first asks the user to authenticate, the second doesn't for whatever other_repo.

This should, however, be checked again on a fresh clone, as things are fluctuating.

The demand for authentication is not a problem for me, but might be a problem for people not familiar with git.

Dan Stanescu (Jul 20 2020 at 15:48):

I just tested it now, and I wasn't prompted for a password/passphrase any more. But this may just be due to my setup.

Reid Barton (Jul 20 2020 at 15:51):

Whatever one you do first will add the passphrase to the ssh agent, then you won't be prompted again (for a while at least).

Dima Pasechnik (Jul 20 2020 at 19:32):

Dan Stanescu said:

It can ask for either. The ssh key is encrypted with a passphrase. But that passphrase can be stored (at least on Linux machines) in the default key ring of the user, which is either unlocked when the user logs in or can be unlocked later with the local user login password.

sending to github the password for the local keyring makes no sense to me - and that's what happens there, if I am not mistaken.

Yakov Pechersky (Jul 20 2020 at 19:35):

My ssh-passphrase is what works here, not my keyring password, in my usage so far.

Yakov Pechersky (Jul 21 2020 at 16:04):

Really, if the user has an SSH key that requires a passphrase, the prompt should indicate which key it is trying to use. This is what happens when I use git manually:

  mathlib-tools git:(master)  git pull
Enter passphrase for key '/home/user/.ssh/id_rsa':
Already up to date.

However, as far as I can tell, paramiko does not expose directly what keyfile it is using to connect (https://github.com/paramiko/paramiko/blob/690d142321f53ae82f49a57b7f6716fb947d5687/paramiko/client.py#L712). I might PR that into Paramiko.

Reid Barton (Jul 21 2020 at 16:09):

I don't understand why any of this is necessary in the first place--doesn't leanproject invoke git pull or something?

Kevin Buzzard (Jul 21 2020 at 16:26):

leanproject get invokes git clone

Patrick Stevens (Jul 21 2020 at 17:06):

Reid Barton said:

I don't understand why any of this is necessary in the first place--doesn't leanproject invoke git pull or something?

git pull requires my SSH key anyway, because I connect to GitHub using SSH:

  mathlib git:(bertrand-postulate)  git remote -v
origin  git@github.com:leanprover-community/mathlib (fetch)
origin  git@github.com:leanprover-community/mathlib (push)

Reid Barton (Jul 21 2020 at 17:07):

Right but e.g. invoking git pull from a shell script would result in the passphrase prompt if needed.

Matt Earnshaw (Jul 23 2020 at 00:07):

this is giving me (non-pebkac) problems too, I have made an issue at https://github.com/leanprover-community/mathlib-tools/issues/72

Kevin Buzzard (Jul 23 2020 at 07:09):

Thanks. This has come up a few times recently.


Last updated: Dec 20 2023 at 11:08 UTC